## Stream: Coq users

### Topic: Coq Art Exercise

#### GhaS Shee (Jul 19 2022 at 08:30):

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.
``````

#### GhaS Shee (Jul 19 2022 at 09:31):

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.

#### Karl Palmskog (Jul 19 2022 at 09:34):

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.

#### GhaS Shee (Jul 19 2022 at 09:40):

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.

#### Pierre Castéran (Jul 19 2022 at 11:08):

@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.

#### Karl Palmskog (Jul 19 2022 at 11:20):

@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.

#### GhaS Shee (Jul 19 2022 at 11:34):

@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.

#### Pierre Castéran (Jul 19 2022 at 13:15):

@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 ?

#### Karl Palmskog (Jul 19 2022 at 13:24):

@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.

#### Karl Palmskog (Jul 19 2022 at 13:26):

@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

#### Pierre Castéran (Jul 19 2022 at 13:59):

Is it OK ? First time I use gist !

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

#### Karl Palmskog (Jul 19 2022 at 14:00):

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

#### GhaS Shee (Jul 19 2022 at 14:54):

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

#### Pierre Castéran (Jul 19 2022 at 15:07):

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.

#### Karl Palmskog (Jul 19 2022 at 15:07):

@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

#### Karl Palmskog (Jul 19 2022 at 15:08):

@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

#### Karl Palmskog (Jul 19 2022 at 15:08):

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

#### Pierre Castéran (Jul 19 2022 at 15:31):

@GhaS Shee Cc: @Karl Palmskog @Yves Bertot
Thanks a lot for this improvement !

#### Karl Palmskog (Jul 19 2022 at 15:34):

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

#### Yves Bertot (Jul 20 2022 at 13:02):

Thanks for the work everybody!

Last updated: Jun 20 2024 at 13:02 UTC