Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Moving between extrinsic and intrinsic proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Moving between extrinsic and intrinsic proofs


Chronological Thread 
  • 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 the
following 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
      | _ => true
      end.

    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 for
that number. So far I have found two ways to do it, but none of
them are very attractive.

One variant runs the checking function and captures the equality
proof "check_foo n = true", and then uses the correctness theorem
as a function to get the property "foo n" with which the argument
of "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_refl
          else None
      in
      match Heq with
      | Some refl =>
        let arg := exist foo n (check_foo_correct_fun n refl)in
        Some (Bar arg)
      | None => None
      end.

This is unattractive because it requires dependent pattern
matching and explicitly passes around an equality proof in an
option 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 a
software engineering perspective as you need to step through the
script to see what it is doing.

Ideally, what I would want is something like this, where the key
inference needed is that "check_foo n = true" since we are in the
"then" branch.

    Definition build_bar'' (n : nat) : option bar :=
      if check_foo n
      then 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, but
I'm interested in hearing if there are cleaner solutions than the
two 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 => None
  end.

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




Archive powered by MHonArc 2.6.18.

Top of Page