These notes re-present the proofs from lecture. ## Proof 1  let rec length = function | [] -> 0 | _::xs -> 1 + length xs let rec append xs1 xs2 = match xs1 with | [] -> xs2 | h::t -> h :: append t xs2 Theorem. for all lists xs and ys, length (append xs ys) ~ length xs + length ys. Proof: by induction on xs Case: xs = [] Show: for all ys, length (append [] ys) ~ length [] + length ys length (append [] ys) ~ length ys (eval) ~ 0 + length ys (math) ~ length [] + length ys (eval,symm.) Case: xs = h::t Show: for all ys, length (append (h::t) ys) ~ length (h::t) + length ys IH: for all ys, length (append t ys) ~ length t + length ys length (append (h::t) ys) ~ length (h :: append t ys) (eval) ~ 1 + length (append t ys) (eval) ~ 1 + length t + length ys (IH,congr.) ~ length (h::t) + length ys (eval,symm.,congr.) QED  We'll start omitting facts about ~ in proofs now, unless they are especially non-obvious. So symmetry, congruence, and transitivity aren't going to show up too much more. ## Proof 2  let (@@) f g x = f (g x) let map = List.map Theorem: for all functions f and g, (map f) @@ (map g) ~ map (f @@ g). Proof: By extensionality, we need to show that for all xs, ((map f) @@ (map g)) xs ~ map (f @@ g) xs. By eval, ((map f) @@ (map g)) xs ~ map f (map g xs). So by transitivity, it suffices to show that map f (map g xs) ~ map (f @@ g) xs. We do so by induction on xs. Case: xs = [] Show: map f (map g []) ~ map (f @@ g) [] map f (map g []) ~ [] (eval) ~ map (f @@ g) [] (eval) Case: xs = h::t Show: map f (map g (h::t)) ~ map (f @@ g) (h::t) IH: map f (map g t) ~ map (f @@ g) t We include hints, below, as to what eval steps are being taken. map f (map g (h::t)) ~ map f ((g h)::map g t) (eval map) ~ (f (g h))::map f (map g t) (eval map) ~ ((f @@ g) h)::map f (map g t) (eval @@) ~ ((f @@ g) h)::map (f @@ g) t (IH) ~ map (f @@ g) (h::t) (eval map) QED  ## Proof 3  Theorem: for all trees t, reflect(reflect t) ~ t. Proof: by induction on t. Case: t = Leaf Show: reflect(reflect Leaf) ~ Leaf reflect(reflect Leaf) ~ Leaf (eval) Case: t = Branch(x,l,r) Show: reflect(reflect(Branch(x,l,r))) ~ Branch(x,l,r) IH: 1. reflect(reflect l) ~ l 2. reflect(reflect r) ~ r reflect(reflect(Branch(x,l,r))) ~ reflect(Branch(x, reflect r, reflect l)) (eval) ~ Branch(x, reflect(reflect l), reflect(reflect r)) (eval) ~ Branch(x, l, reflect(reflect r)) (IH 1) ~ Branch(x, l, r) (IH 2) QED