add_assoc.lean

open nat

theorem my_add_assoc
    -- what we are trying to prove
    : ∀ a b c : nat,
      (a + b) + c = a + (b + c)

-- base case
| 0 b c := by rewrite [
    -- goal is (0 + b) + c = 0 + (b + c)
    zero_add,
    -- goal is      b  + c = 0 + (b + c)
    zero_add
    -- goal is       b + c = b + c
    -- Since this is of the form t = t, rw closes out the goal.
  ]

-- induction step
| (succ a') b c := by rewrite [
    -- goal is (succ a' + b) + c = succ a' + (b + c)
    succ_add,  -- replace (succ ?1 + ?2) with (succ (?1 + ?2))
    -- goal is succ (a' + b) + c = succ a' + (b + c)
    succ_add,  -- same thing again; note that it matches *again* on the LHS!
    -- goal is succ ((a' + b) + c) = succ a' + (b + c)
    succ_add,  -- same thing again, to hit the match on the RHS
    -- goal is succ ((a' + b) + c) = succ (a' + (b + c))
    my_add_assoc a' b c
    -- goal is succ (a' + (b + c)) = succ (a' + (b + c))
    -- Since both sides are the same, rw closes out the goal.
  ]