The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

Hi Elias,.

You can simplify your definition using the depending match a bit.

```
Definition build_bar'' (n : nat) : option bar :=
  (if check_foo n as b return (check_foo n = b -> option bar)
   then fun refl => let arg := exist foo n (check_foo_correct_fun n refl)
                 in Some (Bar arg)
   else fun _ => None) eq_refl.
```

Best
Maximilian


On 09/10/2019 17:16, Elias Castegren 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.
> 
> Cheers
> 
> /Elias
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature