Nat.sqrt

Stream: lean4

[James Gallicchio]

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]

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]

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

[Mario Carneiro]

src#nat.sqrt

[James Gallicchio]

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

[James Gallicchio]

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

[Mario Carneiro]

that should not go in the .Basic file

[James Gallicchio]

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

[James Gallicchio]

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]

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

[James Gallicchio]

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

[Mario Carneiro]

no real arithmetic here

[Mario Carneiro]

just clear all the denominators and do it on nat

[James Gallicchio]

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

[Reid Barton]

Because $1 + \varepsilon \ge 1$, and $1 + \varepsilon \ge \varepsilon$.

[Mario Carneiro]

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]

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]

here's a computation over the reals:

$$0\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]

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

[Mario Carneiro]

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

[James Gallicchio]

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

[James Gallicchio]

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

[Mario Carneiro]

which one?

[Mario Carneiro]

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

[James Gallicchio]

Ohh yes you're right I see

[Kevin Buzzard]

They're adjoint functors

[James Gallicchio]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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