The Coq mailing list

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

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.
>