The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Jeremy,

Pierre Casteran points you to the right place.
I just complete the information by telling you
that the constructor existT is *not* injective
in its third argument.

This means that from

existT P x tx = existT P y ty

you can deduce x = y (with projT1)
but you *cannot* deduce tx = ty (in general).

What you can prove is the following:

existT P x tx = existT P y ty -> exists E : x = y, ty = eq_rect x P tx y E.

If the type X on which P : X -> Type has some extra 
properties, like "proof irrelevance on the type of
equalities over X", or stronger, "decidable equality over X", 
then you can prove

existT P x t1 = existT P x t2 -> t1 = t2

because there is only one proof that x = x
and this is eq_refl.

See the script below and also welcome to the 
wonderful world of dependent types ;-)

Best 

Dominique

----

Section existT_inj.

  Variable (X : Type) (P : X -> Type).

  Fact existT_inv x tx y ty :
     existT P x tx = existT P y ty -> exists E : x = y, ty = eq_rect x P tx y 
E.
  Proof.
    inversion 1; exists eq_refl; reflexivity.
  Qed.

  Hypothesis eq_X_pirr : forall (x y : X) (E1 E2 : x = y), E1 = E2.

  Fact existT_inj2 x t1 t2 :
    existT P x t1 = existT P x t2 -> t1 = t2.
  Proof.
    intros H.
    apply existT_inv in H.
    destruct H as (E & ->).
    rewrite (eq_X_pirr _ _ _ eq_refl).
    simpl; trivial.
  Qed.

End existT_inj.

Check existT_inv.
Check existT_inj2.

----- Mail original -----
> De: "Jeremy Dawson" 
> <Jeremy.Dawson AT anu.edu.au>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Mardi 1 Octobre 2019 09:57:05
> Objet: [Coq-Club] existT

> Hi,
> 
> I have an inductive definition:
> 
> Inductive
> in_dersrec (X : Type) (rules : rlsT X) (prems : X -> Type)
> (concl : X) (d : derrec rules prems concl)
>   : forall concls : list X, dersrec rules prems concls -> Type :=
>     in_dersrec1 : forall (concls : list X) (ds : dersrec rules prems
> concls),
>                   in_dersrec d (dlCons d ds)
>   | in_dersrec2 : forall (concl' : X) (d' : derrec rules prems concl')
>                     (concls : list X) (ds : dersrec rules prems concls),
>                   in_dersrec d ds -> in_dersrec d (dlCons d' ds)
> 
> When I have a goal with
> X0 : in_dersrec d ds
> among the assumptions,
> inversion X0. gives new assumptions
> 
>   ds0 : dersrec rules prems concls
>   H0, H2 : p :: concls = ps
>   H3 : existT (fun x : list X => dersrec rules prems x)
>          (p :: concls) (dlCons d ds0) =
>        existT (fun x : list X => dersrec rules prems x) ps ds
> 
> What I would expect to get is also
> dlCons d ds0 = ds
> 
> Whay do I get this strange assumption?
> 
> Furthermore, it seems that existT is a constructor for the inductive
> definition of sigT.  That being so, why doesn't injection H3
> give that the respective arguments of the two occurrences of existT are
> equal?
> 
> thanks for any help
> 
> Jeremy