content: {-@ LIQUID "--higherorder"     @-}
  {-@ LIQUID "--ple" @-}
  
  -- TAG: absref
  
  module Fibonacci where
  import Language.Haskell.Liquid.ProofCombinators
  
  
  -- | Proves that the fibonacci function is increasing
  
  
  -- | Definition of the function in Haskell
  -- | the annotation axiomatize means that
  -- | in the logic, the body of increase is known
  -- | (each time the function fib is applied,
  -- | there is an unfold in the logic)
  
  {-@ reflect fib @-}
  
  fib :: Int -> Int
  {-@ fib :: i:Nat -> Nat @-}
  fib i | i == 0    = 0
        | i == 1    = 1
        | otherwise = fib (i-1) + fib (i-2)
  
  {-@ fib1 :: () -> {fib 16 == 987 } @-}
  fib1 :: () -> Proof
  fib1 _ = trivial
  
  fibUp :: Int -> Proof
  {-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-}
  fibUp i
    | i == 0
    =   [fib 0, fib 1] *** QED
    | i == 1
    =  [fib 1, fib 0, fib 2] *** QED
    | otherwise
    = [[fib (i+1), fib i] *** QED , fibUp (i-1), fibUp (i-2)] *** QED
  {-
    | otherwise
    =   fibUp (i-1)
    &&& fibUp (i-2)
  -}
  
  -- 0, 1, 2, 3, 4, 5, 6, 7,   8,  9, 10, 11,  12, 13,   14,  15, 16
  -- 0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987
  
  
  {-
  FStar failing
  
  val fib: x:int{x>=0} -> Tot int
  let rec fib n =
    if n = 0 then 0
    else if n = 1 then 1 else fib (n-1) + fib (n-2)
  
  
  val prop: x:int -> Tot (v:int {fib 15 = 610})
  let prop x =  0
  
  -}
  
  -- | How to encode proofs:
  -- | ==., <=., and <. stand for the logical ==, <=, < resp.
  -- | If the proofs do not derive automatically, user can
  -- | optionally provide the Proofean statements, after `?`
  -- | Note, no inference occurs: logic only reasons about
  
  {-
  fibUp :: Int -> Proof
  {-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-}
  fibUp i
    | i == 0
    =   trivial
    | i == 1
    =  trivial --  fib 2 *** QED
    | otherwise
    =   fibUp (i-1)
    &&& fibUp (i-2)
  -}
  {-
  Explicit Proof
  fibMonotonic x y
    | y == x + 1
    =   fib x
    <=. fib (x+1) ? fibUp x
    <=. fib y
    *** QED
    | x < y - 1
    =   fib x
    <=. fib (y-1) ? fibMonotonic x (y-1)
    <=. fib y     ? fibUp (y-1)
    *** QED
  
  FStar Proof
  
  val fibUp :i:int{0 <= i} -> Tot (v:int {fib i <= fib (i+1)})
  let rec fibUp i =
      if i=0 then 0 else
      if i=1 then 1 else (fibUp (i-1) + fibUp (i-2))
  -}
  
  
  fibMonotonic :: Int -> Int -> Proof
  {-@ fibMonotonic :: x:Nat -> y:{Nat | x < y }
       -> {fib x <= fib y}  / [y] @-}
  fibMonotonic x y
    | y == x + 1
    =   fibUp x
    | x < y - 1
    =   fibMonotonic x (y-1)
    &&& fibUp (y-1)
  
  
  fMono :: (Int -> Int)
        -> (Int -> Proof)
        -> Int -> Int -> Proof
  {-@ fMono :: f:(Nat -> Int)
            -> fUp:(z:Nat -> {f z <= f (z+1)})
            -> x:Nat
            -> y:{Nat|x < y}
            -> {f x <= f y} / [y] @-}
  fMono f fUp x y
    | x + 1 == y
    = fUp x
    | x + 1 < y
    =   fMono f fUp x (y-1)
    &&& fUp (y-1)
  
  
  fibMonoHO :: Int -> Int -> Proof
  {-@ fibMonoHO :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m} @-}
  fibMonoHO     = fMono fib fibUp
  
  -- forall n:Nat. exists m: (n<m => exists m'. fib n <== m')
  fibEx :: Int -> (Int, Proof) -> (Int, Proof)
  {-@ fibEx :: n:Nat -> (m::Int, {v:Proof | n < m})
           -> (m'::Int, {v:Proof | fib n <= m' }) @-}
  fibEx n (m, pf) = (fib m, fibMonoHO n m)
  