无法在 Coq 中对元组使用 let-destruct

Question

我是 Coq 的新用户。我已经定义了一些函数：

Definition p (a : nat) := (a + 1, a + 2, a + 3).

Definition q :=
let (s, r, t) := p 1 in
s + r + t.

Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.

我正在尝试将 p 的结果破坏为元组表示。然而coqc抱怨q：

Error: Destructing let on this type expects 2 variables.

while q' 可以通过编译。如果我将 p 更改为返回一对 (a + 1, a + 2)，则相应的 q 和 q' 都可以正常工作。

为什么 let-destruct 只允许对？还是我在语法上有任何错误？我检查了 Coq 手册，但没有发现任何线索。

谢谢！

Answer 1

在 Coq 中有点令人困惑的是，有 两种 不同形式的析构 let。您正在寻找的那个需要在模式之前引用：

Definition p (a : nat) := (a + 1, a + 2, a + 3).

Definition q :=
  let '(s, r, t) := p 1 in
  s + r + t.

在模式前加上引号允许您使用嵌套模式并在其中使用用户定义的符号。不带引号的表单仅适用于一级模式，并且不允许您使用符号，或在您的模式中引用构造函数名称。