The Coq mailing list

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

Dear Gert,

Yep your are very right. When you have a default
value at hand to feed in on unwanted cases, you
can avoid the precondition in the partial
inversion function. And indeed, this is the
case for inl/inr.

Dominique

----- Mail original -----
> De: "Gert Smolka" <smolka AT cs.uni-saarland.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Dimanche 14 Février 2021 11:25:58
> Objet: Re: [Coq-Club] Dependent typing puzzle, constructor injectivity

> Dear Dominique,
> why not use the standard technique for non-indexed inductive types for 
> inr_inj?
> See below.
> Gert
> 
> Fact inr_inj X Y (y y': Y) :
>  inr X y = inr y' -> y = y'.
> Proof.
>  intros H.
>  apply f_equal
>    with (f:= fun a: X + Y => match a with
>                           | inl x => y
>                           | inr y => y
>                           end)
>    in H.
>  exact H.
> Qed.
> 
> 
>> On 14. Feb 2021, at 10:11, Dominique Larchey-Wendling
>> <dominique.larchey-wendling AT loria.fr> wrote:
>> 
>> Dear Gert,
>> 
>> Btw, I was a bit lazy implementing injectivity of inr, which
>> is also interesting when avoiding inversion, because inversion
>> hides what is happening.
>> 
>> The trick is to implement *partial* inversion (inr_inv below).
>> 
>> Best,
>> 
>> Dominique
>> 
>> Section inr_inv.
>> 
>>  Variables (A B : Type).
>> 
>>  Implicit Type (s : A + B).
>> 
>>  Definition not_inl s :=
>>    match s with
>>      | inl _ => False
>>      | _     => True
>>    end.
>> 
>>  Definition inr_inv s : not_inl s -> B :=
>>    match s with
>>      | inl _ => fun H => match H with end
>>      | inr b => fun _ => b
>>    end.
>> 
>>  Lemma inr_inv_fun r s wr ws : r = s -> inr_inv r wr = inr_inv s ws.
>>  Proof.
>>    intros ->; destruct s; auto; destruct ws.
>>  Qed.
>> 
>>  Theorem inr_inj x y : @inr A B x = inr y -> x = y.
>>  Proof. exact (inr_inv_fun (inr _) (inr _) I I). Qed.
>> 
>> End inr_inv.
>> 
>> 
>> 
>> ----- Mail original -----
>>> De: "Gert Smolka" <smolka AT ps.uni-saarland.de>
>>> À: "coq-club" <coq-club AT inria.fr>
>>> Envoyé: Dimanche 14 Février 2021 09:59:30
>>> Objet: Re: [Coq-Club] Dependent typing puzzle, constructor injectivity
>> 
>>> Dear Dominique,
>>> beautiful!  Working with a general inversion operator (K_invert)
>>> and exploiting the injectivity of inr and existT yields an elegant
>>> general scheme.
>>> Thanks, Gert
>>> 
>>>> On 13. Feb 2021, at 22:42, Dominique Larchey-Wendling
>>>> <dominique.larchey-wendling AT loria.fr> wrote:
>>>> 
>>>> Dear Gert,
>>>> 
>>>> This is mainly what you did, which is implementing
>>>> the inversion function by dependent pattern matching.
>>>> Some short code below,
>>>> 
>>>> Best regards,
>>>> 
>>>> Dominique
>>>> 
>>>> PS: I guess if you do not have nat but an unspecified type
>>>> X with S : X -> X, then you cannot show injectivity of
>>>> the constructors.
>>>> 
>>>> -----------------------------
>>>> 
>>>> Fact inr_inj {A B} (x y : B) : @inr A B x = inr y -> x = y.
>>>> Proof. inversion 1; trivial. Qed. (* Lazy here *)
>>>> 
>>>> Fact DPI_nat :
>>>> forall (p: nat -> Type) n a b, existT p n a = existT p n b -> a = b.
>>>> Proof.
>>>> (* Follows with Coq.Logic.Eqdep_dec.UIP_refl_nat *)
>>>> Admitted.
>>>> 
>>>> Inductive K (x: nat) : nat -> Type :=
>>>> | K1: K x (S x)
>>>> | K2: forall y z, K x y -> K y z -> K x z.
>>>> 
>>>> Definition K_invert x y (H : K x y) : (( y = S x ) + { z : nat & K x z * 
>>>> K z y
>>>> })%type :=
>>>> match H with
>>>>   | K1 _           => inl eq_refl
>>>>   | K2 _ y z H1 H2 => inr (existT _ y (H1,H2))
>>>> end.
>>>> 
>>>> Fact K2_injective x y z a b a' b':
>>>> K2 x z y a b = K2 x z y a' b' -> (a,b) = (a',b').
>>>> Proof.
>>>> intros H.
>>>> now apply f_equal with (f := K_invert _ _), inr_inj, DPI_nat in H.
> >>> Qed.