Append is Associative


module AppendAssoc where
import Prelude hiding ((++), length)
import Language.Haskell.Liquid.ProofCombinators 
{-@ infix ++ @-}
{-@ LIQUID "--totality" @-}
{-@ reflect ++ @-}
(++) :: L a -> L a -> L a 
N ++ ys        = ys 
(C x xs) ++ ys = C x (xs ++ ys)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
assoc :: L a -> L a -> L a -> Proof 
{-@ assoc :: xs:L a  -> ys:L a -> zs:L a
          -> { (xs ++ ys) ++ zs == xs ++ (ys ++ zs) } @-}
assoc (C x xs) ys zs 
  =   (C x xs ++ ys) ++ zs
  ==. (C x xs) ++ (ys ++ zs)
  *** QED 
assoc N  ys zs 
  =   (N  ++ ys) ++ zs
  ==. ys ++ zs
  ==. N ++ (ys ++ zs)
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
data L a = N | C {hd :: a, tl :: L a}
{-@ data L [length] a = N | C {hd :: a, tl :: L a} @-}
{-@ measure length @-}
{-@ length :: L a -> Nat @-} 
length :: L a -> Int 
length N = 0 
length (C _ xs) = 1 + length xs
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
leftId :: L a -> Proof 
{-@ leftId :: xs:L a -> {xs ++ N == xs } @-}
leftId _ = undefined 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX