未能在Coq中使用let-destruct for tuple

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中有点令人困惑的是,有两种不同形式的破坏让.您正在寻找的那个需要在模式之前引用:

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

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

使用引号对模式进行前缀允许您使用嵌套模式并在其中使用用户定义的表示法.没有引号的表单仅适用于一级模式,并且不允许您使用符号,或者在模式中引用构造函数名称.