**1.**Introduction**1.1.**What is Liquid Haskell?**1.2.**More precise types**1.3.**An extension of Haskell**1.4.**Refinement types**1.5.**Type synonyms**1.6.**Refinement types must refine**1.7.**One expression, many types**1.8.**Refinement types and functions**1.9.**Preconditions vs. postconditions**1.10.**Integer arithmetic**1.11.**Exercises**2.**Lists**2.1.**Goal**2.2.**Our own list type**2.3.**Termination**2.4.**Measures**2.5.**Mapping**2.6.**Interleaving two lists**2.7.**Disabling termination checking**2.8.**Totality**2.9.**Impossible cases**2.10.**Exercises**2.11.**Taking elements out of a list**2.12.**Dropping elements from a list**2.13.**Computing s sublist**2.14.**Replicating an element**2.15.**Computing a range of numbers**2.16.**Safe indexing**2.17.**Bonus exercises**2.18.**Finding equal elements**2.19.**Grouping elements**2.20.**Run-length encoding**3.**Sets**3.1.**Uninterpreted functions**3.2.**Using an uninterpreted function**3.3.**Sets**3.4.**Lookup tables**3.5.**Another measure on maps**3.6.**A safe lookup function**3.7.**Removing bindings**4.**Proofs**4.1.**Tables again**4.2.**Reflecting functions**4.3.**Proving a simple property**4.4.**And a slightly more complicated one ...**4.5.**A property on lists**5.**Conclusions

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--exact-data-cons" @-}
module Proofs where
import Prelude hiding (length, lookup, reverse)
import Language.Haskell.Liquid.ProofCombinators
data List a = Nil | Cons a (List a)
deriving (Show)
infixr 5 `Cons`
{-@ measure length @-}
{-@ data List [length] @-}
{-@ length :: List a -> Nat @-}
length :: List a -> Int
length Nil = 0
length (x `Cons` xs) = 1 + length xs

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.

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)

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 @-}

{-@ 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

{-@ 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

{-
doubleDelete k Empty =
delete k (delete k Empty)
==. delete k Empty
*** QED
doubleDelete k (Bind k' v r)
| k == k' =
delete k (delete k (Bind k v r))
==. delete k (delete k r)
==. delete k r ? doubleDelete k r
*** QED
| otherwise =
delete k (delete k (Bind k' v r))
==. delete k (Bind k' v (delete k r))
==. Bind k' v (delete k (delete k r))
==. Bind k' v (delete k r) ? doubleDelete k r
*** QED
-}

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

{-
appendNil Nil =
append Nil Nil
==. Nil
*** QED
appendNil (Cons x xs) =
append (Cons x xs) Nil
==. Cons x (append xs Nil) ? appendNil xs
==. Cons x xs
*** QED

{-@ 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
appendAssoc Nil ys zs =
append Nil (append ys zs)
==. append ys zs
==. append (append Nil ys) zs
*** QED
appendAssoc (Cons x xs) ys zs =
append (Cons x xs) (append ys zs)
==. Cons x (append xs (append ys zs)) ? appendAssoc xs ys zs
==. Cons x (append (append xs ys) zs)
==. append (Cons x (append xs ys)) zs
==. append (append (Cons x xs) ys) zs
*** QED
-}