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).