types - 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(或2元组)。

理想情况下，我想要一个允许nat和元组对以及元组和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 的一个很好的表示法。所以这已经是你想要的了。

如果您想查看括号，您应该在 CoqIDE 中勾选查看 -> 显示括号。

请注意，如果您希望三元组不编码为对，您可以将它们定义为:

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