The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello Jeremy,


Le 16/10/2019 à 15:35, Jeremy Dawson a écrit :
> Given the earlier replies to my question, this doesn't seem to make sense

When you "Require Import Coq.Program.Equality",
you implicitly import the "eq_rect_eq" axiom, of:

 https://coq.inria.fr/library/Coq.Logic.Eqdep.html

whereas earlier replies explain how to avoid this axiom in some cases.

To my knowledge, there is no particular issue with this axiom, except 
that it may not be consistent with other axioms, such as univalence.


Sylvain.


> 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.