2 is not a square

Stream: Is there code for X?

[Heather Macbeth]

What's the slick way to prove that 2 is not a square?

import data.nat.basic

example (m : ℕ) : m ^ 2 ≠ 2 := sorry

No luck with library_search (at least not with simple imports), omega, norm_num, ...

[Scott Morrison]

This is terrible. :-) I wanted to use interval_cases, but then couldn't find any of the lemmas I needed for that anyway...

import data.nat.basic
import tactic.interval_cases

lemma nat.le_self_mul_pos (n m : ℕ) (h : 0 < m) : n ≤ n * m :=
begin
  cases m, cases h,
  exact le_add_self,
end

lemma nat.le_self_pow (n k : ℕ) (h : 0 < k) : n ≤ n^k :=
begin
  cases n, { simp, },
  cases k with k, { cases h, },
  rw [pow_succ],
  apply nat.le_self_mul_pos,
  finish,
end

lemma nat.le_square (n : ℕ) : n ≤ n^2 := nat.le_self_pow _ _ zero_lt_two

example (m : ℕ) : m ^ 2 ≠ 2 :=
begin
  intro h,
  have : m ≤ 2 := (nat.le_square m).trans h.le,
  interval_cases m; cases h,
 end

[Scott Morrison]

Surely the first three lemmas already exist somewhere???

[Heather Macbeth]

I found

import tactic

example (m : ℕ) : m ^ 2 ≠ 2 :=
begin
  intros h,
  have : m ∈ finset.range 3 := by simp; nlinarith,
  fin_cases this;
  norm_num at h,
end

which seems rather overkill.

[Heather Macbeth]

Ah, that's basically the same as yours, using overkill instead of proving a lemma nat.le_square, and using fin_cases instead of interval_cases.

[Scott Morrison]

Ah, yes, nlinarith+interval_cases is slightly nicer:

example (m : ℕ) : m ^ 2 ≠ 2 :=
begin
  intros h,
  have : m ≤ 2 := by nlinarith,
  interval_cases m; cases h,
end

[Heather Macbeth]

I think that's not embarrassing!

[Scott Morrison]

Yes! It's actually pretty good. The only problem with it is that I still don't have a good mental model of what nlinarith can and can't do, which makes it feel less "reproducible".

[Scott Morrison]

And I hope someone will explain whether the extra lemmas I had to write exist or not. If they don't exist I should add them.

[Eric Rodriguez]

import algebra.squarefree

example (m : ℕ) : m ^ 2 ≠ 2 :=
begin
  intro h,
  have : squarefree (m^2) := h.symm ▸ (nat.prime_iff.mp nat.prime_two).squarefree,
  specialize this m ⟨1, by rw [sq, mul_one]⟩,
  rw nat.is_unit_iff at this,
  norm_num [this] at h,
end

[Heather Macbeth]

In my opinion, this is better as a way of proving that 43 is not a square, but worse as a way of proving that 2 is not a square.

[Junyan Xu]

import data.nat.prime

example (m : ℕ) : m ^ 2 ≠ 2 :=
λ he, by { cases (nat.dvd_prime nat.prime_two).1
  (⟨m, by rw [← he, pow_two]⟩: m ∣ 2) with h; subst h; cases he }

[Ruben Van de Velde]

Maybe

example (r : ℕ) : r ^ 2 ≠ 2 :=
begin
  have : 1 ≤ 2,
  { norm_num },
  apply monotone.ne_of_lt_of_lt_nat (nat.pow_left_strict_mono this).monotone 1; norm_num,
end

[Ruben Van de Velde]

I.e., no square lies between two consecutive squares

[Ruben Van de Velde]

(Credit to whoever proved that 2 is not a cube here on zulip a while ago)

[Junyan Xu]

I thought of this approach but couldn't find nat.pow_left_strict_mono; here's golfed solution:

import tactic
example (m : ℕ) : m ^ 2 ≠ 2 :=
by apply monotone.ne_of_lt_of_lt_nat (nat.pow_left_strict_mono _).monotone 1; norm_num

[Ruben Van de Velde]

Also, it's clearly a trivial consequence of docs#irrational_sqrt_two, but I feel like it would take some work to convince lean of that

[Kevin Buzzard]

Yeah we had all this out on the discord recently for sqrt(3) with Bhavik suggesting irrationality was a quick approach, but it never seemed to be quicker than the integral approaches

[Ruben Van de Velde]

example (m : ℕ) : m ^ 2 ≠ 2 :=
begin
  intro h,
  have qr : ((2 : ℚ) : ℝ) = 2, { norm_num },
  have := irrational_sqrt_two,
  rw [←qr, irrational_sqrt_rat_iff] at this,
  apply this.1,
  have nq : ((2 : ℕ) : ℚ) = 2, { norm_num },
  rw [←nq, ←h, sq m, nat.cast_mul, rat.sqrt_eq, ←abs_mul, abs_mul_self],
end

[Kevin Buzzard]

Yeah exactly

[Yury G. Kudryashov]

example (k : ℕ) : k ^ 2 ≠ 2 :=
begin
  refine mt (λ h, _) irrational_sqrt_two,
  use k,
  rw [rat.cast_coe_nat, ← sq_eq_sq, ← nat.cast_pow, h, nat.cast_two, real.sq_sqrt],
  exacts [zero_le_two, k.cast_nonneg, real.sqrt_nonneg 2]
end

[Kyle Miller]

This seems like a good codegolf.stackexchange.com question

[Kyle Miller]

Here's a "rational root theorem" solution:

import data.nat.basic
import tactic

example (k : ℕ) : k ^ 2 ≠ 2 :=
begin
  intro h,
  have : k ∣ 2,
  { rw [←h, sq],
    exact dvd.intro k rfl, },
  have : k ≤ 2 := nat.le_of_dvd two_pos this,
  interval_cases k; norm_num at h,
end

Is there a good way to turn k ∣ 2 into k = 1 ∨ k = 2 by computing divisors?

[Junyan Xu]

same idea as https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/2.20is.20not.20a.20square/near/275333827 where I used 2 a prime

[Scott Morrison]

@Kyle Miller:

example (k : ℕ) (h : k ∣ 2) : k = 1 ∨ k = 2 :=
begin
  have : k ∈ nat.divisors 2, { simp [h] },
  fin_cases this; simp,
end

[Johan Commelin]

Sounds like we need dvd_cases

[Scott Morrison]

(Warning, the performance scales very badly for larger values of 2!)

[Kyle Miller]

I got 43 to work this way:

import data.nat.basic
import number_theory.divisors
import tactic

lemma nat.mem_divisors_of_dvd {n m : ℕ} (h : m ≠ 0) (hd : n ∣ m) : n ∈ m.divisors :=
by simp [*]

example (k : ℕ) : k ^ 2 ≠ 43 :=
begin
  intro h,
  have : k ∈ nat.divisors 43,
  { apply nat.mem_divisors_of_dvd (by norm_num : 43 ≠ 0),
    rw [←h, sq],
    exact dvd.intro k rfl, },
  have hd : nat.divisors 43 = {1, 43} := dec_trivial,
  simp only [hd, finset.mem_insert, finset.mem_singleton] at this,
  obtain rfl|rfl := this; norm_num at h,
end

[Kyle Miller]

Proving that it's way too general to prove 2 is not a square :smile:

[Johan Commelin]

@Scott Morrison But with a bit of norm_num, a dvd_cases should be able to be performant, right?

[Kyle Miller]

I was thinking about how it could be implemented similarly to the interval_cases PR I haven't finished yet. (My course's final exam was today, so I should have time to get back to that!)

[Mario Carneiro]

What are the rules of the game here? Are lemmas allowed?

import tactic.norm_num

theorem is_not_square (n a : ℕ) (h₁ : n ^ 2 < a) (h₂ : a < (n+1)^2) (k) : k^2 ≠ a :=
begin
  rintro rfl,
  simp [pow_two, ← nat.mul_self_lt_mul_self_iff] at *,
  cases not_le_of_gt h₂ h₁
end

example : ∀ k, k ^ 2 ≠ 2 := is_not_square 1 _ (by norm_num) (by norm_num)
example : ∀ k, k ^ 2 ≠ 43 := is_not_square 6 _ (by norm_num) (by norm_num)

[Junyan Xu]

theorem is_not_square (n a : ℕ) (h₁ : n ^ 2 < a) (h₂ : a < (n+1)^2) (k) : k^2 ≠ a :=
by apply monotone.ne_of_lt_of_lt_nat (nat.pow_left_strict_mono (by norm_num : 1 ≤ 2)).monotone n h₁ h₂

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/2.20is.20not.20a.20square/near/275334964

[Scott Morrison]

I guess we should add support for nat.sqrt to norm_num so one doesn't even need to compute the constants:

example : ∀ k, k ^ 2 ≠ 43 := is_not_square (nat.sqrt 43) _ (by norm_num) (by norm_num)

[Mario Carneiro]

I'm already writing it

[Kevin Buzzard]

Just to say that two weeks ago this came up on the discord but with sqrt(3) and in particular it does happen "in the wild".

[Mario Carneiro]

On #12735:

import data.nat.sqrt_norm_num

theorem is_not_square {n : ℕ} (h : (nat.sqrt n)^2 < n) (k) : k^2 ≠ n :=
by { rintro rfl, simpa [nat.sqrt_eq'] using h }

example : ∀ k, k ^ 2 ≠ 2 := is_not_square (by norm_num)
example : ∀ k, k ^ 2 ≠ 43 := is_not_square (by norm_num)