The Coq mailing list

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

I could not let loose, this stuff is addictive.
Luckily I found a solution before it ruined my weekend.  
See below.

Anyway, I would be thankful for pointers where these
kinds of things are explained.

Enjoy your weekend,
Gert

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.

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 e.
  pose (p y z := prod (K x z) (K z y)).
  pose (q y := sigT (p y)).
  apply (DPI_nat (p y) z).
  apply (DPI_nat q y).
  pose (f:= fun c: K x y =>
              match c return sigT q with
              | K1 _ => existT q y (existT (p y) z (a,b))
              | K2 _ z y a b => existT q y (existT (p y) z (a,b))
              end).
  apply (f_equal f e).
Qed.


> On 13. Feb 2021, at 12:35, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:
> 
> I would like to prove
> 
> Inductive K (x: nat) : nat -> Type :=
> | K1: K x (S x)
> | K2: forall y z, K x y -> K y z -> K x z.
> 
> Fact K2_injective x y z a b a' b':
> K2 x y z a b = K2 x y z a' b' -> (a,b) = (a',b').
> 
> by hand in a way that is similar to the proof generated       
> by the dependent elimination tactic of the Equations package.
> Does someone have a hand proof bringing across the essential ideas?
> 
> Thanks in advance,
> Gert
> 
> PS. I have a simple proof exploiting the "semantic” fact (K x y -> x < y),
> but so far I failed in finding a "regular” proof using only routine 
> techniques.
>