Zulip Chat Archive

Stream: lean4

Topic: Nat.sqrt


James Gallicchio (Nov 01 2022 at 19:13):

I made a PR to add Nat.sqrt to Std, using a Lean implementation of Newton's method, but should Lean export a sqrt function that calls out to mpz?

James Gallicchio (Nov 01 2022 at 19:25):

It could also be slightly more efficient if the most significant bit function were exposed (I think fast sqrt is basically: get a good starting guess using the MSB, then apply newtons method a couple times to get the exact value)

Mario Carneiro (Nov 01 2022 at 19:26):

You can also use bit operations here, I think the mathlib implementation does that

Mario Carneiro (Nov 01 2022 at 19:26):

src#nat.sqrt

James Gallicchio (Nov 01 2022 at 20:28):

I can see if it makes a big performance difference, but I like the readability of the current implementation :joy:

James Gallicchio (Nov 01 2022 at 20:29):

Oh, I did also prove that it returns the correct value, maybe I should include that lemma in the PR

Mario Carneiro (Nov 01 2022 at 21:59):

that should not go in the .Basic file

James Gallicchio (Nov 01 2022 at 23:52):

:thumbs_up: I committed some ugly proofs to .Lemmas, will try to clean up

James Gallicchio (Nov 02 2022 at 04:51):

I actually have no idea how to finish the correctness proof, I think it suffices to show that
n < succ ((g + n / g) / 2) * succ ((g + n / g) / 2) for all n g : Nat
but I have no clue how to prove this...

Mario Carneiro (Nov 02 2022 at 04:57):

See https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Convergence

James Gallicchio (Nov 02 2022 at 04:58):

Yeah, but I mean without resorting to arithmetic on reals :joy:

Mario Carneiro (Nov 02 2022 at 04:58):

no real arithmetic here

Mario Carneiro (Nov 02 2022 at 04:59):

just clear all the denominators and do it on nat

James Gallicchio (Nov 02 2022 at 05:10):

image.png even in the reals I'm not sure why this step holds

Reid Barton (Nov 02 2022 at 05:15):

Because 1+ε11 + \varepsilon \ge 1, and 1+εε1 + \varepsilon \ge \varepsilon.

Mario Carneiro (Nov 02 2022 at 05:15):

I also recently wrote up the sketch of this proof in the context of an intuitionistic proof of the existence of square roots for metamath, see https://github.com/metamath/set.mm/issues/2101#issuecomment-882301206

James Gallicchio (Nov 11 2022 at 16:58):

theorem lemma (hn : n > 1) (_ : x  n)
  (h_low : n < (x+1)^2) (h_dec : (x + n / x) / 2 < x)
  : n < ((x + n / x) / 2 + 1)^2
  := sorry

This is the missing piece of the proof currently on my branch of std4. It appears to be true, but no clue how to prove it.

Mario Carneiro (Nov 11 2022 at 17:29):

here's a computation over the reals:

0(xn)2=x2+n22xn2xnx2+n2x2+n2nxn/x2nxn/x2nx+n/xn(x+n/x)/2<(x+n/x)/2+1n<(x+n/x)/2+1n<((x+n/x)/2+1)20\le (x-\lfloor\sqrt{n}\rfloor)^2=x^2+\lfloor\sqrt{n}\rfloor^2-2x\lfloor\sqrt{n}\rfloor\\ 2x\lfloor\sqrt{n}\rfloor\le x^2+\lfloor\sqrt{n}\rfloor^2\le x^2+n\\ 2\lfloor\sqrt{n}\rfloor-x\le n/x\\ 2\lfloor\sqrt{n}\rfloor-x\le \lfloor n/x\rfloor\\ 2\lfloor\sqrt{n}\rfloor\le x +\lfloor n/x\rfloor\\ \lfloor\sqrt{n}\rfloor\le(x +\lfloor n/x\rfloor)/2<\lfloor(x +\lfloor n/x\rfloor)/2\rfloor+1\\ \sqrt{n}<\lfloor(x +\lfloor n/x\rfloor)/2\rfloor+1\\ n<(\lfloor(x +\lfloor n/x\rfloor)/2\rfloor+1)^2

Mario Carneiro (Nov 11 2022 at 17:32):

your task @James Gallicchio is to do this computation using only natural numbers and using natural division directly instead of floors

Mario Carneiro (Nov 11 2022 at 17:33):

(note that none of the assumptions are necessary here, except to prove that nn and xx are nonzero so that the divisions are sensible)

James Gallicchio (Nov 11 2022 at 18:25):

I think the step that adds the floor to the division n/x needs some additional assumption

James Gallicchio (Nov 11 2022 at 18:26):

And similar for the one that removes the floor from root n.

Mario Carneiro (Nov 11 2022 at 18:27):

which one?

Mario Carneiro (Nov 11 2022 at 18:27):

I believe both of those are instances of the theorem z <= r <-> z <= floor r when z is an integer

James Gallicchio (Nov 11 2022 at 18:29):

Ohh yes you're right I see

Kevin Buzzard (Nov 12 2022 at 00:11):

They're adjoint functors

James Gallicchio (Nov 12 2022 at 00:25):

I'm... not sure what that means :cry: do you mean the functor pair between R and N formed by flooring and ofNating?

James Gallicchio (Nov 12 2022 at 00:26):

If you mean that this can be proven by moving into the reals, showing the above computation holds, and then going back to the nats, I agree, but since this is going in Std we need to/should be able to give a more elementary proof using just lemmas on Nat

James Gallicchio (Nov 12 2022 at 00:27):

(Or do you mean each step must necessarily be true in Nat and therefore this is a good outline to follow?)

Mario Carneiro (Nov 12 2022 at 00:42):

It's been a while since I got a chance to use the galois connection emoji :repeat:

Kevin Buzzard (Nov 12 2022 at 01:45):

I mean those facts will be in the library because they're the proofs that the maps form a Galois convention


Last updated: Dec 20 2023 at 11:08 UTC