在Coq中展開嵌套定義

Question

我正在使用Coq中的數學類庫。這個庫巧妙地使用了類型來重載符號，就像這樣。

(* From math-classes *) 
Class Equiv A := equiv : relation A. 
Infix "=" := equiv : type_scope. 

(* My code *) 
Definition MyDataType : Type := ... 
Definition MyEquality (x y : MyDataType) : Prop := ... 
Instance MyEq_equiv : Equiv MyDataType := MyEquality. 

我可以定義這種情況下許多不同的數據類型和x = y將 被理解爲我已經註冊了x和y感謝到實例解析機制類型的平等。

然而，與這些等式中證明是處理有點惱人，因爲我有很多unfold連續定義：

Lemma MyEquality_refl : forall x : MyDataType, x = x. 
Proof. 
    intro. 
    unfold equiv, MyEq_equiv, MyEquality. 
    ... 
Qed. 

有沒有更有效的方法來做到這一點unfold？

Answer 1

（1）您可以使用自定義策略：

(* unfolds only in the goal *) 
Ltac unfold_equiv := unfold equiv, MyEq_equiv, MyEquality. 

(* unfolds in the goal and in the context *) 
Ltac unfold_equiv_everywhere := unfold equiv, MyEq_equiv, MyEquality in *. 

Lemma MyEquality_refl : forall x : MyDataType, x = x. 
Proof. 
    intro. 
    unfold_equiv. (* or `unfold_equiv_everywhere.` *) 
    ... 
Qed. 

---

（2）你可以使用提示數據庫。只需將您的定義添加到 Hint Unfold即可。

Hint Unfold equiv MyEq_equiv MyEquality. 

(* a couple more convenient pseudonyms *) 
Ltac unfold_selected := repeat autounfold with *. 
Ltac unfold_selected_everywhere := repeat autounfold with * in *. 

Lemma MyEquality_refl : forall x : MyDataType, x = x. 
Proof. 
    intro. 
    unfold_selected. (* or just literally `repeat autounfold with *.` *) 
    ... 
Qed.