The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Ramon,

Yes, especially the inversion tactic sometimes tends to produce the
need to prove that kind of thing. I generally use the following lemmas
for it. Not sure if it is the best one can get. Maybe somebody else
has something better. Note that I only have been able to prove this
lemma for types in which equality is decidable.

Good luck!
Chris


Require Import Eqdep_dec.

Definition sigT_get_proof:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   P t ->
   sigT P ->
      P t.
intros T eq_dec_T P t H1 H2.
destruct H2 as [t' H2].
destruct (eq_dec_T t t') as [H3|H3].
rewrite H3.
exact H2.
exact H1.
Defined.

Theorem sigT_get_proof_existT_same:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   forall H1 H2: P t,
   sigT_get_proof T eq_dec_T P t H1 (existT P t H2) = H2.
Proof.
intros T eq_dec_T P t H1 H2.
unfold sigT_get_proof.
destruct (eq_dec_T t t) as [H3|H3].
unfold eq_rect_r.
symmetry.
exact (eq_rect_eq_dec eq_dec_T (fun t: T => P t) H2 (sym_eq H3)).
tauto.
Qed.

Theorem existT_injective:
   forall T,
   (forall t1 t2: T, { t1 = t2 } + { t1 <> t2 }) ->
   forall P: T -> Type,
   forall t: T,
   forall pt1 pt2: P t,
   existT P t pt1 = existT P t pt2 ->
   pt1 = pt2.
Proof.
intros T T_dec P t pt1 pt2 H1.
pose (H2 := f_equal (sigT_get_proof T T_dec P t pt1) H1).
repeat rewrite sigT_get_proof_existT_same in H2.
assumption.
Qed.