sbv-14.1: Data/SBV/TP/TP.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.TP.TP
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
-----------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.TP.TP (
Proposition, Proof, proofOf, assumptionFromProof, Instantiatable(..), Inst(..)
, rootOfTrust, RootOfTrust(..), ProofTree(..), showProofTree, showProofTreeHTML
, axiom
, lemma, lemmaWith
, inductiveLemma, inductiveLemmaWith
, calc, calcWith
, induct, inductWith
, sInduct, sInductWith
, sorry
, TP, runTP, runTPWith, tpQuiet, tpStats, tpAsms
, whenDryRun, unlessDryRun
, measureLemma, measureLemmaWith
, (|-), (|->), (⊢), (=:), (≡), (??), (∵), split, split2, cases, (==>), (⟹), qed, trivial, contradiction
, qc, qcWith
, disp
, recall, recallWith
) where
import Data.SBV
import Data.SBV.Core.Model (qSaturateSavingObservables)
import Data.SBV.Core.Data (SBV(..), SVal(..))
import qualified Data.SBV.Core.Symbolic as S (sObserve)
import qualified Data.Text as T
import Data.SBV.Core.Symbolic (rSkipMeasureChecks, rNoTermCheckFunctions)
import Data.SBV.Core.Operations (svEqual)
import Data.SBV.Control hiding (getProof, (|->))
import Data.SBV.TP.Kernel
import Data.SBV.TP.Utils
import qualified Data.SBV.List as SL
import Control.Exception (SomeException)
import Control.Monad (when)
import Control.Monad.Trans (liftIO)
import Data.IORef (readIORef, writeIORef, modifyIORef')
import qualified Data.Set as Set
import Data.Char (isSpace)
import Data.List (intercalate, isPrefixOf, isSuffixOf)
import Data.Maybe (catMaybes, maybeToList)
import Data.Proxy
import Data.Kind (Type)
import GHC.TypeLits (KnownSymbol, symbolVal, Symbol)
import Data.SBV.Utils.TDiff
import Data.Dynamic
import qualified Test.QuickCheck as QC
import Test.QuickCheck (quickCheckWithResult)
-- | Captures the steps for a calculationa proof
data CalcStrategy = CalcStrategy { calcIntros :: SBool
, calcProofTree :: TPProof
, calcQCInstance :: [Int] -> Symbolic SBool
}
-- | Saturatable things in steps
proofTreeSaturatables :: TPProof -> [SBool]
proofTreeSaturatables = go
where go (ProofEnd b hs ) = b : concatMap getH hs
go (ProofStep a hs r) = a : concatMap getH hs ++ go r
go (ProofBranch (_ :: Bool) (_ :: [String]) ps) = concat [b : go p | (b, p) <- ps]
getH (HelperProof p) = [getObjProof p]
getH (HelperAssum b) = [b]
getH HelperQC{} = []
getH HelperString{} = []
getH (HelperDisp _ v) = [SBV (v `svEqual` v)]
-- | Things that are inside calc-strategy that we have to saturate
getCalcStrategySaturatables :: CalcStrategy -> [SBool]
getCalcStrategySaturatables (CalcStrategy calcIntros calcProofTree _calcQCInstance) = calcIntros : proofTreeSaturatables calcProofTree
-- | Use an injective type family to allow for curried use of calc and strong induction steps.
type family StepArgs a t = result | result -> t where
StepArgs SBool t = (SBool, TPProofRaw (SBV t))
StepArgs (Forall na a -> SBool) t = (SBV a -> (SBool, TPProofRaw (SBV t)))
StepArgs (Forall na a -> Forall nb b -> SBool) t = (SBV a -> SBV b -> (SBool, TPProofRaw (SBV t)))
StepArgs (Forall na a -> Forall nb b -> Forall nc c -> SBool) t = (SBV a -> SBV b -> SBV c -> (SBool, TPProofRaw (SBV t)))
StepArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, TPProofRaw (SBV t)))
StepArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, TPProofRaw (SBV t)))
-- | Use an injective type family to allow for curried use of measures in strong induction instances
type family MeasureArgs a t = result | result -> t where
MeasureArgs SBool t = ( SBV t)
MeasureArgs (Forall na a -> SBool) t = (SBV a -> SBV t)
MeasureArgs (Forall na a -> Forall nb b -> SBool) t = (SBV a -> SBV b -> SBV t)
MeasureArgs (Forall na a -> Forall nb b -> Forall nc c -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV t)
MeasureArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> SBV t)
MeasureArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV t)
-- | Use an injective type family to allow for curried use of regular induction steps. The first argument is the inductive arg that comes separately,
-- and hence is not used in the right-hand side of the equation.
type family IStepArgs a t = result | result -> t where
IStepArgs ( Forall nx x -> SBool) t = (SBool, TPProofRaw (SBV t))
IStepArgs ( Forall nx x -> Forall na a -> SBool) t = (SBV a -> (SBool, TPProofRaw (SBV t)))
IStepArgs ( Forall nx x -> Forall na a -> Forall nb b -> SBool) t = (SBV a -> SBV b -> (SBool, TPProofRaw (SBV t)))
IStepArgs ( Forall nx x -> Forall na a -> Forall nb b -> Forall nc c -> SBool) t = (SBV a -> SBV b -> SBV c -> (SBool, TPProofRaw (SBV t)))
IStepArgs ( Forall nx x -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, TPProofRaw (SBV t)))
IStepArgs ( Forall nx x -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, TPProofRaw (SBV t)))
IStepArgs ((Forall nx x, Forall ny y) -> SBool) t = (SBool, TPProofRaw (SBV t))
IStepArgs ((Forall nx x, Forall ny y) -> Forall na a -> SBool) t = (SBV a -> (SBool, TPProofRaw (SBV t)))
IStepArgs ((Forall nx x, Forall ny y) -> Forall na a -> Forall nb b -> SBool) t = (SBV a -> SBV b -> (SBool, TPProofRaw (SBV t)))
IStepArgs ((Forall nx x, Forall ny y) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) t = (SBV a -> SBV b -> SBV c -> (SBool, TPProofRaw (SBV t)))
IStepArgs ((Forall nx x, Forall ny y) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, TPProofRaw (SBV t)))
IStepArgs ((Forall nx x, Forall ny y) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) t = (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, TPProofRaw (SBV t)))
-- | A class for doing equational reasoning style calculational proofs. Use 'calc' to prove a given theorem
-- as a sequence of equalities, each step following from the previous.
class Calc a where
-- | Prove a property via a series of equality steps, using the default solver.
-- Let @H@ be a list of already established lemmas. Let @P@ be a property we wanted to prove, named @name@.
-- Consider a call of the form @calc name P (cond, [A, B, C, D]) H@. Note that @H@ is
-- a list of already proven facts, ensured by the type signature. We proceed as follows:
--
-- * Prove: @(H && cond) -> (A == B)@
-- * Prove: @(H && cond && A == B) -> (B == C)@
-- * Prove: @(H && cond && A == B && B == C) -> (C == D)@
-- * Prove: @(H && (cond -> (A == B && B == C && C == D))) -> P@
-- * If all of the above steps succeed, conclude @P@.
--
-- cond acts as the context. Typically, if you are trying to prove @Y -> Z@, then you want cond to be Y.
-- (This is similar to @intros@ commands in theorem provers.)
--
-- So, calc-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning in the case of
-- non-boolean steps.
--
-- If there are no helpers given (i.e., if @H@ is empty), then this call is equivalent to 'lemmaWith'.
calc :: (Proposition a, SymVal t, EqSymbolic (SBV t)) => String -> a -> StepArgs a t -> TP (Proof a)
-- | Prove a property via a series of equality steps, using the given solver.
calcWith :: (Proposition a, SymVal t, EqSymbolic (SBV t)) => SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
-- | Internal, shouldn't be needed outside the library
{-# MINIMAL calcSteps #-}
calcSteps :: (SymVal t, EqSymbolic (SBV t)) => a -> StepArgs a t -> Symbolic (SBool, CalcStrategy)
calc nm p steps = getTPConfig >>= \cfg -> calcWith cfg nm p steps
calcWith cfg nm p steps = getTPConfig >>= \cfg' -> calcGeneric (tpMergeCfg cfg cfg') nm p steps
calcGeneric :: (SymVal t, EqSymbolic (SBV t), Proposition a) => SMTConfig -> String -> a -> StepArgs a t -> TP (Proof a)
calcGeneric cfg nm result steps = do
cached <- lookupProofCache result
case cached of
Just prf -> returnCachedProof cfg nm prf
Nothing -> do
tpSt <- getTPState
u <- tpGetNextUnique
(_, CalcStrategy {calcQCInstance}) <- liftIO $ runSMTWith cfg (calcSteps result steps)
proof <- liftIO $ runSMTWith cfg $ do
qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out
let header = "Lemma: " ++ nm
message cfg $ header ++ "\n"
liftIO $ do isDry <- readIORef (dryRun tpSt)
when isDry $ modifyIORef' (maxRibbon tpSt) (max (length header))
(calcGoal, strategy@CalcStrategy {calcIntros, calcProofTree}) <- calcSteps result steps
-- Collect all subterms and saturate them
mapM_ qSaturateSavingObservables $ getCalcStrategySaturatables strategy
-- Run measure checks for any newly encountered recursive functions
st <- symbolicEnv
liftIO $ do writeIORef (rSkipMeasureChecks st) True
checkNewMeasures cfg st tpSt
query $ proveProofTree cfg tpSt nm (result, calcGoal) calcIntros calcProofTree u calcQCInstance
addToProofCache result (proofOf proof)
pure proof
-- | In the proof tree, what's the next node label?
nextProofStep :: [Int] -> [Int]
nextProofStep bs = case reverse bs of
i : rs -> reverse $ i + 1 : rs
[] -> [1]
-- | Prove the proof tree. The arguments are:
--
-- result : The ultimate goal we want to prove. Note that this is a general proposition, and we don't actually prove it. See the next param.
-- resultBool : The instance of result that, if we prove it, establishes the result itself
-- initialHypotheses: Hypotheses (conjuncted)
-- calcProofTree : A tree of steps, which give rise to a bunch of equalities
--
-- Note that we do not check the resultBool is the result itself just "instantiated" appropriately. This is the contract with the caller who
-- has to establish that by whatever means it chooses to do so.
--
-- The final proof we have has the following form:
--
-- - For each "link" in the proofTree, prove that intros .=> link
-- - The above will give us a bunch of results, for each leaf node in the tree.
-- - Then prove: (intros .=> sAnd results) .=> resultBool
-- - Then conclude result, based on what assumption that proving resultBool establishes result
--
-- NB. This function needs to be in "sync" with qcRun below for obvious reasons. So, any changes there
-- make it here too!
proveProofTree :: Proposition a
=> SMTConfig
-> TPState
-> String -- ^ the name of the top result
-> (a, SBool) -- ^ goal: as a proposition and as a boolean
-> SBool -- ^ hypotheses
-> TPProof -- ^ proof tree
-> TPUnique -- ^ unique id
-> ([Int] -> Symbolic SBool) -- ^ quick-checker
-> Query (Proof a)
proveProofTree cfg tpSt nm (result, resultBool) initialHypotheses calcProofTree uniq quickCheckInstance = do
results <- walk initialHypotheses 1 ([1], calcProofTree)
queryDebug [T.pack nm <> ": Proof end: proving the result:"]
mbStartTime <- getTimeStampIf printStats
st <- symbolicEnv
noTermFns <- liftIO $ readIORef (rNoTermCheckFunctions st)
let ntcDeps = map noTermCheckProof (Set.toList noTermFns)
smtProofStep cfg tpSt "Result" 1
(TPProofStep False nm [] [""])
(Just (initialHypotheses .=> sAnd results))
resultBool [] $ \d ->
do mbElapsed <- getElapsedTime mbStartTime
let allDeps = getDependencies calcProofTree ++ ntcDeps
modulo = concludeModulo (concatMap getHelperProofs (getAllHelpers calcProofTree) ++ ntcDeps)
finishTP cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])
pure $ Proof $ ProofObj { dependencies = allDeps
, isUserAxiom = False
, getObjProof = label nm (quantifiedBool result)
, getProp = toDyn result
, proofName = nm
, uniqId = uniq
, aliases = []
, wasCached = False
}
where SMTConfig{tpOptions = TPOptions{printStats, printAsms}} = cfg
isEnd ProofEnd{} = True
isEnd ProofStep{} = False
isEnd ProofBranch{} = False
-- trim the branch-name, if we're in a deeper level, and we're at the end
trimBN level bn | level > 1, 1 : _ <- reverse bn = init bn
| True = bn
-- If the next step is ending and we're the 1st step; our number can be skipped
mkStepName level bn nextStep | isEnd nextStep = map show (trimBN level bn)
| True = map show bn
walk :: SBool -> Int -> ([Int], TPProof) -> Query [SBool]
-- End of proof, return what it established. If there's a hint associated here, it was probably by mistake; so tell it to the user.
walk intros level (bn, ProofEnd calcResult hs)
| not (null hs)
= error $ unlines [ ""
, "*** Incorrect calc/induct lemma calculations."
, "***"
, "*** The last step in the proof has a helper, which isn't used."
, "***"
, "*** Perhaps the hint is off-by-one in its placement?"
]
| True
= do -- If we're not at the top-level and this is the only step, print it.
-- Otherwise the noise isn't necessary.
when (level > 1) $ case reverse bn of
1 : _ -> liftIO $ do tab <- startTP cfg False "Step" level (TPProofStep False nm [] (map show (init bn)))
finishTP cfg "Q.E.D." (tab, Nothing) []
_ -> pure ()
pure [intros .=> calcResult]
-- Do the branches separately and collect the results. If there's coverage needed, we do it too; which
-- is essentially the assumption here.
walk intros level (bnTop, ProofBranch checkCompleteness hintStrings ps) = do
let bn = trimBN level bnTop
addSuffix xs s = case reverse xs of
l : p -> reverse $ (l ++ s) : p
[] -> [s]
full | checkCompleteness = ""
| True = "full "
stepName = map show bn
_ <- io $ startTP cfg True "Step" level (TPProofStep False nm hintStrings (addSuffix stepName (" (" ++ show (length ps) ++ " way " ++ full ++ "case split)")))
results <- concat <$> sequence [walk (intros .&& branchCond) (level + 1) (bn ++ [i, 1], p) | (i, (branchCond, p)) <- zip [1..] ps]
when checkCompleteness $ smtProofStep cfg tpSt "Step" (level+1)
(TPProofStep False nm [] (stepName ++ ["Completeness"]))
(Just intros)
(sOr (map fst ps))
[]
(\d -> finishTP cfg "Q.E.D." d [])
pure results
-- Do a proof step
walk intros level (bn, ProofStep cur hs p) = do
let finish et helpers d = finishTP cfg ("Q.E.D." ++ concludeModulo helpers) d et
stepName = mkStepName level bn p
disps = [(n, v) | HelperDisp n v <- hs]
-- First prove the assumptions, if there are any. We stay quiet, unless timing is asked for
(quietCfg, finalizer)
| printStats || printAsms = (cfg, finish [] [])
| True = (cfg{tpOptions = (tpOptions cfg) {quiet = True}}, const (pure ()))
as = concatMap getHelperAssumes hs
ss = getHelperText hs
case as of
[] -> pure ()
_ -> smtProofStep quietCfg tpSt "Asms" level
(TPProofStep True nm [] stepName)
(Just intros)
(sAnd as)
disps
finalizer
-- Are we asked to do quick-check?
case [qcArg | HelperQC qcArg <- hs] of
[] -> do -- No quickcheck. Just prove the step
let by = concatMap getHelperProofs hs
smtProofStep cfg tpSt "Step" level
(TPProofStep False nm ss stepName)
(Just (sAnd (intros : as ++ map getObjProof by)))
cur
disps
(finish [] by)
xs -> do let qcArg = last xs -- take the last one if multiple exists. Why not?
hs' = concatMap xform hs ++ [HelperString ("qc: Running " ++ show (QC.maxSuccess qcArg) ++ " tests")]
xform HelperProof{} = []
xform HelperAssum{} = []
xform h@HelperQC{} = [h]
xform h@HelperString{} = [h]
xform HelperDisp{} = []
liftIO $ do
tab <- startTP cfg (verbose cfg) "Step" level (TPProofStep False nm (getHelperText hs') stepName)
isDry <- readIORef (dryRun tpSt)
when isDry $ modifyIORef' (maxRibbon tpSt) (max tab)
(mbT, r) <- timeIf printStats $ quickCheckWithResult qcArg{QC.chatty = verbose cfg} $ quickCheckInstance bn
case mbT of
Nothing -> pure ()
Just t -> updStats tpSt (\s -> s{qcElapsed = qcElapsed s + t})
let err = case r of
QC.Success {} -> Nothing
QC.Failure {QC.output = out} -> Just out
QC.GaveUp {} -> Just $ unlines [ "*** QuickCheck reported \"GaveUp\""
, "***"
, "*** This can happen if you have assumptions in the environment"
, "*** that makes it hard for quick-check to generate valid test values."
, "***"
, "*** See if you can reduce assumptions. If not, please get in touch,"
, "*** to see if we can handle the problem via custom Arbitrary instances."
]
QC.NoExpectedFailure {} -> Just "Expected failure but test passed." -- can't happen
case err of
Just e -> do putStrLn $ "\n*** QuickCheck failed for " ++ intercalate "." (nm : stepName)
putStrLn e
error "Failed"
Nothing -> let extra = [' ' | printStats] -- aligns better when printing stats
in finishTP cfg ("QC OK" ++ extra) (tab, mbT) []
-- Move to next
walk intros level (nextProofStep bn, p)
-- | Helper data-type for calc-step below
data CalcContext a = CalcStart [Helper] -- Haven't started yet
| CalcStep a a [Helper] -- Intermediate step: first value, prev value
-- | Turn a raw (i.e., as written by the user) proof tree to a tree where the successive equalities are made explicit.
mkProofTree :: SymVal a => (SBV a -> SBV a -> c, SBV a -> SBV a -> SBool) -> TPProofRaw (SBV a) -> TPProofGen c [String] SBool
mkProofTree (symTraceEq, symEq) = go (CalcStart [])
where -- End of the proof; tie the begin and end
go step (ProofEnd () hs) = case step of
-- It's tempting to error out if we're at the start and already reached the end
-- This means we're given a sequence of no-steps. While this is useless in the
-- general case, it's quite valid in a case-split; where one of the case-splits
-- might be easy enough for the solver to deduce so the user simply says "just derive it for me."
CalcStart hs' -> ProofEnd sTrue (hs' ++ hs) -- Nothing proven!
CalcStep begin end hs' -> ProofEnd (begin `symEq` end) (hs' ++ hs)
-- Branch: Just push it down. We use the hints from previous step, and pass the current ones down.
go step (ProofBranch c hs ps) = ProofBranch c (getHelperText hs) [(bc, go step' p) | (bc, p) <- ps]
where step' = case step of
CalcStart hs' -> CalcStart (hs' ++ hs)
CalcStep a b hs' -> CalcStep a b (hs' ++ hs)
-- Step:
go (CalcStart hs) (ProofStep cur hs' p) = go (CalcStep cur cur (hs' ++ hs)) p
go (CalcStep first prev hs) (ProofStep cur hs' p) = ProofStep (prev `symTraceEq` cur) hs (go (CalcStep first cur hs') p)
-- | Turn a sequence of steps into a chain of equalities
mkCalcSteps :: SymVal a => (SBool, TPProofRaw (SBV a)) -> ([Int] -> Symbolic SBool) -> Symbolic CalcStrategy
mkCalcSteps (intros, tpp) qcInstance = do
pure $ CalcStrategy { calcIntros = intros
, calcProofTree = mkProofTree ((.===), (.===)) tpp
, calcQCInstance = qcInstance
}
-- | Given initial hypothesis, and a raw proof tree, build the quick-check walk over this tree for the step that's marked as such.
qcRun :: SymVal a => [Int] -> (SBool, TPProofRaw (SBV a)) -> Symbolic SBool
qcRun checkedLabel (intros, tpp) = do
results <- runTree sTrue 1 ([1], mkProofTree (\a b -> (a, b, a .=== b), (.==)) tpp)
case [b | (l, b) <- results, l == checkedLabel] of
[(caseCond, b)] -> do constrain $ intros .&& caseCond
pure b
[] -> notFound
_ -> die "Hit the label multiple times."
where die why = error $ unlines [ ""
, "*** Data.SBV.patch: Impossible happened."
, "***"
, "*** " ++ why
, "***"
, "*** While trying to quickcheck at level " ++ show checkedLabel
, "*** Please report this as a bug!"
]
-- It is possible that we may not find the node. Why? Because it might be under a case-split (ite essentially)
-- and the random choices we made before-hand may just not get us there. Sigh. So, the right thing to do is
-- to just say "we're good." But this can also indicate a bug in our code. Oh well, we'll ignore it.
notFound = pure sTrue
-- "run" the tree, and if we hit the correct label return the result.
-- This needs to be in "sync" with proveProofTree for obvious reasons. So, any changes there
-- make it here too!
runTree :: SymVal a => SBool -> Int -> ([Int], TPProofGen (SBV a, SBV a, SBool) [String] SBool) -> Symbolic [([Int], (SBool, SBool))]
runTree _ _ (_, ProofEnd{}) = pure []
runTree caseCond level (bn, ProofBranch _ _ ps) = concat <$> sequence [runTree (caseCond .&& branchCond) (level + 1) (bn ++ [i, 1], p)
| (i, (branchCond, p)) <- zip [1..] ps
]
runTree caseCond level (bn, ProofStep (lhs, rhs, cur) hs p) = do rest <- runTree caseCond level (nextProofStep bn, p)
when (bn == checkedLabel) $ do
sObserve "lhs" lhs
sObserve "rhs" rhs
mapM_ (uncurry S.sObserve) [(n, v) | HelperDisp n v <- hs]
pure $ (bn, (caseCond, cur)) : rest
-- | Chaining lemmas that depend on no extra variables
instance Calc SBool where
calcSteps result steps = (result,) <$> mkCalcSteps steps (`qcRun` steps)
-- | Chaining lemmas that depend on a single extra variable.
instance (KnownSymbol na, SymVal a) => Calc (Forall na a -> SBool) where
calcSteps result steps = do a <- free (symbolVal (Proxy @na))
let q checkedLabel = do aa <- free (symbolVal (Proxy @na))
qcRun checkedLabel (steps aa)
(result (Forall a),) <$> mkCalcSteps (steps a) q
-- | Chaining lemmas that depend on two extra variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b) => Calc (Forall na a -> Forall nb b -> SBool) where
calcSteps result steps = do (a, b) <- (,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb))
let q checkedLabel = do (aa, ab) <- (,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb))
qcRun checkedLabel (steps aa ab)
(result (Forall a) (Forall b),) <$> mkCalcSteps (steps a b) q
-- | Chaining lemmas that depend on three extra variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c) => Calc (Forall na a -> Forall nb b -> Forall nc c -> SBool) where
calcSteps result steps = do (a, b, c) <- (,,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc))
let q checkedLabel = do (aa, ab, ac) <- (,,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc))
qcRun checkedLabel (steps aa ab ac)
(result (Forall a) (Forall b) (Forall c),) <$> mkCalcSteps (steps a b c) q
-- | Chaining lemmas that depend on four extra variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d) => Calc (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
calcSteps result steps = do (a, b, c, d) <- (,,,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc)) <*> free (symbolVal (Proxy @nd))
let q checkedLabel = do sb <- steps <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc)) <*> free (symbolVal (Proxy @nd))
qcRun checkedLabel sb
(result (Forall a) (Forall b) (Forall c) (Forall d),) <$> mkCalcSteps (steps a b c d) q
-- | Chaining lemmas that depend on five extra variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e)
=> Calc (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
calcSteps result steps = do (a, b, c, d, e) <- (,,,,) <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc)) <*> free (symbolVal (Proxy @nd)) <*> free (symbolVal (Proxy @ne))
let q checkedLabel = do sb <- steps <$> free (symbolVal (Proxy @na)) <*> free (symbolVal (Proxy @nb)) <*> free (symbolVal (Proxy @nc)) <*> free (symbolVal (Proxy @nd)) <*> free (symbolVal (Proxy @ne))
qcRun checkedLabel sb
(result (Forall a) (Forall b) (Forall c) (Forall d) (Forall e),) <$> mkCalcSteps (steps a b c d e) q
-- | Captures the schema for an inductive proof. Base case might be nothing, to cover strong induction.
data InductionStrategy = InductionStrategy { inductionIntros :: SBool
, inductionMeasure :: Maybe (SBool, [ProofObj])
, inductionBaseCase :: Maybe SBool
, inductionProofTree :: TPProof
, inductiveStep :: SBool
, inductiveQCInstance :: [Int] -> Symbolic SBool
}
-- | Are we doing regular induction or measure based general induction?
data InductionStyle = RegularInduction | GeneralInduction
getInductionStrategySaturatables :: InductionStrategy -> [SBool]
getInductionStrategySaturatables (InductionStrategy inductionIntros
inductionMeasure
inductionBaseCase
inductionProofSteps
inductiveStep
_inductiveQCInstance)
= inductionIntros
: inductiveStep
: proofTreeSaturatables inductionProofSteps
++ measureDs
++ maybeToList inductionBaseCase
where objDeps p = getObjProof p : concatMap objDeps (dependencies p)
measureDs = case inductionMeasure of
Nothing -> []
Just (a, ps) -> a : concatMap objDeps ps
-- | A class for doing regular inductive proofs.
class Inductive a where
type IHType a :: Type
type IHArg a :: Type
-- | Inductively prove a lemma, using the default config.
-- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
-- partial correctness is guaranteed if non-terminating functions are involved.
induct :: (Proposition a, SymVal t, EqSymbolic (SBV t)) => String -> a -> (Proof (IHType a) -> IHArg a -> IStepArgs a t) -> TP (Proof a)
-- | Same as 'induct', but with the given solver configuration.
-- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
-- partial correctness is guaranteed if non-terminating functions are involved.
inductWith :: (Proposition a, SymVal t, EqSymbolic (SBV t)) => SMTConfig -> String -> a -> (Proof (IHType a) -> IHArg a -> IStepArgs a t) -> TP (Proof a)
induct nm p steps = getTPConfig >>= \cfg -> inductWith cfg nm p steps
inductWith cfg nm p steps = getTPConfig >>= \cfg' -> inductionEngine RegularInduction (tpMergeCfg cfg cfg') nm p (inductionStrategy p steps)
-- | Internal, shouldn't be needed outside the library
{-# MINIMAL inductionStrategy #-}
inductionStrategy :: (Proposition a, SymVal t, EqSymbolic (SBV t)) => a -> (Proof (IHType a) -> IHArg a -> IStepArgs a t) -> Symbolic InductionStrategy
-- | A class for doing generalized measure based strong inductive proofs.
class SInductive a where
-- | Inductively prove a lemma, using measure based induction, using the default config.
-- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
-- partial correctness is guaranteed if non-terminating functions are involved.
sInduct :: (Proposition a, Zero m, SymVal t, EqSymbolic (SBV t)) => String -> a -> (MeasureArgs a m, [ProofObj]) -> (Proof a -> StepArgs a t) -> TP (Proof a)
-- | Same as 'sInduct', but with the given solver configuration.
-- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
-- partial correctness is guaranteed if non-terminating functions are involved.
sInductWith :: (Proposition a, Zero m, SymVal t, EqSymbolic (SBV t)) => SMTConfig -> String -> a -> (MeasureArgs a m, [ProofObj]) -> (Proof a -> StepArgs a t) -> TP (Proof a)
sInduct nm p mhs steps = getTPConfig >>= \cfg -> sInductWith cfg nm p mhs steps
sInductWith cfg nm p mhs steps = getTPConfig >>= \cfg' -> inductionEngine GeneralInduction (tpMergeCfg cfg cfg') nm p (sInductionStrategy p mhs steps)
-- | Internal, shouldn't be needed outside the library
{-# MINIMAL sInductionStrategy #-}
sInductionStrategy :: (Proposition a, Zero m, SymVal t, EqSymbolic (SBV t)) => a -> (MeasureArgs a m, [ProofObj]) -> (Proof a -> StepArgs a t) -> Symbolic InductionStrategy
-- | Do an inductive proof, based on the given strategy
inductionEngine :: Proposition a => InductionStyle -> SMTConfig -> String -> a -> Symbolic InductionStrategy -> TP (Proof a)
inductionEngine style cfg nm result getStrategy = do
cached <- lookupProofCache result
case cached of
Just prf -> returnCachedProof cfg nm prf
Nothing -> do
tpSt <- getTPState
u <- tpGetNextUnique
proof <- liftIO $ runSMTWith cfg $ do
qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out
let qual = case style of
RegularInduction -> ""
GeneralInduction -> " (strong)"
let header = "Inductive lemma" ++ qual ++ ": " ++ nm
message cfg $ header ++ "\n"
liftIO $ do isDry <- readIORef (dryRun tpSt)
when isDry $ modifyIORef' (maxRibbon tpSt) (max (length header))
strategy@InductionStrategy { inductionIntros
, inductionMeasure
, inductionBaseCase
, inductionProofTree
, inductiveStep
, inductiveQCInstance
} <- getStrategy
mapM_ qSaturateSavingObservables $ getInductionStrategySaturatables strategy
-- Run measure checks for any newly encountered recursive functions
st <- symbolicEnv
liftIO $ do writeIORef (rSkipMeasureChecks st) True
checkNewMeasures cfg st tpSt
query $ do
case inductionMeasure of
Nothing -> queryDebug [T.pack nm <> ": Induction" <> T.pack qual <> ", there is no custom measure to show non-negativeness."]
Just (m, hs) -> do queryDebug [T.pack nm <> ": Induction, proving measure is always non-negative:"]
smtProofStep cfg tpSt "Step" 1
(TPProofStep False nm [] ["Measure is non-negative"])
(Just (sAnd (inductionIntros : map getObjProof hs)))
m
[]
(\d -> finishTP cfg "Q.E.D." d [])
case inductionBaseCase of
Nothing -> queryDebug [T.pack nm <> ": Induction" <> T.pack qual <> ", there is no base case to prove."]
Just bc -> do queryDebug [T.pack nm <> ": Induction, proving base case:"]
smtProofStep cfg tpSt "Step" 1
(TPProofStep False nm [] ["Base"])
(Just inductionIntros)
bc
[]
(\d -> finishTP cfg "Q.E.D." d [])
proveProofTree cfg tpSt nm (result, inductiveStep) inductionIntros inductionProofTree u inductiveQCInstance
addToProofCache result (proofOf proof)
pure proof
-- Induction strategy helper
mkIndStrategy :: (SymVal a, EqSymbolic (SBV a)) => Maybe (SBool, [ProofObj]) -> Maybe SBool -> (SBool, TPProofRaw (SBV a)) -> SBool -> ([Int] -> Symbolic SBool) -> Symbolic InductionStrategy
mkIndStrategy mbMeasure mbBaseCase indSteps step indQCInstance = do
CalcStrategy { calcIntros, calcProofTree, calcQCInstance } <- mkCalcSteps indSteps indQCInstance
pure $ InductionStrategy { inductionIntros = calcIntros
, inductionMeasure = mbMeasure
, inductionBaseCase = mbBaseCase
, inductionProofTree = calcProofTree
, inductiveStep = step
, inductiveQCInstance = calcQCInstance
}
-- | Create a new variable with the given name, return both the variable and the name
mkVar :: (KnownSymbol n, SymVal a) => proxy n -> Symbolic (SBV a, String)
mkVar x = do let nn = symbolVal x
n <- free nn
pure (n, nn)
-- | Create a new variable with the given name, return both the variable and the name. List version.
mkLVar :: (KnownSymbol n, SymVal a) => proxy n -> Symbolic (SBV a, SList a, String, String, String)
mkLVar x = do let nxs = symbolVal x
nx = singular nxs
e <- free nx
es <- free nxs
pure (e, es, nx, nxs, nx ++ ":" ++ nxs)
-- | Helper for induction result
indResult :: [String] -> SBool -> SBool
indResult nms = observeIf not ("P(" ++ intercalate ", " nms ++ ")")
-- | Induction over 'SInteger'
instance KnownSymbol nn => Inductive (Forall nn Integer -> SBool) where
type IHType (Forall nn Integer -> SBool) = SBool
type IHArg (Forall nn Integer -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
let bc = result (Forall 0)
ih = internalAxiom "IH" (n .>= zero .=> result (Forall n))
mkIndStrategy Nothing
(Just bc)
(steps ih n)
(indResult [nn ++ "+1"] (result (Forall (n+1))))
(\checkedLabel -> free nn >>= qcRun checkedLabel . steps ih)
-- | Induction over 'SInteger', taking an extra argument
instance (KnownSymbol nn, KnownSymbol na, SymVal a) => Inductive (Forall nn Integer -> Forall na a -> SBool) where
type IHType (Forall nn Integer -> Forall na a -> SBool) = Forall na a -> SBool
type IHArg (Forall nn Integer -> Forall na a -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
(a, na) <- mkVar (Proxy @na)
let bc = result (Forall 0) (Forall a)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> n .>= zero .=> result (Forall n) (Forall a'))
mkIndStrategy Nothing
(Just bc)
(steps ih n a)
(indResult [nn ++ "+1", na] (result (Forall (n+1)) (Forall a)))
(\checkedLabel -> steps ih <$> free nn <*> free na >>= qcRun checkedLabel)
-- | Induction over 'SInteger', taking two extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) where
type IHType (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) = Forall na a -> Forall nb b -> SBool
type IHArg (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
let bc = result (Forall 0) (Forall a) (Forall b)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b'))
mkIndStrategy Nothing
(Just bc)
(steps ih n a b)
(indResult [nn ++ "+1", na, nb] (result (Forall (n+1)) (Forall a) (Forall b)))
(\checkedLabel -> steps ih <$> free nn <*> free na <*> free nb >>= qcRun checkedLabel)
-- | Induction over 'SInteger', taking three extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) where
type IHType (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> SBool
type IHArg (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
let bc = result (Forall 0) (Forall a) (Forall b) (Forall c)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c'))
mkIndStrategy Nothing
(Just bc)
(steps ih n a b c)
(indResult [nn ++ "+1", na, nb, nc] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c)))
(\checkedLabel -> steps ih <$> free nn <*> free na <*> free nb <*> free nc >>= qcRun checkedLabel)
-- | Induction over 'SInteger', taking four extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
type IHType (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
type IHArg (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
let bc = result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d'))
mkIndStrategy Nothing
(Just bc)
(steps ih n a b c d)
(indResult [nn ++ "+1", na, nb, nc, nd] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d)))
(\checkedLabel -> steps ih <$> free nn <*> free na <*> free nb <*> free nc <*> free nd >>= qcRun checkedLabel)
-- | Induction over 'SInteger', taking five extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
type IHType (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool
type IHArg (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = SInteger
inductionStrategy result steps = do
(n, nn) <- mkVar (Proxy @nn)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
(e, ne) <- mkVar (Proxy @ne)
let bc = result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))
mkIndStrategy Nothing
(Just bc)
(steps ih n a b c d e)
(indResult [nn ++ "+1", na, nb, nc, nd, ne] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
(\checkedLabel -> steps ih <$> free nn <*> free na <*> free nb <*> free nc <*> free nd <*> free ne >>= qcRun checkedLabel)
-- Given a user name for the list, get a name for the element, in the most suggestive way possible
-- xs -> x
-- xss -> xs
-- foo -> fooElt
singular :: String -> String
singular n = case reverse n of
's':_:_ -> init n
_ -> n ++ "Elt"
-- | Induction over 'SList'
instance (KnownSymbol nxs, SymVal x) => Inductive (Forall nxs [x] -> SBool) where
type IHType (Forall nxs [x] -> SBool) = SBool
type IHArg (Forall nxs [x] -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
let bc = result (Forall [])
ih = internalAxiom "IH" (result (Forall xs))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs))
(indResult [nxxs] (result (Forall (x SL..: xs))))
(\checkedLabel -> ((,) <$> free nx <*> free nxs) >>= qcRun checkedLabel . steps ih)
-- | Induction over 'SList', taking an extra argument
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a) => Inductive (Forall nxs [x] -> Forall na a -> SBool) where
type IHType (Forall nxs [x] -> Forall na a -> SBool) = Forall na a -> SBool
type IHArg (Forall nxs [x] -> Forall na a -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(a, na) <- mkVar (Proxy @na)
let bc = result (Forall []) (Forall a)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs) (Forall a'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs) a)
(indResult [nxxs, na] (result (Forall (x SL..: xs)) (Forall a)))
(\checkedLabel -> steps ih <$> ((,) <$> free nx <*> free nxs) <*> free na >>= qcRun checkedLabel)
-- | Induction over 'SList', taking two extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) where
type IHType (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) = Forall na a -> Forall nb b -> SBool
type IHArg (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
let bc = result (Forall []) (Forall a) (Forall b)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs) (Forall a') (Forall b'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs) a b)
(indResult [nxxs, na, nb] (result (Forall (x SL..: xs)) (Forall a) (Forall b)))
(\checkedLabel -> steps ih <$> ((,) <$> free nx <*> free nxs) <*> free na <*> free nb >>= qcRun checkedLabel)
-- | Induction over 'SList', taking three extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) where
type IHType (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> SBool
type IHArg (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
let bc = result (Forall []) (Forall a) (Forall b) (Forall c)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs) (Forall a') (Forall b') (Forall c'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs) a b c)
(indResult [nxxs, na, nb, nc] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c)))
(\checkedLabel -> steps ih <$> ((,) <$> free nx <*> free nxs) <*> free na <*> free nb <*> free nc >>= qcRun checkedLabel)
-- | Induction over 'SList', taking four extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
type IHType (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
type IHArg (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
let bc = result (Forall []) (Forall a) (Forall b) (Forall c) (Forall d)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs) a b c d)
(indResult [nxxs, na, nb, nc, nd] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d)))
(\checkedLabel -> steps ih <$> ((,) <$> free nx <*> free nxs) <*> free na <*> free nb <*> free nc <*> free nd >>= qcRun checkedLabel)
-- | Induction over 'SList', taking five extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
type IHType (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool
type IHArg (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = (SBV x, SList x)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
(e, ne) <- mkVar (Proxy @ne)
let bc = result (Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs) a b c d e)
(indResult [nxxs, na, nb, nc, nd, ne] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
(\checkedLabel -> steps ih <$> ((,) <$> free nx <*> free nxs) <*> free na <*> free nb <*> free nc <*> free nd <*> free ne >>= qcRun checkedLabel)
-- | Induction over two 'SList', simultaneously
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y) => Inductive ((Forall nxs [x], Forall nys [y]) -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> SBool) = SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
let bc = result (Forall [], Forall []) .&& result (Forall [], Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall [])
ih = internalAxiom "IH" (result (Forall xs, Forall ys))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys))
(indResult [nxxs, nyys] (result (Forall (x SL..: xs), Forall (y SL..: ys))))
(\checkedLabel -> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) >>= qcRun checkedLabel . steps ih)
-- | Induction over two 'SList', simultaneously, taking an extra argument
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) = Forall na a -> SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
(a, na) <- mkVar (Proxy @na)
let bc = result (Forall [], Forall []) (Forall a) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall []) (Forall a)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs, Forall ys) (Forall a'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys) a)
(indResult [nxxs, nyys, na] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a)))
(\checkedLabel -> steps ih <$> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) <*> free na >>= qcRun checkedLabel)
-- | Induction over two 'SList', simultaneously, taking two extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) = Forall na a -> Forall nb b -> SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
let bc = result (Forall [], Forall []) (Forall a) (Forall b) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs, Forall ys) (Forall a') (Forall b'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys) a b)
(indResult [nxxs, nyys, na, nb] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b)))
(\checkedLabel -> steps ih <$> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) <*> free na <*> free nb >>= qcRun checkedLabel)
-- | Induction over two 'SList', simultaneously, taking three extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys) a b c)
(indResult [nxxs, nyys, na, nb, nc] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c)))
(\checkedLabel -> steps ih <$> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) <*> free na <*> free nb <*> free nc >>= qcRun checkedLabel)
-- | Induction over two 'SList', simultaneously, taking four extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c) (Forall d)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys) a b c d)
(indResult [nxxs, nyys, na, nb, nc, nd] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d)))
(\checkedLabel -> steps ih <$> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) <*> free na <*> free nb <*> free nc <*> free nd >>= qcRun checkedLabel)
-- | Induction over two 'SList', simultaneously, taking five extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
type IHType ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool
type IHArg ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = (SBV x, SList x, SBV y, SList y)
inductionStrategy result steps = do
(x, xs, nx, nxs, nxxs) <- mkLVar (Proxy @nxs)
(y, ys, ny, nys, nyys) <- mkLVar (Proxy @nys)
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
(e, ne) <- mkVar (Proxy @ne)
let bc = result (Forall [], Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall [], Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall []) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)
ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))
mkIndStrategy Nothing
(Just bc)
(steps ih (x, xs, y, ys) a b c d e)
(indResult [nxxs, nyys, na, nb, nc, nd, ne] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
(\checkedLabel -> steps ih <$> ((,,,) <$> free nx <*> free nxs <*> free ny <*> free nys) <*> free na <*> free nb <*> free nc <*> free nd <*> free ne >>= qcRun checkedLabel)
-- | Generalized induction with one parameter
instance (KnownSymbol na, SymVal a) => SInductive (Forall na a -> SBool) where
sInductionStrategy result (measure, helpers) steps = do
(a, na) <- mkVar (Proxy @na)
let ih = internalAxiom "IH" (\(Forall a' :: Forall na a) -> measure a' .< measure a .=> result (Forall a'))
conc = result (Forall a)
mkIndStrategy (Just (nonNeg (measure a), helpers))
Nothing
(steps ih a)
(indResult [na] conc)
(\checkedLabel -> free na >>= qcRun checkedLabel . steps ih)
-- | Generalized induction with two parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b) => SInductive (Forall na a -> Forall nb b -> SBool) where
sInductionStrategy result (measure, helpers) steps = do
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
let ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> measure a' b' .< measure a b .=> result (Forall a') (Forall b'))
conc = result (Forall a) (Forall b)
mkIndStrategy (Just (nonNeg (measure a b), helpers))
Nothing
(steps ih a b)
(indResult [na, nb] conc)
(\checkedLabel -> steps ih <$> free na <*> free nb >>= qcRun checkedLabel)
-- | Generalized induction with three parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> SBool) where
sInductionStrategy result (measure, helpers) steps = do
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
let ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> measure a' b' c' .< measure a b c .=> result (Forall a') (Forall b') (Forall c'))
conc = result (Forall a) (Forall b) (Forall c)
mkIndStrategy (Just (nonNeg (measure a b c), helpers))
Nothing
(steps ih a b c)
(indResult [na, nb, nc] conc)
(\checkedLabel -> steps ih <$> free na <*> free nb <*> free nc >>= qcRun checkedLabel)
-- | Generalized induction with four parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
sInductionStrategy result (measure, helpers) steps = do
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
let ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> measure a' b' c' d' .< measure a b c d .=> result (Forall a') (Forall b') (Forall c') (Forall d'))
conc = result (Forall a) (Forall b) (Forall c) (Forall d)
mkIndStrategy (Just (nonNeg (measure a b c d), helpers))
Nothing
(steps ih a b c d)
(indResult [na, nb, nc, nd] conc)
(\checkedLabel -> steps ih <$> free na <*> free nb <*> free nc <*> free nd >>= qcRun checkedLabel)
-- | Generalized induction with five parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
sInductionStrategy result (measure, helpers) steps = do
(a, na) <- mkVar (Proxy @na)
(b, nb) <- mkVar (Proxy @nb)
(c, nc) <- mkVar (Proxy @nc)
(d, nd) <- mkVar (Proxy @nd)
(e, ne) <- mkVar (Proxy @ne)
let ih = internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> measure a' b' c' d' e' .< measure a b c d e .=> result (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))
conc = result (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)
mkIndStrategy (Just (nonNeg (measure a b c d e), helpers))
Nothing
(steps ih a b c d e)
(indResult [na, nb, nc, nd, ne] conc)
(\checkedLabel -> steps ih <$> free na <*> free nb <*> free nc <*> free nd <*> free ne >>= qcRun checkedLabel)
-- | Instantiation for a universally quantified variable
newtype Inst (nm :: Symbol) a = Inst (SBV a)
instance KnownSymbol nm => Show (Inst nm a) where
show (Inst a) = symbolVal (Proxy @nm) ++ " |-> " ++ show a
-- | Instantiating a proof at a particular choice of arguments
class Instantiatable a where
type IArgs a :: Type
-- | Apply a universal proof to some arguments, creating a boolean expression guaranteed to be true
at :: Proof a -> IArgs a -> Proof Bool
-- | Instantiation a single parameter proof
instance (KnownSymbol na, Typeable a) => Instantiatable (Forall na a -> SBool) where
type IArgs (Forall na a -> SBool) = Inst na a
at = instantiate $ \f (Inst a) -> f (Forall a :: Forall na a)
-- | Two parameters
instance ( KnownSymbol na, HasKind a, Typeable a
, KnownSymbol nb, HasKind b, Typeable b
) => Instantiatable (Forall na a -> Forall nb b -> SBool) where
type IArgs (Forall na a -> Forall nb b -> SBool) = (Inst na a, Inst nb b)
at = instantiate $ \f (Inst a, Inst b) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b)
-- | Three parameters
instance ( KnownSymbol na, HasKind a, Typeable a
, KnownSymbol nb, HasKind b, Typeable b
, KnownSymbol nc, HasKind c, Typeable c
) => Instantiatable (Forall na a -> Forall nb b -> Forall nc c -> SBool) where
type IArgs (Forall na a -> Forall nb b -> Forall nc c -> SBool) = (Inst na a, Inst nb b, Inst nc c)
at = instantiate $ \f (Inst a, Inst b, Inst c) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c)
-- | Four parameters
instance ( KnownSymbol na, HasKind a, Typeable a
, KnownSymbol nb, HasKind b, Typeable b
, KnownSymbol nc, HasKind c, Typeable c
, KnownSymbol nd, HasKind d, Typeable d
) => Instantiatable (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) where
type IArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) = (Inst na a, Inst nb b, Inst nc c, Inst nd d)
at = instantiate $ \f (Inst a, Inst b, Inst c, Inst d) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d)
-- | Five parameters
instance ( KnownSymbol na, HasKind a, Typeable a
, KnownSymbol nb, HasKind b, Typeable b
, KnownSymbol nc, HasKind c, Typeable c
, KnownSymbol nd, HasKind d, Typeable d
, KnownSymbol ne, HasKind e, Typeable e
) => Instantiatable (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) where
type IArgs (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) = (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
at = instantiate $ \f (Inst a, Inst b, Inst c, Inst d, Inst e) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d) (Forall e :: Forall ne e)
-- | Instantiate a proof over an arg. This uses dynamic typing, kind of hacky, but works sufficiently well.
instantiate :: (Typeable f, Show arg) => (f -> arg -> SBool) -> Proof a -> arg -> Proof Bool
instantiate ap (Proof p@ProofObj{getProp, proofName}) a = case fromDynamic getProp of
Nothing -> cantInstantiate
Just f -> let result = f `ap` a
nm = proofName ++ " @ " ++ paren sha
in Proof $ p { getObjProof = label nm result
, getProp = toDyn result
, proofName = nm
}
where sha = show a
cantInstantiate = error $ unlines [ "***"
, "Data.SBV.TP: Impossible happened: Cannot instantiate proof:"
, ""
, " Name: " ++ proofName
, " Type: " ++ trim (show getProp)
, " At : " ++ sha
, ""
, "Please report this as a bug!"
]
-- dynamic puts funky <</>> at the beginning and end; trim it:
trim ('<':'<':s) = reverse (trimE (reverse s))
trim s = s
trimE ('>':'>':s) = s
trimE s = s
-- Add parens if necessary
paren s | "(" `isPrefixOf` s && ")" `isSuffixOf` s = s
| not (any isSpace s) = s
| True = '(' : s ++ ")"
-- | Helpers for a step
data Helper = HelperProof ProofObj -- A previously proven theorem
| HelperAssum SBool -- A hypothesis
| HelperQC QC.Args -- Quickcheck with these args
| HelperString String -- Just a text, only used for diagnostics
| HelperDisp String SVal -- Show the value of this expression in case of failure
-- | Get all helpers used in a proof
getAllHelpers :: TPProof -> [Helper]
getAllHelpers (ProofStep _ hs p) = hs ++ getAllHelpers p
getAllHelpers (ProofBranch (_ :: Bool) (_ :: [String]) ps) = concatMap (getAllHelpers . snd) ps
getAllHelpers (ProofEnd _ hs ) = hs
-- | Get proofs from helpers
getHelperProofs :: Helper -> [ProofObj]
getHelperProofs (HelperProof p) = [p]
getHelperProofs HelperAssum {} = []
getHelperProofs HelperQC {} = [quickCheckProof]
getHelperProofs HelperString{} = []
getHelperProofs HelperDisp{} = []
-- | Get proofs from helpers
getHelperAssumes :: Helper -> [SBool]
getHelperAssumes HelperProof {} = []
getHelperAssumes (HelperAssum b) = [b]
getHelperAssumes HelperQC {} = []
getHelperAssumes HelperString {} = []
getHelperAssumes HelperDisp{} = []
-- | Get hint strings from helpers. If there's an explicit comment given, just pass that. If not, collect all the names
getHelperText :: [Helper] -> [String]
getHelperText hs = case [s | HelperString s <- hs] of
[] -> concatMap collect hs
ss -> ss
where collect :: Helper -> [String]
collect (HelperProof p) = [proofName p | isUserAxiom p] -- Don't put out internals (inductive hypotheses)
collect HelperAssum {} = []
collect (HelperQC i) = ["qc: Running " ++ show (QC.maxSuccess i) ++ " tests"]
collect (HelperString s) = [s]
collect HelperDisp{} = []
-- | A proof is a sequence of steps, supporting branching
data TPProofGen a bh b = ProofStep a [Helper] (TPProofGen a bh b) -- ^ A single step
| ProofBranch Bool bh [(SBool, TPProofGen a bh b)] -- ^ A branching step. Bool indicates if completeness check is needed
| ProofEnd b [Helper] -- ^ End of proof
-- | A proof, as written by the user. No produced result, but helpers on branches
type TPProofRaw a = TPProofGen a [Helper] ()
-- | A proof, as processed by TP. Producing a boolean result and each step is a boolean. Helpers on branches dispersed down, only strings are left for printing
type TPProof = TPProofGen SBool [String] SBool
-- | Collect dependencies for a TPProof
getDependencies :: TPProof -> [ProofObj]
getDependencies = collect
where collect (ProofStep _ hs next) = concatMap getHelperProofs hs ++ collect next
collect (ProofBranch _ _ bs) = concatMap (collect . snd) bs
collect (ProofEnd _ hs) = concatMap getHelperProofs hs
-- | Class capturing giving a proof-step helper
type family Hinted a where
Hinted (TPProofRaw a) = TPProofRaw a
Hinted a = TPProofRaw a
-- | Attaching a hint
(??) :: HintsTo a b => a -> b -> Hinted a
(??) = addHint
infixl 2 ??
-- | Alternative unicode for `??`.
(∵) :: HintsTo a b => a -> b -> Hinted a
(∵) = (??)
infixl 2 ∵
-- | Class capturing hints
class HintsTo a b where
addHint :: a -> b -> Hinted a
-- | Giving just one proof as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a (Proof b) where
a `addHint` p = ProofStep a [HelperProof (proofOf p)] qed
-- | Giving a bunch of proofs at the same type as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a [Proof b] where
a `addHint` ps = ProofStep a (map (HelperProof . proofOf) ps) qed
-- | Giving just one proof-obj as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a ProofObj where
a `addHint` p = ProofStep a [HelperProof p] qed
-- | Giving a bunch of proof-objs at the same type as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a [ProofObj] where
a `addHint` ps = ProofStep a (map HelperProof ps) qed
-- | Giving just one boolean as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a SBool where
a `addHint` p = ProofStep a [HelperAssum p] qed
-- | Giving a list of booleans as a helper.
instance Hinted a ~ TPProofRaw a => HintsTo a [SBool] where
a `addHint` ps = ProofStep a (map HelperAssum ps) qed
-- | Giving just one helper
instance Hinted a ~ TPProofRaw a => HintsTo a Helper where
a `addHint` h = ProofStep a [h] qed
-- | Giving a list of helper
instance Hinted a ~ TPProofRaw a => HintsTo a [Helper] where
a `addHint` hs = ProofStep a hs qed
-- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability
instance Hinted a ~ TPProofRaw a => HintsTo a String where
a `addHint` s = ProofStep a [HelperString s] qed
-- | Giving a bunch of strings
instance Hinted a ~ TPProofRaw a => HintsTo a [String] where
a `addHint` ss = ProofStep a (map HelperString ss) qed
-- | Giving just one proof as a helper, starting from a proof
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) (Proof b) where
ProofStep a hs ps `addHint` h = ProofStep a (hs ++ [HelperProof (proofOf h)]) ps
ProofBranch b hs bs `addHint` h = ProofBranch b (hs ++ [HelperProof (proofOf h)]) bs
ProofEnd b hs `addHint` h = ProofEnd b (hs ++ [HelperProof (proofOf h)])
-- | Giving just one proofobj as a helper, starting from a proof
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) ProofObj where
ProofStep a hs ps `addHint` h = ProofStep a (hs ++ [HelperProof h]) ps
ProofBranch b hs bs `addHint` h = ProofBranch b (hs ++ [HelperProof h]) bs
ProofEnd b hs `addHint` h = ProofEnd b (hs ++ [HelperProof h])
-- | Giving a bunch of proofs at the same type as a helper, starting from a proof
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) [Proof b] where
ProofStep a hs ps `addHint` hs' = ProofStep a (hs ++ map (HelperProof . proofOf) hs') ps
ProofBranch b hs bs `addHint` hs' = ProofBranch b (hs ++ map (HelperProof . proofOf) hs') bs
ProofEnd b hs `addHint` hs' = ProofEnd b (hs ++ map (HelperProof . proofOf) hs')
-- | Giving just one boolean as a helper.
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) SBool where
ProofStep a hs ps `addHint` h = ProofStep a (hs ++ [HelperAssum h]) ps
ProofBranch b hs bs `addHint` h = ProofBranch b (hs ++ [HelperAssum h]) bs
ProofEnd b hs `addHint` h = ProofEnd b (hs ++ [HelperAssum h])
-- | Giving a bunch of booleans as a helper.
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) [SBool] where
ProofStep a hs ps `addHint` hs' = ProofStep a (hs ++ map HelperAssum hs') ps
ProofBranch b hs bs `addHint` hs' = ProofBranch b (hs ++ map HelperAssum hs') bs
ProofEnd b hs `addHint` hs' = ProofEnd b (hs ++ map HelperAssum hs')
-- | Giving just one helper
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) Helper where
ProofStep a hs ps `addHint` h = ProofStep a (hs ++ [h]) ps
ProofBranch b hs bs `addHint` h = ProofBranch b (hs ++ [h]) bs
ProofEnd b hs `addHint` h = ProofEnd b (hs ++ [h])
-- | Giving a set of helpers
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) [Helper] where
ProofStep a hs ps `addHint` hs' = ProofStep a (hs ++ hs') ps
ProofBranch b hs bs `addHint` hs' = ProofBranch b (hs ++ hs') bs
ProofEnd b hs `addHint` hs' = ProofEnd b (hs ++ hs')
-- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) String where
a `addHint` s = a `addHint` HelperString s
-- | Giving a bunch of strings as hints. This doesn't actually do anything for the solver, it just helps with readability
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) [String] where
a `addHint` ss = a `addHint` map HelperString ss
-- | Giving a set of proof objects as helpers. This is helpful since we occasionally put a bunch of proofs together.
instance {-# OVERLAPPING #-} Hinted (TPProofRaw a) ~ TPProofRaw a => HintsTo (TPProofRaw a) [ProofObj] where
ProofStep a hs ps `addHint` hs' = ProofStep a (hs ++ map HelperProof hs') ps
ProofBranch b hs bs `addHint` hs' = ProofBranch b (hs ++ map HelperProof hs') bs
ProofEnd b hs `addHint` hs' = ProofEnd b (hs ++ map HelperProof hs')
-- | Capture what a given step can chain-to. This is a closed-type family, i.e.,
-- we don't allow users to change this and write other chainable things. Probably it is not really necessary,
-- but we'll cross that bridge if someone actually asks for it.
type family ChainsTo a where
ChainsTo (TPProofRaw a) = TPProofRaw a
ChainsTo a = TPProofRaw a
-- | Chain steps in a calculational proof.
(=:) :: ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
(=:) = chain
infixr 1 =:
-- | Unicode alternative for `=:`.
(≡) :: ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
(≡) = (=:)
infixr 1 ≡
-- | Chaining two steps together
class ChainStep a b where
chain :: a -> b -> b
-- | Chaining from a value without any annotation
instance ChainStep a (TPProofRaw a) where
chain x y = ProofStep x [] y
-- | Chaining from another proof step
instance ChainStep (TPProofRaw a) (TPProofRaw a) where
chain (ProofStep a hs p) y = ProofStep a hs (chain p y)
chain (ProofBranch c hs ps) y = ProofBranch c hs [(branchCond, chain p y) | (branchCond, p) <- ps]
chain (ProofEnd () hs) y = case y of
ProofStep a hs' p -> ProofStep a (hs' ++ hs) p
ProofBranch b hs' bs -> ProofBranch b (hs' ++ hs) bs
ProofEnd () hs' -> ProofEnd () (hs' ++ hs)
-- | Mark the end of a calculational proof.
qed :: TPProofRaw a
qed = ProofEnd () []
-- | Mark a trivial proof. This is essentially the same as 'qed', but reads better in proof scripts.
class Trivial a where
-- | Mark a proof as trivial, i.e., the solver should be able to deduce it without any help.
trivial :: a
-- | Trivial proofs with no arguments
instance Trivial (TPProofRaw a) where
trivial = qed
-- | Trivial proofs with many arguments arguments
instance Trivial a => Trivial (b -> a) where
trivial = const trivial
-- | Mark a contradictory proof path. This is essentially the same as @sFalse := qed@, but reads better in proof scripts.
class Contradiction a where
-- | Mark a proof as contradiction, i.e., the solver should be able to conclude it by reasoning that the current path is infeasible
contradiction :: a
-- | Contradiction proofs with no arguments
instance Contradiction (TPProofRaw SBool) where
contradiction = sFalse =: qed
-- | Contradiction proofs with many arguments
instance Contradiction a => Contradiction (b -> a) where
contradiction = const contradiction
-- | Start a calculational proof, with the given hypothesis. Use @[]@ as the
-- first argument if the calculation holds unconditionally. The first argument is
-- typically used to introduce hypotheses in proofs of implications such as @A .=> B .=> C@, where
-- we would put @[A, B]@ as the starting assumption. You can name these and later use in the derivation steps.
(|-) :: [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
bs |- p = (sAnd bs, p)
infixl 0 |-
-- | Start an implicational proof, with the given hypothesis. Use @[]@ as the
-- first argument if the calculation holds unconditionally. Each step will be a cascading
-- chain of conjunctions of the previous, starting from @sTrue@.
(|->) :: [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
bs |-> p = (sAnd bs, xform sTrue p)
where xform :: SBool -> TPProofGen SBool [Helper] () -> TPProofGen SBool [Helper] ()
xform conj (ProofStep a hs r) = let ca = conj .&& a in ProofStep ca hs (xform ca r)
xform conj (ProofBranch b bh ss) = ProofBranch b bh [(bc, xform conj r) | (bc, r) <- ss]
xform _ (ProofEnd b hs ) = ProofEnd b hs
infixl 0 |->
-- | Alternative unicode for `|-`.
(⊢) :: [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
(⊢) = (|-)
infixl 0 ⊢
-- | The boolean case-split
cases :: [(SBool, TPProofRaw a)] -> TPProofRaw a
cases = ProofBranch True []
-- | Case splitting over a list; empty and full cases
split :: SymVal a => SList a -> TPProofRaw r -> (SBV a -> SList a -> TPProofRaw r) -> TPProofRaw r
split xs empty cons = ProofBranch False [] [(cnil, empty), (ccons, cons h t)]
where cnil = SL.null xs
(h, t) = SL.uncons xs
ccons = sNot cnil .&& xs .=== h SL..: t
-- | Case splitting over two lists; empty and full cases for each
split2 :: (SymVal a, SymVal b)
=> (SList a, SList b)
-> TPProofRaw r
-> ((SBV b, SList b) -> TPProofRaw r) -- empty first
-> ((SBV a, SList a) -> TPProofRaw r) -- empty second
-> ((SBV a, SList a) -> (SBV b, SList b) -> TPProofRaw r) -- neither empty
-> TPProofRaw r
split2 (xs, ys) ee ec ce cc = ProofBranch False
[]
[ (xnil .&& ynil, ee)
, (xnil .&& ycons, ec (hy, ty))
, (xcons .&& ynil, ce (hx, tx))
, (xcons .&& ycons, cc (hx, tx) (hy, ty))
]
where xnil = SL.null xs
(hx, tx) = SL.uncons xs
xcons = sNot xnil .&& xs .=== hx SL..: tx
ynil = SL.null ys
(hy, ty) = SL.uncons ys
ycons = sNot ynil .&& ys .=== hy SL..: ty
-- | A quick-check step, taking number of tests.
qc :: Int -> Helper
qc cnt = HelperQC QC.stdArgs{QC.maxSuccess = cnt}
-- | A quick-check step, with specific quick-check args.
qcWith :: QC.Args -> Helper
qcWith = HelperQC
-- | Observing values in case of failure.
disp :: String -> SBV a -> Helper
disp n v = HelperDisp n (unSBV v)
-- | Specifying a case-split, helps with the boolean case.
(==>) :: SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
(==>) = (,)
infix 0 ==>
-- | Alternative unicode for `==>`
(⟹) :: SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
(⟹) = (==>)
infix 0 ⟹
-- | Recalling a proof. If the proposition was previously proved and cached, the cached result
-- is returned without re-proving. The output is kept brief: a single "Q.E.D." line.
-- If stats mode is on, we show the full proof steps as the point of stats is to see detail.
recall :: TP (Proof a) -> TP (Proof a)
recall prf = getTPConfig >>= \cfg -> recallWith cfg prf
-- | Recalling a proof, using a given config. Sets the recall context flag so that
-- proof engines check the cache before proving.
recallWith :: SMTConfig -> TP (Proof a) -> TP (Proof a)
recallWith cfgIn prf = do
topCfg <- getTPConfig
tpSt <- getTPState
let cfg@SMTConfig{tpOptions = TPOptions{printStats}} = cfgIn `tpMergeCfg` topCfg
-- Set recall context so proof engines check the cache
liftIO $ modifyIORef' (inRecallContext tpSt) (+1)
let cleanup = liftIO $ modifyIORef' (inRecallContext tpSt) (subtract 1)
if printStats
then restoring cfg topCfg $ do r <- prf
cleanup
pure r
else do let new = cfg{tpOptions = (tpOptions cfg) {quiet = True}}
restoring new topCfg $ do
res <- tryTP prf
cleanup
case res of
Left (_ :: SomeException) ->
-- Re-run with original config so failure details are visible
restoring cfg topCfg prf >> pure (error "unreachable")
Right r@Proof{proofOf = po@ProofObj{dependencies, aliases = aka, wasCached = cached}} -> do
let nm = proofName po
liftIO $ printLemmaResult cfg (verbose cfg) nm dependencies cached aka
pure r
where restoring new old act = do setTPConfig new
res <- act
setTPConfig old
pure res
{- HLint ignore module "Eta reduce" -}
{- HLint ignore module "Reduce duplication" -}