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

Question

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

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

理想情况下，我想要一个允许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
}