The Coq mailing list

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

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.