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

Posted 2023-03-15

【中文标题】Coq 数据类型 - 一对带括号的对

【英文标题】：Coq datatype - pair of pair with bracket

【发布时间】：2021-09-10 09:47:04

【问题描述】：

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

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

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

【参考方案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

【讨论】：

Set Printing Parentheses. 做同样的事情（如果你没有使用 CoqIDE）。