IndPal0.hs

{-# LANGUAGE GADTs #-}

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

module IndPalindrome where

import Prelude hiding ((++))
import Language.Haskell.Liquid.ProofCombinators

{-@ infixr ++  @-}
{-@ reflect ++ @-}
(++) :: [a] -> [a] -> [a] 
[]     ++ ys = ys 
(x:xs) ++ ys = x : (xs ++ ys)

{-@ reflect rev @-}
rev :: [a] -> [a] 
rev []     = [] 
rev (x:xs) = rev xs ++ [x] 

{-@ reflect mkPal @-}
mkPal :: a -> [a] -> [a]
mkPal x xs = x : (xs ++ [x])

{-@ reflect single @-}
single :: a -> [a]
single x = [x]

--------------------------------------------------------------------------------
-- | The Prop declaring the Palindrome predicate 
data PalP a where
  Pal :: [a] -> PalP a

-- | The Predicate implementing the Palindrom predicate 
data Pal a where
  Pal0 :: Pal a 
  Pal1 :: a -> Pal a 
  Pals :: a -> [a] -> Pal a -> Pal a 

{-@ data Pal a where
        Pal0 :: Prop (Pal []) 
        Pal1 :: x:_ -> Prop (Pal (single x)) 
        Pals :: x:_ -> xs:_ -> Prop (Pal xs) -> Prop (Pal (mkPal x xs)) 
  @-}

{-@ assume admit :: _ -> { false } @-}
admit () = ()

{-@ ple lemma_pal @-}
{-@ lemma_pal :: xs:_ -> p:Prop (Pal xs) -> { xs = rev xs } @-}
lemma_pal :: [a] -> Pal a -> Proof
lemma_pal []  Pal0           = () 
lemma_pal [_] (Pal1 _)       = () 
lemma_pal xs (Pals y ys pys) = admit ()