无法在 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.

而q'可以通过编译。如果我将 p 更改为 return a pair(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.

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

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

Fail to use let-destruct for tuple in Coq

coq