square roots are square roots

Stream: mathlib4

[Siddhartha Gadgil]

All but one function in Data/Nat/Sqrt has been ported by @Anand Rao in mathlib4#1142 but that one is a little tricky. As far as I can tell the definition of sqrt is new, so the ported proof gives nothing. I started proving it and it is conceptually interesting. We will keep working on this, but as there are experts here I am sharing the current state (extracted from file).

-- Porting note: as the definition of square root has changed, the proof of `sqrt_IsSqrt` is attempted from scratch.
/-
Sketch of proof:
Up to rounding, in terms of the definition of `sqrt.iter`,

* By AM-GM inequality, `next² ≥ n` giving one of the bounds.
* When we terminated, we have `guess ≥ next` from which we deduce the other bound `n ≥ next²`.

To turn this into a lean proof we need to manipulate, use properties of natural number division etc.
-/
private theorem sqrt_IsSqrt (n : ℕ) : IsSqrt n (sqrt n) := by
  by_cases n ≤ 1
  case pos =>
    match n with
    | 0 => simp [IsSqrt]
    | 1 => simp [IsSqrt]
    | m + 2 => contradiction
  case neg =>
    simp [IsSqrt, h]
    have l : sqrt n = sqrt.iter n (n/2) :=
      by unfold sqrt; apply if_neg h
    rw [l]
    sorry

[Siddhartha Gadgil]

To make the above more self-contained, the key definition from sqrt.iter is:
let next := (guess + n / guess) / 2

[Siddhartha Gadgil]

and the termination condition is next ≥ guess

[Johan Commelin]

You can golf the first four lines of case neg down to simp only [IsSqrt, sqrt, h, ite_false]

[Siddhartha Gadgil]

Thanks. Done that.

[Johan Commelin]

Hmm, I don't know how to prove this.

[Heather Macbeth]

Should we go back to the mathlib3 definition of nat.sqrt? It looks like this is where the Lean 4 definition was introduced:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Nat.2Esqrt

[Johan Commelin]

I think we can fix the sorried proof above.

[Johan Commelin]

But maybe @Mario Carneiro should confirm that he's happy with the current Nat.sqrt def'n

[Mario Carneiro]

The new definition is better. As usual, this comes with some mathematics and we haven't tried to sit down and do it yet, so it's inevitable that some sorries will get introduced when the porting wave hits. I don't like the pressure this is bringing to try to use short ad hoc fixes so that it remains sorry-free at all times without actually thinking about the mathematics

[Heather Macbeth]

Maybe for now we can just write a definition Nat.sqrt' and sorry'd lemma Nat.sqrt = Nat.sqrt', and then port the mathlib3 stuff intact?

[Heather Macbeth]

That seems safer than putting in many separate sorries -- if there is a mistake somewhere it will be easy with that setup to go back to the mathlib3 definition.

[Mario Carneiro]

okay, but I don't think there is a future where we will adopt the old definition unless we just completely run out of time and the project goes on life support. If the new definition is buggy the bugs will be fixed in the process of proving that theorem

[Mario Carneiro]

I just don't see the point in keeping a somewhat technical proof about a definition we aren't going to keep anyway on our way to a different technical proof

[Mario Carneiro]

We know that there exists a function equal to nat.sqrt since we proved it in lean 3. So I think the sqrt lemmas are a pretty safe bet

[Siddhartha Gadgil]

Good progress is being made on this along with (now mainly by) @Anand Rao and @Johan Commelin and it is worth trying a little longer. I am hopeful this will get done today or tomorrow.

[Kevin Buzzard]

Is anyone working on this now? I might have a go at the sorry in data.nat.sqrt (I think I have a paper proof)

[Dan Velleman]

I think I have a paper proof too. The idea is to use lt_div_mul_add twice to get 2 * guess * (next + 1) > guess^2 + n. Then square both sides, and rewrite the right side as (guess^2 - n)^2 + 4 * guess^2 * n, which is ≥ 4 * guess^2 * n.

[Kevin Buzzard]

I've got a Lean proof :-) modulo some lemmas which are much simpler. And no natural subtraction ;-) I'll tidy it up a little and push.

[Kevin Buzzard]

When library_search fails to close a goal it instead barfs out 100 things I don't want to hear all beginning refine :-(

[Ruben Van de Velde]

Yeah, what's up with that anyway?

[Kevin Buzzard]

Any takers for

lemma aux_lemma_one {a b : ℕ} : 4 * a * b ≤ (a + b) * (a + b) := sorry
lemma aux_lemma_five {a : ℕ} : a / 2 + 1 = (a + 2) / 2 := sorry
lemma aux_lemma_six {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := sorry

[Kevin Buzzard]

Modulo that we're done; I've just pushed.

[Kevin Buzzard]

lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
  n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1) := by
  unfold sqrt.iter
  -- m was `next`
  let m := (guess + n / guess) / 2
  by_cases h : m < guess
  case pos =>
    have : n < (m + 1) * (m + 1) := by
      refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
      apply lt_of_le_of_lt aux_lemma_one
      rw [show (4 : ℕ) = 2 * 2 from rfl]
      rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
      refine mul_self_lt_mul_self ?_
      rw [aux_lemma_five, mul_comm 2, mul_assoc,
        show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
      refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma_six)
      rw [add_assoc, mul_add]
      exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
    simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
  case neg =>
    simpa only [dif_neg h] using hn

[Heather Macbeth]

Only tested on Lean 3, but:

lemma aux_lemma_one {a b : ℕ} : 4 * a * b ≤ (a + b) * (a + b) := by
  linarith [sq_nonneg (a - b : ℤ)]

[Kevin Buzzard]

ring isn't imported in this file, this is why it's so annoying :-(

[Mario Carneiro]

heh, you're really trying to make this hard to port to std

[Kevin Buzzard]

yeah linarith isn't there either

[Kevin Buzzard]

you wouldn't catch me doing rw [add_assoc, mul_add] normally, it's all rw [show thing = rearranged_thing by ring] as far as I'm concerned, but not here.

[Dan Velleman]

You should be able to get aux_lemma_six by applying lt_div_mul_add to get a + 1 < ((a + 1)/2) * 2 + 2

[Kevin Buzzard]

Thanks!

lemma aux_lemma_six {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
  rw [mul_comm]
  exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 (by decide)

[Kevin Buzzard]

In fact @Dan Velleman I should stop trying to prove my lemmas and just use lt_div_mul_add in the actual proof as you've been telling me all along.

[Kevin Buzzard]

OK I couldn't get anyone to bite so I've just finished it myself and pushed :D

[Kevin Buzzard]

bleurgh it doesn't lint because of other issues. I'm still working on this file.

[Kevin Buzzard]

OK I'm cheating because it's bedtime. Hopefully we'll get a green tick but I had to avoid a linter. @Mario Carneiro I can't figure out how to write the equation lemmas for sqrtAux because unfold unfolds too much and well-founded fix is inscrutible to me. I'm cheating and nolinting. In Lean 3 I would be all over the equation lemmas but in Lean 4 it seems that the relevant ones are marked unsafe. It's really hard to minimise too because the declaration uses all kind of bit stuff.