|
Program Verification Related Reading: Chapter 10 in the Omnibus, Chapter 11 in SOE. Due: Midnight Sunday April 20, 2008
Solution to problem 11.5 "Consider this definition of the factorial function: > fac1 :: Integer -> Integer and this alternative definition: > fac2 :: Integer -> Integer Prove that fac1 n = fac2 n for all non-negative integers n." Solution: Base case (n=0): fac1 0 => 1 => fac' 0 1 => fac2 0 Induction step: fac1 (n+1) Lemma 1: (n+1) * fac' n 1 = fac' n (n+1) To prove Lemma 1 it is easier to first prove a more general lemma: Lemma 2: a * fac' n x = fac' n (a*x) Indeed, Lemma 1 follows immediately from Lemma 2. Proof of Lemma 2: Base case (n=0): a * fac' 0 x => a * x => fac' 0 (a*x) Induction step (n=n+1): a * fac' (n+1) x |