在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.