Proofs

Sometimes, we want to prove properties that require more complex reasoning and/or cannot easily be attached to the type of one particular function.

Liquid Haskell provides proof combinators for this purpose.

Tables again

Let's use a more classic version of lookup tables as the basic for our properties.

data Table key val = Empty | Bind key val (Table key val) {-@ measure size @-} {-@ size :: Table key val -> Nat @-} size :: Table key val -> Int size Empty = 0 size (Bind _ _ t) = 1 + size t {-@ data Table [size] @-}

Our lookup function returns a Maybe now:

lookup :: Ord key => key -> Table key val -> Maybe val lookup _ Empty = Nothing lookup k (Bind k' v r) | k == k' = Just v | otherwise = lookup k r

And delete is as before:

delete :: Ord key => key -> Table key val -> Table key val delete _ Empty = Empty delete k (Bind k' v r) | k == k' = delete k r | otherwise = Bind k' v (delete k r)

Reflecting functions

In order to prove theorems about lookup and delete, we have to be able to talk about them in types.

But we cannot make them measures, because they have more than one argument.

However, we can use reflect instead. (This requires passing the --exact-data-cons flag to Liquid Haskell.)

{-@ reflect lookup @-} {-@ reflect delete @-}

Proving a simple property

{-@ lookupInsert :: k1 : key -> { k2 : key | k2 /= k1 } -> v : val -> t : Table key val -> { lookup k1 (Bind k2 v t) == lookup k1 t } @-} lookupInsert :: Ord key => key -> key -> val -> Table key val -> Proof lookupInsert = undefined

And a slightly more complicated one ...

{-@ doubleDelete :: k : key -> t : Table key val -> { delete k (delete k t) == delete k t } @-} doubleDelete :: Ord key => key -> Table key val -> Proof doubleDelete = undefined

A property on lists

Let's also prove some properties on lists. We use our own version of lists again.

append :: List a -> List a -> List a append Nil ys = ys append (Cons x xs) ys = Cons x (append xs ys) {-@ reflect append @-}
{-@ appendNil :: xs : List a -> { append xs Nil == xs } @-} appendNil :: List a -> Proof appendNil = undefined
{-@ appendAssoc :: xs : List a -> ys : List a -> zs : List a -> { (append xs (append ys zs)) == (append (append xs ys) zs) } @-} appendAssoc :: List a -> List a -> List a -> Proof appendAssoc xs ys zs = undefined