The Coq mailing list

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

> But why is this?  I thought constructors are always injective.

Well ... the short answer is no, this is not provable in Coq's 
Type theory when you have dependencies. I assumed that you believed 
it was true and this is why I insisted on that point ... It goes 
against intuition but that is just the way it is.

So when you invert identities with (user defined) dependent 
types, Coq produce new identities like

   existT ... = existT ... 

that you might later invert using tools from the
Eqdep_dec module, when the base type has proof 
irrelevant identities for instance.

Sometimes, you can work with eg the existT_inv 
I provided in combination with the subst tactic 
that replace 

x with t and E with eq_refl 

simultaneously everywhere whenever

E : x = t 

occurs in the context. x must not occur
in a cycle in the hypothesis, eg
E : x = f x would fail.

Then matching on eq_refl reduces and the 
identity proof disappears from your terms. 
subst is usually more convenient than rewrite 
when you have dependencies. 

Good luck,

Dominique


----- Mail original -----
> De: "Jeremy Dawson" 
> <Jeremy.Dawson AT anu.edu.au>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Mercredi 2 Octobre 2019 13:17:23
> Objet: Re: [Coq-Club] existT

> 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