coq - 无法在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更改为返回一对(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.

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