-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Fibonacci
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving that the naive version of fibonacci and the faster tail-recursive
-- version are equivalent.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Fibonacci(correctness) where

import Data.SBV
import Data.SBV.TP

-- * Naive fibonacci

-- | Calculate fibonacci using the textbook definition.
fibonacci :: SInteger -> SInteger
fibonacci :: SInteger -> SInteger
fibonacci = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"fibonacci" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1) SInteger
1 (SInteger -> SInteger
fibonacci (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fibonacci (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
2))

-- * Tail recursive version

-- | Tail recursive version
fib :: SInteger -> SInteger -> SInteger -> SInteger
fib :: SInteger -> SInteger -> SInteger -> SInteger
fib = String
-> (SInteger -> SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"fib" ((SInteger -> SInteger -> SInteger -> SInteger)
 -> SInteger -> SInteger -> SInteger -> SInteger)
-> (SInteger -> SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
a SInteger
b SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
a (SInteger -> SInteger -> SInteger -> SInteger
fib SInteger
b (SInteger
aSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
b) (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1))

-- | Faster version of fibonacci, using the tail-recursive version.
fibTail :: SInteger -> SInteger
fibTail :: SInteger -> SInteger
fibTail = SInteger -> SInteger -> SInteger -> SInteger
fib SInteger
1 SInteger
1

-- * Correctness

-- | Proving the the tail version of fibonacci is equivalent to the textbook version.
--
-- We have:
--
-- >>> correctness
-- Inductive lemma: helper
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2 (unfold fibonacci)            Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: fibCorrect
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] fibCorrect :: Ɐn ∷ Integer → Bool
correctness :: IO (Proof (Forall "n" Integer -> SBool))
correctness :: IO (Proof (Forall "n" Integer -> SBool))
correctness = TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "n" Integer -> SBool))
 -> IO (Proof (Forall "n" Integer -> SBool)))
-> TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
helper <- String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer -> Forall "k" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> Forall "k" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs (Forall "n" Integer -> Forall "k" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"helper"
                   (\(Forall SInteger
n) (Forall SInteger
k) ->
                       SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger -> SInteger
fib (SInteger -> SInteger
fibonacci SInteger
k) (SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
n)) ((Proof
    (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
  -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
  -> IStepArgs
       (Forall "n" Integer -> Forall "k" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)))
-> (Proof
      (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
    -> IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
    -> IStepArgs
         (Forall "n" Integer -> Forall "k" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \Proof (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
ih IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger
k -> [SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, SInteger
k SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0]
                           [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger -> SInteger -> SInteger
fib (SInteger -> SInteger
fibonacci SInteger
k) (SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) (SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                           SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
fib (SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) (SInteger -> SInteger
fibonacci SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n
                           SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold fibonacci"
                           TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
fib (SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)) (SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
2)) SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n
                           SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "n" Integer -> Forall "k" Integer -> SBool))
Proof (Forall "k" Integer -> SBool)
ih Proof (Forall "k" Integer -> SBool)
-> IArgs (Forall "k" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                           TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
fibonacci (SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
IHArg (Forall "n" Integer -> Forall "k" Integer -> SBool)
n)
                           SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed

  String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"fibCorrect"
       (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
fibonacci SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
fibTail SInteger
n) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
       \SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
fibTail SInteger
n
                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger -> SInteger -> SInteger
fib SInteger
1 SInteger
1 SInteger
n
                       SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
helper Proof (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> IArgs (Forall "n" Integer -> Forall "k" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"k" SInteger
0)
                       TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
fibonacci SInteger
n
                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed