由於未知原因導致的內部依賴類型化表達式中的術語重寫失敗

Question

下面是捕獲有問題行爲的更大證明的簡化片段。

Section foo. 
    Parameter t : Type. 
    Parameter x : t. 
    Parameter y : t. 
    Parameter prop : x = y <-> True. 
    Parameter prop2 : x = y. 
    Lemma lemma : forall e : t, x = y. 
    rewrite prop2. 
    intro e; trivial. 
    Qed. 
End foo. 

當您更換rewrite prop2通過rewrite prop COQ失敗，神祕的錯誤。然而在我的看法coq應該在重寫步驟後產生forall e : t, True。誰能幫我這個？

Answer 1

正如reference manual說：

rewrite term 
This tactic applies to any goal. The type of term must have the form 
forall (x1:A1) … (xn:An)eq term1 term2. 
where eq is the Leibniz equality or a registered setoid equality. 

但prop不與萊布尼茨平等的一種形式：

Coq < Unset Printing Notations. 
Coq < Print prop. 
prop : iff (eq x y) True 

所以COQ需要Setoid檢查iff是setiod平等。