content: {-@ LIQUID "--exactdc" @-}
  {-@ LIQUID "--higherorder" @-}
  {-@ LIQUID "--ple-local" @-}
  {-@ infix   ++ @-}
  
  module T1223 where
  
  import Prelude hiding (reverse, (++))
  
  data Defined = Defined
  infixl 2 ^^^
  x ^^^ Defined = x 
  infixl 3 ==., ? 
  
  x ? _ = x 
  
  (==.) :: a -> a -> a 
  _ ==. x = x 
   
  
  
  
  -------------------------------------------------------------------------------
  -- | Specification of reverse' ------------------------------------------------
  -------------------------------------------------------------------------------
  
  {-@ specReverse' :: xs:[a] -> ys:[a] -> {reverse' xs ys = reverse xs ++ ys} @-}
  specReverse' :: [a] -> [a] -> ()
  specReverse' _ _ = undefined   
  
  -------------------------------------------------------------------------------
  -- | Derivation of reverse' ---------------------------------------------------
  -------------------------------------------------------------------------------
  
  -- LH TODO: LH is not letting you define a measure and a Haskell function
  -- with the same name, for now...
  {-@ measure reverse' :: [a] -> [a] -> [a] @-}
  reverse' :: [a] -> [a] -> [a]
  {-@ reverse' :: xs:[a] -> ys:[a] -> { reverse' xs ys = reverse xs ++ ys } @-}
  reverse' [] ys 
    =   reverse [] ++ ys 
    ==. [] ++ ys ? specReverse' [] ys 
    ==. ys 
    ^^^ Defined 
  
  
  reverse' (x:xs) ys 
    =   reverse (x:xs) ++ ys  
    ==. (reverse xs ++ [x]) ++ ys ? specReverse' (x:xs) ys
    ==. reverse xs ++ ([x] ++ ys) ? assoc (reverse xs) [x] ys
    ==. reverse xs ++ (x:ys) 
    ==. reverse' xs (x:ys)
    ^^^ Defined 
  
  -------------------------------------------------------------------------------
  -- | Helpers: Definitions & Theorems Used -------------------------------------
  -------------------------------------------------------------------------------
  
  {-@ reflect reverse @-}
  reverse :: [a] -> [a]
  reverse []     = []
  reverse (x:xs) = reverse xs ++ [x]
  
  {-@ reflect ++ @-}
  (++) :: [a] -> [a] -> [a]
  []     ++ ys = ys
  (x:xs) ++ ys = x:(xs ++ ys)
  
  
  {-@ automatic-instances assoc @-}
  {-@ assoc :: xs:[a] -> ys:[a] -> zs:[a] 
            -> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs }  @-}
  assoc :: [a] -> [a] -> [a] -> () 
  assoc [] _ _       = ()
  assoc (x:xs) ys zs = assoc xs ys zs
  
  
  