GhaS Shee (Jul 19 2022 at 08:30): GhaS Shee (Jul 19 2022 at 08:30):(deleted)
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 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
Wow, 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 !
Its now refered in https://github.com/coq-community/coq-art/blob/master/ch15_general_recursion/sqrt_nat_wf.html
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: Jan 29 2023 at 01:02 UTC