proof2.txt

Generalized statement (*): acc + nlen n l = fold_left (+) acc (map (fun _ -> n) l)
---
Base Case: l = []
Statement being proven in base case: acc + nlen n [] = fold_left (+) acc (map (fun _ -> n) [])
Proof of base case:

acc + nlen n []
(nlen) = acc + match [] with [] -> 0 | h::t -> n + nlen n t
(match) = acc + 0
(arith) = acc

fold_left (+) acc (map (fun _ -> n) [])
(fold_left) = match (map (fun _ -> n) []) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(map) = match (match [] with [] -> [] | h::t -> (fun _ -> n) h :: map (fun _ -> n) t) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(match) = match [] with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(match) = acc
---
Inductive Step:
Induction hypothesis (or hypotheses): acc + nlen n xs = fold_left (+) acc (map (fun _ -> n) xs), where length xs >= 0
Statement being proved in inductive step: acc + nlen n (x::xs) = fold_left (+) acc (map (fun _ -> n) (x::xs))
Proof of inductive step:
acc + nlen n (x::xs)
(nlen) = acc + (match (x::xs) with [] -> 0 | h::t -> n + nlen n t)
(match) = acc + n + nlen n xs
(assoc) = (acc + n) + nlen n xs
(I.H.) = fold_left (+) (acc + n) (map (fun _ -> n) xs)
(+) = fold_left (+) ((+) acc n) (map (fun _ -> n) xs)
(match) = match (n :: map (fun _ -> n) xs) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(fun) = match ((fun _ -> n) x :: map (fun _ -> n) xs) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(match) = match (match (x::xs) with [] -> [] | h::t -> (fun _ -> n) h :: map (fun _ -> n) t) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(map) = match (map (fun _ -> n) (x::xs)) with [] -> acc | h::t -> fold_left (+) ((+) acc h) t
(fold_left) = fold_left (+) acc (map (fun _ -> n) (x::xs))
---
Instantiation of generalization:
nlen n l
(arith) = 0 + nlen n l
(*) = fold_left (+) 0 (map (fun _ -> n) l)
---
QED