Coq 数据类型 - 一对带括号的对

Question

我正在规范一个支持元组和 nat 对作为函数输入的系统。但是，我对 Coq 中的 pair 类型有一些问题。

根据我对 Coq 的了解，pair 被定义为左结合。即 (1, 2, 3) 和 ((1, 2), 3) 具有相同类型的 nat * nat * nat。有时，它可以被视为nat的一个三元组。另一方面，(1, (2, 3)) 的类型为 nat * (nat * nat)，它是一对 nat 和 pair（或二元组）。

理想情况下，我想要一个允许nat 和tuple 对 和 tuple 和nat 对 的系统。即 (1, (2, 3)) 和 ((1, 2), 3) 都不同于 (1, 2, 3)。 Coq 中是否有针对此类模型的建议数据类型？

Answer 1

(1, 2, 3) 只是 ((1, 2), 3) 的一个很好的表示法，而 nat * nat * nat 只是 (nat * nat) * nat 的一个很好的表示法。所以这已经是你想要的了。

如果你想看到括号，你应该勾选 View -> Display parentheses in CoqIDE.

请注意，如果您想要三元组而不是成对编码，您可以将它们定义为：

Record triple (A B C : Type): Type :=
{
  t_fst : A;
  t_snd : B;
  t_trd : C
}

Coq 数据类型 - 一对带括号的对

Coq datatype - pair of pair with bracket

types

functional-programming

coq

coqide