The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

On 13/2/21 10:35 pm, Gert Smolka 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.

Hi Gert,

I don't understand the logic behind all of this, but it can be proved thus:

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

Require Import Coq.Program.Equality.

intro.
dependent destruction H.
reflexivity.
Qed.

Coq < Print Assumptions K2_injective.
Fetching opaque proofs from disk for Coq.Logic.EqdepFacts
Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq : forall (U : Type) (p : U)
                                (Q : U -> Type) (x : Q p)
                                (h : p = p), x = eq_rect p Q x p h
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y

alternatively you can get part way there
(and in the past when I've had the same sort of situation
before I've been able to complete a proof this way)

intro.
inversion H.
inversion_sigma.
rewrite <- Eqdep.EqdepTheory.eq_rect_eq in H5.
(* I don't understand why the following line
doesn't work in this case *)
rewrite <- Eqdep.EqdepTheory.eq_rect_eq in H4.

Cheers,

Jeremy