Coq定义和Let的区别

Question

Defintion和Coq的'Let'有什么区别？为什么有些定义需要证明？ 例如。这是g1.v在Group theory中的一段代码。

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的东西时，那是加利纳的一个程序。

但是，在做证明时，人们通常会使用另一种语言，称为Ltac。这是出现在您的exp示例中的语言。这可能导致您相信Coq中的证据以不同的语言表示，但这不是事实：Ltac脚本所做的是在Gallina中实际构建证明条款。您可以通过使用Print命令（例如，

Print exp. 

的原因有写证明，即使证据和程序是用同一种语言独立的语言，是加利纳是有点硬写打样时直接使用。尝试直接通过复杂的定理使用Print命令，看看有多难。

现在，尽管Ltac主要用于书写样张，但由于最终产品是相同的：Gallina术语，所以没有什么东西禁止您使用它来编写正常程序。通常，人们更喜欢在编写程序时使用Gallina，因为它更易于阅读。然而，人们可能会诉诸Ltac编写程序，因为直接在Gallina执行该程序会非常麻烦。在我的例子中，我个人宁愿直接使用Gallina编写函数，例如exp，虽然这可以说是一个品味问题。