mynat_add_comm_monoid.lean

-- I just want us not to get bogged down with non-maths issues.
-- I would be happy to use any tactics
import tactic_mathematician

inductive mynat
| zero : mynat
| succ (n : mynat) : mynat

namespace mynat

instance : has_zero mynat := ⟨mynat.zero⟩

def one := succ 0

instance : has_one mynat := ⟨mynat.one⟩

def two := succ 1

def add : mynat → mynat → mynat
| m 0 := m
| m (succ n) := succ (add m n)

instance : has_add mynat := ⟨mynat.add⟩

-- note what just happened:
example : mynat := 37

lemma add_zero (m : mynat) : m + 0 = m :=
begin
  refl
end

lemma add_succ (m n : mynat) : m + succ n = succ (m + n) :=
begin
  refl
end

example : (1 : mynat) + 1 = 2 :=
begin
  refl
end

lemma zero_add (n : mynat) : 0 + n = n :=
begin
  induction n with d hd,
  {
    refl,
  },
  { rw add_succ,
    rw hd,
  }
end

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=
begin
  induction c with d hd,
  { -- (a + b) + zero = a + (b + zero)
   -- I don't want zero leakage
    show a + b + 0 = a + (b + 0),
    rw add_zero,
    -- or:   show (a + b) = a + (b + 0),
    rw add_zero, -- goal goes 
    -- or    show a + b = a + b, refl,
  },
  { -- (a + b) + succ d = a + (b + succ d)
    rw add_succ,
    rw add_succ,
    rw add_succ,
    rw hd,
  }
end

-- level up
-- #print add_monoid
/-
class add_monoid α extends add_semigroup α :=
(zero_add : ∀ a : α, 0 + a = a) (add_zero : ∀ a : α, a + 0 = a)

-/
-- Lean should automatically generate this proof from my naming conventions.
-- i.e.
-- instance : add_monoid my_nat := by common_sense
instance : add_monoid mynat := by i_checked_all_teh_axioms

-- For pedagogical reasons I would like to make this structure
-- at this point, not when making add_comm_monoid (we are a long
-- way from add_comm)

instance : add_semigroup mynat := by apply_instance

lemma add_one (n : mynat) : n + 1 = succ n :=
begin
  refl
end

lemma one_add (n : mynat) : 1 + n = succ n :=
begin
  induction n with d hd,
  {
    refl
  },
  { rw add_succ,
    rw hd
  }
end

-- failed attempt to prove add_comm because we 
-- are going too fast.

-- isolate independent useful thing and prove it first
lemma succ_add (a b : mynat) : succ a + b = succ (a + b) :=
begin
  induction b with d hd,
  {
    refl
  }, 
  { rw add_succ,
    rw hd,
    refl
  }
end

lemma add_comm (a b : mynat) : a + b = b + a :=
begin
  induction b with d hd,
  { -- leaky zero
    show a + 0 = 0 + a,
    rw zero_add,
    rw add_zero
  },
  {
    rw add_succ,
-- or    show succ (a + d) = _,
    rw hd,
    rw succ_add,
  }
end

-- level up

/-
class add_comm_semigroup X extends add_semigroup X :=
(add_comm : ∀ a b : X, a + b = b + a)
-/
instance : add_comm_semigroup mynat := by i_checked_all_teh_axioms

-- class add_comm_monoid (α : Type u) extends add_monoid α, add_comm_semigroup α
instance : add_comm_monoid mynat := by i_checked_all_teh_axioms

end mynat

adding cool new tactic