The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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.