The Coq mailing list

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

Hello Domique,

Here is more or less a proof of it, but it only works if you can prove
that the type you are working in has decidable equality. As others
point out, it is apparently not in general provable.

All the best,
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.