The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Thanks for these replies, several of them say in different ways that
(only) under certain conditions, existT is injective in its 3rd argument.

But it seems that now I've been proving it without making any such 
assumption:

[jeremy@localhost sysadmin]$  coqtop -color no
Welcome to Coq 8.8.2 (January 2019)

Coq < Require Import Coq.Program.Equality. (* for dependent 
induction/destruction *)

Coq < Lemma existT_inj: forall A P (x : A) px px',
   existT P x px = existT P x px' -> (px = px').
Coq < 1 subgoal

   ============================
   forall (A : Type) (P : A -> Type) (x : A) (px px' : P x),
   existT P x px = existT P x px' -> px = px'

existT_inj < Proof. intros. dependent destruction H. tauto. Defined.

1 subgoal

   A : Type
   P : A -> Type
   x : A
   px, px' : P x
   H : existT P x px = existT P x px'
   ============================
   px = px'

1 subgoal

   A : Type
   P : A -> Type
   x : A
   px' : P x
   ============================
   px' = px'

No more subgoals.

existT_inj is defined

Given the earlier replies to my question, this doesn't seem to make sense

Cheers,

Jeremy
On 2/10/19 11:12 pm, Tom de Jong wrote:
>  > 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.
> https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html
> 
> Best,
> 
> Tom
> 
> On 02/10/2019 1:47 pm, Chris Dams wrote:
>> 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.
>>