The Coq mailing list

[Elias Castegren <eliasca AT kth.se>]

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