Feedback on proof of `Irrational √2`

Stream: new members

[J. Simon Richard]

I've been learning LEAN for the past few months, and I finally had the time to write a proof of the irrationality of the square root of two.

Questions: Could you give me feedback on this proof?

• It seems pretty verbose... is there a better way to do this?
• Is there a better way to structure the proof so that I don't have to do quite so many type castings?

The Proof:

lemma sq_even_even {m : ℕ} (h : Even (m^2)) : Even m := by
  apply (Nat.even_pow' _).mp
  exact h
  norm_num


lemma l1 {m n : ℕ} (h : m^2 = 2*n^2) : 2 ∣ m.gcd n :=  by
  have h1: Even (m^2) := by
    rw [h]
    exact even_two_mul (n^2)
  have h2: Even m := sq_even_even h1
  have h2' := h2
  rcases h2' with ⟨k, hk⟩

  have h3: m^2 = 4*k^2 := by
    rw [hk]
    ring
  have h4: n^2 = 2*k^2 := by
    rw [h3] at h
    symm at h
    rw [show 4 = 2 * 2 by norm_num] at h
    rw [mul_assoc] at h
    apply Nat.mul_left_cancel at h
    exact h
    norm_num

  have h5: Even (n^2) := by
    rw [h4]
    exact even_two_mul (k^2)
  have h6: Even n := sq_even_even h5

  apply Nat.dvd_gcd (even_iff_two_dvd.mp h2) (even_iff_two_dvd.mp h6)


theorem irr_root2 : Irrational √2 := by
  by_contra hn
  unfold Irrational at hn
  have h := not_not.mp hn
  rcases h with ⟨r, hr⟩

  have h1 : (2 : ℝ) = r^2 := calc
    2 = (√2)^2 := by
      symm
      apply Real.sq_sqrt
      norm_num
    _ = r^2 := by
      rw [hr]

  have h2 : (2 : ℚ) = ↑(r.num^2) / ↑(r.den^2) := calc
    2 = r^2 := by
      exact_mod_cast h1
    _ = ↑(r.num^2) / ↑(r.den^2) := by
      rw [Rat.pow_def]
      exact (Rat.num_div_den _).symm

  have h3 : (2 : ℚ) * r.den^2 = r.num^2 := by
    rw [h2]
    simp

  have h4 : 2 * r.den^2 = r.num^2 := by
    exact_mod_cast h3

  have h5 : 2 * r.den^2 = r.num.natAbs^2 := by
    rw [←Int.natAbs_sq r.num] at h4
    exact_mod_cast h4

  have h6 := l1 h5.symm
  absurd h6
  rw [r.reduced]
  norm_num

[J. Simon Richard]

Also, I have have h2' = h2 because I wanted to destructure the hypothesis AND use the entire hypothesis later. Is there a better way to do this? Is there some kind of copy h2 function that I could use so that the meaning is more clear semantically?

[Ruben Van de Velde]

I think you can do

  rcases id  h2 with ⟨k, hk⟩

to not lose h2

[Vlad Tsyrklevich]

I haven't looked too closely at optimizing the logic, there are some cases where you can use more high-powered tactics to move more quickly, e.g. simp, and sometimes it's a question of whether it's 'better' or just 'more densely compressed', e.g.

lemma sq_even_even {m : ℕ} (h : Even (m^2)) : Even m :=
  (@Nat.even_pow' m 2 (by omega)).mp h

  -- delete h4
  have h5: Even (n^2) := by
    simp [show n^2 = 2*k^2 by omega]

This one I found by using hint

  have h1 : (2 : ℝ) = r^2 := by simp_all

[Zhang Qinchuan]

You can look how Mathlib prove this: docs#irrational_sqrt_two

[Matt Diamond]

I have a proof of the irrationality of the square root of two which uses the same strategy. I've been revising it over time and it's pretty concise at this point. I'll share in a spoiler tag in case you'd prefer to find your own way:

import Mathlib

lemma even_of_even_pow {n k : ℕ} (hn : Even (n ^ k)) : Even n :=
(Nat.even_pow.mp hn).left

example : Irrational (Real.sqrt 2) :=
by
  intro ⟨n, hn⟩
  have h : (n : ℝ) ^ 2 = 2 := by simp [hn]
  rw [Rat.cast_def, div_pow, div_eq_iff (by simp)] at h

  -- move to ℕ
  rw [← Int.cast_pow, ← Int.natAbs_sq] at h
  norm_cast at h

  have even_num : Even n.num.natAbs := even_of_even_pow (h ▸ even_two_mul _)

  have even_den : Even n.den
  · rw [even_iff_exists_two_mul] at even_num
    rcases even_num with ⟨k, hk⟩
    rw [hk, mul_pow, pow_two, mul_assoc] at h
    rw [Nat.mul_left_cancel_iff Nat.two_pos] at h
    exact even_of_even_pow (h ▸ even_two_mul _)

  rw [even_iff_two_dvd] at even_num even_den
  have not_reduced := Nat.not_coprime_of_dvd_of_dvd Nat.one_lt_two even_num even_den
  exact not_reduced n.reduced

[Matt Diamond]

I'll add that I managed to avoid type-casting hell by using a couple of rewrites and norm_cast to move everything over to ℕ at a suitable point in the middle of the proof

[Matt Diamond]

one way to avoid needing to copy h2: move the rcases statement and all of the logic involving k and hk within the proof of Even (n^2)

the idea is to arrange the proof so that the destructuring of h2 occurs within a subproof and does not affect h2 at the top level... I did something similar in my proof when I needed to rewrite Even n.num.natAbs to ∃ b, n.num.natAbs = 2 * b without losing the proof that the numerator was even

[Matt Diamond]

another tip: you can replace this:

by_contra hn
unfold Irrational at hn
have h := not_not.mp hn
rcases h with ⟨r, hr⟩

with

intro ⟨r, hr⟩

since Irrational is already a Not statement, so it can be introed (and destructured at the same time)

[Matt Diamond]

if you have any questions about the above (or about the proof that I shared) feel free to ask!

[J. Simon Richard]

Thanks everyone for your help! I decided to keep some of the more explicit stuff in so it works as a teaching tool (I'm sharing this with my math club tomorrow), but it's a lot cleaner than before. Here's what I ended up with:

import Mathlib

lemma sq_even_even {m : ℕ} (h : Even (m^2)) : Even m :=
  (Nat.even_pow.mp h).left


lemma l1 {m n : ℕ} (h : m^2 = 2*n^2) : 2 ∣ m.gcd n :=  by
  have h1: Even (m^2) := by
    rw [h]
    exact even_two_mul (n^2)
  have h2: Even m := sq_even_even h1
  rcases id h2 with ⟨k, hk⟩

  have h3: n^2 = 2*k^2 := by
    rw [hk] at h
    ring_nf at h
    omega

  have h4: Even (n^2) := by
    simp [h3]
  have h5: Even n := sq_even_even h4

  apply Nat.dvd_gcd
  exact even_iff_two_dvd.mp h2
  exact even_iff_two_dvd.mp h5


example : Irrational √2 := by
  intro ⟨r, hr⟩

  have h : (2 : ℝ) = r^2 := by simp [hr]

  rw [Rat.cast_def, div_pow] at h

  have h : (2 : ℝ) * r.den^2 = r.num^2 := by
    rw [h]
    simp

  rw [← Int.cast_pow, ←Int.natAbs_sq r.num] at h
  norm_cast at h

  absurd l1 h.symm
  rw [r.reduced]
  simp

[Kevin Buzzard]

After apply Nat.dvd_gcd you have two goals not one, so the next line should start with a \.:

  apply Nat.dvd_gcd
  · exact even_iff_two_dvd.mp h2
  · exact even_iff_two_dvd.mp h5

You should not be writing tactics if there is more than one goal in your local context (this is a style point).

[Kevin Buzzard]

Why do you prove Even (m^2) with rw [h]; exact even_two_mul (n^2) but you prove Even (n^2) with simp [h3]`?

[J. Simon Richard]

Kevin Buzzard said:

After apply Nat.dvd_gcd you have two goals not one, so the next line should start with a \.:

  apply Nat.dvd_gcd
  · exact even_iff_two_dvd.mp h2
  · exact even_iff_two_dvd.mp h5

You should not be writing tactics if there is more than one goal in your local context (this is a style point).

You're right, that would make it more clear.

Kevin Buzzard said:

Why do you prove Even (m^2) with rw [h]; exact even_two_mul (n^2) but you prove Even (n^2) with simp [h3]`?

I think at one point I might have kept the rw,exact to show case how those tactics works.... but there are better places to do that. I'll switch that as well.

[J. Simon Richard]

Simplified version of l1:

lemma l1 {m n : ℕ} (h : m^2 = 2*n^2) : 2 ∣ m.gcd n :=  by
  have h1: Even m := by
    simp [h, sq_even_even]

  rcases id h1 with ⟨k, hk⟩

  have h2: n^2 = 2*k^2 := by
    rw [hk] at h
    ring_nf at h
    omega

  have h3: Even n := by
    simp [h2, sq_even_even]

  apply Nat.dvd_gcd
  . exact even_iff_two_dvd.mp h1
  . exact even_iff_two_dvd.mp h3

[Vlad Tsyrklevich]

small changes: use linarith to squash 2 lines into one, replace simp->rw when the simp is unnecessary, turn an rw+simp into simp

import Mathlib

lemma sq_even_even {m : ℕ} (h : Even (m^2)) : Even m :=
  (Nat.even_pow.mp h).left

lemma l1 {m n : ℕ} (h : m^2 = 2*n^2) : 2 ∣ m.gcd n :=  by
  have h1: Even m := by
    simp [h, sq_even_even]

  rcases id h1 with ⟨k, hk⟩

  have h2: n^2 = 2*k^2 := by
    rw [hk] at h
    linarith

  have h3: Even n := by
    simp [h2, sq_even_even]

  apply Nat.dvd_gcd
  . exact even_iff_two_dvd.mp h1
  . exact even_iff_two_dvd.mp h3

example : Irrational √2 := by
  intro ⟨r, hr⟩

  have h : (2 : ℝ) = r^2 := by simp [hr]

  rw [Rat.cast_def, div_pow] at h

  have h : (2 : ℝ) * r.den^2 = r.num^2 := by
    simp [h]

  rw [← Int.cast_pow, ←Int.natAbs_sq r.num] at h
  norm_cast at h

  absurd l1 h.symm
  simp [r.reduced]