functional-programming - 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.

这个证明的目的是什么？

Answer 1

我认为你所问的问题与 Coq 中的 Definition 和 Let 命令之间的区别并不真正相关。相反，您似乎想知道为什么 Coq 中的某些定义包含证明脚本。

Coq 的一个有趣的特性是，用于编写证明和程序的语言实际上是相同。这种语言被称为 Gallina，它是人们在使用 Coq 时使用的编程语言。当您编写类似 fun x => x + 5 的内容时，这就是 Gallina 中的程序。

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

Print exp.

之所以要使用单独的语言来编写证明，即使证明和程序是用同一种语言编写的，也是因为在编写证明时直接使用 Gallina 有点困难。尝试直接在复杂的定理上使用 Print 命令，看看这有多难。

现在，尽管 Ltac 主要用于编写证明，但没有什么可以禁止您使用它来编写普通程序，因为最终产品是相同的:Gallina 术语。通常，人们在编写程序时更喜欢使用 Gallina，因为它更易于阅读。然而，人们可能会求助于 Ltac 来编写程序，因为直接在 Gallina 中编写程序太麻烦了。我个人更喜欢直接使用 Gallina 来编写示例中的函数，例如 exp，尽管这可能是一个品味问题。