    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.ProofTools.Fibonacci
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Example inductive proof to show partial correctness of the for-loop
    -- based fibonacci algorithm:
    --
    -- @
    --     i = 0
    --     k = 1
    --     m = 0
    --     while i < n:
    --        m, k = k, m + k
    --        i++
    -- @
    --
    -- We do the proof against an axiomatized fibonacci implementation using an
    -- uninterpreted function.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass        #-}
    {-# LANGUAGE DeriveGeneric         #-}
    {-# LANGUAGE DeriveTraversable     #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE NamedFieldPuns        #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.ProofTools.Fibonacci where

    import Data.SBV
    import Data.SBV.Tools.Induction
    import Data.SBV.Control

    import GHC.Generics hiding (S)

    -- * System state

    -- | System state. We simply have two components, parameterized
    -- over the type so we can put in both concrete and symbolic values.
    data S a = S { forall a. S a -> a
    i :: a, forall a. S a -> a
    k :: a, forall a. S a -> a
    m :: a, forall a. S a -> a
    n :: a }
             deriving (Int -> S a -> ShowS
    [S a] -> ShowS
    S a -> String
    (Int -> S a -> ShowS)
    -> (S a -> String) -> ([S a] -> ShowS) -> Show (S a)
    forall a. Show a => Int -> S a -> ShowS
    forall a. Show a => [S a] -> ShowS
    forall a. Show a => S a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> S a -> ShowS
    showsPrec :: Int -> S a -> ShowS
    $cshow :: forall a. Show a => S a -> String
    show :: S a -> String
    $cshowList :: forall a. Show a => [S a] -> ShowS
    showList :: [S a] -> ShowS
    Show, Bool -> SBool -> S a -> S a -> S a
    (Bool -> SBool -> S a -> S a -> S a)
    -> (forall b.
        (Ord b, SymVal b, Num b) =>
        [S a] -> S a -> SBV b -> S a)
    -> Mergeable (S a)
    forall b. (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a
    forall a. Mergeable a => Bool -> SBool -> S a -> S a -> S a
    forall a b.
    (Mergeable a, Ord b, SymVal b, Num b) =>
    [S a] -> S a -> SBV b -> S a
    forall a.
    (Bool -> SBool -> a -> a -> a)
    -> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
    -> Mergeable a
    $csymbolicMerge :: forall a. Mergeable a => Bool -> SBool -> S a -> S a -> S a
    symbolicMerge :: Bool -> SBool -> S a -> S a -> S a
    $cselect :: forall a b.
    (Mergeable a, Ord b, SymVal b, Num b) =>
    [S a] -> S a -> SBV b -> S a
    select :: forall b. (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a
    Mergeable, (forall x. S a -> Rep (S a) x)
    -> (forall x. Rep (S a) x -> S a) -> Generic (S a)
    forall x. Rep (S a) x -> S a
    forall x. S a -> Rep (S a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (S a) x -> S a
    forall a x. S a -> Rep (S a) x
    $cfrom :: forall a x. S a -> Rep (S a) x
    from :: forall x. S a -> Rep (S a) x
    $cto :: forall a x. Rep (S a) x -> S a
    to :: forall x. Rep (S a) x -> S a
    Generic, (forall a b. (a -> b) -> S a -> S b)
    -> (forall a b. a -> S b -> S a) -> Functor S
    forall a b. a -> S b -> S a
    forall a b. (a -> b) -> S a -> S b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> S a -> S b
    fmap :: forall a b. (a -> b) -> S a -> S b
    $c<$ :: forall a b. a -> S b -> S a
    <$ :: forall a b. a -> S b -> S a
    Functor, (forall m. Monoid m => S m -> m)
    -> (forall m a. Monoid m => (a -> m) -> S a -> m)
    -> (forall m a. Monoid m => (a -> m) -> S a -> m)
    -> (forall a b. (a -> b -> b) -> b -> S a -> b)
    -> (forall a b. (a -> b -> b) -> b -> S a -> b)
    -> (forall b a. (b -> a -> b) -> b -> S a -> b)
    -> (forall b a. (b -> a -> b) -> b -> S a -> b)
    -> (forall a. (a -> a -> a) -> S a -> a)
    -> (forall a. (a -> a -> a) -> S a -> a)
    -> (forall a. S a -> [a])
    -> (forall a. S a -> Bool)
    -> (forall a. S a -> Int)
    -> (forall a. Eq a => a -> S a -> Bool)
    -> (forall a. Ord a => S a -> a)
    -> (forall a. Ord a => S a -> a)
    -> (forall a. Num a => S a -> a)
    -> (forall a. Num a => S a -> a)
    -> Foldable S
    forall a. Eq a => a -> S a -> Bool
    forall a. Num a => S a -> a
    forall a. Ord a => S a -> a
    forall m. Monoid m => S m -> m
    forall a. S a -> Bool
    forall a. S a -> Int
    forall a. S a -> [a]
    forall a. (a -> a -> a) -> S a -> a
    forall m a. Monoid m => (a -> m) -> S a -> m
    forall b a. (b -> a -> b) -> b -> S a -> b
    forall a b. (a -> b -> b) -> b -> S a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => S m -> m
    fold :: forall m. Monoid m => S m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> S a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> S a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> S a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> S a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> S a -> a
    foldr1 :: forall a. (a -> a -> a) -> S a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> S a -> a
    foldl1 :: forall a. (a -> a -> a) -> S a -> a
    $ctoList :: forall a. S a -> [a]
    toList :: forall a. S a -> [a]
    $cnull :: forall a. S a -> Bool
    null :: forall a. S a -> Bool
    $clength :: forall a. S a -> Int
    length :: forall a. S a -> Int
    $celem :: forall a. Eq a => a -> S a -> Bool
    elem :: forall a. Eq a => a -> S a -> Bool
    $cmaximum :: forall a. Ord a => S a -> a
    maximum :: forall a. Ord a => S a -> a
    $cminimum :: forall a. Ord a => S a -> a
    minimum :: forall a. Ord a => S a -> a
    $csum :: forall a. Num a => S a -> a
    sum :: forall a. Num a => S a -> a
    $cproduct :: forall a. Num a => S a -> a
    product :: forall a. Num a => S a -> a
    Foldable, Functor S
    Foldable S
    (Functor S, Foldable S) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> S a -> f (S b))
    -> (forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> S a -> m (S b))
    -> (forall (m :: * -> *) a. Monad m => S (m a) -> m (S a))
    -> Traversable S
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    $cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    $csequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    sequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    Traversable)

    -- | 'Fresh' instance for our state
    instance Fresh IO (S SInteger) where
       fresh :: QueryT IO (S SInteger)
    fresh = SInteger -> SInteger -> SInteger -> SInteger -> S SInteger
    forall a. a -> a -> a -> a -> S a
    S (SInteger -> SInteger -> SInteger -> SInteger -> S SInteger)
    -> QueryT IO SInteger
    -> QueryT IO (SInteger -> SInteger -> SInteger -> S SInteger)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_ QueryT IO (SInteger -> SInteger -> SInteger -> S SInteger)
    -> QueryT IO SInteger
    -> QueryT IO (SInteger -> SInteger -> S SInteger)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_ QueryT IO (SInteger -> SInteger -> S SInteger)
    -> QueryT IO SInteger -> QueryT IO (SInteger -> S SInteger)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_ QueryT IO (SInteger -> S SInteger)
    -> QueryT IO SInteger -> QueryT IO (S SInteger)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_

    -- | Encoding partial correctness of the sum algorithm. We have:
    --
    -- >>> fibCorrect
    -- Q.E.D.
    --
    -- NB. In my experiments, I found that this proof is quite fragile due
    -- to the use of quantifiers: If you make a mistake in your algorithm
    -- or the coding, z3 pretty much spins forever without finding a counter-example.
    -- However, with the correct coding, the proof is almost instantaneous!
    fibCorrect :: IO (InductionResult (S Integer))
    fibCorrect :: IO (InductionResult (S Integer))
    fibCorrect = Bool
    -> Symbolic ()
    -> (S SInteger -> SBool)
    -> (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> (S SInteger -> SBool)
    -> (S SInteger -> (SBool, SBool))
    -> IO (InductionResult (S Integer))
    forall res st.
    (Show res, Queriable IO st, res ~ QueryResult st) =>
    Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> [(String, st -> SBool)]
    -> (st -> SBool)
    -> (st -> (SBool, SBool))
    -> IO (InductionResult res)
    induct Bool
    chatty Symbolic ()
    setup S SInteger -> SBool
    initial S SInteger -> [S SInteger]
    trans [(String, S SInteger -> SBool)]
    strengthenings S SInteger -> SBool
    inv S SInteger -> (SBool, SBool)
    goal
      where -- Set this to True for SBV to print steps as it proceeds
            -- through the inductive proof
            chatty :: Bool
            chatty :: Bool
    chatty = Bool
    False

            -- Declare fib as un uninterpreted function:
            fib :: SInteger -> SInteger
            fib :: SInteger -> SInteger
    fib = String -> SInteger -> SInteger
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "fib"

            -- We setup to axiomatize the textbook definition of fib in SMT-Lib
            setup :: Symbolic ()
            setup :: Symbolic ()
    setup = do SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SInteger -> SInteger
    fib SInteger
    0 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0
                       SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SInteger -> SInteger
    fib SInteger
    1 SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    1
                       (Forall Any Integer -> SBool) -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Integer -> SBool) -> Symbolic ())
    -> (Forall Any Integer -> SBool) -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SInteger
    x) -> SInteger -> SInteger
    fib (SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    2) SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger -> SInteger
    fib (SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1) SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger -> SInteger
    fib SInteger
    x

            -- Initialize variables
            initial :: S SInteger -> SBool
            initial :: S SInteger -> SBool
    initial S{SInteger
    i :: forall a. S a -> a
    i :: SInteger
    i, SInteger
    k :: forall a. S a -> a
    k :: SInteger
    k, SInteger
    m :: forall a. S a -> a
    m :: SInteger
    m, SInteger
    n :: forall a. S a -> a
    n :: SInteger
    n} = SInteger
    i SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0 SBool -> SBool -> SBool
    .&& SInteger
    k SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    1 SBool -> SBool -> SBool
    .&& SInteger
    m SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0 SBool -> SBool -> SBool
    .&& SInteger
    n SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0

            -- We code the algorithm almost literally in SBV notation:
            trans :: S SInteger -> [S SInteger]
            trans :: S SInteger -> [S SInteger]
    trans st :: S SInteger
    st@S{SInteger
    i :: forall a. S a -> a
    i :: SInteger
    i, SInteger
    k :: forall a. S a -> a
    k :: SInteger
    k, SInteger
    m :: forall a. S a -> a
    m :: SInteger
    m, SInteger
    n :: forall a. S a -> a
    n :: SInteger
    n} = [SBool -> S SInteger -> S SInteger -> S SInteger
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< SInteger
    n)
                                          S SInteger
    st { i = i + 1, k = m + k, m = k }
                                          S SInteger
    st
                                     ]

            -- No strengthenings needed for this problem!
            strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = []

            -- Loop invariant: @i@ remains at most @n@, @k@ is @fib (i+1)@
            -- and @m@ is fib(i)@:
            inv :: S SInteger -> SBool
            inv :: S SInteger -> SBool
    inv S{SInteger
    i :: forall a. S a -> a
    i :: SInteger
    i, SInteger
    k :: forall a. S a -> a
    k :: SInteger
    k, SInteger
    m :: forall a. S a -> a
    m :: SInteger
    m, SInteger
    n :: forall a. S a -> a
    n :: SInteger
    n} =    SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SInteger
    n
                               SBool -> SBool -> SBool
    .&& SInteger
    k SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger -> SInteger
    fib (SInteger
    iSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1)
                               SBool -> SBool -> SBool
    .&& SInteger
    m SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger -> SInteger
    fib SInteger
    i

            -- Final goal. When the termination condition holds, the value @m@
            -- holds the @n@th fibonacc number. Note that SBV does not prove the
            -- termination condition; it simply is the indication that the loop
            -- has ended as specified by the user.
            goal :: S SInteger -> (SBool, SBool)
            goal :: S SInteger -> (SBool, SBool)
    goal S{SInteger
    i :: forall a. S a -> a
    i :: SInteger
    i, SInteger
    m :: forall a. S a -> a
    m :: SInteger
    m, SInteger
    n :: forall a. S a -> a
    n :: SInteger
    n} = (SInteger
    i SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    n, SInteger
    m SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger -> SInteger
    fib SInteger
    n)