LiquidHutton.hs

module NaturalDeduction where

{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--exact-data-con" @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

import Language.Haskell.Liquid.ProofCombinators

import Prelude hiding (length, head, tail, map, (++))

-- need to use a hand-rolled list type, it seems

data L a = N | C {hd :: a, tl :: L a}
{-@ data L [length] a = N | C {hd :: a, tl :: L a} @-}

length :: L a -> Int
{-@ length :: L a -> Nat @-}
{-@ measure length @-}
length N        = 0
length (C _ xs) = 1 + length xs

{-@ infix   ++ @-}
{-@ reflect ++ @-}
(++) :: L a-> L a -> L a
N        ++ ys = ys
(C x xs) ++ ys = C x (xs ++ ys)

appendNilId     :: L a -> Proof
{-@ appendNilId ::  xs:_ -> { xs ++ N = xs } @-}
appendNilId N        = ()
appendNilId (C _ xs) = appendNilId xs

appendAssoc :: L a -> L a -> L a -> Proof
{-@ appendAssoc :: xs:_ -> ys:_ -> zs:_ -> { xs ++ (ys ++ zs) = (xs ++ ys) ++ zs } @-}
appendAssoc N _ _          = ()
appendAssoc (C _ xs) ys zs = appendAssoc xs ys zs

-- huttons razor

data Expr = Val Int | Add Expr Expr
{-@ data Expr [height] = Val {theVal :: Int} | Add {summand1 :: Expr, summand2 :: Expr}  @-}


{-@ height :: Expr -> Nat @-}
{-@ measure height @-}
height :: Expr -> Int
height (Val _) = 0
height (Add e1 e2) = 1 + if height e1 > height e2 then  height e1 else height e2

{- @ eval :: e:Expr -> Int @-}
{-@ reflect eval @-}
eval :: Expr -> Int
eval (Val n)   = n
eval (Add x y) = eval x + eval y

type Stack = L Int

type Code = L Op

data Op = PUSH Int | ADD
{-@ data Op = PUSH {thePushed :: Int} | ADD @-}

{-@ reflect exec @-}
exec :: Code -> Stack -> Stack
exec N s = s
exec (C (PUSH n) c) s = exec c (C n s)
exec (C ADD      c) (C m (C n s)) = exec c (C (n+m) s)
exec (C ADD      c) (C n N) = N -- default case added
exec (C ADD      c) N = N -- default case added (need to be sparate cases)

{-@ reflect comp @-}
comp :: Expr -> Code
comp (Val n) = C (PUSH n) N
comp (Add x y) = (comp x ++ comp y) ++ (C ADD N)

-- Proofs

{-@ correctness :: e:Expr -> c:Code -> s:Stack ->
                  { exec (comp e ++ c) s = exec c (C (eval e) s) }
@-}
correctness :: Expr -> Code -> Stack -> Proof
correctness (Val n) c s =
       exec (comp (Val n) ++ c) s
   ==. exec ((C (PUSH n) N) ++ c) s
   ==. exec (C (PUSH n) c) s
   ==. exec c (C n s)
   ==. exec c (C (eval (Val n)) s)
   *** QED
correctness (Add e1 e2) c s =
       exec (comp (Add e1 e2) ++ c) s
   ==. exec (((comp e1 ++ comp e2) ++ (C ADD N)) ++ c) s
   ==. exec ((comp e1 ++ comp e2) ++ ((C ADD N) ++ c)) s
        ? appendAssoc (comp e1 ++ comp e2) (C ADD N) c
   ==. exec (comp e1 ++ (comp e2 ++ ((C ADD N) ++ c))) s
        ? appendAssoc (comp e1) (comp e2) ((C ADD N) ++ c)
   ==. exec (comp e2 ++ ((C ADD N) ++ c)) (C (eval e1) s)
        ? correctness e1 (comp e2 ++ ((C ADD N) ++ c)) s
   ==. exec ((C ADD N) ++ c) (C (eval e2) (C (eval e1) s))
        ? correctness e2 ((C ADD N) ++ c) (C (eval e1) s)
   ==. exec (C ADD c) (C (eval e2) (C (eval e1) s))
   ==. exec c (C (eval e1 + eval e2) s)
   ==. exec c (C (eval (Add e1 e2)) s)
   *** QED

{-@ lemma_app_nil :: x:a -> ys:L a -> { (C x N) ++ ys = C x ys } @-}
lemma_app_nil :: a -> L a -> Proof
lemma_app_nil _ _ = ()

{-@ correctness2 :: e:Expr -> c:Code -> s:Stack ->
                  { exec (comp e ++ c) s = exec c (C (eval e) s) }
@-}
correctness2 :: Expr -> Code -> Stack -> Proof
correctness2 (Val n) c s = trivial
correctness2 (Add e1 e2) c s =
       appendAssoc (comp e1 ++ comp e2) (C ADD N) c
   &&& appendAssoc (comp e1) (comp e2) ((C ADD N) ++ c)
   &&& correctness e1 (comp e2 ++ ((C ADD N) ++ c)) s
   &&& correctness e2 ((C ADD N) ++ c) (C (eval e1) s)
   -- &&& lemma_app_nil ADD c