如果類型類別具有支柱，Coq將不會計算類型類型函數

Question

我無法理解類型類別函數的Coq計算（或缺少它）的行爲。下面是一個最小的工作示例：

Class class1 : Set := { class_func1 : nat -> nat }. 
Class class2 : Set := { class_func2 : nat -> nat 
         ; class_prop2 : forall x : nat, x = x 
         }. 

Instance class1_instance : class1 := { class_func1 := S }. 
Instance class2_instance : class2 := { class_func2 := S }. 
Proof. 
    auto. 
Qed. 

Compute class_func1 5. 
Compute class_func2 5. 

當我打電話Compute class_func1 5.，勒柯克輸出6 : nat預期。然而，當我打電話Compute class_func2 5.，我得到

= (let (class_func2, _) := class2_instance in class_func2) 5 
: nat 

我已經在校對編輯模式相關條款使用unfold和compute試過，但沒有任何結果。我也嘗試用Type替換Prop的實例，但沒有結果。

有人可以澄清爲什麼Coq不會計算從類型類的函數，如果該類型類有一個Prop它？

Answer 1

發生這種情況是因爲您使用了Qed而不是Defined來完成class2_instance的定義。 Qed呈現您的定義不透明，使計算不可能。

以下工作：

Instance class2_instance : class2 := { class_func2 := S }. 
Proof. trivial. Defined. 

Compute class_func2 5. (* returns 6 *) 

這是一個普遍的事情，這是因爲使用類型類與Prop的不是。例如。以下定義的身份識別功能將無法計算出來

Definition id (x : nat) : nat. 
    exact x. Qed.