Zulip Chat Archive
Stream: new members
Topic: Divisibility Proof
Vir Malhotra (Mar 04 2024 at 16:46):
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 (Mar 04 2024 at 16:48):
Could you tell us why you're using lean 3?
Vir Malhotra (Mar 04 2024 at 16:49):
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 (Mar 04 2024 at 16:59):
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 (Mar 04 2024 at 17:44):
I of course agree with Ruben, but anyway have you a math proof?
Vir Malhotra (Mar 04 2024 at 20:49):
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 (Mar 04 2024 at 20:50):
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 (Mar 04 2024 at 20:53):
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 (Mar 05 2024 at 12:26):
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 (Mar 05 2024 at 15:02):
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 (Mar 05 2024 at 15:05):
Check edit history for clearer versions I guess, I just golf it for fun
Peter Hansen (Mar 05 2024 at 17:55):
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 (Mar 06 2024 at 00:52):
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 (Mar 06 2024 at 07:53):
When I've got my golf trousers on I'm sometimes annoyed about how one has to occasionally revert
before decide
.
Joseph Myers (Mar 06 2024 at 10:21):
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.
Last updated: May 02 2025 at 03:31 UTC