The Coq mailing list

[Kenji Maillard <chocobodralliam AT gmail.com>]

Dear Gert Smolka,

The approach of the Equations package using the noConfusion property is 
quite well explained at point 1.5 of 
https://www.irif.fr/~sozeau//research/publications/Equations_Reloaded-ICFP19.pdf.

Here is my hand-rolled version, specialized a bit to your inductive to 
simplify the proof but maintaining the main relevant elements

Inductive K (x: nat) : nat -> Type :=
| K1: K x (S x)
| K2: forall y z, K x y -> K y z -> K x z.

Import EqNotations.

Definition noConfusionK {x z z'} (t : K x z) (t' : K x z') : Type :=
  match t, t' return Type with
  | (K1 _), (K1 _) => unit
  | (K2 _ y z a b), (K2 _ y' z' a' b') =>
    { yy' : y = y' &
            { zz' : z = z' &
                    ((rew [fun y => K x y] yy' in a = a') *
                     (rew [fun z => K y' z] zz' in rew [fun y => K y z] 
yy' in b = b'))%type }}
  | _, _ => False
  end.

(*  We only need one direction of the equivalence here *)
Lemma noConfusionK_impl {x z} (t t' : K x z) :
  t = t' -> noConfusionK t t'.
Proof.
  intros ->; destruct t' as [|y z a b]; cbn.
  1: easy.
  do 2 exists eq_refl; easy.
Qed.


From Coq.Logic Require Import Eqdep_dec.

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').
Proof.
  intros h%(noConfusionK_impl _ _).
  destruct h as [yy' [zz' [aa' bb']]].
  rewrite (UIP_refl_nat _ yy') in aa', bb'.
  rewrite (UIP_refl_nat _ zz') in bb'.
  rewrite <- aa', <- bb'.
  reflexivity.
Qed.


Best Regards,
Kenji

Le 13/02/2021 à 14:21, Gert Smolka a écrit :
> 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.