TypeclassにPropがある場合、Coqはtypeclass関数を計算しません。

Question

Coqのtypeclass関数の計算（またはその不足）の動作を理解できません。

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を使用してみました。また、PropのインスタンスをTypeに置き換えようとしましたが、結果はありません。

TypeclassにPropがある場合、Coqが関数を計算しない理由を誰かが明確にすることはできますか？

Answer 1

これはDefinedの代わりにQedを使用して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.