(deleted)

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

Wow, 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: Jan 29 2023 at 01:02 UTC