In the below example,

what's the difference between `sqrt`

and `sqrt'`

?

They are two instances of answers of the exercise 15.11 in the Coq Art book.

The `sqrt 10`

function actually computes the answer `3`

, while `sqrt' 10`

not.

Both functions are defined with the specification `sqrt_type`

.

```
(* 15.2.6 Well-founded Euclidean Division *)
Check le_plus_minus.
Check plus_assoc.
Definition div_type (m:nat) := forall n, 0<n -> {q & { r | m = q*n+r /\ r < n }}.
Definition sqrt_type (n:nat) := {s & { r | n = s*s+r /\ n < (S s)*(S s) }}.
Definition div_type' m n q := { r | m = q*n+r /\ r < n }.
Definition sqrt_type' n s := { r | n = s*s+r /\ n < (S s)*(S s) }.
Definition div_type'' m n q r := m = q*n+r /\ r < n.
Definition sqrt_type'' n s r := n = s*s+r /\ n < (S s)*(S s).
Check Acc_inv_dep.
Definition div_F :
forall x, (forall y, y < x -> div_type y) -> div_type x.
Proof.
unfold div_type at 2.
refine (fun m div_rec n Hlt =>
match le_gt_dec n m with
| left H_n_le_m =>
match div_rec (m-n) _ n _ with
| existT _ q (exist _ r H_spec) =>
existT (div_type' m n)(S q)(exist (div_type'' m n (S q)) r _ ) end
| right H_n_gt_m =>
existT (div_type' m n) O (exist (div_type'' m n O) m _ ) end );
unfold div_type'' ; lia.
Defined.
Definition div : forall m n, 0 < n -> {q & {r | m = q*n+r /\ r < n }} :=
well_founded_induction lt_wf div_type div_F.
Definition sqrt_F :
forall x, (forall y, y < x -> sqrt_type y) -> sqrt_type x.
Proof.
destruct x.
refine (fun sqrt_rec => existT _ 0 (exist _ 0 _ )); lia.
unfold sqrt_type at 2.
refine (fun sqrt_rec =>
let n := S x in
match div n 4 _ with
| existT _ q (exist _ r0 _ ) =>
match sqrt_rec q _ with
| existT _ s' (exist _ r' H_spec) =>
match le_gt_dec (S(4*s')) (4*r'+r0) with
| left HSs =>
let s := 2*s'+1 in
let r := 4*r'+r0 - S(4*s') in
existT(sqrt_type' n) s (exist (sqrt_type'' n s) r _ )
| right Hs =>
let s := 2*s' in
let r := 4*r'+r0 in
existT(sqrt_type' n) s (exist (sqrt_type'' n s) r _ ) end end end);
unfold sqrt_type''; auto with zarith.
Defined.
Definition sqrt : forall n, {s & {r | n = s*s+r /\ n <(S s)*(S s)}} :=
well_founded_induction lt_wf sqrt_type sqrt_F.
Eval compute in
match sqrt 10 with
| existT _ s _ => s end .
Eval compute in
match div 100 15 _ with
| existT _ q (exist _ r _ ) => (q,r) end .
(* the second answer *)
Definition sqrt_F' :
forall x, (forall y, y < x -> sqrt_type y) -> sqrt_type x.
Proof.
destruct x.
- intros. exists 0. exists 0. auto with arith.
- intros sqrt_rec. set (S x) as n. fold n.
destruct (div n 4) as [q [r0 [H1 H2]]]; auto with zarith.
+ destruct (sqrt_rec q) as [s' [r' [H1' H2']]]; auto with zarith.
* { case (le_gt_dec (S(4*s')) (4*r'+r0)).
- intros. exists (S(2*s')), (4*r'+r0-4*s'-1). auto with zarith.
- intros. exists (2*s' ), (4*r'+r0 ). auto with zarith. }
Defined.
Definition sqrt' : forall n:nat, {s & { r | n = s*s+r /\ n < (S s)*(S s) }} :=
well_founded_induction lt_wf sqrt_type sqrt_F'.
Eval compute in match sqrt' 10 with
existT _ s _ => s end.
```

Replacing the line `destruct (div n 4) as [q [r0 [H1 H2]]]; auto with zarith. `

with

`refine (match div n 4 _ with | existT _ q (exist r0 _) => _ end); auto with zarith. `

solved it.

it's not a good idea to compute with types like `{x | P x}`

inside Coq, since you will be computing the proof(s) as well, which can get stuck and/or take ages. Unfortunately, there is no easy way to fix this other than extracting the function to OCaml or Haskell, which makes the proof parts disappear.

Thanks for the reply.

And I have understood what was the wrong part, just now.

It worked if we replace the line

`destruct (div n 4) as [q [r0 [H1 H2]]]; auto with zarith. `

with

`refine (match div n 4 _ with | existT _ q (exist r0 _) => _ end); auto with zarith. `

in the Proof Definition of `sqrt_F'`

.

`div n 4`

should have taken another argument whose type is `0<4`

.

Rather, we should have put the term in the form `div n 4 _`

which forces the computation of `div`

function if it is placed in the condition of `match ~ with `

clause.

@GhaS Shee Thank you !

By the way, may I ask you on which repo you found `sqrt_F'`

? I just could find another version in

https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/SRC/sqrt_nat_wf.v, with a similar evaluation issue.

@Pierre Castéran ah, so it's a problem in the Coq'Art sources? We probably need to update CI and so on if you want to do changes, but you can make a PR and I'll be happy to take care of CI configuration updates.

@Pierre Castéran

With my pleasure!

I wrote the code following the convention written in the great book, with my bug.

I have just uploaded on github: https://github.com/ghasshee/coq/blob/master/art/chap15.v

(Wow, I am so honoured to have a reply from one of the authors! I could not express my appreciation for the book! )

@Karl Palmskog

Yes, I also think so! I also tried the coq-community's answer code but I failed to compute it.

It seems there is the similar bug in that.

@GhaS Shee @Karl Palmskog If you agree, we add to the Coq-community' coq-art repo a file, e.g. `sqrt_by_Ghas_Shee.v`

(extracted from your `chap15.v`

) with a mention that it solves the computation issue.

Karl, a better solution would be that GhaS Shee appears as a contributor of the collective coq-art repo. Is there a simple github way to do that ? I have prepared a file with some very minor changes. I can send it or upload it in gist ?

@Pierre Castéran @GhaS Shee the easiest way to have GhaS as contributor is for GhaS to open a pull request with the changes. My recommendation is to make a fork of https://github.com/coq-community/coq-art - add a commit in a branch, say `sqrt-new`

, which has the changes, and then open a pull request via GitHub. Then, Pierre and I can make changes directly in the pull request branch (GitHub by default allows this) to better fit our purpose of improving the coq-art repo, and then merge it.

@Pierre Castéran feel free to put the changes in a Gist, and I can then use these changes to improve the pull request by GhaS

Is it OK ? First time I use gist !

https://gist.github.com/Casteran/2f8949c8030db9c4aa3a681fd2734658

thanks, I can work with that, now we'd just like the pull request from @GhaS Shee if possible

@Karl Palmskog

I have opened a request with the gist with @Pierre Castéran 's comment. Thank you for the great repository too! :)

Indeed, what we have to do is to add a line in _CoqProject and a link in https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/sqrt_nat_wf.html, right ?

When recompiling coq-art, I noticed a lot of 8.16 deprecation warnings. When it is a little cooler in Bordeaux, I will fix them.

@Pierre Castéran I did a pass over the pull request, maybe you can take a quick look and then merge if it looks good to you (one change is that I call the new file `sqrt_compute.v`

as memento of why we add it): https://github.com/coq-community/coq-art/pull/24

@Pierre Castéran we should probably roll back these changes, now that Coq 8.15.1 and later does not have the problem with Scheme: https://github.com/coq-community/coq-art/commit/905812646d536bc8c168699199d2fc71862e313f

due to people being busy, we never did a coq-art repo tag for Coq 8.15, there probably should be one

@GhaS Shee Cc: @Karl Palmskog @Yves Bertot

Thanks a lot for this improvement !

Its now refered in https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/sqrt_nat_wf.html

Also deployed here: https://coq-community.org/coq-art/ch15_general_recursion/sqrt_nat_wf.html

Thanks for the work everybody!

Last updated: Jun 20 2024 at 13:02 UTC