Déplier les définitions imbriquées en Coq

Question

Je travaille avec la bibliothèque math-classes dans Coq. Cette bibliothèque utilise intelligemment les classes de type pour surcharger les notations, comme ceci.

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

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

Je peux définir de telles instances pour de nombreux types de données différents, et x = y sera compris comme l'égalité que j'ai enregistrée pour le type de x et y grâce au mécanisme de résolution d'instance.

Cependant, manipuler ces égalités dans les preuves est un peu ennuyeux car je dois unfold plusieurs définitions successives :

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

Y a-t-il un moyen plus efficace de faire cet unfold ?

Answer 1

(1) Vous pourriez utiliser une tactique personnalisée :

(* déplie uniquement dans le but *)
Ltac unfold_equiv := unfold equiv, MyEq_equiv, MyEquality.

(* déplie dans le but et dans le contexte *)
Ltac unfold_equiv_everywhere := unfold equiv, MyEq_equiv, MyEquality in *.

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

---

(2) Vous pourriez utiliser les bases de connaissances d'indices. Il suffit d'ajouter vos définitions avec Hint Unfold aux bases de connaissances.

Hint Unfold equiv MyEq_equiv MyEquality.

(* quelques pseudonymes plus pratiques *)
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. (* ou simplement `repeat autounfold with *.` *)
   ...