coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kenji Maillard <chocobodralliam AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Dependent typing puzzle, constructor injectivity
- Date: Sat, 13 Feb 2021 14:58:24 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chocobodralliam AT gmail.com; spf=Pass smtp.mailfrom=chocobodralliam AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f42.google.com
- Ironport-phdr: 9a23:NiCfChaOAG7HucGWOHd9vPj/LSx+4OfEezUN459isYplN5qZrs+5bnLW6fgltlLVR4KTs6sC17OH9f67EjBQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba52IRmsrAjcuMYajIRhJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lL9VrgyvpxJ/wIDabo+aO/V8cazBct0XXnZBU8VLWiBdHo+xYYkCAuwcNuhYtYn9oF4OoAO7CwayAuPvyD5IjWLx06Ig0uQhFQXG0xY6H90TrX/Zq8n6NKcVUe+py6nH1jLDYO5M2Tjn7IjIdhEhruuJXb9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HUiowbzl3I6yt3zJopKdC7VEN1bt6qHYdRuiyYOYZ4QsIvTW5stSs61rELuYC3cScKxZkmxBPSd/yJfoiI7x//UuuaPDl2hHVgeL2lhhay91CtyuzmVsm13lZGtCRFksPKu3sQ1BLT8tCKRuVh8kqlwzqC1ADe5vtaLUwqiKbXMZEszqAompYNq0vPAjL6lUDog6OKbEop//ak5/njb7jju5CROZJ4hh37P6ksgcOyD+Q1Pw0SUGWY9+Swybju8E35TbpQgPA7l7PWvZDEKcsAoKOyHhVb3Zw56xmlCjeryNQYkmcDLFJCYB+HipLmO1DKIPzhA/a/mUmgnC5lx/3JILHtGJrNLn/EkLfuebZy9VRQxxY0zdBa/55UC7cBL+zvWkLpqtDUEhs0Pxa3zuvnEtlxyJ0SVX+VDqKWLq/eqVqI6fguI+mIao8VojH9K/096vHyjX85nkMSfa6y0psQdX+4BO5pI0GdYXrtmNgBFHwHvgU7TOPwiV2CVSRfaGq1X6I5/j07Ep6pDZ/fRoCxh7yMxDu0HppPZmxfFl+MFWroeJ6fVvcXaCOSJ9dhnSYeWbigTY8hzxCuuxXgx7ppNOqHshEf4JnkzZ1+4/DZvRA07z19ScqHgE+XSGQhvW4ORT5++al+pUh00FvLhaN4hPdfH9tf/fpNVgYzMLbTyuV7D5b5XQeXLYTBc0qvXtjzWWJ5ddk22dJbOx8gSeXntQjK2m+RO5FQl7GPA8ZpoKfV3ny0ONwkjniaju8uiF4pRsYJPmqj1PYmplrjQrXRmkDcrJ6EMKEV3SrD7mCGlDPcs0RRUQo2WqLADylGOhnm6O/h70aHdIeATKw9O1IYm8GHI6pOLNbuiAceSQ==
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.
- [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/13/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/13/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Kenji Maillard, 02/13/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Dominique Larchey-Wendling, 02/13/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Dominique Larchey-Wendling, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Dominique Larchey-Wendling, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Dominique Larchey-Wendling, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Message not available
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/14/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Gert Smolka, 02/13/2021
- Re: [Coq-Club] Dependent typing puzzle, constructor injectivity, Jeremy Dawson, 02/14/2021
Archive powered by MHonArc 2.6.19+.