Simple nat.sqrt lemmas

Stream: Is there code for X?

[Adrián Doña Mateo]

I couldn't find any of these in the library so I wrote them myself.

lemma sqrt_pred_lt (n : ℕ) (h : n ≠ 0) :
    sqrt (n - 1) * sqrt (n - 1) < n := lt_of_le_of_lt (sqrt_le _) (pred_lt h)

lemma le_succ_sqrt_pred (n : ℕ) (h : n ≠ 0) :
    n ≤ (sqrt (n - 1) + 1) * (sqrt (n - 1) + 1) := le_of_pred_lt (lt_succ_sqrt _)

/-- There are no perfect squares strictly between a² and (a+1)² -/
lemma no_middle_square {n a : ℕ} (hl : a * a < n) (hr : n < (a + 1) * (a + 1)):
    ¬ ∃ t, t * t = n :=
begin
    rintro ⟨t, rfl⟩,
    have : a < t, from nat.mul_self_lt_mul_self_iff.mpr hl,
    have : t < a + 1, from nat.mul_self_lt_mul_self_iff.mpr hr,
    linarith,
end

I was wondering if it would be good to add any them to data.nat.sqrt.
The last one is very useful for proving that a natural number is not a square.

[Kevin Buzzard]

Make a PR!

[Yakov Pechersky]

Some golfing to remove unnecessary n \ne 0 hypotheses. Do you really need to state it on the pred versions?

import data.nat.sqrt
import tactic.linarith

open nat

lemma sqrt_lt (n : ℕ) : sqrt n * sqrt n < n + 1 :=
lt_succ_iff.mpr (sqrt_le _)

lemma le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
le_of_pred_lt (lt_succ_sqrt _)

/-- There are no perfect squares strictly between a² and (a+1)² -/
lemma no_middle_square {n a : ℕ} (hl : a * a < n) (hr : n < (a + 1) * (a + 1)):
    ¬ ∃ t, t * t = n :=
begin
    rintro ⟨t, rfl⟩,
    have : a < t, from nat.mul_self_lt_mul_self_iff.mpr hl,
    have : t < a + 1, from nat.mul_self_lt_mul_self_iff.mpr hr,
    linarith,
end

[Yakov Pechersky]

Further golfing, no linarith dep, and no necessary hyps for the no_middle_square:

import data.nat.sqrt

open nat

lemma sqrt_lt (n : ℕ) : sqrt n * sqrt n < n + 1 :=
lt_succ_iff.mpr (sqrt_le _)

lemma le_succ_sqrt (n : ℕ) : n + 1 ≤ (sqrt n + 1) * (sqrt n + 1) :=
le_of_pred_lt (lt_succ_sqrt _)

lemma not_exists_between_succ (n : ℕ) : ¬ ∃ k, n < k ∧ k < n + 1 :=
not_exists.mpr (λ k, not_and.mpr (λ h H, absurd H (not_lt_of_le (lt_of_succ_le h))))

/-- There are no perfect squares strictly between n² and (n+1)² -/
lemma no_middle_square (n : ℕ) :
  ¬ ∃ t, n * n < t * t ∧ t * t < (n + 1) * (n + 1) :=
begin
  rintro ⟨t, ht, ht'⟩,
  rw ←nat.mul_self_lt_mul_self_iff at ht ht',
  rcases eq_or_lt_of_le (le_of_lt_succ ht') with rfl|H,
  { exact absurd ht (lt_irrefl t) },
  { exact not_exists_between_succ t ⟨n, H, lt_succ_of_lt ht⟩ },
end

[Eric Wieser]

Constructively, it seems like it would be more useful to have that last lemma as a for all / or

[Eric Wieser]

The previous lemma, with hypotheses, looks easier to work with

[Yakov Pechersky]

lemma no_middle_square' {n t : ℕ} (h : n * n < t * t) :
  (n + 1) * (n + 1) ≤ t * t :=
nat.mul_self_le_mul_self (succ_le_of_lt (nat.mul_self_lt_mul_self_iff.mpr h))