Proving n^2 not equal 2

Stream: new members

[Yuhan Du]

I am trying to prove the statement that $n^2 \neq 2$

import algebra.group_power
theorem what_i_need: ¬ (∃ n : ℤ , n ^ 2 = 2 ) := sorry

Could someone possibly help me?

[Kevin Buzzard]

Yesterday there was some chat about proving integer squares were 0 or 1 or 4 mod 8. It just occurs to me that an analogous approach mod 4 would do this (or mod 3)

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/0.3C.3Dd.3C3.20implies.20d.3D0.2C1.2C2

[Patrick Massot]

have you looked at https://github.com/leanprover/mathlib/blob/master/data/nat/prime.lean?

[Mario Carneiro]

Well, this is quite a bit easier than proving that sqrt 2 is irrational

[Mario Carneiro]

You can do it by cases on n.nat_abs

[Mario Carneiro]

too small when it is 0 or 1, too big when it is >= 2

[Chris Hughes]

This is one method.

import data.zmod

example : ¬ ∃ n : ℤ, n ^ 2 = 2 :=
λ ⟨n, hn⟩, have h : ∀ n : zmod 3, n ^ 2 ≠ (2 : ℤ), from dec_trivial,
by have := h n; rw ← hn at this; simpa

[Kevin Buzzard]

The congruence trick is somehow better -- if a positive integer is not a square then it's not a square mod p for infinitely many p, and so you can just work in zmod p for the smallest such p :-)

[Chris Hughes]

It's also not very easy to come up with.

[Mario Carneiro]

Even easier, you can square the square root and see if it matches

[Mario Carneiro]

that should make it an easy dec_trivial proof

[Kevin Buzzard]

Oh that's a good idea -- prove that n is a square iff (sqrt n)^2=n

[Chris Hughes]

Not quite sure why this doesn't work

instance h (m : ℤ) : decidable (∃ n : ℤ, n ^ 2 = m) :=
decidable_of_iff (0 ≤ m ∧ m.nat_abs.sqrt ^ 2 = m.nat_abs)
⟨λ h, ⟨nat.sqrt m.nat_abs, by rw [← int.coe_nat_pow, h.2, int.nat_abs_of_nonneg h.1]⟩,
 λ ⟨s, hs⟩, ⟨hs ▸ (pow_two_nonneg _), by rw [← hs, pow_two, int.nat_abs_mul, nat.sqrt_eq, nat.pow_two]⟩⟩

#eval (¬ ∃ n : ℤ, n ^ 2 = 2 : bool)

lemma two_not_square : ¬ ∃ n : ℤ, n ^ 2 = 2 := dec_trivial

[Mario Carneiro]

nat.sqrt is defined through well founded recursion, which may cause a problem on all but the simplest problems. A similar issue came up with nat.prime

[Mario Carneiro]

I assume the #eval worked

[Chris Hughes]

The eval did work. So the issue is that it's just too slow?

[Mario Carneiro]

I think it won't reduce well founded proofs because it requires evaluating theorems

[Mario Carneiro]

you can probably get #reduce to do it but that's not so helpful

[Mario Carneiro]

We need another norm_num extension for this

[Chris Hughes]

Why can I prove example : nat.gcd 4 5 = 1 := rfl? That uses well founded recursion I take it.

[Mario Carneiro]

I think it is just a complexity problem. The #reduce times out for the sqrt example but not gcd

[Patrick Massot]

This thread is really depressing. Sometimes I feel like we are going somewhere (like when we make progress on topological groups or noetherian modules) but then some super elementary problem is raised and we abruptly come back to reality: trivial things are not trivial at all in Lean.

[Kevin Buzzard]

The proof that there's no integer whose square is 2 is "it doesn't work for small n, and big n are too big". Formalising this is a bore. Automating it is possible, but it hasn't been done yet. That's not depressing, it just means things need to be done. Chris made an attempt. In 1 year's time there might be 10 Chris's at Imperial (here's hoping).

[Ali Sever]

I aspire to be a Chris one day

[Kevin Buzzard]

That would be great Ali :-) come along on Thursday evenings in Oct and help me deal with the inevitable pile of freshers!

[Kenny Lau]

import data.nat.basic algebra.group_power

instance nat.decidable_bex_lt (n : nat) (P : Π k < n, Prop) :
  ∀ [H : ∀ n h, decidable (P n h)], decidable (∃ k h, P k h) :=
begin
  induction n with n IH; intro; resetI,
  { exact is_false (λ ⟨_, h, _⟩, nat.not_lt_zero _ h) },
  cases IH (λ k h, P k (nat.lt_succ_of_lt h)) with h,
  { by_cases p : P n (nat.lt_succ_self n),
    { exact is_true ⟨n, nat.lt_succ_self n, p⟩ },
    { apply is_false,
      intro hk,
      rcases hk with ⟨k, hk1, hk2⟩,
      cases nat.lt_succ_iff_lt_or_eq.1 hk1 with hk hk,
      { exact h ⟨k, hk, hk2⟩ },
      { subst hk, exact p hk2 } } },
  apply is_true,
  rcases h with ⟨k, hk1, hk2⟩,
  exact ⟨k, nat.lt_succ_of_lt hk1, hk2⟩
end

instance nat.decidable_bex_le (n : nat) (P : Π k ≤ n, Prop)
  [Π n h, decidable (P n h)] : decidable (∃ k h, P k h) :=
decidable_of_iff (∃ k < n + 1, P k (nat.le_of_lt_succ H))
⟨λ ⟨k, h1, h2⟩, ⟨k, nat.le_of_lt_succ h1, h2⟩,
λ ⟨k, h1, h2⟩, ⟨k, nat.lt_succ_of_le h1, h2⟩⟩

instance decidable_mul_self_nat (n : ℕ) : decidable (∃ k, k * k = n) :=
decidable_of_iff (∃ k ≤ n, k * k = n)
⟨λ ⟨k, h1, h2⟩, ⟨k, h2⟩, λ ⟨k, h1⟩, ⟨k, h1 ▸ nat.le_mul_self k, h1⟩⟩

instance decidable_sqr_nat (n : ℕ) : decidable (∃ k, k^2 = n) :=
decidable_of_iff (∃ k, k * k = n)
⟨λ ⟨k, h⟩, ⟨k, by rwa [nat.pow_two]⟩, λ ⟨k, h⟩, ⟨k, by rwa [nat.pow_two] at h⟩⟩

instance decidable_mul_self_int : Π (n : ℤ), decidable (∃ k, k * k = n)
| (int.of_nat n) := decidable_of_iff (∃ k, k * k = n)
    ⟨λ ⟨k, hk⟩, ⟨k, by rw [← int.coe_nat_mul, hk]; refl⟩,
    λ ⟨k, hk⟩, ⟨int.nat_abs k, by rw [← int.nat_abs_mul, hk]; refl⟩⟩
| -[1+ n] := is_false $ λ ⟨k, h1⟩, not_lt_of_ge (mul_self_nonneg k) $
    h1.symm ▸ int.neg_succ_of_nat_lt_zero n

instance decidable_sqr_int (n : ℤ) : decidable (∃ k, k^2 = n) :=
decidable_of_iff (∃ k, k * k = n)
⟨λ ⟨k, h⟩, ⟨k, by rwa [pow_two]⟩, λ ⟨k, h⟩, ⟨k, by rwa [pow_two] at h⟩⟩

theorem what_i_need: ¬ (∃ n : ℤ , n ^ 2 = 2 ) := dec_trivial

[Kenny Lau]

btw the first part of my code is from this discussion four months ago

[Kenny Lau]

(and mathlib still doesn't know it's true :P)

[Kenny Lau]

This thread is really depressing. Sometimes I feel like we are going somewhere (like when we make progress on topological groups or noetherian modules) but then some super elementary problem is raised and we abruptly come back to reality: trivial things are not trivial at all in Lean.

@Patrick Massot Well this is just a puzzle that cannot be generalized to more useful maths...

[Mario Carneiro]

Yes, of course this is the other option - to check n is a square, just look at all the squares and see if n is in the list. It is much slower than squaring the square root, but it works better in small cases in the kernel since there are no wf definitions involved

[Patrick Massot]

Kenny, why don't you PR the general stuff above? That could be useful in lots of small annoying situations

[Bryan Gin-ge Chen]

Following Patrick Massot's suggestion to look at data.nat.prime, I started trying to prove it using nat.not_prime_mulbut I got stuck.

import algebra.group_power data.nat.prime

theorem what_i_need: ¬ (∃ n : ℤ , n ^ 2 = 2 ) :=
have p2: nat.prime 2, from nat.prime_two,
begin
unfold pow, unfold monoid.pow,
intro h,
exact exists.elim h (assume n,
begin
clear h,
rw [mul_one],
assume h1,
_
--have pnn : nat.prime (n*n), by sorry,
--exact false.elim ((nat.not_prime_mul (sorry) (sorry)) h1)
end
)
end

I think the main thing I'm missing how to do is showing that proving it for $1<n \in \mathbb{N}$ suffices to show it for all $n\in\mathbb{Z}$.

[Mario Carneiro]

In this direction, I suggest proving ¬ nat.prime (n*n). It has no assumptions, but you have to special case 0 and 1

[Patrick Massot]

yes, this is what I had in mind

[Patrick Massot]

I hoped that proving that from prime.lean wouldn't be too hard

[Mario Carneiro]

I thought it was a theorem already but I could be mistaken

[Mario Carneiro]

there is not_prime_mul which takes care of the large n case

[Patrick Massot]

Even without trying to go to the heart of the matter, natural number hell strikes:

import algebra.group_power data.nat.prime

lemma aux (n : ℕ) : ¬ nat.prime (n*n) :=
sorry

theorem what_i_need: ¬ (∃ n : ℕ , n ^ 2 = 2 ) :=
begin
  rintro ⟨n, h⟩,
  apply aux n,
  rw ←pow_two,
  rw h,
  exact nat.prime_two,
end

The rw h doesn't work. simp [h] does work, but these kind of things is really the worse of Lean

[Patrick Massot]

And I'm not even talking about trying to deduce the result with integers instead of natural numbers

[Mario Carneiro]

you have to use rw ← nat.pow_two

[Patrick Massot]

I'm sure there is a solution, but having to know all that is really painful

[Mario Carneiro]

most of this "ambient knowledge" is encoded in the simp lemmas, which is why simp [h] worked. If you look at the rewrites used you will see normalization of the group_power instance on nat to nat.pow

[Mario Carneiro]

the problem is that nat has two power notations, one elementary from nat.pow and another from the group power instance

[Mario Carneiro]

nat.pow is the canonical one, at least until it is removed (it's in core)

[Patrick Massot]

@Bryan Gin-ge Chen

import algebra.group_power data.nat.prime

open nat

lemma aux (n : ℕ) : ¬ nat.prime (n*n) :=
begin
  intro h,
  cases n,
  { simpa [not_prime_zero] using h },
  { cases n,
    { simpa [not_prime_one] using h },
    { have : succ (succ n) > 1 := dec_trivial,
      exact not_prime_mul this this h } }
end

theorem what_i_need: ¬ (∃ n : ℕ , n ^ 2 = 2 ) :=
begin
  rintro ⟨n, h⟩,
  apply aux n,
  rw [←nat.pow_two, h],
  exact nat.prime_two,
end

[Patrick Massot]

This is still cheating because there is nothing about negative integers

[Bryan Gin-ge Chen]

A few days late and not very pretty, but I managed to complete your proof @Patrick Massot

import algebra.group_power data.nat.prime

open nat

lemma aux (n : ℕ) : ¬ prime (n*n) :=
begin
  intro h,
  cases n,
  { simpa [not_prime_zero] using h },
  { cases n,
    { simpa [not_prime_one] using h },
    { have : succ (succ n) > 1 := dec_trivial,
      exact not_prime_mul this this h } }
end

theorem what_i_need_N: ¬ (∃ n : ℕ , n ^ 2 = 2 ) :=
begin
  rintro ⟨n, h⟩,
  apply aux n,
  rw [←nat.pow_two, h],
  exact prime_two,
end

open int

lemma sq_eq_nat_abs_sq {n : ℤ} {m : ℕ} : n^2 = (nat_abs n^2) :=
by rw [_root_.pow_two, _root_.pow_two,
← int.coe_nat_mul, nat_abs_mul_self]

lemma nat_sq_of_int_sq {n : ℤ} {m : ℕ} : n^2 = m → (∃ nn : ℕ, nn ^ 2 = m) :=
begin
  intro h,
  existsi (nat_abs n),
    apply int.coe_nat_inj,
    rw [nat.pow_two, int.coe_nat_mul, ← _root_.pow_two,
    ← sq_eq_nat_abs_sq],
  exact h,
  exact m
end

theorem what_i_need : ¬ (∃ n : ℤ, n^2 = 2) :=
begin
  rintro ⟨n,h⟩,
  exact false.elim (what_i_need_N (nat_sq_of_int_sq h))
end

I think I learned a few things along the way, though it still feels like I've got a long way to go before I can do anything useful...

[Kevin Buzzard]

of course anyone reading this thread and seeing several very long proofs that 2 isn't a square might argue that we all have a long way to go before we can do anything useful...