-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.KDKernel
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Kernel of the KnuckleDragger prover API.
-----------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE NamedFieldPuns       #-}
{-# LANGUAGE ScopedTypeVariables  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KDKernel (
         Proposition,  Proof
       , axiom
       , lemma,        lemmaWith,   lemmaGen
       , theorem,      theoremWith
       , Induction(..)
       , sorry
       ) where

import Control.Monad.Trans  (liftIO)
import Control.Monad.Reader (ask)

import Data.List (intercalate, sort, nub)

import Data.SBV
import Data.SBV.Core.Data (Constraint)

import Data.SBV.Tools.KDUtils

import qualified Data.SBV.List as SL

-- | A proposition is something SBV is capable of proving/disproving. We capture this
-- with a set of constraints. This type might look scary, but for the most part you
-- can ignore it and treat it as anything you can pass to 'prove' or 'sat' in SBV.
type Proposition a = ( QuantifiedBool a
                     , QNot a
                     , Skolemize (NegatesTo a)
                     , Satisfiable (Symbolic (SkolemsTo (NegatesTo a)))
                     , Constraint  Symbolic  (SkolemsTo (NegatesTo a))
                     )

-- | Keeping track of where the sorry originates from. Used in displaying dependencies.
data RootOfTrust = None        -- ^ Trusts nothing (aside from SBV, underlying solver etc.)
                 | Self        -- ^ Trusts itself, i.e., established by a call to sorry
                 | Prop String -- ^ Trusts a parent that itself trusts something else. Note the name here is the
                               --   name of the proposition itself, not the parent that's trusted.

-- | Proof for a property. This type is left abstract, i.e., the only way to create on is via a
-- call to 'lemma'/'theorem' etc., ensuring soundness. (Note that the trusted-code base here
-- is still large: The underlying solver, SBV, and KnuckleDragger kernel itself. But this
-- mechanism ensures we can't create proven things out of thin air, following the standard LCF
-- methodology.)
data Proof = Proof { Proof -> RootOfTrust
rootOfTrust :: RootOfTrust -- ^ Root of trust, described above.
                   , Proof -> Bool
isUserAxiom :: Bool        -- ^ Was this an axiom given by the user?
                   , Proof -> SBV Bool
getProof    :: SBool       -- ^ Get the underlying boolean
                   , Proof -> String
proofName   :: String      -- ^ User given name
                   }

-- | Show instance for 'Proof'
instance Show Proof where
  show :: Proof -> String
show Proof{RootOfTrust
rootOfTrust :: Proof -> RootOfTrust
rootOfTrust :: RootOfTrust
rootOfTrust, Bool
isUserAxiom :: Proof -> Bool
isUserAxiom :: Bool
isUserAxiom, String
proofName :: Proof -> String
proofName :: String
proofName} = Char
'[' Char -> ShowS
forall a. a -> [a] -> [a]
: String
tag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
proofName
     where tag :: String
tag | Bool
isUserAxiom = String
"Axiom"
               | Bool
True        = case RootOfTrust
rootOfTrust of
                                 RootOfTrust
None   -> String
"Proven"
                                 RootOfTrust
Self   -> String
"Sorry"
                                 Prop String
s -> String
"Modulo: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

-- | Accept the given definition as a fact. Usually used to introduce definitial axioms,
-- giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions,
-- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to
-- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.
axiom :: Proposition a => String -> a -> KD Proof
axiom :: forall a. Proposition a => String -> a -> KD Proof
axiom String
nm a
p = do Bool -> String -> [String] -> KD Int
start Bool
False String
"Axiom" [String
nm] KD Int -> (Int -> KD ()) -> KD ()
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Int -> KD ()
finish String
"Axiom."

                Proof -> KD Proof
forall a. a -> KD a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> a -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
nm a
p) { isUserAxiom = True }

-- | Internal axiom generator; so we can keep truck of KnuckleDrugger's trusted axioms, vs. user given axioms.
-- Not exported.
internalAxiom :: Proposition a => String -> a -> Proof
internalAxiom :: forall a. Proposition a => String -> a -> Proof
internalAxiom String
nm a
p = Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
None
                           , isUserAxiom :: Bool
isUserAxiom = Bool
False
                           , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
p)
                           , proofName :: String
proofName   = String
nm
                           }

-- | A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver
-- cannot deal with, or if we want to postpone the proof for the time being. KnuckleDragger will keep
-- track of the uses of 'sorry' and will print them appropriately while printing proofs.
sorry :: Proof
sorry :: Proof
sorry = Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
Self
              , isUserAxiom :: Bool
isUserAxiom = Bool
False
              , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
"sorry" ((Forall Any Bool -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool Forall Any Bool -> SBV Bool
forall {nm :: Symbol}. Forall nm Bool -> SBV Bool
p)
              , proofName :: String
proofName   = String
"sorry"
              }
  where -- ideally, I'd rather just use 
        --   p = sFalse
        -- but then SBV constant folds the boolean, and the generated script
        -- doesn't contain the actual contents, as SBV determines unsatisfiability
        -- itself. By using the following proposition (which is easy for the backend
        -- solver to determine as false, we avoid the constant folding.
        p :: Forall nm Bool -> SBV Bool
p (Forall (SBV Bool
x :: SBool)) = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
"SORRY: KnuckleDragger, proof uses \"sorry\"" SBV Bool
x

-- | Helper to generate lemma/theorem statements.
lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen :: forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen cfg :: SMTConfig
cfg@SMTConfig{Bool
verbose :: Bool
verbose :: SMTConfig -> Bool
verbose} String
what [String]
nms a
inputProp [Proof]
by = do
    tab <- Bool -> String -> [String] -> KD Int
start Bool
verbose String
what [String]
nms

    let nm = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
nms

        -- What to do if all goes well
        good = do String -> Int -> KD ()
finish (String
"Q.E.D." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
modulo) Int
tab
                  Proof -> KD Proof
forall a. a -> KD a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
ros
                             , isUserAxiom :: Bool
isUserAxiom = Bool
False
                             , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
inputProp)
                             , proofName :: String
proofName   = String
nm
                             }

          where parentRoots :: [RootOfTrust]
parentRoots = (Proof -> RootOfTrust) -> [Proof] -> [RootOfTrust]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> RootOfTrust
rootOfTrust [Proof]
by
                hasSelf :: Bool
hasSelf     = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | RootOfTrust
Self <- [RootOfTrust]
parentRoots]
                depNames :: [String]
depNames    = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort [String
p | Prop String
p <- [RootOfTrust]
parentRoots]

                -- What's the root-of-trust for this node?
                -- If there are no "sorry" parents, and no parent nodes
                -- that are marked with a root of trust, then we don't have it either.
                -- Otherwise, mark it accordingly.
                (RootOfTrust
ros, String
modulo)
                   | Bool -> Bool
not Bool
hasSelf Bool -> Bool -> Bool
&& [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
depNames = (RootOfTrust
None,    String
"")
                   | Bool
True                         = (String -> RootOfTrust
Prop String
nm, String
" [Modulo: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
why String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]")
                   where why :: String
why | Bool
hasSelf = String
"sorry"
                             | Bool
True    = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
depNames

        -- What to do if the proof fails
        cex  = IO a -> KD a
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> KD a) -> IO a -> KD a
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."

                           -- When trying to get a counter-example, only include in the
                           -- implication those facts that are user-given axioms. This
                           -- way our counter-example will be more likely to be relevant
                           -- to the proposition we're currently proving. (Hopefully.)
                           -- Remember that we first have to negate, and then skolemize!
                           SatResult res <- SMTConfig -> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall a. Satisfiable a => SMTConfig -> a -> IO SatResult
satWith SMTConfig
cfg (Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult)
-> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
                                               (SBV Bool -> SymbolicT IO ()) -> [SBV Bool] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV Bool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain [SBV Bool
getProof | Proof{Bool
isUserAxiom :: Proof -> Bool
isUserAxiom :: Bool
isUserAxiom, SBV Bool
getProof :: Proof -> SBV Bool
getProof :: SBV Bool
getProof} <- [Proof]
by, Bool
isUserAxiom] :: Symbolic ()
                                               SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a)))
-> SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a b. (a -> b) -> a -> b
$ NegatesTo a -> SkolemsTo (NegatesTo a)
forall a.
(Skolemize a, Constraint Symbolic (SkolemsTo a), Skolemize a) =>
a -> SkolemsTo a
skolemize (a -> NegatesTo a
forall a. QNot a => a -> NegatesTo a
qNot a
inputProp)

                           print $ ThmResult res
                           error "Failed"

        -- bailing out
        failed a
r = IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
                               a -> IO ()
forall a. Show a => a -> IO ()
print a
r
                               String -> IO a
forall a. HasCallStack => String -> a
error String
"Failed"

    pRes <- liftIO $ proveWith cfg $ do
                mapM_ (constrain . getProof) by :: Symbolic ()
                pure $ skolemize (quantifiedBool inputProp)

    case pRes of
      ThmResult Unsatisfiable{} -> KD Proof
good
      ThmResult Satisfiable{}   -> KD Proof
forall {a}. KD a
cex
      ThmResult DeltaSat{}      -> KD Proof
forall {a}. KD a
cex
      ThmResult SatExtField{}   -> KD Proof
forall {a}. KD a
cex
      ThmResult Unknown{}       -> ThmResult -> KD Proof
forall {m :: * -> *} {a} {a}. (MonadIO m, Show a) => a -> m a
failed ThmResult
pRes
      ThmResult ProofError{}    -> ThmResult -> KD Proof
forall {m :: * -> *} {a} {a}. (MonadIO m, Show a) => a -> m a
failed ThmResult
pRes

-- | Prove a given statement, using auxiliaries as helpers. Using the default solver.
lemma :: Proposition a => String -> a -> [Proof] -> KD Proof
lemma :: forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
nm a
f [Proof]
by = do cfg <- KD SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
                   lemmaWith cfg nm f by

-- | Prove a given statement, using auxiliaries as helpers. Using the given solver.
lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith SMTConfig
cfg String
nm = SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Lemma" [String
nm]

-- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemma', except for the name, using the default solver.
theorem :: Proposition a => String -> a -> [Proof] -> KD Proof
theorem :: forall a. Proposition a => String -> a -> [Proof] -> KD Proof
theorem String
nm a
f [Proof]
by = do cfg <- KD SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
                     theoremWith cfg nm f by

-- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name.
theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith SMTConfig
cfg String
nm = SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Theorem" [String
nm]

-- | Given a predicate, return an induction principle for it. Typically, we only have one viable
-- induction principle for a given type, but we allow for alternative ones.
class Induction a where
  induct     :: a -> Proof
  inductAlt1 :: a -> Proof
  inductAlt2 :: a -> Proof

  -- The second and third principles are the same as first by default, unless we provide them explicitly.
  inductAlt1 = a -> Proof
forall a. Induction a => a -> Proof
induct
  inductAlt2 = a -> Proof
forall a. Induction a => a -> Proof
induct

-- | Induction over SInteger. We provide various induction principles here: The first one
-- is over naturals, will only prove predicates that explicitly restrict the argument to >= 0.
-- The second and third ones are induction over the entire range of integers, two different
-- principles that might work better for different problems.
instance Induction (SInteger -> SBool) where

   -- | Induction over naturals. Will prove predicates of the form @\n -> n >= 0 .=> predicate n@.
   induct :: (SInteger -> SBV Bool) -> Proof
induct SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Nat.induct" SBV Bool
principle
      where qb :: (Forall Any Integer -> SBV Bool) -> SBV Bool
qb = (Forall Any Integer -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool

            principle :: SBV Bool
principle =       SInteger -> SBV Bool
p SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any Integer -> SBV Bool) -> SBV Bool
qb (\(Forall SInteger
n) -> (SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.&& SInteger -> SBV Bool
p SInteger
n) SBV Bool -> SBV Bool -> SBV Bool
.=> SInteger -> SBV Bool
p (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                      SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any Integer -> SBV Bool) -> SBV Bool
qb -----------------------------------------------------------
                                        (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.=> SInteger -> SBV Bool
p SInteger
n)


   -- | Induction over integers, using the strategy that @P(n)@ is equivalent to @P(n+1)@
   -- (i.e., not just @P(n) => P(n+1)@), thus covering the entire range.
   inductAlt1 :: (SInteger -> SBV Bool) -> Proof
inductAlt1 SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Integer.inductAlt1" SBV Bool
principle
     where qb :: (Forall Any Integer -> SBV Bool) -> SBV Bool
qb = (Forall Any Integer -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool

           principle :: SBV Bool
principle =           SInteger -> SBV Bool
p SInteger
0
                             SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any Integer -> SBV Bool) -> SBV Bool
qb (\(Forall SInteger
i) -> SInteger -> SBV Bool
p SInteger
i SBV Bool -> SBV Bool -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
.== SInteger -> SBV Bool
p (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                     SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any Integer -> SBV Bool) -> SBV Bool
qb -----------------------------------------
                                 (\(Forall SInteger
i) -> SInteger -> SBV Bool
p SInteger
i)

   -- | Induction over integers, using the strategy that @P(n) => P(n+1)@ and @P(n) => P(n-1)@.
   inductAlt2 :: (SInteger -> SBV Bool) -> Proof
inductAlt2 SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Integer.inductAlt2" SBV Bool
principle
     where qb :: (Forall Any Integer -> SBV Bool) -> SBV Bool
qb = (Forall Any Integer -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool

           principle :: SBV Bool
principle =           SInteger -> SBV Bool
p SInteger
0
                             SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any Integer -> SBV Bool) -> SBV Bool
qb (\(Forall SInteger
i) -> SInteger -> SBV Bool
p SInteger
i SBV Bool -> SBV Bool -> SBV Bool
.=> SInteger -> SBV Bool
p (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SBV Bool -> SBV Bool -> SBV Bool
.&& SInteger -> SBV Bool
p (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1))
                     SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any Integer -> SBV Bool) -> SBV Bool
qb -----------------------------------------------------
                                 (\(Forall SInteger
i) -> SInteger -> SBV Bool
p SInteger
i)

-- | Induction over two argument predicates, with the last argument SInteger.
instance SymVal a => Induction (SBV a -> SInteger -> SBool) where
  induct :: (SBV a -> SInteger -> SBV Bool) -> Proof
induct SBV a -> SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Nat.induct2" SBV Bool
principle
     where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

           principle :: SBV Bool
principle =           (Forall Any a -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) -> SBV a -> SInteger -> SBV Bool
p SBV a
a SInteger
0)
                             SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a -> Forall Any Integer -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SInteger
n) -> (SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.&& SBV a -> SInteger -> SBV Bool
p SBV a
a SInteger
n) SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SInteger -> SBV Bool
p SBV a
a (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                     SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a -> Forall Any Integer -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb ----------------------------------------------------------------------
                                 (\(Forall SBV a
a) (Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SInteger -> SBV Bool
p SBV a
a SInteger
n)

-- | Induction over three argument predicates, with last argument SInteger.
instance (SymVal a, SymVal b) => Induction (SBV a -> SBV b -> SInteger -> SBool) where
  induct :: (SBV a -> SBV b -> SInteger -> SBV Bool) -> Proof
induct SBV a -> SBV b -> SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Nat.induct3" SBV Bool
principle
     where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

           principle :: SBV Bool
principle =           (Forall Any a -> Forall Any b -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) -> SBV a -> SBV b -> SInteger -> SBV Bool
p SBV a
a SBV b
b SInteger
0)
                             SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a -> Forall Any b -> Forall Any Integer -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SInteger
n) -> (SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.&& SBV a -> SBV b -> SInteger -> SBV Bool
p SBV a
a SBV b
b SInteger
n) SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SInteger -> SBV Bool
p SBV a
a SBV b
b (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                     SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a -> Forall Any b -> Forall Any Integer -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb -------------------------------------------------------------------------------------
                                 (\(Forall SBV a
a) (Forall SBV b
b) (Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SInteger -> SBV Bool
p SBV a
a SBV b
b SInteger
n)

-- | Induction over four argument predicates, with last argument SInteger.
instance (SymVal a, SymVal b, SymVal c) => Induction (SBV a -> SBV b -> SBV c -> SInteger -> SBool) where
  induct :: (SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool) -> Proof
induct SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"Nat.induct4" SBV Bool
principle
     where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

           principle :: SBV Bool
principle =           (Forall Any a -> Forall Any b -> Forall Any c -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) -> SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool
p SBV a
a SBV b
b SBV c
c SInteger
0)
                             SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a
 -> Forall Any b -> Forall Any c -> Forall Any Integer -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) (Forall SInteger
n) -> (SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.&& SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool
p SBV a
a SBV b
b SBV c
c SInteger
n) SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool
p SBV a
a SBV b
b SBV c
c (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1))
                     SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a
 -> Forall Any b -> Forall Any c -> Forall Any Integer -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb ----------------------------------------------------------------------------------------------------
                                 (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) (Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBV Bool
forall a. OrdSymbolic a => a -> a -> SBV Bool
.>= SInteger
0 SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SBV c -> SInteger -> SBV Bool
p SBV a
a SBV b
b SBV c
c SInteger
n)


-- | Induction over lists
instance SymVal a => Induction (SList a -> SBool) where
  induct :: (SList a -> SBV Bool) -> Proof
induct SList a -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"List(a).induct" SBV Bool
principle
    where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

          principle :: SBV Bool
principle =           SList a -> SBV Bool
p SList a
forall a. SymVal a => SList a
SL.nil
                            SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a -> Forall Any [a] -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
x) (Forall SList a
xs) -> SList a -> SBV Bool
p SList a
xs SBV Bool -> SBV Bool -> SBV Bool
.=> SList a -> SBV Bool
p (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SList a
xs))
                    SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any [a] -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb -------------------------------------------------------------
                                (\(Forall SList a
xs) -> SList a -> SBV Bool
p SList a
xs)

-- | Induction over two argument predicates, with last argument a list.
instance (SymVal a, SymVal e) => Induction (SBV a -> SList e -> SBool) where
  induct :: (SBV a -> SList e -> SBV Bool) -> Proof
induct SBV a -> SList e -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"List(a).induct2" SBV Bool
principle
    where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

          principle :: SBV Bool
principle =           (Forall Any a -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) -> SBV a -> SList e -> SBV Bool
p SBV a
a SList e
forall a. SymVal a => SList a
SL.nil)
                            SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a -> Forall Any e -> Forall Any [e] -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV e
e) (Forall SList e
es) -> SBV a -> SList e -> SBV Bool
p SBV a
a SList e
es SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SList e -> SBV Bool
p SBV a
a (SBV e
e SBV e -> SList e -> SList e
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SList e
es))
                    SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a -> Forall Any [e] -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb ------------------------------------------------------------------------------
                                (\(Forall SBV a
a) (Forall SList e
es) -> SBV a -> SList e -> SBV Bool
p SBV a
a SList e
es)

-- | Induction over three argument predicates, with last argument a list.
instance (SymVal a, SymVal b, SymVal e) => Induction (SBV a -> SBV b -> SList e -> SBool) where
  induct :: (SBV a -> SBV b -> SList e -> SBV Bool) -> Proof
induct SBV a -> SBV b -> SList e -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"List(a).induct3" SBV Bool
principle
    where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

          principle :: SBV Bool
principle =           (Forall Any a -> Forall Any b -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) -> SBV a -> SBV b -> SList e -> SBV Bool
p SBV a
a SBV b
b SList e
forall a. SymVal a => SList a
SL.nil)
                            SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a
 -> Forall Any b -> Forall Any e -> Forall Any [e] -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV e
e) (Forall SList e
es) -> SBV a -> SBV b -> SList e -> SBV Bool
p SBV a
a SBV b
b SList e
es SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SList e -> SBV Bool
p SBV a
a SBV b
b (SBV e
e SBV e -> SList e -> SList e
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SList e
es))
                    SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a -> Forall Any b -> Forall Any [e] -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb -------------------------------------------------------------------------------------------
                                (\(Forall SBV a
a) (Forall SBV b
b) (Forall SList e
xs) -> SBV a -> SBV b -> SList e -> SBV Bool
p SBV a
a SBV b
b SList e
xs)

-- | Induction over four argument predicates, with last argument a list.
instance (SymVal a, SymVal b, SymVal c, SymVal e) => Induction (SBV a -> SBV b -> SBV c -> SList e -> SBool) where
  induct :: (SBV a -> SBV b -> SBV c -> SList e -> SBV Bool) -> Proof
induct SBV a -> SBV b -> SBV c -> SList e -> SBV Bool
p = String -> SBV Bool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"List(a).induct4" SBV Bool
principle
    where qb :: a -> SBV Bool
qb a
a = a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
a

          principle :: SBV Bool
principle =           (Forall Any a -> Forall Any b -> Forall Any c -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) -> SBV a -> SBV b -> SBV c -> SList e -> SBV Bool
p SBV a
a SBV b
b SBV c
c SList e
forall a. SymVal a => SList a
SL.nil)
                            SBV Bool -> SBV Bool -> SBV Bool
.&& (Forall Any a
 -> Forall Any b
 -> Forall Any c
 -> Forall Any e
 -> Forall Any [e]
 -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) (Forall SBV e
e) (Forall SList e
es) -> SBV a -> SBV b -> SBV c -> SList e -> SBV Bool
p SBV a
a SBV b
b SBV c
c SList e
es SBV Bool -> SBV Bool -> SBV Bool
.=> SBV a -> SBV b -> SBV c -> SList e -> SBV Bool
p SBV a
a SBV b
b SBV c
c (SBV e
e SBV e -> SList e -> SList e
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SList e
es))
                    SBV Bool -> SBV Bool -> SBV Bool
.=> (Forall Any a
 -> Forall Any b -> Forall Any c -> Forall Any [e] -> SBV Bool)
-> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
qb ----------------------------------------------------------------------------------------------------------
                                (\(Forall SBV a
a) (Forall SBV b
b) (Forall SBV c
c) (Forall SList e
xs) -> SBV a -> SBV b -> SBV c -> SList e -> SBV Bool
p SBV a
a SBV b
b SBV c
c SList e
xs)

{- HLint ignore module "Eta reduce" -}