GhaS Shee (Jul 19 2022 at 08:30): 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.
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 !
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: Oct 01 2023 at 19:01 UTC