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