Coq中定义与Let之间的区别

Question

Coq中的Defintion和'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在你的例子中,尽管这可能是一个品味问题.