natural-number-game

Solututions to the Natural Number Game

Diffstat

2 files changed, 171 insertions, 0 deletions

diff --git a/advanced-multiplication.lean b/advanced-multiplication.lean
@@ -0,0 +1,74 @@
+theorem mul_pos (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
+begin
+  intros ha hb,
+  cases b with d,
+  exfalso,
+  apply hb,
+  refl,
+  rw mul_succ,
+  rw add_comm,
+  intro h,
+  apply ha,
+  apply add_right_eq_zero,
+  exact h,
+end
+
+theorem eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) 
+                                          (h : a * b = 0) : a = 0 ∨ b = 0 :=
+begin
+  cases b with c,
+  right,
+  refl,
+  rw mul_succ at h,
+  cases a with d,
+  left,
+  refl,
+  exfalso,
+  rw add_succ at h,
+  apply succ_ne_zero,
+  exact h,
+end
+
+theorem mul_eq_zero_iff (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 :=
+begin
+  split,
+  intro h,
+  apply eq_zero_or_eq_zero_of_mul_eq_zero,
+  exact h,
+  intro h,
+  cases h with a_zero b_zero,
+  rw a_zero,
+  rw zero_mul,
+  refl,
+  rw b_zero,
+  rw mul_zero,
+  refl,
+end
+
+theorem mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c :=
+begin
+  revert b,
+  induction c with n,
+  rw mul_zero,
+  intros b h,
+  cases eq_zero_or_eq_zero_of_mul_eq_zero a b h with a_zero b_zero,
+  exfalso,
+  apply ha,
+  exact a_zero,
+  exact b_zero,
+  intro b,
+  intro h,
+  cases b with d,
+  exfalso,
+  rw mul_zero at h,
+  rw mul_succ at h,
+  symmetry at h,
+  apply ha,
+  exact add_left_eq_zero h,
+  rw mul_succ at h,
+  rw mul_succ at h,
+  have p := add_right_cancel _ _ _ h,
+  have q := c_ih d p,
+  rw q,
+  refl,
+end

diff --git a/multiplication.lean b/multiplication.lean
@@ -0,0 +1,97 @@
+lemma zero_mul (m : ℕ) : 0 * m = 0 :=
+begin
+  induction m,
+  rw mul_zero,
+  refl,
+  rw mul_succ,
+  rw add_zero,
+  rw m_ih,
+  refl,
+end
+
+lemma mul_one (m : ℕ) : m * 1 = m :=
+begin
+  rw one_eq_succ_zero,
+  rw mul_succ,
+  rw mul_zero,
+  rw zero_add,
+  refl,
+end
+
+lemma one_mul (m : ℕ) : 1 * m = m :=
+begin
+  induction m,
+  rw mul_zero,
+  refl,
+  rw mul_succ,
+  rw m_ih,
+  rw succ_eq_add_one,
+  refl,
+end
+
+lemma mul_add (t a b : ℕ) : t * (a + b) = t * a + t * b :=
+begin
+  induction b,
+  rw mul_zero,
+  repeat {rw add_zero},
+  rw add_succ,
+  repeat {rw mul_succ},
+  rw ← add_assoc,
+  rw b_ih,
+  refl,
+end
+
+lemma mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) :=
+begin
+  induction c,
+  repeat {rw mul_zero},
+  repeat {rw mul_succ},
+  rw mul_add,
+  rw c_ih,
+  refl,
+end
+
+lemma succ_mul (a b : ℕ) : succ a * b = a * b + b :=
+begin
+  induction b,
+  repeat {rw mul_zero},
+  rw add_zero,
+  refl,
+  repeat {rw mul_succ},
+  rw b_ih,
+  repeat {rw add_succ},
+  rw add_right_comm,
+  refl,
+end
+
+lemma add_mul (a b t : ℕ) : (a + b) * t = a * t + b * t :=
+begin
+  induction b,
+  rw zero_mul,
+  repeat {rw add_zero},
+  rw add_succ,
+  repeat {rw succ_mul},
+  rw b_ih,
+  rw add_assoc,
+  refl,
+end
+
+lemma mul_comm (a b : ℕ) : a * b = b * a :=
+begin
+  induction b,
+  rw mul_zero,
+  rw zero_mul,
+  refl,
+  rw mul_succ,
+  rw succ_mul,
+  rw b_ih,
+  refl,
+end
+
+lemma mul_left_comm (a b c : ℕ) : a * (b * c) = b * (a * c) :=
+begin
+  rw ← mul_assoc,
+  rw mul_comm a b,
+  rw mul_assoc,
+  refl,
+end