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，雖然這可以說是一個品味問題。