The Coq mailing list

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

Well, thanks.  But why is this?  I thought constructors are always 
injective.

And why does the inversion step produce this assumption involving 
existT?  I would have expected one subgoal with assumptions saying that 
the occurrence of in_dersrec d ds is an instance of in_dersrec1, and 
another subgoal with assumptions saying that the occurrence of 
in_dersrec d ds is an instance of in_dersrec2, but that isn't what I am 
getting - why not?

Thanks

Jeremy


On 1/10/19 7:18 pm, Dominique Larchey-Wendling wrote:
> 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