The Monoid Laws, Proved in Lean

In an earlier post the monoid laws showed up as an OCaml fold. Here they are again as theorems in Lean 4 — and this time the proofs are interactive.

Each proof below is rendered with Alectryon driven by LeanInk. Hover over a tactic (or the goal markers in the gutter) to see the proof state at that point: the hypotheses in context and the goal that remains.

/-! # The monoid laws for `Nat`, proved in Lean

The proofs below are processed by LeanInk + Alectryon, so each tactic step
shows the intermediate proof state when you hover or step through it. -/

/- Associativity of addition. We go by induction on the last argument. -/
theorem nat_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
Goals accomplished! 🐙
  
a, b, c: Nat
a + b + c = a + (b + c)induction c with
  
a, b, c: Nat
a + b + c = a + (b + c)| zero =>
Goals accomplished! 🐙 
a, b, c: Nat
a + b + c = a + (b + c)rfl
Goals accomplished! 🐙
  
a, b, c: Nat
a + b + c = a + (b + c)| succ c ih =>
a, b, c: Nat
ih: a + b + c = a + (b + c)
succ
a + b + (c + 1) = a + (b + (c + 1)) 
a, b, c: Nat
a + b + c = a + (b + c)simp [Nat.add_succ, ih]
Error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
a, b, c: Nat
ih: a + b + c = a + (b + c)
succ
a + b + (c + 1) = a + (b + (c + 1))

/- `0` is a left identity. (It is a right identity definitionally.) -/
theorem nat_zero_add (a : Nat) : 0 + a = a := by
Goals accomplished! 🐙
  
a: Nat
0 + a = ainduction a with
  
a: Nat
0 + a = a| zero =>
Goals accomplished! 🐙 
a: Nat
0 + a = arfl
Goals accomplished! 🐙
  
a: Nat
0 + a = a| succ a ih =>
a: Nat
ih: 0 + a = a
succ
0 + (a + 1) = a + 1 
a: Nat
0 + a = asimp [Nat.add_succ, ih]
Error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
a: Nat
ih: 0 + a = a
succ
0 + (a + 1) = a + 1

The associativity proof goes by induction on c: the zero case closes by rfl, and the succ case rewrites with the inductive hypothesis. Step through it above to watch the goal shrink.