# Induction and Recursion Today we will practice proving behavioral equivalence of expressions involving variants and functions. ##### Exercise: behead [&#10029;] Prove that for any list xs and element x, behead (prepend xs x) ~ xs, where prepend and behead are defined as follows:  let prepend xs x = x::xs let behead = function | [] -> [] | _::t -> t  *Hint: induction is not needed.* &square; ##### Exercise: noop [&#10029;&#10029;] Prove that for any list xs, noop xs ~ xs, where noop is defined as follows:  let rec noop = function | [] -> [] | h::t -> h :: noop t  Use the following template for an inductive proof:  Theorem: TODO(xs) Proof: by induction on xs Case: xs = [] Show: TODO TODO Case: xs=h::t Show: TODO IH : TODO TODO QED  ##### Exercise: append assoc [&#10029;&#10029;] Prove that for all lists l1, l2, and l3, it holds that l1 @ (l2 @ l3) ~ (l1 @ l2) @ l3. &square; ##### Exercise: size reflect [&#10029;&#10029;] Prove that for all trees t, size (reflect t) ~ size t, given the following definitions:  type 'a tree = Leaf | Branch of 'a * 'a tree * 'a tree let rec reflect = function | Leaf -> Leaf | Branch(x,l,r) -> Branch(x, reflect r, reflect l) let rec size = function | Leaf -> 0 | Branch(x,l,r) -> 1 + size l + size r  &square; ##### Exercise: apply assoc [&#10029;] Prove that for all functions f, g, and h (of appropriate types), (f @@ g) @@ h ~ f @@ (g @@ h), where (@@) is defined as follows:  let (@@) f g x = f (g x)  *Hint: use extensionality; induction is not needed.* &square; ## Additional exercises ##### Exercise: map append [&#10029;&#10029;&#10029;] Prove that for all f, xs, and ys, map f (xs @ ys) = (map f xs) @ (map f ys), where map and (@) are defined as follows:  let rec append l1 l2 = match l1 with | [] -> l2 | h::t -> h :: (append t l2) let (@) = append let rec map f = function | [] -> [] | h::t -> (f h) :: map f t  &square; ##### Exercise: rev_append [&#10029;&#10029;&#10029;] Prove that for all lists xs, and for all lists ys, rev_append xs ys ~ (nrev xs) @ ys, where rev_append and nrev are defined as follows:  let rec rev_append l1 l2 = match l1 with | [] -> l2 | h::t -> rev_append t (h :: l2) let rec nrev = function | [] -> [] | h::t -> (nrev t) @ [h]  *Hint: use a previous exercise as a lemma.* &square; ##### Exercise: rev [&#10029;&#10029;] Next, prove that for all lists xs, rev xs ~ nrev xs, where rev is defined as follows:  let rev xs = rev_append xs []  *Hint: Make use of previous exercises. You might discover that it would be helpful to state and prove a relatively simple lemma involving [] and @.* Note that this definition of rev is, in fact, how OCaml's List.rev is defined. You have therefore proved the correctness of a tail-recursive implementation of list reversal by showing its equivalence to a non-tail-recursive implementation. &square;