Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The explanation for the proof of edivnP #148

Open
akr opened this issue Mar 11, 2023 · 0 comments
Open

The explanation for the proof of edivnP #148

akr opened this issue Mar 11, 2023 · 0 comments

Comments

@akr
Copy link

akr commented Mar 11, 2023

I found that the explanation of the proof of edivnP on p. 110 is not updated.
I read the book version 1.0.2.

The proof of edivnP is changed in the commit:
3448f11

The current proof is as follows.

(* 1 *) rewrite -[m]/(0 * d + m).
(* 2 *) case: d => [//= | d /=] in ed *.
(* 3 *) rewrite -[edivn m d.+1]/(edivn_rec d m 0) in ed *.
(* 4 *) case: (ubnPgeq m) @ed; elim: m 0 => [|m IHm] q [/=|n] leq_nm //.
(* 5 *) rewrite edivn_recE subn_if_gt; case: ifP => [le_dm ed|lt_md]; last first.
(* 6 *)   by rewrite /= ltnS ltnNge lt_md eqxx.
(* 7 *) rewrite -ltnS in le_dm; rewrite -(subnKC le_dm) addnA -mulSnr subSS.
(* 8 *) by apply: IHm q.+1 (n-d) _; apply: leq_trans (leq_subr d n) leq_nm.

The old proof is follows.

(* 1 *) case: d => [//=|d /=] in ed *.
(* 2 *) rewrite -[edivn m d.+1]/(edivn_rec d m 0) in ed *.
(* 3 *) rewrite -[m]/(0 * d.+1 + m).
(* 4 *) elim: m {-2}m 0 (leqnn m) @ed => [[]//=|n IHn [//=|m]] q le_mn.
(* 5 *) rewrite edivn_recE subn_if_gt; case: ifP => [le_dm|lt_md]; last first.
(* 6 *)   by rewrite /= ltnS ltnNge lt_md eqxx.
(* 7 *) have /(IHn _ q.+1) : m - d <= n by rewrite (leq_trans (leq_subr d m)).
(* 8 *) by rewrite /= mulSnr -addnA -subSS subnKC.

"Line 1 handles the case of d being zero." refers to the first "case" line
but it wrongly refers to the first "rewrite" line now.
"Line 1" should be changed to "Line 2".

"Lines 2 and 3 prepare the induction ..." refers
first two "rewrite" lines.
"Lines 2 and 3" should be changed to "Line 1 and 3".

"replacing m by (0 * d.+1 + m). Recall the case d being 0 has already been handled."
is not appropriate now because m is replaced by (0 * d + m) in the current proof.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant