Helper.hs

-- | Proving ackermann properties from
-- | http://www.cs.yorku.ca/~gt/papers/Ackermann-function.pdf

{-@ LIQUID "--reflection"     @-}
{- LIQUID "--betaequivalence" @-}
{- LIQUID "--autoproofs"      @-}


module Helper (
    gen_increasing, gen_increasing2
  , gen_incr
  , lambda_expand, beta_application
  ) where

import Language.Haskell.Liquid.ProofCombinators
import Proves (Arg, (=*=:))

{-@ assume beta_application :: bd:b -> f:(a -> {bd':b | bd' == bd}) -> x:a -> {f x == bd } @-}
beta_application :: b -> (a -> b) -> a -> Proof  
beta_application bd f x 
  = trivial

lambda_expand :: Arg r => (r -> a) -> Proof 
{-@ assume lambda_expand :: r:(r -> a) -> { (\x:r -> r x) == r } @-}
lambda_expand r 
  = ( r =*=: \x -> r x) (body_lambda_expand r) *** QED 


body_lambda_expand :: Arg r => (r -> a) -> r -> Proof 
{-@ assume body_lambda_expand :: r:(r -> a) -> y:r -> { (\x:r -> r x) (y)  == r y } @-}
body_lambda_expand r y = trivial 


-- | forall f :: a -> a
-- |   if    forall x:Nat.   f x < f (x+1)
-- |   then  forall x,y:Nat.  x < y => f x < f y

{-@ type Greater N = {v:Int | N < v } @-}

gen_increasing :: (Int -> Int) -> (Int -> Proof) -> (Int -> Int -> Proof)
{-@ gen_increasing :: f:(Nat -> Int)
                   -> (z:Nat -> {v:Proof | f z < f (z+1) })
                   ->  x:Nat -> y:Greater x -> {v:Proof | f x < f y } / [y] @-}
gen_increasing f thm x y

  | x + 1 == y
  =    f y 
  ===  f (x + 1)
    ?  thm x
  =>=  f x       
  ***  QED

  | x + 1 < y
  =    f x
       ? gen_increasing f thm x (y-1)
  =<=  f (y-1)
       ?   thm (y-1)
  =<=  f y       
  *** QED

revgen_increasing :: (Int -> Int) -> (Int -> Int -> Proof) -> (Int -> Proof)
{-@ revgen_increasing :: f:(Nat -> Int)
                   ->  (x:Nat -> y:Greater x -> {v:Proof | f x < f y })
                   -> z:Nat -> {v:Proof | f z < f (z+1) } @-}
revgen_increasing f thm z
  = thm z (z+1)

gen_incr :: (Int -> Int) -> (Int -> Proof) -> (Int -> Int -> Proof)
{-@ gen_incr :: f:(Nat -> Int)
                   -> (z:Nat -> {f z <= f (z+1)})
                   ->  x:Nat -> y:Greater x -> {f x <= f y} / [y] @-}
gen_incr f thm x y
  | x + 1 == y
  =   f x 
      ? thm x 
  =<= f (x + 1) 
  =<= f y
  *** QED

  | x + 1 < y
  =   f x  
      ? gen_incr f thm x (y-1)
  =<= f (y-1)   
      ? thm (y-1)
  =<= f y
  *** QED


gen_increasing2 :: (Int -> a -> Int) -> (a -> Int -> Proof) -> (a -> Int -> Int -> Proof)
{-@ gen_increasing2 :: f:(Nat -> a -> Int)
                    -> (w:a -> z:Nat -> {v:Proof | f z w < f (z+1) w })
                    ->  c:a -> x:Nat -> y:Greater x -> {v:Proof | f x c < f y c } / [y] @-}
gen_increasing2 f thm c x y
  | x + 1 == y
  = f y c 
  === f (x + 1) c
      ? thm c x 
  =>= f x c
  *** QED

  | x + 1 < y
  =   f x c    
      ? gen_increasing2 f thm c x (y-1)
  =<= f (y-1) c 
      ? thm c (y-1)
  =<= f y c 
  *** QED