Divisibility Proof

Stream: new members

[Vir Malhotra]

Hello everyone! I am an undergraduate new to Lean usage. Could someone please help me to solve this theorem in Lean3?
Prove that if a is an integer that is not divisible by 3, then (a + 1)(a + 2) is divisible by 3.

I am currently using the web Lean3 version as that is the one required by my professor for a certain project. Any help would be greatly appreciated.

[Ruben Van de Velde]

Could you tell us why you're using lean 3?

[Vir Malhotra]

That's the version my professor is asking me to use. I assume it's because it's more intuitive to learn.

[Ruben Van de Velde]

Unfortunately you'll find it exceedingly hard to find help with lean 3 here, and we'd strongly recommend your professor moves to lean 4

[Riccardo Brasca]

I of course agree with Ruben, but anyway have you a math proof?

[Vir Malhotra]

I will talk to my professor about it, but if anyone is able to help me with the proof I'd be really grateful.

[Vir Malhotra]

This is the math proof for the same in a nutshell:

a can be written as 3b+1 or 3b+2 for some integer b

If a=3b+1, then a+2 is divisible by 3.

If a=3b+2, then a+1 is divisible by 3.

Since either a+1 or a+2 is divisible by 3, (a+1)(a+2) is divisible by 3.

[Kevin Buzzard]

docs#Int.div_add_mod gives you a=3b+r -- maybe you can take it from there? Oh wait -- you want Lean 3?? It will still be called something like that I guess.

[Peter Hansen]

I can't help with Lean 3, but here is (I believe) a proof in Lean 4:

import Mathlib.Tactic

-- The theorem states: if an integer a is not divisible by 3, then (a + 1) * (a + 2) is divisible by 3.
theorem div_by_three (a : ℤ) (h : ¬(3 ∣ a)) : 3 ∣ (a + 1) * (a + 2) := by
  -- First, calculate the remainder of a when divided by 3.
  let r := a % 3

  -- Establish the two possible cases for the remainder: it can only be 1 or 2 since a is not divisible by 3.
  have h_cases : r = 1 ∨ r = 2 := by
    rw [Int.dvd_iff_emod_eq_zero, ← @ne_eq] at h
    have rlt : r < 3 := Int.emod_lt_of_pos a zero_lt_three
    have rge : 0 < r := lt_of_le_of_ne (Int.emod_nonneg a three_ne_zero) h.symm
    interval_cases r
    left; rfl
    right; rfl

  -- Use case analysis on the remainder.
  rcases h_cases with hr | hr

  -- Case 1: Remainder is 1. Show a can be written as 3b + 1, and hence (a + 2) is divisible by 3.
  obtain ⟨Z1, Z2⟩ : ∃ b, 3 * b + 1 = a := by
    rw [← hr]
    use (a/3)
    exact Int.ediv_add_emod a 3

  -- Use the expression for a to prove that (a + 2) is divisible by 3.
  have W2 : 3 ∣ a + 2 := by
    rw [← Z2]
    use Z1 + 1
    ring

  -- Conclude that (a + 1) * (a + 2) is divisible by 3, completing the proof for the first case.
  exact Dvd.dvd.mul_left W2 (a + 1)

  -- Case 2: Remainder is 2. Similar to Case 1, but now showing that (a + 1) is divisible by 3.
  obtain ⟨Z1, Z2⟩ : ∃ b, 3 * b + 2 = a := by
    rw [← hr]
    use (a/3)
    exact Int.ediv_add_emod a 3

  -- Use the expression for a to prove that (a + 1) is divisible by 3.
  have W3 : 3 ∣ a + 1 := by
    rw [← Z2]
    use Z1 + 1
    ring

  -- Conclude that (a + 1) * (a + 2) is divisible by 3, completing the proof for the second case.
  exact Dvd.dvd.mul_right W3 (a + 2)

[Gareth Ma]

example (a : ℕ) (ha : ¬3 ∣ a) : 3 ∣ (a + 1) * (a + 2) := by
  have ha' := (div_add_mod a 3).symm
  have hr : a % 3 < 3 := mod_lt _ zero_lt_three
  interval_cases (a % 3)
  /- first goal -/
  rw [ha'] at ha ⊢
  simp at ha
  /- remaining goals -/
  all_goals
    rw [ha']
    ring_nf
    repeat apply dvd_add
    norm_num
    repeat exact dvd_mul_of_dvd_right (by norm_num) _

[Gareth Ma]

Check edit history for clearer versions I guess, I just golf it for fun

[Peter Hansen]

Though the theorem holds for all integers; not just the natural numbers. Anywho - I golfed along and came up with the following:

import Mathlib.Tactic
open Int

theorem div_by_three (a : ℤ) (h : ¬(3 ∣ a)) : 3 ∣ (a + 1) * (a + 2) := by
    rw [dvd_iff_emod_eq_zero, ← ne_eq] at h
    have : a % 3 < 3 := emod_lt_of_pos a zero_lt_three
    have : 0 < a % 3 := lt_of_le_of_ne (emod_nonneg a three_ne_zero) h.symm
    rw [dvd_iff_emod_eq_zero, mul_emod, add_emod a, add_emod a]
    interval_cases (a % 3)
    · rfl
    · rfl

Though now it hardly follows the mathematical proof that was originally presented. On the flip side, it was easy to turn into Lean 3 code:

import data.int.order.basic
import tactic.interval_cases

open int

theorem div_by_three (a : ℤ) (h : ¬(3 ∣ a)) : 3 ∣ (a + 1) * (a + 2) := begin
    rw [dvd_iff_mod_eq_zero] at h,
    have H : a % 3 ≠ 0 := by exact h,
    have : a % 3 < 3 := mod_lt_of_pos a zero_lt_three,
    have : 0 < a % 3 := lt_of_le_of_ne (mod_nonneg a three_ne_zero) H.symm,
    rw [dvd_iff_mod_eq_zero, mul_mod, add_mod a, add_mod a],
    interval_cases (a % 3),
    finish,
    finish,
  end

[Joseph Myers]

You can also golf this using ZMod:

import Mathlib.Data.ZMod.Basic

theorem div_by_three (a : ℤ) (h : ¬(3 ∣ a)) : 3 ∣ (a + 1) * (a + 2) := by
  revert h
  simp_rw [← (by norm_num : ((3 : ℕ) : ℤ) = 3), ← ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.cast_mul,
           Int.cast_add]
  generalize (a : ZMod 3) = b
  revert b
  decide

[Kevin Buzzard]

When I've got my golf trousers on I'm sometimes annoyed about how one has to occasionally revert before decide.

[Joseph Myers]

Avoiding revert before decide is why Lean 3 had the dec_trivial! tactic variant. I think we've lost that in Lean 4, though since we also lack a Lean 4 equivalent of https://leanprover-community.github.io/mathlib_docs/tactics.html I find it hard to be sure exactly what tactics exist at present.