import MyNat.Definition
import MyNat.Addition -- add_succ
import MyNat.Multiplication -- mul_succ
import AdvancedAdditionWorld.Level9 -- succ_ne_zero
namespace MyNat
open MyNat

Advanced Multiplication World

Level 1: mul_pos

Recall that if b : MyNat is a hypothesis and you do cases b with, your one goal will split into two goals, namely the cases b = 0 and b = succ n. So cases here is like a weaker version of induction (you don't get the inductive hypothesis).

Tricks

1. if your goal is ⊢ X ≠ Y then intro h will give you h : X = Y and a goal of ⊢ false. This is because X ≠ Y means (X = Y) → false. Conversely if your goal is false and you have h : X ≠ Y as a hypothesis then apply h will work backwards and turn the goal into X = Y.

2. if hab : succ (3 * x + 2 * y + 1) = 0 is a hypothesis and your goal is ⊢ false, then exact succ_ne_zero _ hab will solve the goal, because Lean will figure out that _ is supposed to be 3 * x + 2 * y + 1.

Theorem

The product of two non-zero natural numbers is non-zero.

theorem 
mul_pos: ∀ (a b : MyNat), a ≠ 0 → b ≠ 0 → a * b ≠ 0
mul_pos (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a ≠ 
0: MyNat
0 → 
b: MyNat
b ≠ 
0: MyNat
0 → 
a: MyNat
a * 
b: MyNat
b ≠ 
0: MyNat
0 := by
a, b: MyNat
a ≠ 0 → b ≠ 0 → a * b ≠ 0
  intros 
ha: a ≠ 0
ha 
hb: b ≠ 0
hb
a, b: MyNat
ha: a ≠ 0
hb: b ≠ 0
a * b ≠ 0
  intro 
hab: a * b = 0
hab
a, b: MyNat
ha: a ≠ 0
hb: b ≠ 0
hab: a * b = 0
False
  cases 
b: MyNat
b with
a, b: MyNat
ha: a ≠ 0
hb: b ≠ 0
hab: a * b = 0
False
  | 
zero: MyNat
zero =>
a: MyNat
ha: a ≠ 0
hb: zero ≠ 0
hab: a * zero = 0
zero
False
    apply 
hb: zero ≠ 0
hb
a: MyNat
ha: a ≠ 0
hb: zero ≠ 0
hab: a * zero = 0
zero
zero = 0
    rfl
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
b': MyNat
b' =>
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * succ b' = 0
succ
False
    rw [
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * succ b' = 0
succ
False
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * b' + a = 0
succ
False]
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * b' + a = 0
succ
False at 
hab: a * succ b' = 0
hab
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * b' + a = 0
succ
False
    apply 
ha: a ≠ 0
ha
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * b' + a = 0
succ
a = 0
    cases 
a: MyNat
a with
a: MyNat
ha: a ≠ 0
b': MyNat
hb: succ b' ≠ 0
hab: a * b' + a = 0
succ
a = 0
    | 
zero: MyNat
zero =>
b': MyNat
hb: succ b' ≠ 0
ha: zero ≠ 0
hab: zero * b' + zero = 0
succ.zero
zero = 0
      rfl
Goals accomplished! 🐙
    | 
succ: MyNat → MyNat
succ 
a': MyNat
a' =>
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ a' * b' + succ a' = 0
succ.succ
succ a' = 0
      rw [
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ a' * b' + succ a' = 0
succ.succ
succ a' = 0
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ (succ a' * b' + a') = 0
succ.succ
succ a' = 0]
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ (succ a' * b' + a') = 0
succ.succ
succ a' = 0 at 
hab: succ a' * b' + succ a' = 0
hab
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ (succ a' * b' + a') = 0
succ.succ
succ a' = 0
      exfalso
b': MyNat
hb: succ b' ≠ 0
a': MyNat
ha: succ a' ≠ 0
hab: succ (succ a' * b' + a') = 0
succ.succ.h
False
      exact 
succ_ne_zero: ∀ (a : MyNat), succ a ≠ 0
succ_ne_zero 
_: MyNat
_ 
hab: succ (succ a' * b' + a') = 0
hab
Goals accomplished! 🐙

Next up Level 2