Given: data Nat = Zero | Succ Nat plus Zero m = m plus (Succ n) m = Succ (plus n m) mult Zero m = Zero mult (Succ n) m = plus n (mult n m) Prove: for all x :: Nat, y::Nat . plus x y = plus y x Proof by induction, on x :: Nat: Base case: x = Zero [ goal is now ] plus Zero y = plus y Zero { goal propn with x = Zero } y = plus y Zero { LHS, by first eqn for plus } y = y { Lemma 1: for all n, plus n Zero = n } Recursive case: x = Succ z Therefore, assuming: for all y. plus z y = plus y z plus (Succ z) y = plus y (Succ z) { goal propn with x = Succ z } Succ (plus z y) = plus y (Succ z) { LHS, by snd. eqn for plus } Succ (plus y z) = plus y (Succ z) { LHS, by ind. assm. } Succ (plus y z) = Succ (plus y z) { RHS, Lemma 2: plus y (Succ z) = Succ (plus y z) } QED Lemma 1: Prove for all n :: Nat, plus n Zero = n Proof by induction on n :: Nat. Base case: n = Zero: plus Zero Zero = Zero { goal propn with n = Zero } Zero = Zero { LHS by fst rules plus } QED / trivial, since LHS = RHS / etc. Recursive case: n = Succ q Assume plus q Zero = q. [ local ind. goal ] plus (Succ q) Zero = Succ q Succ (plus q Zero) = Succ q { LHS by snd rule plus } Succ q = Succ q { by ind. assm. } QED Lemma 2 for all y :: Nat, z :: Nat. plus y (Succ z) = Succ (plus y z) Proof by induction on y: Base case: y = Zero plus Zero (Succ z) = Succ (plus Zero z) { sub-goal with y = Zero } Succ z = Succ (plus Zero z) { LHS, by fst rule plus } Succ z = Succ z { RHS, by fst rule plus } QED Recursive case: Assume: plus w (Succ z) = Succ (plus w z) Prove: plus (Succ w) (Succ z) = Succ (plus (Succ w) z) Succ (plus w (Succ z)) = Succ (plus (Succ w) z) { LHS, by snd rule plus } Succ (Succ (plus w z)) = Succ (plus (Succ w) z) { LHS, by ind. assm. } Succ (Succ (plus w z)) = Succ (Succ (plus w z)) { RHS, by snd rule plus } QED