The Coq mailing list

[Elias Castegren <eliasca AT kth.se>]

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.

Cheers

/Elias