    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.ProofTools.Strengthen
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- An example showing how traditional state-transition invariance problems
    -- can be coded using SBV, using induction. We also demonstrate the use of
    -- invariant strengthening.
    --
    -- This example comes from Bradley's [Understanding IC3](http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf) paper,
    -- which considers the following two programs:
    --
    -- @
    --      x, y := 1, 1                    x, y := 1, 1
    --      while *:                        while *:
    --        x, y := x+1, y+x                x, y := x+y, y+x
    -- @
    --
    -- Where @*@ stands for non-deterministic choice. For each program we try to prove that @y >= 1@ is an invariant.
    --
    -- It turns out that the property @y >= 1@ is indeed an invariant, but is
    -- not inductive for either program. We proceed to strengten the invariant
    -- and establish it for the first case. We then note that the same strengthening
    -- doesn't work for the second program, and find a further strengthening to
    -- establish that case as well. This example follows the introductory example
    -- in Bradley's paper quite closely.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.ProofTools.Strengthen where

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

    -- * 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
    x :: a, forall a. S a -> a
    y :: 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, (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 -> S SInteger
    forall a. a -> a -> S a
    S (SInteger -> SInteger -> S SInteger)
    -> QueryT IO SInteger -> QueryT IO (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 -> 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 the problem

    -- | We parameterize over the transition relation and the strengthenings to
    -- investigate various combinations.
    problem :: (S SInteger -> [S SInteger]) -> [(String, S SInteger -> SBool)] -> IO (InductionResult (S Integer))
    problem :: (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    trans [(String, S SInteger -> SBool)]
    strengthenings = 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

            -- This is where we would put solver options, typically via
            -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
            -- so we simply do nothing.
            setup :: Symbolic ()
            setup :: Symbolic ()
    setup = () -> Symbolic ()
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

            -- Initially, @x@ and @y@ are both @1@
            initial :: S SInteger -> SBool
            initial :: S SInteger -> SBool
    initial S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = SInteger
    x SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    1 SBool -> SBool -> SBool
    .&& SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    1

            -- Invariant to prove:
            inv :: S SInteger -> SBool
            inv :: S SInteger -> SBool
    inv S{SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = SInteger
    y SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    1

            -- We're not interested in termination/goal for this problem, so just pass trivial values
            goal :: S SInteger -> (SBool, SBool)
            goal :: S SInteger -> (SBool, SBool)
    goal S SInteger
    _ = (SBool
    sTrue, SBool
    sTrue)

    -- | The first program, coded as a transition relation:
    pgm1 :: S SInteger -> [S SInteger]
    pgm1 :: S SInteger -> [S SInteger]
    pgm1 S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = [S{x :: SInteger
    x = SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1, y :: SInteger
    y = SInteger
    ySInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    x}]

    -- | The second program, coded as a transition relation:
    pgm2 :: S SInteger -> [S SInteger]
    pgm2 :: S SInteger -> [S SInteger]
    pgm2 S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = [S{x :: SInteger
    x = SInteger
    xSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    y, y :: SInteger
    y = SInteger
    ySInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    x}]

    -- * Examples

    -- | Example 1: First program, with no strengthenings. We have:
    --
    -- >>> ex1
    -- Failed while establishing consecution.
    -- Counter-example to inductiveness:
    --   S {x = -1, y = 1}
    ex1 :: IO (InductionResult (S Integer))
    ex1 :: IO (InductionResult (S Integer))
    ex1 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm1 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = []

    -- | Example 2: First program, strengthened with @x >= 0@. We have:
    --
    -- >>> ex2
    -- Q.E.D.
    ex2 :: IO (InductionResult (S Integer))
    ex2 :: IO (InductionResult (S Integer))
    ex2 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm1 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = [(String
    "x >= 0", \S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x} -> SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0)]

    -- | Example 3: Second program, with no strengthenings. We have:
    --
    -- >>> ex3
    -- Failed while establishing consecution.
    -- Counter-example to inductiveness:
    --   S {x = -1, y = 1}
    ex3 :: IO (InductionResult (S Integer))
    ex3 :: IO (InductionResult (S Integer))
    ex3 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm2 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = []

    -- | Example 4: Second program, strengthened with @x >= 0@. We have:
    --
    -- >>> ex4
    -- Failed while establishing consecution for strengthening "x >= 0".
    -- Counter-example to inductiveness:
    --   S {x = 0, y = -1}
    ex4 :: IO (InductionResult (S Integer))
    ex4 :: IO (InductionResult (S Integer))
    ex4 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm2 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = [(String
    "x >= 0", \S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x} -> SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0)]

    -- | Example 5: Second program, strengthened with @x >= 0@ and @y >= 1@ separately. We have:
    --
    -- >>> ex5
    -- Failed while establishing consecution for strengthening "x >= 0".
    -- Counter-example to inductiveness:
    --   S {x = 0, y = -1}
    --
    -- Note how this was sufficient in 'ex2' to establish the invariant for the first
    -- program, but fails for the second.
    ex5 :: IO (InductionResult (S Integer))
    ex5 :: IO (InductionResult (S Integer))
    ex5 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm2 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = [ (String
    "x >= 0", \S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x} -> SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0)
                             , (String
    "y >= 1", \S{SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} -> SInteger
    y SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    1)
                             ]

    -- | Example 6: Second program, strengthened with @x >= 0 \/\\ y >= 1@ simultaneously. We have:
    --
    -- >>> ex6
    -- Q.E.D.
    --
    -- Compare this to 'ex5'. As pointed out by Bradley, this shows that
    -- /a conjunction of assertions can be inductive when none of its components, on its own, is inductive./
    -- It remains an art to find proper loop invariants, though the science is improving!
    ex6 :: IO (InductionResult (S Integer))
    ex6 :: IO (InductionResult (S Integer))
    ex6 = (S SInteger -> [S SInteger])
    -> [(String, S SInteger -> SBool)]
    -> IO (InductionResult (S Integer))
    problem S SInteger -> [S SInteger]
    pgm2 [(String, S SInteger -> SBool)]
    strengthenings
      where strengthenings :: [(String, S SInteger -> SBool)]
            strengthenings :: [(String, S SInteger -> SBool)]
    strengthenings = [(String
    "x >= 0 /\\ y >= 1", \S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} -> SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0 SBool -> SBool -> SBool
    .&& SInteger
    y SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    1)]