proof1.txt

to prove mul c (sum l 0) 0 = c * summa l, one can prove the generalized statement mul c (sum l acc1) acc2 = acc2 + c * (summa l + acc1)
Lemma 1: sum l acc1 = acc1 + summa l
Base Case: l = []
Statement being proven in base case: sum [] acc1 = acc1 + summa []
Proof of base case:
sum [] acc1
(sum) = match [] with [] -> acc1 | h::t -> sum t (h+acc1)
(match) = acc1
(arith) = acc1 + 0
(match) = acc1 + (match [] with [] -> 0 | h::t -> h + summa t)
(summa) = acc1 + summa []
---
Inductive Step:
Induction hypothesis (or hypotheses): sum xs acc1 = acc1 + summa xs, where length xs >= 0.
Statement being proved in inductive step: sum x::xs acc1 = acc1 + summa x::xs
Proof of inductive step:
sum x::xs acc1
(sum) = match x::xs with [] -> acc1 | h::t -> sum t (h+acc1)
(match) = sum xs (x+acc1)
(I.H.) = (x+acc1) + summa xs
(arith) = acc1 + x + summa xs
(match) = acc1 + match x::xs with [] -> 0 | h::t -> h + summa t
(summa) = acc1+ summa x::xs
---
Now prove mul c (sum l acc1) acc2 = acc2 + c * (summa l + acc1) inducted on c.
Base Case: c = 0
Statement being proven in base case: mul 0 (sum l acc1) acc2 = acc2 + 0 * (summa l + acc1)
Proof of base case:
mul 0 (sum l acc1) acc2
(mul) = if 0 <= 0 then acc2 else mul (0-1) (sum l acc1) ((sum l acc1)+acc2)
(if) = acc2
(arith) = acc2 + 0 * (summa l + acc1)
---
Inductive Step:
Induction hypothesis (or hypotheses): mul c (sum l acc1) acc2 = acc2 + c * (summa l + acc1), where c >= 0.
Statement being proved in inductive step: mul (c+1) (sum l acc1) acc2 = acc2 + (c+1) * (summa l + acc1)
Proof of inductive step:
mul (c+1) (sum l acc1) acc2
(mul) = if (c+1) <= 0 then acc2 else mul ((c+1)-1) (sum l acc1) ((sum l acc1)+acc2)
(if) = mul ((c+1)-1) (sum l acc1) ((sum l acc1)+acc2)
(arith) = mul c (sum l acc1) ((sum l acc1)+acc2)
(I.H.) = ((sum l acc1)+acc2) + c * (summa l + acc1)
(L1) = ((acc1 + summa l)+acc2) + c * (summa l + acc1)
(arith) = acc2 + (c + 1) * (summa l + acc1)
---
refer generalized statement mul c (sum l acc1) acc2 = acc2 + c * (summa l + acc1) as *:
mul c (sum l 0) 0
(*) = 0 + c * (summa l + 0)
(arith) = c * summa l
---
QED