Proving dependent equalities in Coq with SSReflect

Proving dependent equalities in Coq is boring, but quite frequently done.

I got so annoyed with it that I wrote a little tactic to automatize it a bit.

It does use ssreflect routines but it should not be hard to adapt it to vanilla Coq.

Ltac depcomp H := apply EqdepFacts.eq_sigT_eq_dep in H; 
apply Coq.Logic.Eqdep.EqdepTheory.eq_dep_eq in H.
Ltac eq_comp c x y := 
  move: (c x y); 
  last try do [by [right; case]| 
  right; case; let H' := fresh "H" in move=>H'; by depcomp H'];
  first try let H' := fresh "H" in move=> H'; subst.

Definition eq_dec T := forall x y: T, {x = y} + {~ x = y}.

(* Example *)
Theorem pair_eq_dec T U: eq_dec T -> eq_dec U -> eq_dec (prod T U).
move=> HT HU [x y] [a b].
eq_comp HT x a.
eq_comp HU y b.
by left.

Related Posts

Advice for programming students

Why every programming student should learn Coq

Taking notes in markdown: insert a part of a screenshot

Bigger sphere inside of a smaller one

Memory in CompCert: overview

A beautiful intuition on associativity

On teaching mathematics -- a summary of Kudryavtsev's book

On teaching programmers and mathematicians

A word about René Magritte

goto, the marvelous