chore(Data/Nat/Defs): Integrate Nat.sqrt material (#11866)

Move the content of `Data.Nat.ForSqrt` and `Data.Nat.Sqrt` to `Data.Nat.Defs` by using `Nat`-specific Std lemmas rather than the mathlib general ones. This makes it ready to move to Std if wanted.

Archive/Imo/Imo2021Q1.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys
 -/
 import Mathlib.Data.Nat.Interval
-import Mathlib.Data.Nat.Sqrt
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.Linarith
 

Mathlib.lean

@@ -1978,7 +1978,6 @@ import Mathlib.Data.Nat.Factorization.Root
 import Mathlib.Data.Nat.Factors
 import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Data.Nat.Fib.Zeckendorf
-import Mathlib.Data.Nat.ForSqrt
 import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Nat.GCD.BigOperators
 import Mathlib.Data.Nat.Hyperoperation
@@ -2000,7 +1999,6 @@ import Mathlib.Data.Nat.PrimeFin
 import Mathlib.Data.Nat.PrimeNormNum
 import Mathlib.Data.Nat.Set
 import Mathlib.Data.Nat.Size
-import Mathlib.Data.Nat.Sqrt
 import Mathlib.Data.Nat.SqrtNormNum
 import Mathlib.Data.Nat.Squarefree
 import Mathlib.Data.Nat.SuccPred

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
+import Mathlib.Algebra.Parity
 import Mathlib.Order.Filter.AtTopBot
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.LinearCombination

Mathlib/Computability/Ackermann.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 -/
+import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Computability.Primrec
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Linarith

Mathlib/Data/Int/Parity.lean

@@ -3,8 +3,9 @@ Copyright (c) 2019 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
 -/
-import Mathlib.Data.Nat.Parity
 import Mathlib.Algebra.Ring.Int
+import Mathlib.Data.Int.Sqrt
+import Mathlib.Data.Nat.Parity
 import Mathlib.Tactic.Abel
 
 #align_import data.int.parity from "leanprover-community/mathlib"@"e3d9ab8faa9dea8f78155c6c27d62a621f4c152d"
@@ -95,6 +96,11 @@ instance : DecidablePred (Even : ℤ → Prop) := fun _ => decidable_of_iff _ ev
 
 instance : DecidablePred (Odd : ℤ → Prop) := fun _ => decidable_of_iff _ odd_iff_not_even.symm
 
+/-- `IsSquare` can be decided on `ℤ` by checking against the square root. -/
+instance : DecidablePred (IsSquare : ℤ → Prop) :=
+  fun m ↦ decidable_of_iff' (sqrt m * sqrt m = m) <| by
+    simp_rw [← exists_mul_self m, IsSquare, eq_comm]
+
 @[simp]
 theorem not_even_one : ¬Even (1 : ℤ) := by
   rw [even_iff]

Mathlib/Data/Int/Sqrt.lean

@@ -3,7 +3,9 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Data.Nat.Sqrt
+import Mathlib.Data.Int.Defs
+import Mathlib.Data.Nat.Defs
+import Mathlib.Tactic.Common
 
 #align_import data.int.sqrt from "leanprover-community/mathlib"@"ba2245edf0c8bb155f1569fd9b9492a9b384cde6"
 
@@ -37,9 +39,4 @@ theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
   natCast_nonneg _
 #align int.sqrt_nonneg Int.sqrt_nonneg
 
-/-- `IsSquare` can be decided on `ℤ` by checking against the square root. -/
-instance : DecidablePred (IsSquare : ℤ → Prop) :=
-  fun m => decidable_of_iff' (sqrt m * sqrt m = m) <| by
-    simp_rw [← exists_mul_self m, IsSquare, eq_comm]
-
 end Int

Mathlib/Data/Nat/Defs.lean

@@ -12,6 +12,7 @@ import Mathlib.Tactic.PushNeg
 import Mathlib.Util.AssertExists
 
 #align_import data.nat.basic from "leanprover-community/mathlib"@"bd835ef554f37ef9b804f0903089211f89cb370b"
+#align_import data.nat.sqrt from "leanprover-community/mathlib"@"ba2245edf0c8bb155f1569fd9b9492a9b384cde6"
 
 /-!
 # Basic operations on the natural numbers
@@ -678,6 +679,22 @@ protected lemma eq_div_of_mul_eq_left (hc : c ≠ 0) (h : a * c = b) : a = b / c
 protected lemma eq_div_of_mul_eq_right (hc : c ≠ 0) (h : c * a = b) : a = b / c := by
   rw [← h, Nat.mul_div_cancel_left _ (Nat.pos_iff_ne_zero.2 hc)]
 
+protected lemma mul_le_of_le_div (k x y : ℕ) (h : x ≤ y / k) : x * k ≤ y := by
+  if hk : k = 0 then
+    rw [hk, Nat.mul_zero]; exact zero_le _
+  else
+    rwa [← le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hk)]
+
+protected lemma div_mul_div_le (a b c d : ℕ) :
+    (a / b) * (c / d) ≤ (a * c) / (b * d) := by
+  if hb : b = 0 then simp [hb] else
+  if hd : d = 0 then simp [hd] else
+  have hbd : b * d ≠ 0 := Nat.mul_ne_zero hb hd
+  rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]
+  transitivity ((a / b) * b) * ((c / d) * d)
+  · apply Nat.le_of_eq; simp only [Nat.mul_assoc, Nat.mul_left_comm]
+  · apply Nat.mul_le_mul <;> apply div_mul_le_self
+
 /-!
 ### `pow`
 
@@ -1419,6 +1436,235 @@ lemma div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d
   exact lt_of_le_of_lt (mul_div_le a d) h
 #align nat.div_lt_div_of_lt_of_dvd Nat.div_lt_div_of_lt_of_dvd
 
+/-!
+### `sqrt`
+
+See [Wikipedia, *Methods of computing square roots*]
+(https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).
+-/
+
+private lemma iter_fp_bound (n k : ℕ) :
+    let iter_next (n guess : ℕ) := (guess + n / guess) / 2;
+    sqrt.iter n k ≤ iter_next n (sqrt.iter n k) := by
+  intro iter_next
+  unfold sqrt.iter
+  if h : (k + n / k) / 2 < k then
+    simpa [if_pos h] using iter_fp_bound _ _
+  else
+    simpa [if_neg h] using Nat.le_of_not_lt h
+
+private lemma AM_GM : {a b : ℕ} → (4 * a * b ≤ (a + b) * (a + b))
+  | 0, _ => by rw [Nat.mul_zero, Nat.zero_mul]; exact zero_le _
+  | _, 0 => by rw [Nat.mul_zero]; exact zero_le _
+  | a + 1, b + 1 => by
+    simpa only [Nat.mul_add, Nat.add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, Nat.one_mul,
+      Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_le_add_iff_left]
+      using Nat.add_le_add_right (@AM_GM a b) 4
+
+-- These two lemmas seem like they belong to `Std.Data.Nat.Basic`.
+
+lemma sqrt.iter_sq_le (n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n := by
+  unfold sqrt.iter
+  let next := (guess + n / guess) / 2
+  if h : next < guess then
+    simpa only [dif_pos h] using sqrt.iter_sq_le n next
+  else
+    simp only [dif_neg h]
+    apply Nat.mul_le_of_le_div
+    apply Nat.le_of_add_le_add_left (a := guess)
+    rw [← Nat.mul_two, ← le_div_iff_mul_le]
+    · exact Nat.le_of_not_lt h
+    · exact Nat.zero_lt_two
+
+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
+  dsimp
+  split_ifs with h
+  · suffices n < (m + 1) * (m + 1) by
+      simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
+    refine Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))
+    apply Nat.lt_of_le_of_lt AM_GM
+    rw [show (4 : ℕ) = 2 * 2 from rfl]
+    rw [Nat.mul_mul_mul_comm 2, Nat.mul_mul_mul_comm (2 * guess)]
+    refine Nat.mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
+    rw [← add_div_right _ (by decide), Nat.mul_comm 2, Nat.mul_assoc,
+      show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
+    have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by omega
+    refine lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)
+    rw [Nat.add_assoc, Nat.mul_add]
+    exact Nat.add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
+  · simpa only [dif_neg h] using hn
+
+#align nat.sqrt Nat.sqrt
+-- Porting note: the implementation òf `Nat.sqrt` in `Std` no longer needs `sqrt_aux`.
+#noalign nat.sqrt_aux_dec
+#noalign nat.sqrt_aux
+#noalign nat.sqrt_aux_0
+#noalign nat.sqrt_aux_1
+#noalign nat.sqrt_aux_2
+private def IsSqrt (n q : ℕ) : Prop :=
+  q * q ≤ n ∧ n < (q + 1) * (q + 1)
+-- 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 lemma sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n) := by
+  match n with
+  | 0 => simp [IsSqrt, sqrt]
+  | 1 => simp [IsSqrt, sqrt]
+  | n + 2 =>
+    have h : ¬ (n + 2) ≤ 1 := by simp
+    simp only [IsSqrt, sqrt, h, ite_false]
+    refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
+    simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc]
+    rw [lt_add_one_iff, Nat.add_assoc, ← Nat.mul_two]
+    refine le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_
+    rw [Nat.add_comm, Nat.add_le_add_iff_right, add_mod_right]
+    simp only [Nat.zero_lt_two, add_div_right, succ_mul_succ]
+    refine le_trans (b := 1) ?_ ?_
+    · exact (lt_succ.1 <| mod_lt n Nat.zero_lt_two)
+    · exact Nat.le_add_left _ _
+
+lemma sqrt_le (n : ℕ) : sqrt n * sqrt n ≤ n := (sqrt_isSqrt n).left
+#align nat.sqrt_le Nat.sqrt_le
+
+lemma sqrt_le' (n : ℕ) : sqrt n ^ 2 ≤ n := by simpa [Nat.pow_two] using sqrt_le n
+#align nat.sqrt_le' Nat.sqrt_le'
+
+lemma lt_succ_sqrt (n : ℕ) : n < succ (sqrt n) * succ (sqrt n) := (sqrt_isSqrt n).right
+#align nat.lt_succ_sqrt Nat.lt_succ_sqrt
+
+lemma lt_succ_sqrt' (n : ℕ) : n < succ (sqrt n) ^ 2 := by simpa [Nat.pow_two] using lt_succ_sqrt n
+#align nat.lt_succ_sqrt' Nat.lt_succ_sqrt'
+
+lemma sqrt_le_add (n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n := by
+  rw [← succ_mul]; exact le_of_lt_succ (lt_succ_sqrt n)
+#align nat.sqrt_le_add Nat.sqrt_le_add
+
+lemma le_sqrt : m ≤ sqrt n ↔ m * m ≤ n :=
+  ⟨fun h ↦ le_trans (mul_self_le_mul_self h) (sqrt_le n),
+    fun h ↦ le_of_lt_succ <| Nat.mul_self_lt_mul_self_iff.1 <| lt_of_le_of_lt h (lt_succ_sqrt n)⟩
+#align nat.le_sqrt Nat.le_sqrt
+
+lemma le_sqrt' : m ≤ sqrt n ↔ m ^ 2 ≤ n := by simpa only [Nat.pow_two] using le_sqrt
+#align nat.le_sqrt' Nat.le_sqrt'
+
+lemma sqrt_lt : sqrt m < n ↔ m < n * n := by simp only [← not_le, le_sqrt]
+#align nat.sqrt_lt Nat.sqrt_lt
+
+lemma sqrt_lt' : sqrt m < n ↔ m < n ^ 2 := by simp only [← not_le, le_sqrt']
+#align nat.sqrt_lt' Nat.sqrt_lt'
+
+lemma sqrt_le_self (n : ℕ) : sqrt n ≤ n := le_trans (le_mul_self _) (sqrt_le n)
+#align nat.sqrt_le_self Nat.sqrt_le_self
+
+lemma sqrt_le_sqrt (h : m ≤ n) : sqrt m ≤ sqrt n := le_sqrt.2 (le_trans (sqrt_le _) h)
+#align nat.sqrt_le_sqrt Nat.sqrt_le_sqrt
+
+@[simp] lemma sqrt_zero : sqrt 0 = 0 := rfl
+#align nat.sqrt_zero Nat.sqrt_zero
+
+@[simp] lemma sqrt_one : sqrt 1 = 1 := rfl
+#align nat.sqrt_one Nat.sqrt_one
+
+lemma sqrt_eq_zero : sqrt n = 0 ↔ n = 0 :=
+  ⟨fun h ↦
+      Nat.eq_zero_of_le_zero <| le_of_lt_succ <| (@sqrt_lt n 1).1 <| by rw [h]; decide,
+    by rintro rfl; simp⟩
+#align nat.sqrt_eq_zero Nat.sqrt_eq_zero
+
+lemma eq_sqrt : a = sqrt n ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1) :=
+  ⟨fun e ↦ e.symm ▸ sqrt_isSqrt n,
+   fun ⟨h₁, h₂⟩ ↦ le_antisymm (le_sqrt.2 h₁) (le_of_lt_succ <| sqrt_lt.2 h₂)⟩
+#align nat.eq_sqrt Nat.eq_sqrt
+
+lemma eq_sqrt' : a = sqrt n ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2 := by
+  simpa only [Nat.pow_two] using eq_sqrt
+#align nat.eq_sqrt' Nat.eq_sqrt'
+
+lemma le_three_of_sqrt_eq_one (h : sqrt n = 1) : n ≤ 3 :=
+  le_of_lt_succ <| (@sqrt_lt n 2).1 <| by rw [h]; decide
+#align nat.le_three_of_sqrt_eq_one Nat.le_three_of_sqrt_eq_one
+
+lemma sqrt_lt_self (h : 1 < n) : sqrt n < n :=
+  sqrt_lt.2 <| by have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); rwa [Nat.mul_one] at this
+#align nat.sqrt_lt_self Nat.sqrt_lt_self
+
+lemma sqrt_pos : 0 < sqrt n ↔ 0 < n :=
+  le_sqrt
+#align nat.sqrt_pos Nat.sqrt_pos
+
+lemma sqrt_add_eq (n : ℕ) (h : a ≤ n + n) : sqrt (n * n + a) = n :=
+  le_antisymm
+    (le_of_lt_succ <|
+      sqrt_lt.2 <| by
+        rw [succ_mul, mul_succ, add_succ, Nat.add_assoc];
+          exact lt_succ_of_le (Nat.add_le_add_left h _))
+    (le_sqrt.2 <| Nat.le_add_right _ _)
+#align nat.sqrt_add_eq Nat.sqrt_add_eq
+
+lemma sqrt_add_eq' (n : ℕ) (h : a ≤ n + n) : sqrt (n ^ 2 + a) = n := by
+  simpa [Nat.pow_two] using sqrt_add_eq n h
+#align nat.sqrt_add_eq' Nat.sqrt_add_eq'
+
+lemma sqrt_eq (n : ℕ) : sqrt (n * n) = n := sqrt_add_eq n (zero_le _)
+#align nat.sqrt_eq Nat.sqrt_eq
+
+lemma sqrt_eq' (n : ℕ) : sqrt (n ^ 2) = n := sqrt_add_eq' n (zero_le _)
+#align nat.sqrt_eq' Nat.sqrt_eq'
+
+lemma sqrt_succ_le_succ_sqrt (n : ℕ) : sqrt n.succ ≤ n.sqrt.succ :=
+  le_of_lt_succ <| sqrt_lt.2 <| lt_succ_of_le <|
+  succ_le_succ <| le_trans (sqrt_le_add n) <| Nat.add_le_add_right
+    (by refine' add_le_add (Nat.mul_le_mul_right _ _) _ <;> exact Nat.le_add_right _ 2) _
+#align nat.sqrt_succ_le_succ_sqrt Nat.sqrt_succ_le_succ_sqrt
+
+lemma exists_mul_self (x : ℕ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x :=
+  ⟨fun ⟨n, hn⟩ ↦ by rw [← hn, sqrt_eq], fun h ↦ ⟨sqrt x, h⟩⟩
+#align nat.exists_mul_self Nat.exists_mul_self
+
+lemma exists_mul_self' (x : ℕ) : (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x := by
+  simpa only [Nat.pow_two] using exists_mul_self x
+#align nat.exists_mul_self' Nat.exists_mul_self'
+
+lemma sqrt_mul_sqrt_lt_succ (n : ℕ) : sqrt n * sqrt n < n + 1 :=
+  Nat.lt_succ_iff.mpr (sqrt_le _)
+#align nat.sqrt_mul_sqrt_lt_succ Nat.sqrt_mul_sqrt_lt_succ
+
+lemma sqrt_mul_sqrt_lt_succ' (n : ℕ) : sqrt n ^ 2 < n + 1 :=
+  Nat.lt_succ_iff.mpr (sqrt_le' _)
+#align nat.sqrt_mul_sqrt_lt_succ' Nat.sqrt_mul_sqrt_lt_succ'
+
+lemma succ_le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
+  le_of_pred_lt (lt_succ_sqrt _)
+#align nat.succ_le_succ_sqrt Nat.succ_le_succ_sqrt
+
+lemma succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (sqrt n + 1) ^ 2 :=
+  le_of_pred_lt (lt_succ_sqrt' _)
+#align nat.succ_le_succ_sqrt' Nat.succ_le_succ_sqrt'
+
+/-- There are no perfect squares strictly between m² and (m+1)² -/
+lemma not_exists_sq (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ t, t * t = n := by
+  rintro ⟨t, rfl⟩
+  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
+  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
+  exact (not_lt_of_ge <| le_of_lt_succ h2) h1
+#align nat.not_exists_sq Nat.not_exists_sq
+
+lemma not_exists_sq' : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n := by
+  simpa only [Nat.pow_two] using not_exists_sq
+#align nat.not_exists_sq' Nat.not_exists_sq'
+
 /-! ### `find` -/
 
 section Find