coq - 你如何在 Coq 中定义有序对？

Question

我是一名程序员，但对 Coq 来说是个超级新手，并且试图弄清楚这些教程，但没有取得多大成功。我的问题很简单：如何在 Coq 中定义有序对（自然数）？

这是我的尝试：

Variable node1 : nat.
Variable node2 : nat.
Inductive edge : type := node1 -> node2.

（请注意，“edge”是我用于有序对的名称。）第三行给出了一个语法错误，表明我需要一个 '.' 在某处的句子中。

我不知道该怎么办。任何帮助都会很棒！（另外，有没有一个教程可以帮助教授非常基本的 Coq 概念，而不是那些在谷歌搜索“Coq 教程”时很容易看到的教程？）

Answer 1

您只需使用 Coq 定义就可以做到这一点：

Definition ordered_pair := (nat * nat) % type.

这ordered_pair作为同义词引入(nat * nat) % type（请注意，% type需要让 Coq*在类型范围内进行解释，而不是在自然范围内解释）。真正的力量在于使用*：

Inductive prod (A B:Type) : Type :=
  pair : A -> B -> prod A B.

（来自http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html）

您可以从那里获得所有必要的消除原则等。