Coq 中 Definition 和 Let 的区别
Difference between Definition and Let in Coq
Defintion 和 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.
这个证明的目的是什么？
我认为您所问的与 Coq 中 Definition 和 Let 命令之间的区别并没有真正的关系。相反，您似乎想知道为什么 Coq 中的某些定义包含证明脚本。
Coq 的一个有趣特性是用于编写证明和程序的语言实际上是相同。这种语言被称为 Gallina，这是人们在使用 Coq 时使用的编程语言。当您编写类似 fun x => x + 5 的内容时，这就是 Gallina 中的程序。
然而，在做证明时，人们通常使用另一种语言，称为 Ltac。这是出现在 exp 示例中的语言。这可能会让您相信 Coq 中的证明是用不同的语言表示的，但事实并非如此：Ltac 脚本所做的实际上是在 Gallina 中构建 proof terms。您可以使用 Print 命令查看，例如
Print exp.
之所以使用单独的语言来编写证明，即使证明和程序是用同一种语言编写的，也是因为 Gallina 在编写证明时直接使用起来有点困难。尝试直接在复杂的定理上使用 Print 命令，看看这有多难。
现在，即使 Ltac 主要用于编写校样，也没有什么可以禁止您使用它来编写普通程序，因为最终产品是相同的：Gallina 项。通常，人们在编写程序时更喜欢使用 Gallina，因为它更易于阅读。但是，当直接在 Gallina 中编写程序太麻烦时，人们可能会求助于 Ltac 来编写程序。我个人更喜欢直接使用 Gallina 来编写函数，例如您示例中的 exp，尽管这可以说是个人喜好问题。
Defintion 和 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.
这个证明的目的是什么？
我认为您所问的与 Coq 中 Definition 和 Let 命令之间的区别并没有真正的关系。相反，您似乎想知道为什么 Coq 中的某些定义包含证明脚本。
Coq 的一个有趣特性是用于编写证明和程序的语言实际上是相同。这种语言被称为 Gallina，这是人们在使用 Coq 时使用的编程语言。当您编写类似 fun x => x + 5 的内容时，这就是 Gallina 中的程序。
然而，在做证明时，人们通常使用另一种语言，称为 Ltac。这是出现在 exp 示例中的语言。这可能会让您相信 Coq 中的证明是用不同的语言表示的，但事实并非如此：Ltac 脚本所做的实际上是在 Gallina 中构建 proof terms。您可以使用 Print 命令查看，例如
Print exp.
之所以使用单独的语言来编写证明，即使证明和程序是用同一种语言编写的，也是因为 Gallina 在编写证明时直接使用起来有点困难。尝试直接在复杂的定理上使用 Print 命令，看看这有多难。
现在，即使 Ltac 主要用于编写校样，也没有什么可以禁止您使用它来编写普通程序，因为最终产品是相同的：Gallina 项。通常，人们在编写程序时更喜欢使用 Gallina，因为它更易于阅读。但是，当直接在 Gallina 中编写程序太麻烦时，人们可能会求助于 Ltac 来编写程序。我个人更喜欢直接使用 Gallina 来编写函数，例如您示例中的 exp，尽管这可以说是个人喜好问题。