coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Elias Castegren <eliasca AT kth.se>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Moving between extrinsic and intrinsic proofs
- Date: Thu, 10 Oct 2019 08:17:57 +0000
- Accept-language: sv-SE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=eliasca AT kth.se; spf=Pass smtp.mailfrom=eliasca AT kth.se; spf=Pass smtp.helo=postmaster AT smtp-4.sys.kth.se
- Ironport-phdr: 9a23:NQzrMB9f+kkG6/9uRHKM819IXTAuvvDOBiVQ1KB40OscTK2v8tzYMVDF4r011RmVBN6dtakP07CempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgtFiCC8bL58Ixm6sRvdvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh8G/ZlNF+jL5VrhyiqRxwwY/Ub52aO/dlZKzRYdYaSHBdUspNVSFMBJ63YYsVD+oGOOZVt4bzp18PrRSkHgmnGf3ixSVThn/qw6I63P4hHh/A3Ac9GN8BrnDUrNTvO6cJTe+61rLFzTbfb/NWwzv985bHfwknrPqRXrxwadLcxVQhGg/ZlFmct4LoMjGP2ukCsGWX9fdsWOahhmI/tg18rCSjyt0yhoXXgo8Z0E3I+CR9zYovONG0VUB2bNi5G5VKrS6aLZF5QsY6TmFopik6zroGtIagfCgP1JQn3wfTZvOdf4iT4hPjT/ydITRkhHJlYr6/nAi9/VChyu36SMa0zE5HojdLn9XQrHwByRLe58qdRvZy/UqtwyuD2gTd5+1cJEA7j6vbK5ovwr4qkZoTtFzOETHymEX3lqCWbVkr9fKz5uTkfrXmpoWQN5RqhQ3mKKQhhtS/AfgkMggJR2WU5eO81KT68ULlRLVKk+Y5n7LCsJHaIMQbvrS2DxVU0oYl8Ra/Di2p3M4WnXkdfxp5f0fNhI/wflrKPfrQDPGlgl3qni0hj6TNOaSkCZHQJFDClq3gdPBz8RgP5hA0yIVy45NdEfkqKenvV0DrudqQWhI9MgWvyO/PC8l9kJgTDzHcSpSFOb/f5AfbrtkkJPOBMddM5WTNbsM97vurtkcX3F8Qea7wjMkMbWygW6ggOFSCJ3nwgpEaHDVT51ZsfKnRkFSHFAVrSTOqRatstDInCMS9ANWbH9H/sPm6xC6+W6ZuSCVDA1GIH23vctXWWOsMLjmfcJZs
Thanks for all your answers! For completeness, to get Xavier’s version
with Program Definition to work without leaving unproved obligations, I
had to add "Hint Extern 1 => apply check_foo_correct”. With this addition
though, the code is about as clean as I could hope for!
Best
/Elias
9 okt. 2019 kl. 17:31 skrev Xavier Leroy <xavier.leroy AT college-de-france.fr>:
On Wed, Oct 9, 2019 at 5:20 PM Elias Castegren <eliasca AT kth.se> wrote:
Hi Coq clubbers
I'm looking for ideas on how to smoothly go from extrinsic proofs
to code with intrinsic proofs. As an example, consider thefollowing simplified scenario.
I have some property "foo" on natural numbers, and a data type"bar" which carries with it a number for which "foo" holds:
Definition foo (x : nat) := x < 5.
Inductive bar :=Bar : {x | foo x} -> bar.
In addition, I have created an algorithm which checks if the"foo" property holds. I have also proven it correct:
Definition check_foo (x : nat) :=match x with| S (S (S (S (S _)))) => false| _ => trueend.
Require Import Lia.
Theorem check_foo_correct :forall x, check_foo x = true <-> foo x.Proof.unfold foo. unfold check_foo.intros. split.- intros H. do 5 (destruct x; try lia).inversion H.- intros Hlt. do 5 (destruct x; try reflexivity).lia.Qed.
What I would like now is a function of type "nat -> option bar"which builds a "bar" from a natural number only if "foo" holds forthat number. So far I have found two ways to do it, but none ofthem are very attractive.
One variant runs the checking function and captures the equalityproof "check_foo n = true", and then uses the correctness theoremas a function to get the property "foo n" with which the argumentof "Bar" can be built:
Theorem check_foo_correct_fun :forall x, check_foo x = true -> foo x.Proof.apply check_foo_correct.Qed.
Definition build_bar (n : nat) : option bar :=let Heq :=if check_foo n as res return option (res = true)then Some eq_reflelse Noneinmatch Heq with| Some refl =>let arg := exist foo n (check_foo_correct_fun n refl)inSome (Bar arg)| None => Noneend.
This is unattractive because it requires dependent patternmatching and explicitly passes around an equality proof in anoption type just to make the typechecker happy.
The second approach builds the function with a proof script:
Definition build_bar' (n : nat) : option bar.remember (check_foo n) as res.symmetry in Heqres. destruct res.- apply check_foo_correct in Heqres.apply (Some (Bar (exist foo n Heqres))).- apply None.Defined.
While this version is shorter, it is arguably worse from asoftware engineering perspective as you need to step through thescript to see what it is doing.
Ideally, what I would want is something like this, where the keyinference needed is that "check_foo n = true" since we are in the"then" branch.
Definition build_bar'' (n : nat) : option bar :=if check_foo nthen Some (Bar (exist foo n _)) (* This does not typecheck *)else None.
I'm guessing that I won't be able to get something this short, butI'm interested in hearing if there are cleaner solutions than thetwo working versions I have found so far.
You could try Program Definition:
Program Definition build_bar'' (n : nat) : option bar :=match check_foo n with
| true => Some (Bar n)| false => Noneend.
Internally it will build something close to your build_bar'. But from the programmer's standpoint it looks much clearer.
Note that you need a "match"; "if" will not remember the equality "check_foo n = true" that you need.
Hope this helps,
- Xavier Leroy
Cheers
/Elias
- [Coq-Club] Moving between extrinsic and intrinsic proofs, Elias Castegren, 10/09/2019
- Re: [Coq-Club] Moving between extrinsic and intrinsic proofs, Xavier Leroy, 10/09/2019
- Re: [Coq-Club] Moving between extrinsic and intrinsic proofs, Elias Castegren, 10/10/2019
- Re: [Coq-Club] Moving between extrinsic and intrinsic proofs, Maximilian Wuttke, 10/09/2019
- Re: [Coq-Club] Moving between extrinsic and intrinsic proofs, Laurent Thery, 10/09/2019
- Re: [Coq-Club] Moving between extrinsic and intrinsic proofs, Xavier Leroy, 10/09/2019
Archive powered by MHonArc 2.6.18.