solution feedback (MoP exercise sets and modular arithmetic)

Stream: new members

[rzeta0]

MoP 9.2 ex 7 is about sets but the detail is about modular arithmetic.

example :
    {n : ℤ | 3 ∣ n} ∪ {n : ℤ | 2 ∣ n} ⊆ {n : ℤ | n ^ 2 ≡ 1 [ZMOD 6]}ᶜ := by
  sorry

Question: My solution is probably the longest lean4 code I've ever written. That suggests I've missed a trick. I'd welcome feedback.

My Approach: I did this pen-n-paper first, and took a different approach to the two parts of the proof.

• The first part can be done algebraically by considering n = 3*k in cases where k is even and odd.. That is, n = 3*(2j) and n=3*(2j+1).The algebra leads to n^2 ≡ 0 or 3 mod 6.
• The second part I couldn't do with the same algebraic approach so had to do by cases on c where n=2*c. This means testing all 6 cases, which feels like I've missed something.

---

spoiler MoP Exercise 9.2 ex 7

example :
    {n : ℤ | 3 ∣ n} ∪ {n : ℤ | 2 ∣ n} ⊆ {n : ℤ | n ^ 2 ≡ 1 [ZMOD 6]}ᶜ := by
  dsimp [Set.subset_def]
  intro x hx
  obtain ha | hb := hx
  · -- 3 | x
    dsimp [· ∣ ·] at *
    obtain ⟨ m, hm ⟩ := ha
    obtain ga | gb := Int.even_or_odd m
    · obtain ⟨ k, hk⟩ := ga
      have hh := calc
        x ^ 2 = (3 * m)^2 := by rw [hm]
        _ = 9 * m^2 := by ring
        _ = 9 * (2 * k)^2 := by rw [hk]
        _ = 0 + 6 * (6 * k^2) := by ring
        _ ≡ 0 [ZMOD 6] := by extra
      by_contra gx
      have gx2 := calc
        0 ≡ x^2 [ZMOD 6] := by rel [hh]
        _ ≡ 1 [ZMOD 6] := by rel [gx]
      numbers at gx2
    · obtain ⟨ k, hk⟩ := gb
      have hh := calc
        x ^ 2 = (3 * m)^2 := by rw [hm]
        _ = 9 * m^2 := by ring
        _ = 9 * (2 * k + 1)^2 := by rw [hk]
        _ = 9 * (4 * k^2 + 4*k + 1) := by ring
        _ = 36 * (k^2 + k) + 9:= by ring
        _ = 3 + 6 * (6*(k^2 +k) + 1) := by ring
        _ ≡ 3 [ZMOD 6] := by extra
      by_contra gx
      have gx2 := calc
        3 ≡ x^2 [ZMOD 6] := by rel [hh]
        _ ≡ 1 [ZMOD 6] := by rel [gx]
      numbers at gx2
  · -- 2 | x
    dsimp [· ∣ ·] at *
    obtain ⟨ c, hc ⟩ := hb
    have hc2:= calc
      x^2 = (2*c)^2 := by rw [hc]
      _ = 4 * c^2 := by ring
    mod_cases hx : c % 6
    · -- c ≡ 0 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (0)^2 [ZMOD 6] := by rel [hx]
        _ = 0 := by norm_num
        _ ≡ 0 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        0 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx
    · -- c ≡ 1 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (1)^2 [ZMOD 6] := by rel [hx]
        _ = 4 := by norm_num
        _ ≡ 4 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        4 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx
    · -- c ≡ 2 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (2)^2 [ZMOD 6] := by rel [hx]
        _ = 4 + 6*2 := by norm_num
        _ ≡ 4 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        4 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx
    · -- c ≡ 3 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (3)^2 [ZMOD 6] := by rel [hx]
        _ = 0 + 6*6 := by norm_num
        _ ≡ 0 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        0 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx
    · -- c ≡ 4 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (4)^2 [ZMOD 6] := by rel [hx]
        _ = 4 + 6*10 := by norm_num
        _ ≡ 4 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        4 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx
    · -- c ≡ 5 mod 6
      have hy:= calc
        x ^ 2 = 4 * c^2 := by rw [hc2]
        _ ≡ 4 * (5)^2 [ZMOD 6] := by rel [hx]
        _ = 4 + 6*16 := by norm_num
        _ ≡ 4 [ZMOD 6] := by extra
      by_contra gx
      have xx:= calc
        4 ≡ x^2 [ZMOD 6] := by rel [hy]
        _ ≡ 1 [ZMOD 6] :=  by rel [gx]
      numbers at xx

[rzeta0]

(I should apologise that this is MoP code and won't run in live-lean.)

[rzeta0]

I did also think about using <;> but couldn't see it.

[Damiano Testa]

Here is an alternative

example :
    {n : ℤ | 3 ∣ n} ∪ {n : ℤ | 2 ∣ n} ⊆ {n : ℤ | n ^ 2 ≡ 1 [ZMOD 6]}ᶜ := by
  simp only [Int.modEq_iff_dvd, Set.union_subset_iff]
  constructor <;>
  · intro n hn  -- can merge this and the next line with `rintro n ⟨n', rfl⟩`
    obtain ⟨n', rfl⟩ := hn
    simp [mul_pow]
    omega

[Kevin Buzzard]

When I'd been writing Lean 3 for a few months I remember producing a monstrously large proof that $\sqrt{3}$ was irrational (perhaps even longer than the code snippet above). I was triumphant when I got it compiling. I then #printed the proof, captured it as an image, ray-traced it, imported it into blender and then one of my kids thickened it up, coloured it in, bent it around and added a little character who could jump on the code so the proof became a platformer with the goal being to jump from one end of the proof to the other (I don't think anyone ever succeeded, the proof was that long). We then took a screenshot of the result, and a year or two later when I was asked by the London Maths Society to write something about Lean I sent them the image and they put it on the front page of their newsletter https://www.lms.ac.uk/sites/lms.ac.uk/files/files/NLMS_484-forweb2.pdf . Maybe there's a moral there somewhere.

[rzeta0]

Love this story - and that is a very cool visualisation* !

( * did I mention that I used to run the London Algorithmic Art meet-up in a previous life ... )