The Coq mailing list

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

Hello all,

Actually, under some conditions existT is injective. It is the case if

the underlying type has decidable equality. See proof below. IIRC

a proof of this nowadays is also in the standard library, but I do not

seem to be able to find it that quickly.

Good luck,

Chris

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 eq_dec_T 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_dec t pt1) H1).
repeat rewrite sigT_get_proof_existT_same in H2.
assumption.
Qed.