Entfaltete verschachtelte Definitionen in Coq

Question

Ich arbeite mit der Mathematik-Klassen-Bibliothek in Coq. Diese Bibliothek verwendet geschickt Klassen, um Notationen zu überladen.

(* 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. 

kann ich solchen Fällen für viele verschiedene Datentypen definieren und x = y wird als Gleichheit verstanden werden, ich für die Art von x und y dank der Instanz Bewältigungsmechanismus registriert haben.

jedoch in Proofs mit diesen Gleichheiten zu tun ist ein bisschen ärgerlich, weil ich zu unfold vielen aufeinander folgenden Definitionen:

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

Gibt es eine effizientere Art und Weise diesen unfold zu tun?

Answer 1

(1) Sie könnten eine eigene Taktik verwenden:

(* 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) Sie die Hinweis-Datenbanken verwenden können. Fügen Sie einfach Ihre Definitionen mit Hint Unfold zu den Datenbanken hinzu.

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.