The Coq mailing list

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

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.