MonoidList.hs

{-@ LIQUID "--reflection" @-} 

module MonoidList where

import Prelude hiding (mappend, mempty)

import Language.Haskell.Liquid.ProofCombinators 

-- | Monoid
-- | mempty-left ∀ x . mappend mempty  x ≡ x
-- | mempty-right ∀ x . mappend x  mempty ≡ x
-- | mappend-assoc ∀ x y z . mappend (mappend x  y) z ≡ mappend x (mappend y z)

{-@ reflect mappend @-}
mappend :: L a -> L a -> L a
mappend Emp      ys = ys
mappend (x :::xs) ys = x ::: mappend xs ys

{-@ reflect mempty @-}
mempty :: L a
mempty = Emp

mempty_left :: L a -> Proof
{-@ mempty_left :: x:L a -> { mappend mempty x == x }  @-}
mempty_left xs
  =   mappend mempty xs
  === mappend Emp xs
  === xs
  *** QED

mempty_right :: L a -> Proof
{-@ mempty_right :: x:L a -> { mappend x mempty == x}  @-}
mempty_right Emp
  = mappend Emp mempty === Emp
  *** QED

mempty_right (x ::: xs)
  =   mappend (x ::: xs) mempty
  === mappend (x:::xs) Emp
  === x ::: (mappend xs Emp)
    ? mempty_right xs
  === x ::: xs             
  *** QED

{-@ mappend_assoc :: xs:L a -> ys:L a -> zs:L a
               -> {mappend (mappend xs ys) zs == mappend xs (mappend ys zs) } @-}
mappend_assoc :: L a -> L a -> L a -> Proof
mappend_assoc Emp ys zs
  =   mappend (mappend Emp ys) zs
  === mappend ys zs
  === mappend Emp (mappend ys zs)
  *** QED

mappend_assoc (x ::: xs) ys zs
  =   mappend (mappend (x ::: xs) ys) zs
  === mappend (x ::: mappend xs ys) zs
  === x ::: mappend (mappend xs ys) zs
    ? mappend_assoc xs ys zs
  === x ::: mappend xs (mappend ys zs)  
  === mappend (x ::: xs) (mappend ys zs)
  *** QED

{-@ data L [llen] @-} 
data L a = Emp | a ::: L a


{-@ measure llen @-}
llen :: L a -> Int
{-@ llen :: L a -> Nat @-}
llen Emp        = 0
llen (_ ::: xs) = 1 + llen xs