Zulip Chat Archive

Stream: Is there code for X?

Topic: Simple nat.sqrt lemmas


view this post on Zulip Adrián Doña Mateo (Nov 30 2020 at 18:43):

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.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 18:48):

Make a PR!

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 18:55):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 19:21):

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

view this post on Zulip Eric Wieser (Nov 30 2020 at 19:50):

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

view this post on Zulip Eric Wieser (Nov 30 2020 at 19:50):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 20:23):

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))

Last updated: May 17 2021 at 16:26 UTC