content: {-@ LIQUID "--higherorder"                         @-}
  {-@ LIQUID "--ple" @-}
  
  module FibEq where
  
  fibInv  :: Int -> Int -> () 
  fibLin  :: Int -> Int 
  fibLin' :: Int -> Int -> Int -> Int 
  fibExp  :: Int -> Int 
  fibEq   :: Int -> () 
  
  -- | Exponential `fib` implementation --------------------------------
  
  {-@ reflect fibExp @-}
  {-@ fibExp :: Nat -> Nat @-}
  fibExp n 
    | n == 0    = 0 
    | n == 1    = 1 
    | otherwise = fibExp (n-2) + fibExp (n-1)
  
  -- | Linear `fib` implementation ------------------------------------ 
  
  {-@ reflect fibLin' @-}
  {-@ fibLin' :: Nat -> Nat -> Nat -> Nat @-}
  fibLin' n a b 
    | n == 0    = b 
    | otherwise = fibLin' (n - 1) (a + b) a
  
  {-@ reflect fibLin @-}
  {-@ fibLin :: Nat -> Nat @-}
  fibLin n = fibLin' n 1 0
  
  -- | Invariant relating the two implementations -------------------- 
  
  {-@ fibInv :: d:Nat -> u:Nat -> 
        {fibLin' d (fibExp (1+u)) (fibExp u) = fibExp (d+u)} 
    @-}
  fibInv d u 
    | d == 0    = () 
    | otherwise = fibInv (d-1) (u+1)
  
  -- | Equivalence of two implementations ---------------------------- 
  
  {-@ fibEq :: n:Nat -> {fibLin n = fibExp n} @-}
  fibEq n = fibInv n 0 
  
  
  