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)
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
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
leftId :: L a -> Proof
{-@ leftId :: xs:L a -> {xs ++ N == xs } @-}
leftId _ = undefined