Liquid Haskell Proofs Goals Formally prove the theorems outlined in the “Reasoning about Programs” chapter of the book “Programming in Haskell” using Liquid Haskell Formally prove the theoerms in the paper “Calculating Correct Compilers” which the chapter was adapted from. Tasks Chapter reverse [x] = [x] add n Zero = n add x (add y z) = add (add x y) z length (replicate n x) = n reverse (reverse xs) = xs and corresponding lemmas reverse xs = reverse′ xs [] reverse xs = foldl (flip (:)) [] xs flatten t = flatten′ t [] exec (comp e) [] = [eval e] and corresponding lemmas exec (comp′ e c) s = exec c (eval e : s) Exercises add n (Succ m) = Succ (add n m) add n m = add m n all (== x) (replicate n x) xs ++ [] = xs xs ++ (ys ++ zs) = (xs ++ ys) ++ zs reverse (xs ++ [x]) = x : reverse xs map f (map g xs) = map (f . g) xs take n xs ++ drop n xs = xs the number of leaves in a binary tree without empty nodes is one more than the number of internal nodes construct comp′ given comp′ e c = comp e ++ c (this might not be in scope).
