CODEWITHSUNDEEP
typeclasscoq
pintoch
pintoch

Reputation: 2468

Unfolding nested definitions in Coq

I am working with the math-classes library in Coq. This library makes a clever use of type classes to overload notations, like this.

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

I can define such instances for many different datatypes, and x = y will be understood as the equality I have registered for the type of x and y thanks to the instance resolution mechanism.

However, dealing with these equalities in proofs is a bit annoying because I have to unfold many successive definitions:

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

Is there a more efficient way to do this unfold?

Upvotes: 3

Views: 282

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

(1) You could use a custom tactic:

(* 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) You could use the hint databases. Just add your definitions with Hint Unfold to the databases.

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.

Upvotes: 1

Related Questions