Coq中Definition和Let的区别

Question

什么是Coq中“定义”和“Let”的区别？为什么有些定义需要证明呢？ 例如，这是群论中g1.v文件中的一段代码。

Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n; clear n.
exact e.
intro n.
 elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.

这个证明的目的是什么？

- Sai Ganesh Muthuraman

Answer 1

我认为你所问的与Coq中Definition和Let命令的区别并没有直接关系，而是在想知道为什么一些Coq中的定义包含证明脚本。

Coq中的一个有趣特点是编写证明和程序时使用的语言实际上是相同的。这种语言称为Gallina，当使用Coq进行工作时，人们使用的是Gallina编程语言。例如，像fun x => x + 5这样的内容就是Gallina中的一个程序。

然而，在进行证明时，人们通常使用另一种语言，称为Ltac。这是您在exp示例中看到的语言。这可能会让您相信Coq中的证明是用不同的语言表示的，但这不是真的：Ltac脚本实际上是在Gallina中构建证明项。您可以使用Print命令查看，例如：

Print exp.

即使证明和程序使用相同的语言编写，也需要为编写证明单独使用一种语言，原因是Gallina在直接编写证明时有些难以使用。尝试直接在一个复杂的定理上使用Print命令, 就可以看出有多困难。

虽然Ltac主要用于编写证明，但并没有禁止您将其用于编写普通程序，因为最终产品都是Gallina术语。通常，人们更喜欢在编写程序时使用Gallina，因为它更容易阅读。然而，当直接在Gallina中编写程序变得太麻烦时，人们可能会采用Ltac来编写程序。就像你的例子中的exp函数，我个人更喜欢直接使用Gallina进行编写，不过这可能是主观品味问题。

- Arthur Azevedo De Amorim

---

谢谢。我还想知道let和define之间的区别。 - Sai Ganesh Muthuraman

两者之间的区别，粗略地说，就是Let在Section结束后不会保留，而Definition会。因此，在其所属的部分之外，你不能通过名称引用Let定义的内容。 - Arthur Azevedo De Amorim