# Behavioral Equivalence Today we will do proofs with behavioral equivalence and induction. ##### Exercise: double [&#10029;] Prove that for all integers x, double x ~ 2*x, where double is defined as follows:  let double n = n + n  &square; ##### Exercise: exp [&#10029;&#10029;] Prove that for all integers a and natural numbers x, exp a x ~ a ** x, where ** denotes the mathematical operation of integer exponentiation (hence overloading the built-in ** operator), and where exp is defined as follows:  let rec exp a x = if x = 0 then 1 else a*(exp a (x-1))  Use the following as a template for your proof about exp:  Theorem: for all ints a, for all naturals x, exp a x ~ a ** x Proof: by induction on x Case: x=0 Show: TODO TODO Case: x=k+1, where k >= 0 Show: TODO IH: TODO TODO QED  &square; ##### Exercise: facti [&#10029;&#10029;] Prove that for all natural numbers n and for all ints p, facti n p ~ n! * p, where facti is defined as follows:  (* [facti n p] is [n! * p]. * The implementation is a tail-recursive (sometimes called *iterative*) * generalization of the usual recursive factorial function. * Precondition: n >= 0 *) let rec facti n p = if n = 0 then p else facti (n-1) (n*p)  Use the following as a template for your proof about facti. Note carefully how induction on n leaves p universally quantified&mdash;which you will need to finish the second case.  Theorem: for all naturals n, for all ints p, facti n p ~ n! * p Proof: by induction on n Case: n=0 Show: for all ints p, facti 0 p ~ 0! * p TODO Case: n=k+1, where k >= 0 Show: for all ints p, facti (k+1) p ~ (k+1)! * p IH: for all ints p, facti k p ~ k! * p TODO QED  &square; ##### Exercise: fact [&#10029;] Prove that for all natural numbers n, fact n ~ n!, where fact is defined as follows:  let fact n = facti n 1  *Hint: use the previous theorem as a lemma.* &square; Let fact have the following *specification*:  (* precondition: n >= 0 *) (* postcondition: (fact n) = n! *) val fact : int -> int  You have proven the correctness of a tail-recursive implementation of the factorial function. Reflect on why that is so. ## Additional exercises ##### Exercise: sum_sqrs [&#10029;&#10029;] Prove that for all natural numbers n, sum_sqrs n ~ (n * (n+1) * (2*n + 1))/6, where sum_sqrs is defined as follows:  let rec sum_sqrs n = if n <= 0 then 0 else (n*n) + sum_sqrs(n-1)  &square; ##### Exercise: exp square [&#10029;&#10029;&#10029;&#10029;] The recursive implementation of exp, above, is inefficient. Implement [exponentiation by squaring][exp-square] in OCaml. Prove the correctness of your implementation. Use the proofs you did for fact as an inspiration. *Hint: recall strong induction (aka [complete induction][compl-ind]) from CS 2800.* [exp-square]: https://en.wikipedia.org/wiki/Exponentiation_by_squaring [compl-ind]: https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction &square;