sbv 11.1 → 11.2
raw patch · 52 files changed
+1968/−577 lines, 52 files
Files
- CHANGES.md +20/−6
- Data/SBV.hs +9/−9
- Data/SBV/Char.hs +1/−1
- Data/SBV/Client/BaseIO.hs +2/−2
- Data/SBV/Control.hs +6/−2
- Data/SBV/Control/BaseIO.hs +2/−1
- Data/SBV/Control/Query.hs +1/−1
- Data/SBV/Control/Utils.hs +7/−6
- Data/SBV/Core/Kind.hs +1/−1
- Data/SBV/Core/Operations.hs +3/−1
- Data/SBV/Core/Symbolic.hs +30/−21
- Data/SBV/List.hs +32/−4
- Data/SBV/Provers/ABC.hs +0/−1
- Data/SBV/Provers/Bitwuzla.hs +0/−1
- Data/SBV/Provers/Boolector.hs +0/−1
- Data/SBV/Provers/CVC4.hs +0/−1
- Data/SBV/Provers/CVC5.hs +0/−1
- Data/SBV/Provers/DReal.hs +0/−1
- Data/SBV/Provers/MathSAT.hs +0/−1
- Data/SBV/Provers/OpenSMT.hs +0/−1
- Data/SBV/Provers/Yices.hs +0/−1
- Data/SBV/Provers/Z3.hs +0/−1
- Data/SBV/SMT/SMTLib2.hs +128/−116
- Data/SBV/Tools/BVOptimize.hs +1/−1
- Data/SBV/Tools/CodeGen.hs +1/−1
- Data/SBV/Tools/KD/Kernel.hs +6/−3
- Data/SBV/Tools/KD/KnuckleDragger.hs +563/−144
- Data/SBV/Tools/KnuckleDragger.hs +11/−8
- Data/SBV/Tools/Polynomial.hs +1/−1
- Data/SBV/Tuple.hs +26/−0
- Documentation/SBV/Examples/BitPrecise/PrefixSum.hs +3/−4
- Documentation/SBV/Examples/CodeGeneration/Fibonacci.hs +1/−1
- Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs +24/−10
- Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs +225/−0
- Documentation/SBV/Examples/KnuckleDragger/Kleene.hs +7/−7
- Documentation/SBV/Examples/KnuckleDragger/Lists.hs +554/−53
- Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +27/−24
- Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs +114/−114
- Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs +2/−2
- Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs +134/−0
- Documentation/SBV/Examples/Misc/ProgramPaths.hs +3/−3
- Documentation/SBV/Examples/Misc/SetAlgebra.hs +2/−2
- Documentation/SBV/Examples/Misc/Tuple.hs +1/−1
- Documentation/SBV/Examples/Puzzles/Birthday.hs +1/−1
- Documentation/SBV/Examples/Puzzles/Coins.hs +1/−1
- Documentation/SBV/Examples/Puzzles/Sudoku.hs +1/−1
- README.md +7/−6
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/SBVConnectionTest.hs +2/−2
- SBVTestSuite/TestSuite/Basics/Lambda.hs +1/−1
- SBVTestSuite/TestSuite/Queries/Tuples.hs +1/−1
- sbv.cabal +3/−1
CHANGES.md view
@@ -1,6 +1,20 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 11.2, 2025-03-08++ * Renamed the all-sat partitioning function from 'partition' to 'allSatPartiton'++ * Added support for 'partition' and 'splitAt' to Data.SBV.List++ * KnuckleDragger:+ - Renamed ? to ?? (which aligns better), and added unicode equivalent of it, named ⁇+ - Added strong-induction as a proof-method, with examples for both numeric and list examples+ - Added a double-induction principle, allowing inductive proofs over two lists simultaneously+ - Added a case-splitting tactic for calculational style proofs+ - Added many other example KD proofs, for lists in particular+ - Added a proof of the (functional) insertion sort algorithm+ ### Version 11.1, 2025-02-21 * Completely reworked KnuckleDragger interfaces and proof styles, adding calculational and induction@@ -81,7 +95,7 @@ * [BACKWARDS COMPATIBILITY] Changed the signature of the functions bmc (and bmcWith), induct (and inductWith) functions, so they take the transition as a relation, instead of a function returning multiple values. This generalizes the use cases, and it is easy to translate from existing applications. Simply change your old- 'State -> [State]' function to 'State -> State -> SBool', which can be achieved by + 'State -> [State]' function to 'State -> State -> SBool', which can be achieved by 'newTrans s1 s2 = s2 `sElem` oldTrans s1', though you probably want to code this in a more readable way depending on the actual transition relation you want to model. Furthermore, the function bmc is now split into two bmcRefute and bmcCover, to indicate use cases more clearly.@@ -143,7 +157,7 @@ ### Version 10.7, 2024-03-23 * Fix SMTDefinable instances for functions of arity 8-12. Thanks to Nick Lewchenko for the patch.- + ### Version 10.6, 2024-03-16 * Added Data.SBV.Tools.BVOptimize module, which implements a custom optimizer for unsigned bit-vector@@ -261,7 +275,7 @@ formula has no existential (replaced by uninterpeted functions), and is equisatisfiable to the original. See the following files demonstrating reasoning with quantifiers:- + * Documentation/SBV/Examples/Puzzles/Birthday.hs * Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs * Documentation/SBV/Examples/Puzzles/Rabbits.hs@@ -387,7 +401,7 @@ * Added concrete type instances of Mergeable class. * Fixed a bug in the implementation of the concrete-path for sPopCount- + * Added complement, power, and difference operators for regular expressions. Also added `everything`, `nothing`, `anyChar` as new recognizers. @@ -577,11 +591,11 @@ * Add "extraArgs" parameter to SMTConfig to simplify passing extra command line arguments to the solver. - * Add a method + * Add a method sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b - to the `SymArray` class, which allows for creation of arrays from lists of constant or + to the `SymArray` class, which allows for creation of arrays from lists of constant or symbolic lists of pairs. The first argument is the value to use for uninitialized entries. Note that the initializer must be a known constant, i.e., it cannot be symbolic. Latter elements of the list will overwrite the earlier ones, if there are repeated keys.
Data/SBV.hs view
@@ -335,7 +335,7 @@ , solve -- ** Partitioning result space -- $partitionIntro- , partition+ , allSatPartition -- * Constraints and Quantifiers -- $constrainIntro@@ -837,18 +837,18 @@ -} {- $partitionIntro-The function 'partition' allows one to restrict the results returned by calls to 'Data.SBV.allSat'.+The function 'allSatPartition' one to restrict the results returned by calls to 'Data.SBV.allSat'. In certain cases, we might consider certain models to be "equivalent," i.e., we might want to create equivalence classes over the search space when it comes to what we consider all satisfying-solutions. In these cases, we can use 'partition' to tell SBV what classes of solutions to consider+solutions. In these cases, we can use 'allSatPartition' tell SBV what classes of solutions to consider as unique. Consider: >>> :{ allSat $ do x <- sInteger "x" y <- sInteger "y"- partition "p1" $ x .>= 0- partition "p2" $ y .>= 0+ allSatPartition "p1" $ x .>= 0+ allSatPartition "p2" $ y .>= 0 :} Solution #1: x = 0 :: Integer@@ -872,16 +872,16 @@ p2 = True :: Bool Found 4 different solutions. -Without the call to 'partition' in the above example, 'allSat' would return all possible combinations of @x@ and @y@ subject to the constraints. (Since we have none here,-the call would try to enumerate the infinite set of all integer tuples!) But 'partition' allows us to restrict our attention to the examples that satisfy the partitioning-constraints. The first argument to 'partition' is simply a name, for diagnostic purposes. Note that the conditions given by 'partition' are /not/ imposed on the search+Without the call to 'allSatPartition' the above example, 'allSat' would return all possible combinations of @x@ and @y@ subject to the constraints. (Since we have none here,+the call would try to enumerate the infinite set of all integer tuples!) But 'allSatPartition' us to restrict our attention to the examples that satisfy the partitioning+constraints. The first argument to 'allSatPartition' simply a name, for diagnostic purposes. Note that the conditions given by 'allSatPartition' /not/ imposed on the search space at all: They're only used when we construct the search space. In the above example, we pick one example from each quadrant. Furthermore, while it is typical to pass a boolean as a partitioning argument, it is not required: Any expression is OK, whose value creates the equivalence class: >>> :{ allSat $ do x <- sInteger "x"- partition "p" $ x `sMod` 3+ allSatPartition "p" $ x `sMod` 3 :} Solution #1: x = 2 :: Integer
Data/SBV/Char.hs view
@@ -208,7 +208,7 @@ isPrintL1 :: SChar -> SBool isPrintL1 = liftPredL1 C.isPrint --- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumberL1' +-- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumberL1'. -- -- >>> prove $ \c -> isDigit c .=> isNumberL1 c -- Q.E.D.
Data/SBV/Client/BaseIO.hs view
@@ -226,8 +226,8 @@ output = Trans.output -- | Create a partitioning constraint, for all-sat calls.-partition :: SymVal a => String -> SBV a -> Symbolic ()-partition nm term = do+allSatPartition :: SymVal a => String -> SBV a -> Symbolic ()+allSatPartition nm term = do State{rPartitionVars} <- symbolicEnv -- Generate a unique variable with the prefix nm if necessary and
Data/SBV/Control.hs view
@@ -71,9 +71,13 @@ , SMTOption(..) ) where -import Data.SBV.Core.Symbolic (Symbolic, QueryContext(..))+import Data.SBV.Core.Symbolic (Symbolic, QueryContext(..), Query, MonadQuery(..), SMTConfig(..)) -import Data.SBV.Trans.Control hiding (query)+import Data.SBV.Control.BaseIO+import Data.SBV.Control.Types+import Data.SBV.Control.Query ((|->))++import Data.SBV.Utils.ExtractIO (ExtractIO(..)) import qualified Data.SBV.Control.Utils as Trans
Data/SBV/Control/BaseIO.hs view
@@ -191,7 +191,8 @@ -- 'Data.SBV.setOption' $ 'Data.SBV.Control.ProduceUnsatCores' 'True' -- @ ----- for this call to not error out!+-- for this call to not error out! Furthermore, unsat-cores require for the user to name the+-- constraints to be considered as part of the set, which is done via 'Data.SBV.Core.namedConstraint'. -- -- NB. There is no notion of a minimal unsat-core, in case unsatisfiability can be derived -- in multiple ways. Furthermore, Z3 does not guarantee that the generated unsat
Data/SBV/Control/Query.hs view
@@ -157,7 +157,7 @@ , ("timeout", UnknownTimeOut) ] --- | Generalization of 'Data.SBV.Control.getInfo'+-- | Generalization of 'Data.SBV.Control.getOption' getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption) getOption f = case f undefined of DiagnosticOutputChannel{} -> askFor "DiagnosticOutputChannel" ":diagnostic-output-channel" $ string DiagnosticOutputChannel
Data/SBV/Control/Utils.hs view
@@ -967,12 +967,13 @@ interpretRational xs = error $ "Expected a rational constant, received: <" ++ show xs ++ ">" interpretList ek topExpr = walk topExpr- where walk (EApp [ECon "as", ECon "seq.empty", _]) = []- walk (EApp [ECon "seq.unit", v]) = case recoverKindedValue ek v of- Just w -> [cvVal w]- Nothing -> error $ "Cannot parse a sequence item of kind " ++ show ek ++ " from: " ++ show v ++ extra v- walk (EApp (ECon "seq.++" : rest)) = concatMap walk rest- walk cur = error $ "Expected a sequence constant, but received: " ++ show cur ++ extra cur+ where walk (EApp [ECon "as", v, _]) = walk v+ walk (ECon "seq.empty") = []+ walk (EApp [ECon "seq.unit", v]) = case recoverKindedValue ek v of+ Just w -> [cvVal w]+ Nothing -> error $ "Cannot parse a sequence item of kind " ++ show ek ++ " from: " ++ show v ++ extra v+ walk (EApp (ECon "seq.++" : rest)) = concatMap walk rest+ walk cur = error $ "Expected a sequence constant, but received: " ++ show cur ++ extra cur extra cur | show cur == t = "" | True = "\nWhile parsing: " ++ t
Data/SBV/Core/Kind.hs view
@@ -132,7 +132,7 @@ noS ('S':s) = s noS s = s --- For historical reasons, we show 8-16-32-64 bit values with no space; others with a space. +-- For historical reasons, we show 8-16-32-64 bit values with no space; others with a space. pickType :: Int -> String -> String -> String pickType i standard other | i `elem` [8, 16, 32, 64] = standard
Data/SBV/Core/Operations.hs view
@@ -178,7 +178,7 @@ svAbs :: SVal -> SVal svAbs = liftSym1 (mkSymOp1 Abs) abs abs abs abs abs abs --- | Signum. +-- | Signum. -- -- NB. The following "carefully" tests the number for == 0, as Float/Double's NaN and +/-0 -- cases would cause trouble with explicit equality tests.@@ -601,6 +601,7 @@ | a == falseSV || b == falseSV = Just falseSV | a == trueSV = Just b | b == trueSV = Just a+ | a == b = Just a | True = Nothing -- | Bitwise or.@@ -616,6 +617,7 @@ | a == trueSV || b == trueSV = Just trueSV | a == falseSV = Just b | b == falseSV = Just a+ | a == b = Just a | True = Nothing -- | Bitwise xor.
Data/SBV/Core/Symbolic.hs view
@@ -544,16 +544,17 @@ | SeqSuffixOf -- ^ See StrSuffixOf | SeqReplace -- ^ See StrReplace -- Polymorphic and higher order functions- | SBVReverse Kind -- ^ reverse k. Where k is either [a] or String. Reverses the argument, accordingly.- | SBVZip Kind Kind -- ^ zip a b. Where we zip [a] and [b] to produce [(a, b)]- | SBVZipWith Kind Kind Kind SMTLambda -- ^ zipWith a b c fun. Where fun :: a -> b -> c, and zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]- | SBVMap Kind Kind SMTLambda -- ^ map a b fun. Where fun :: a -> b, and map :: (a -> b) -> [a] -> [b]- | SBVFoldl Kind Kind SMTLambda -- ^ foldl a b fun. Where fun :: b -> a -> b, and foldl :: (b -> a -> b) -> b -> [a] -> b- | SBVFoldr Kind Kind SMTLambda -- ^ foldr a b fun. Where fun :: a -> b -> b, and foldr :: (a -> b -> b) -> b -> [a] -> b- | SBVFilter Kind SMTLambda -- ^ filter a fun. Where fun :: a -> Bool, and filter :: (a -> Bool) -> [a] -> [a]- | SBVAll Kind SMTLambda -- ^ all a fun. Where fun :: a -> Bool, and all :: (a -> Bool) -> [a] -> Bool- | SBVAny Kind SMTLambda -- ^ any a fun. Where fun :: a -> Bool, and any :: (a -> Bool) -> [a] -> Bool- | SBVConcat Kind -- ^ concat a. Where we concat [[a]] to get [a] (a is the inside-element type)+ | SBVReverse Kind -- ^ reverse k. Where k is either [a] or String. Reverses the argument, accordingly.+ | SBVZip Kind Kind -- ^ zip a b. Where we zip [a] and [b] to produce [(a, b)]+ | SBVZipWith Kind Kind Kind SMTLambda -- ^ zipWith a b c fun. Where fun :: a -> b -> c, and zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]+ | SBVPartition Kind SMTLambda -- ^ partition a fun. Where fun :: a -> SBool, and partition :: (a -> Bool) -> [a] -> ([a], [a])+ | SBVMap Kind Kind SMTLambda -- ^ map a b fun. Where fun :: a -> b, and map :: (a -> b) -> [a] -> [b]+ | SBVFoldl Kind Kind SMTLambda -- ^ foldl a b fun. Where fun :: b -> a -> b, and foldl :: (b -> a -> b) -> b -> [a] -> b+ | SBVFoldr Kind Kind SMTLambda -- ^ foldr a b fun. Where fun :: a -> b -> b, and foldr :: (a -> b -> b) -> b -> [a] -> b+ | SBVFilter Kind SMTLambda -- ^ filter a fun. Where fun :: a -> Bool, and filter :: (a -> Bool) -> [a] -> [a]+ | SBVAll Kind SMTLambda -- ^ all a fun. Where fun :: a -> Bool, and all :: (a -> Bool) -> [a] -> Bool+ | SBVAny Kind SMTLambda -- ^ any a fun. Where fun :: a -> Bool, and any :: (a -> Bool) -> [a] -> Bool+ | SBVConcat Kind -- ^ concat a. Where we concat [[a]] to get [a] (a is the inside-element type) deriving (Eq, Ord, G.Data, NFData, Generic) -- | Show instance for SeqOp. Again, mapping is important.@@ -570,16 +571,17 @@ show SeqReplace = "seq.replace" -- Note: The followings aren't part of SMTLib, we explicitly handle them- show (SBVReverse a) = funcWithKind "sbv.reverse" a Nothing- show (SBVZip a b) = funcWithKind "sbv.zip" (KTuple [a, b]) Nothing- show (SBVZipWith a b c f) = funcWithKind "sbv.zipWith" (KTuple [a, b, c]) (Just f)- show (SBVMap a b f) = funcWithKind "sbv.map" (KTuple [a, b]) (Just f)- show (SBVFoldl a b f) = funcWithKind "sbv.foldl" (KTuple [a, b]) (Just f)- show (SBVFoldr a b f) = funcWithKind "sbv.foldr" (KTuple [a, b]) (Just f)- show (SBVFilter a f) = funcWithKind "sbv.filter" a (Just f)- show (SBVAll a f) = funcWithKind "sbv.all" a (Just f)- show (SBVAny a f) = funcWithKind "sbv.any" a (Just f)- show (SBVConcat a) = funcWithKind "sbv.concat" a Nothing+ show (SBVReverse a) = funcWithKind "sbv.reverse" a Nothing+ show (SBVZip a b) = funcWithKind "sbv.zip" (KTuple [a, b]) Nothing+ show (SBVZipWith a b c f) = funcWithKind "sbv.zipWith" (KTuple [a, b, c]) (Just f)+ show (SBVPartition a f) = funcWithKind "sbv.partition" a (Just f)+ show (SBVMap a b f) = funcWithKind "sbv.map" (KTuple [a, b]) (Just f)+ show (SBVFoldl a b f) = funcWithKind "sbv.foldl" (KTuple [a, b]) (Just f)+ show (SBVFoldr a b f) = funcWithKind "sbv.foldr" (KTuple [a, b]) (Just f)+ show (SBVFilter a f) = funcWithKind "sbv.filter" a (Just f)+ show (SBVAll a f) = funcWithKind "sbv.all" a (Just f)+ show (SBVAny a f) = funcWithKind "sbv.any" a (Just f)+ show (SBVConcat a) = funcWithKind "sbv.concat" a Nothing -- helper for above funcWithKind :: String -> Kind -> Maybe SMTLambda -> String@@ -1414,6 +1416,14 @@ UIPrefix n | not (nm `isPrefixOf` n) -> " (Given prefix: " ++ n ++ ")" _ -> "" + -- Check if reserved:+ when (isReserved nm) $+ error $ unlines [ ""+ , "*** Data.SBV: User given name " ++ show nm ++ " is a reserved name in SMTLib."+ , "***"+ , "*** Please use a different name to avoid collisions."+ ]+ isCurried <- case uiCode of UINone c -> pure c UISMT d -> do modifyState st rDefns (\defs -> (d, t) : filter (\(o, _) -> smtDefGivenName o /= Just nm) defs)@@ -2239,7 +2249,6 @@ , supportsBitVectors :: Bool -- ^ Supports bit-vectors? , supportsUninterpretedSorts :: Bool -- ^ Supports SMT-Lib2 style uninterpreted-sorts , supportsUnboundedInts :: Bool -- ^ Supports unbounded integers?- , supportsInt2bv :: Bool -- ^ Supports int2bv? , supportsReals :: Bool -- ^ Supports reals? , supportsApproxReals :: Bool -- ^ Supports printing of approximations of reals? , supportsDeltaSat :: Maybe String -- ^ Supports delta-satisfiability? (With given precision query)
Data/SBV/List.hs view
@@ -29,7 +29,7 @@ -- * Containment , elem, notElem, isInfixOf, isSuffixOf, isPrefixOf -- * Sublists- , take, drop, subList, replace, indexOf, offsetIndexOf+ , take, drop, splitAt, subList, replace, indexOf, offsetIndexOf -- * Reverse , reverse -- * Mapping@@ -39,12 +39,12 @@ -- * Zipping , zip, zipWith -- * Filtering- , filter+ , filter, partition -- * Other list functions , all, any, and, or ) where -import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem,+import Prelude hiding (head, tail, init, length, take, drop, splitAt, concat, null, elem, notElem, reverse, (++), (!!), map, concatMap, foldl, foldr, zip, zipWith, filter, all, any, and, or) import qualified Prelude as P@@ -56,10 +56,12 @@ import Data.SBV.Lambda +import Data.SBV.Tuple hiding (fst, snd)+ import Data.Maybe (isNothing, catMaybes) import Data.List (genericLength, genericIndex, genericDrop, genericTake)-import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf)+import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf, partition) import Data.Proxy @@ -278,6 +280,10 @@ $ subList s i (ls - i) where ls = length s +-- | @splitAt n xs = (take n xs, drop n xs)@+splitAt :: SymVal a => SInteger -> SList a -> (SList a, SList a)+splitAt n xs = (take n xs, drop n xs)+ -- | @`subList` s offset len@ is the sublist of @s@ at offset @offset@ with length @len@. -- This function is under-specified when the offset is outside the range of positions in @s@ or @len@ -- is negative or @offset+len@ exceeds the length of @s@.@@ -623,6 +629,28 @@ r st = do sva <- sbvToSV st l lam <- lambdaStr st HigherOrderArg KBool f let op = SeqOp (SBVFilter (kindOf (Proxy @a)) lam)+ registerSpecialFunction st op+ newExpr st k (SBVApp op [sva])++-- | @partition f xs@ splits the list into two and returns those that satisfy the predicate in the+-- first element, and those that don't in the second.+partition :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]+partition f l+ | Just l' <- unliteral l, Just concResult <- concretePartition l'+ = concResult+ | True+ = SBV $ SVal k $ Right $ cache r+ where concretePartition l' = case P.map (unliteral . f . literal) l' of+ xs | P.any isNothing xs -> Nothing+ | True -> let (ts, fs) = L.partition fst (P.zip (catMaybes xs) l')+ in Just $ tuple (literal (P.map snd ts), literal (P.map snd fs))+++ k = kindOf (Proxy @(STuple [a] [a]))++ r st = do sva <- sbvToSV st l+ lam <- lambdaStr st HigherOrderArg KBool f+ let op = SeqOp (SBVPartition (kindOf (Proxy @a)) lam) registerSpecialFunction st op newExpr st k (SBVApp op [sva])
Data/SBV/Provers/ABC.hs view
@@ -35,7 +35,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = False , supportsUnboundedInts = False- , supportsInt2bv = False , supportsReals = False , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/Bitwuzla.hs view
@@ -33,7 +33,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = False- , supportsInt2bv = False , supportsReals = False , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/Boolector.hs view
@@ -33,7 +33,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = False , supportsUnboundedInts = False- , supportsInt2bv = False , supportsReals = False , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/CVC4.hs view
@@ -37,7 +37,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = True , supportsReals = True -- Not quite the same capability as Z3; but works more or less.. , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/CVC5.hs view
@@ -37,7 +37,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = True , supportsReals = True -- Not quite the same capability as Z3; but works more or less.. , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/DReal.hs view
@@ -37,7 +37,6 @@ , supportsBitVectors = False , supportsUninterpretedSorts = False , supportsUnboundedInts = True- , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Just "(get-option :precision)"
Data/SBV/Provers/MathSAT.hs view
@@ -37,7 +37,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/OpenSMT.hs view
@@ -33,7 +33,6 @@ , supportsBitVectors = False , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/Yices.hs view
@@ -35,7 +35,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = False , supportsReals = True , supportsApproxReals = False , supportsDeltaSat = Nothing
Data/SBV/Provers/Z3.hs view
@@ -35,7 +35,6 @@ , supportsBitVectors = True , supportsUninterpretedSorts = True , supportsUnboundedInts = True- , supportsInt2bv = True , supportsReals = True , supportsApproxReals = True , supportsDeltaSat = Nothing
Data/SBV/SMT/SMTLib2.hs view
@@ -22,7 +22,6 @@ import qualified Data.ByteString.Base16 as B import qualified Data.ByteString.Char8 as BC -import Data.Bits (bit) import Data.List (intercalate, partition, nub, elemIndex) import Data.Maybe (listToMaybe, catMaybes) @@ -37,7 +36,7 @@ import Data.SBV.SMT.Utils import Data.SBV.Control.Types -import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName', getSV, regExpToSMTString+import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName', getSV, regExpToSMTString, NROp(..) , SMTDef(..), ResultInp(..), ProgInfo(..), SpecialRelOp(..), SMTLambda(..) ) @@ -51,23 +50,24 @@ -- we create a firstified name based on the operation. The suffix appended will have at most uniqLen length. firstify :: Int -> Op -> String firstify uniqLen o = prefix o ++ "_" ++ take uniqLen (BC.unpack (B.encode (hash (BC.pack (compress (show o))))))- where prefix (SeqOp SBVReverse {}) = "sbv.reverse"- prefix (SeqOp SBVZip {}) = "sbv.zip"- prefix (SeqOp SBVZipWith {}) = "sbv.zipWith"- prefix (SeqOp SBVMap {}) = "sbv.map"- prefix (SeqOp SBVFoldl {}) = "sbv.foldl"- prefix (SeqOp SBVFoldr {}) = "sbv.foldr"- prefix (SeqOp SBVFilter {}) = "sbv.filter"- prefix (SeqOp SBVAll {}) = "sbv.all"- prefix (SeqOp SBVAny {}) = "sbv.any"- prefix (SeqOp SBVConcat {}) = "sbv.concat"- prefix _ = error $ unlines [ "***"- , "*** Data.SBV.firstify: Didn't expect firstification to be called."- , "***"- , "*** Operator: " ++ show o- , "***"- , "*** Please report this as a bug."- ]+ where prefix (SeqOp SBVReverse {}) = "sbv.reverse"+ prefix (SeqOp SBVZip {}) = "sbv.zip"+ prefix (SeqOp SBVZipWith {}) = "sbv.zipWith"+ prefix (SeqOp SBVPartition {}) = "sbv.partition"+ prefix (SeqOp SBVMap {}) = "sbv.map"+ prefix (SeqOp SBVFoldl {}) = "sbv.foldl"+ prefix (SeqOp SBVFoldr {}) = "sbv.foldr"+ prefix (SeqOp SBVFilter {}) = "sbv.filter"+ prefix (SeqOp SBVAll {}) = "sbv.all"+ prefix (SeqOp SBVAny {}) = "sbv.any"+ prefix (SeqOp SBVConcat {}) = "sbv.concat"+ prefix _ = error $ unlines [ "***"+ , "*** Data.SBV.firstify: Didn't expect firstification to be called."+ , "***"+ , "*** Operator: " ++ show o+ , "***"+ , "*** Please report this as a bug."+ ] -- compress and make spaces uniform; get words, and then unwords compress = unwords . words@@ -106,14 +106,15 @@ hasRational = any isRational kindInfo rm = roundingMode cfg solverCaps = capabilities (solver cfg)- hasLambdas = let needsLambda SBVZipWith{} = True- needsLambda SBVMap{} = True- needsLambda SBVFoldl{} = True- needsLambda SBVFoldr{} = True- needsLambda SBVFilter{} = True- needsLambda SBVAll{} = True- needsLambda SBVAny{} = True- needsLambda _ = False+ hasLambdas = let needsLambda SBVZipWith{} = True+ needsLambda SBVPartition{} = True+ needsLambda SBVMap{} = True+ needsLambda SBVFoldl{} = True+ needsLambda SBVFoldr{} = True+ needsLambda SBVFilter{} = True+ needsLambda SBVAll{} = True+ needsLambda SBVAny{} = True+ needsLambda _ = False in (not . null) [() | o :: SeqOp <- G.universeBi allTopOps, needsLambda o] (needsQuantifiers, needsSpecialRels, specialFuncs) = case curProgInfo of@@ -334,14 +335,15 @@ -- same if the same op sans the lambda getFuncs :: Op -> Op -> Maybe (SMTLambda, SMTLambda)- getFuncs (SeqOp (SBVZipWith a b c f)) (SeqOp (SBVZipWith x y z g)) | [a, b, c] == [x, y, z] = Just (f, g)- getFuncs (SeqOp (SBVMap a b f)) (SeqOp (SBVMap x y g)) | [a, b ] == [x, y ] = Just (f, g)- getFuncs (SeqOp (SBVFoldl a b f)) (SeqOp (SBVFoldl x y g)) | [a, b ] == [x, y ] = Just (f, g)- getFuncs (SeqOp (SBVFoldr a b f)) (SeqOp (SBVFoldr x y g)) | [a, b ] == [x, y ] = Just (f, g)- getFuncs (SeqOp (SBVFilter a f)) (SeqOp (SBVFilter x g)) | [a ] == [x ] = Just (f, g)- getFuncs (SeqOp (SBVAll a f)) (SeqOp (SBVAll x g)) | [a ] == [x ] = Just (f, g)- getFuncs (SeqOp (SBVAny a f)) (SeqOp (SBVAny x g)) | [a ] == [x ] = Just (f, g)- getFuncs _ _ = Nothing+ getFuncs (SeqOp (SBVZipWith a b c f)) (SeqOp (SBVZipWith x y z g)) | [a, b, c] == [x, y, z] = Just (f, g)+ getFuncs (SeqOp (SBVPartition a f)) (SeqOp (SBVPartition x g)) | [a ] == [x ] = Just (f, g)+ getFuncs (SeqOp (SBVMap a b f)) (SeqOp (SBVMap x y g)) | [a, b ] == [x, y ] = Just (f, g)+ getFuncs (SeqOp (SBVFoldl a b f)) (SeqOp (SBVFoldl x y g)) | [a, b ] == [x, y ] = Just (f, g)+ getFuncs (SeqOp (SBVFoldr a b f)) (SeqOp (SBVFoldr x y g)) | [a, b ] == [x, y ] = Just (f, g)+ getFuncs (SeqOp (SBVFilter a f)) (SeqOp (SBVFilter x g)) | [a ] == [x ] = Just (f, g)+ getFuncs (SeqOp (SBVAll a f)) (SeqOp (SBVAll x g)) | [a ] == [x ] = Just (f, g)+ getFuncs (SeqOp (SBVAny a f)) (SeqOp (SBVAny x g)) | [a ] == [x ] = Just (f, g)+ getFuncs _ _ = Nothing equate :: (Op, (String, SMTLambda), (String, SMTLambda)) -> [String] equate (o, (nm1, f), (nm2, g)) = [ "; Equality for " ++ nm1 ++ " vs. " ++ nm2@@ -353,14 +355,15 @@ args = unwords $ map fst params decls = unwords ['(' : n ++ " " ++ smtType k ++ ")" | (n, k) <- params] - paramsOf (SeqOp (SBVZipWith k1 k2 _ _)) = [ ("xs", KList k1), ("ys", KList k2)]- paramsOf (SeqOp (SBVMap k1 _ _)) = [ ("xs", KList k1)]- paramsOf (SeqOp (SBVFoldl k1 k2 _)) = [("b", k2), ("xs", KList k1)]- paramsOf (SeqOp (SBVFoldr k1 k2 _)) = [("b", k2), ("xs", KList k1)]- paramsOf (SeqOp (SBVFilter k1 _)) = [ ("xs", KList k1)]- paramsOf (SeqOp (SBVAll k1 _)) = [ ("xs", KList k1)]- paramsOf (SeqOp (SBVAny k1 _)) = [ ("xs", KList k1)]- paramsOf op = error $ "Data.SBV.firstifiedEqualities: Unexpected op: " ++ show op+ paramsOf (SeqOp (SBVZipWith k1 k2 _ _)) = [ ("xs", KList k1), ("ys", KList k2)]+ paramsOf (SeqOp (SBVPartition k1 _)) = [ ("xs", KList k1)]+ paramsOf (SeqOp (SBVMap k1 _ _)) = [ ("xs", KList k1)]+ paramsOf (SeqOp (SBVFoldl k1 k2 _)) = [("b", k2), ("xs", KList k1)]+ paramsOf (SeqOp (SBVFoldr k1 k2 _)) = [("b", k2), ("xs", KList k1)]+ paramsOf (SeqOp (SBVFilter k1 _)) = [ ("xs", KList k1)]+ paramsOf (SeqOp (SBVAll k1 _)) = [ ("xs", KList k1)]+ paramsOf (SeqOp (SBVAny k1 _)) = [ ("xs", KList k1)]+ paramsOf op = error $ "Data.SBV.firstifiedEqualities: Unexpected op: " ++ show op userDefs = declUserFuns defs exportedDefs@@ -424,40 +427,44 @@ comment = ["; Firstified function: " ++ htyp] body = case op of- SeqOp (SBVReverse KString) -> mkStringRev- SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k)- SeqOp (SBVZip k1 k2) -> mkZip k1 k2 Nothing- SeqOp (SBVZipWith k1 k2 k3 (SMTLambda f)) -> mkZip k1 k2 (Just (k3, f))- SeqOp (SBVMap k1 k2 (SMTLambda f)) -> mkMap k1 k2 f- SeqOp (SBVFoldl k1 k2 (SMTLambda f)) -> mkFoldl k1 k2 f- SeqOp (SBVFoldr k1 k2 (SMTLambda f)) -> mkFoldr k1 k2 f- SeqOp (SBVFilter ek (SMTLambda f)) -> mkFilter ek f- SeqOp (SBVAll ek (SMTLambda f)) -> mkAnyAll True ek f- SeqOp (SBVAny ek (SMTLambda f)) -> mkAnyAll False ek f- SeqOp (SBVConcat ek) -> mkConcat ek- _ -> error $ "Data.SBV.declSBVFunc.body: Unexpected internal function: "- ++ show (op, nm)+ SeqOp (SBVReverse KString) -> mkStringRev+ SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k)+ SeqOp (SBVZip k1 k2) -> mkZip k1 k2 Nothing+ SeqOp (SBVZipWith k1 k2 k3 (SMTLambda f)) -> mkZip k1 k2 (Just (k3, f))+ SeqOp (SBVPartition ek (SMTLambda f)) -> mkPartition ek f+ SeqOp (SBVMap k1 k2 (SMTLambda f)) -> mkMap k1 k2 f+ SeqOp (SBVFoldl k1 k2 (SMTLambda f)) -> mkFoldl k1 k2 f+ SeqOp (SBVFoldr k1 k2 (SMTLambda f)) -> mkFoldr k1 k2 f+ SeqOp (SBVFilter ek (SMTLambda f)) -> mkFilter ek f+ SeqOp (SBVAll ek (SMTLambda f)) -> mkAnyAll True ek f+ SeqOp (SBVAny ek (SMTLambda f)) -> mkAnyAll False ek f+ SeqOp (SBVConcat ek) -> mkConcat ek+ _ -> error $ "Data.SBV.declSBVFunc.body: Unexpected internal function: " ++ show (op, nm) + -- helper when there's no higher order arg shf :: String -> [Kind] -> Kind -> String shf f args rt = f ++ " :: " ++ intercalate " -> " (map show (args ++ [rt])) + -- helper when there's a function arg shh :: String -> ([Kind], Kind) -> ([Kind], Kind) -> String shh f (fargs, fret) (args, rt) = f ++ " :: (" ++ intercalate " -> " (map show (fargs ++ [fret])) ++ ") -> " ++ intercalate " -> " (map show (args ++ [rt])) + -- This is the haskell type htyp = case op of- SeqOp (SBVReverse KString) -> shf "reverse" [KString] KString- SeqOp (SBVReverse k@KList{}) -> shf "reverse" [k] k- SeqOp (SBVZip a b) -> shf "zip" [KList a, KList b] (KList (KTuple [a, b]))- SeqOp (SBVZipWith a b c _) -> shh "zipWith" ([a, b], c) ([KList a, KList b], KList c)- SeqOp (SBVMap a b _) -> shh "map" ([a], b) ([KList a], KList b)- SeqOp (SBVFoldl a b _) -> shh "foldl" ([b, a], b) ([b, KList a], b)- SeqOp (SBVFoldr a b _) -> shh "foldr" ([a, b], b) ([b, KList a], b)- SeqOp (SBVFilter a _) -> shh "filter" ([a], KBool) ([KList a], KList a)- SeqOp (SBVAll a _) -> shh "all" ([a], KBool) ([KList a], KBool)- SeqOp (SBVAny a _) -> shh "any" ([a], KBool) ([KList a], KBool)- SeqOp (SBVConcat a) -> shf "concat" [KList (KList a)] (KList a)- _ -> error $ "Data.SBV.declSBVFunc.htyp: Unexpected internal function: " ++ show (op, nm)+ SeqOp (SBVReverse KString) -> shf "reverse" [KString] KString+ SeqOp (SBVReverse k@KList{}) -> shf "reverse" [k] k+ SeqOp (SBVZip a b) -> shf "zip" [KList a, KList b] (KList (KTuple [a, b]))+ SeqOp (SBVZipWith a b c _) -> shh "zipWith" ([a, b], c) ([KList a, KList b], KList c)+ SeqOp (SBVPartition a _) -> shh "partition" ([a], KBool) ([KList a], KTuple [KList a, KList a])+ SeqOp (SBVMap a b _) -> shh "map" ([a], b) ([KList a], KList b)+ SeqOp (SBVFoldl a b _) -> shh "foldl" ([b, a], b) ([b, KList a], b)+ SeqOp (SBVFoldr a b _) -> shh "foldr" ([a, b], b) ([b, KList a], b)+ SeqOp (SBVFilter a _) -> shh "filter" ([a], KBool) ([KList a], KList a)+ SeqOp (SBVAll a _) -> shh "all" ([a], KBool) ([KList a], KBool)+ SeqOp (SBVAny a _) -> shh "any" ([a], KBool) ([KList a], KBool)+ SeqOp (SBVConcat a) -> shf "concat" [KList (KList a)] (KList a)+ _ -> error $ "Data.SBV.declSBVFunc.htyp: Unexpected internal function: " ++ show (op, nm) -- in Z3, lambdas are applied with select. In CVC5, it's @. This might change with higher-order features being added to SMTLib in v3 par x = "(" ++ x ++ ")"@@ -509,6 +516,24 @@ Nothing -> app tup [x, y] tup = app "as" ["mkSBVTuple2", app "SBVTuple2" [smtType a, smtType b]] + -- (a -> Bool) -> [a] -> ([a], [a])+ mkPartition a f = [ "(define-fun-rec " ++ nm ++ " ((lst " ++ tla ++ ")) " ++ tpla+ , " (ite " ++ isEmpty "lst" tla+ , " " ++ base+ , " (let ((a " ++ hd "lst" ++ "))"+ , " (let ((ua (seq.unit a)))"+ , " (let ((rest " ++ app nm [tl "lst"] ++ "))"+ , " (let ((ts (proj_1_SBVTuple2 rest)))"+ , " (let ((fs (proj_2_SBVTuple2 rest)))"+ , " (ite " ++ happ f [hd "lst"]+ , " " ++ pair "(seq.++ ua ts)" "fs"+ , " " ++ pair "ts" "(seq.++ ua fs)" ++ "))))))))"+ ]+ where tla = smtType (KList a)+ tpla = smtType (KTuple [KList a, KList a])+ base = "(mkSBVTuple2 (as seq.empty " ++ tla ++ ") (as seq.empty " ++ tla ++ "))"+ pair ts fs = "((as mkSBVTuple2 (SBVTuple2 " ++ tla ++ " " ++ tla ++ ")) " ++ ts ++ " " ++ fs ++ ")"+ -- (b -> a -> b) -> b -> [a] -> b mkFoldl a b f = [ "(define-fun-rec " ++ nm ++ " ((base " ++ tb ++ ") (lst " ++ tla ++ ")) " ++ tb , " (ite " ++ isEmpty "lst" tla@@ -572,7 +597,7 @@ declSort (s, _) | s == "RoundingMode" -- built-in-sort; so don't declare. = []-declSort (s, Nothing) = [ "(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted sort." +declSort (s, Nothing) = [ "(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted sort." , "(declare-fun " ++ witnessName s ++ " () " ++ s ++ ")" ] declSort (s, Just fs) = [ "(declare-datatypes ((" ++ s ++ " 0)) ((" ++ unwords (map (\c -> "(" ++ c ++ ")") fs) ++ ")))"@@ -773,7 +798,7 @@ -- Make a function equality of nm against the internal function fun mkRelEq :: String -> (String, String) -> Kind -> String mkRelEq nm (fun, order) ak = res- where lhs = "(" ++ nm ++ " x y)" + where lhs = "(" ++ nm ++ " x y)" rhs = "((_ " ++ fun ++ " " ++ order ++ ") x y)" tk = smtType ak res = "(forall ((x " ++ tk ++ ") (y " ++ tk ++ ")) (= " ++ lhs ++ " " ++ rhs ++ "))"@@ -947,7 +972,6 @@ cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> String cvtExp cfg curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr where hasPB = supportsPseudoBooleans caps- hasInt2bv = supportsInt2bv caps hasDistinct = supportsDistinct caps specialRels = progSpecialRels curProgInfo @@ -969,6 +993,14 @@ addRM s = s ++ " " ++ smtRoundingMode rm + isZ3 = case name (solver cfg) of+ Z3 -> True+ _ -> False++ isCVC5 = case name (solver cfg) of+ CVC5 -> True+ _ -> False+ hd _ (a:_) = a hd w [] = error $ "Impossible: " ++ w ++ ": Received empty list of args!" @@ -1130,7 +1162,7 @@ le0 = "(" ++ less ++ " " ++ cvtSV i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ cvtSV i ++ ")" - sh (SBVApp (KindCast f t) [a]) = handleKindCast hasInt2bv f t (cvtSV a)+ sh (SBVApp (KindCast f t) [a]) = handleKindCast f t (cvtSV a) sh (SBVApp (ArrayLambda s) []) = show s sh (SBVApp ReadArray [a, i]) = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"@@ -1204,6 +1236,13 @@ sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (cvtSV m) (unwords (map cvtSV args)) sh (SBVApp (IEEEFP w ) args) = "(" ++ show w ++ " " ++ unwords (map cvtSV args) ++ ")" + -- Some non-linear operators are supported by z3/CVC5 specifically, so do the custom translation Otherwise+ -- we pass them along.+ sh (SBVApp (NonLinear NR_Sqrt) [a]) | isZ3 = "(^ " ++ cvtSV a ++ " 0.5)"+ | isCVC5 = "(sqrt " ++ cvtSV a ++ ")"++ sh (SBVApp (NonLinear NR_Pow) [a, b]) | isZ3 || isCVC5 = "(^ " ++ cvtSV a ++ " " ++ cvtSV b ++ ")"+ sh (SBVApp (NonLinear w) args) = "(" ++ show w ++ " " ++ unwords (map cvtSV args) ++ ")" sh (SBVApp (PseudoBoolean pb) args)@@ -1223,17 +1262,18 @@ sh (SBVApp (RegExOp o@RegExNEq{}) []) = show o -- Reverse and higher order functions are special- sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVZip{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVZipWith{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVMap{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVFoldl{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVFoldr{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVFilter{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVAll{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVAny{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"- sh (SBVApp o@(SeqOp SBVConcat{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVZip{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVZipWith{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVPartition{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVReverse{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVMap{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVFoldl{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVFoldr{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVFilter{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVAll{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVAny{} ) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")"+ sh (SBVApp o@(SeqOp SBVConcat{}) args) = "(" ++ firstifiedName o ++ " " ++ unwords (map cvtSV args) ++ ")" sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" @@ -1572,20 +1612,21 @@ where o = if hasSign x then oS else oW -- Various casts-handleKindCast :: Bool -> Kind -> Kind -> String -> String-handleKindCast hasInt2bv kFrom kTo a+handleKindCast :: Kind -> Kind -> String -> String+handleKindCast kFrom kTo a | kFrom == kTo = a | True = case kFrom of KBounded s m -> case kTo of KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n- KUnbounded -> b2i s m+ KUnbounded -> if s then "(sbv_to_int " ++ a ++ ")"+ else "(ubv_to_int " ++ a ++ ")" _ -> tryFPCast KUnbounded -> case kTo of KReal -> "(to_real " ++ a ++ ")"- KBounded _ n -> i2b n+ KBounded _ n -> "((_ int_to_bv " ++ show n ++ ") " ++ a ++ ")" _ -> tryFPCast KReal -> case kTo of@@ -1607,38 +1648,9 @@ | m == n = a | True = extract (n - 1) - b2i False _ = "(bv2nat " ++ a ++ ")"- b2i True 1 = "(ite (= " ++ a ++ " #b0) 0 (- 1))"- b2i True m = "(ite (= " ++ msb ++ " #b0" ++ ") " ++ ifPos ++ " " ++ ifNeg ++ ")"- where offset :: Integer- offset = 2^(m-1)- rest = extract (m - 2)-- msb = let top = show (m-1) in "((_ extract " ++ top ++ " " ++ top ++ ") " ++ a ++ ")"- ifPos = "(bv2nat " ++ rest ++")"- ifNeg = "(- " ++ ifPos ++ " " ++ show offset ++ ")"- signExtend i = "((_ sign_extend " ++ show i ++ ") " ++ a ++ ")" zeroExtend i = "((_ zero_extend " ++ show i ++ ") " ++ a ++ ")" extract i = "((_ extract " ++ show i ++ " 0) " ++ a ++ ")"-- -- Some solvers support int2bv, but not all. So, we use a capability to determine.- --- -- NB. The "manual" implementation works regardless n < 0 or not, because the first thing we- -- do is to compute "reduced" to bring it down to the correct range. It also works- -- regardless were mapping to signed or unsigned bit-vector; because the representation- -- is the same.- i2b n- | hasInt2bv- = "((_ int2bv " ++ show n ++ ") " ++ a ++ ")"- | True- = "(let (" ++ reduced ++ ") (let (" ++ defs ++ ") " ++ body ++ "))"- where b i = show (bit i :: Integer)- reduced = "(__a (mod " ++ a ++ " " ++ b n ++ "))"- mkBit 0 = "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))"- mkBit i = "(__a" ++ show i ++ " (ite (= (mod (div __a " ++ b i ++ ") 2) 0) #b0 #b1))"- defs = unwords (map mkBit [0 .. n - 1])- body = foldr1 (\c r -> "(concat " ++ c ++ " " ++ r ++ ")") ["__a" ++ show i | i <- [n-1, n-2 .. 0]] -- Translation of pseudo-booleans, in case the solver supports them handlePB :: PBOp -> [String] -> String
Data/SBV/Tools/BVOptimize.hs view
@@ -96,7 +96,7 @@ | hasSign v = error $ "minMaxBV works on unsigned bitvectors, received: " ++ show (kindOf v) | True- = do when getUC $ setOption $ ProduceUnsatCores True + = do when getUC $ setOption $ ProduceUnsatCores True query $ go (blastBE v) where uc | getUC = Just <$> getUnsatCore | True = pure Nothing
Data/SBV/Tools/CodeGen.hs view
@@ -18,7 +18,7 @@ SBVCodeGen, cgSym -- ** Setting code-generation options- , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile, cgOverwriteFiles, cgShowU8UsingHex + , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile, cgOverwriteFiles, cgShowU8UsingHex -- ** Designating inputs , cgInput, cgInputArr
Data/SBV/Tools/KD/Kernel.hs view
@@ -36,7 +36,7 @@ import Data.SBV.Core.Data hiding (None) import Data.SBV.Core.Symbolic (isEmptyModel)-import Data.SBV.Control hiding (getProof)+import Data.SBV.Trans.Control hiding (getProof) import Data.SBV.SMT.SMT import Data.SBV.Core.Model@@ -87,7 +87,7 @@ , getProp = toDyn p , proofName = "sorry" }- where -- ideally, I'd rather just use + 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@@ -184,7 +184,10 @@ die = error "Failed" - fullNm = intercalate "." (filter (not . null) (fromMaybe nms fullNms))+ fullNm = intercalate "." $ squeeze $ filter (not . null) (fromMaybe nms fullNms)+ squeeze (x:y:rest) | x == y = squeeze (y:rest)+ squeeze (x:rest) = x : squeeze rest+ squeeze [] = [] unknown = do r <- getUnknownReason liftIO $ do putStrLn $ "\n*** Failed to prove " ++ fullNm ++ "."
Data/SBV/Tools/KD/KnuckleDragger.hs view
@@ -32,11 +32,12 @@ , axiom , lemma, lemmaWith , theorem, theoremWith- , calc, calcWith, calcThm, calcThmWith- , induct, inductWith, inductThm, inductThmWith+ , calc, calcWith, calcThm, calcThmWith+ , induct, inductWith, inductThm, inductThmWith+ , sInduct, sInductWith, sInductThm, sInductThmWith , sorry , KD, runKD, runKDWith, use- , (|-), (⊢), (=:), (≡), (?), hyp, hprf, qed+ , (|-), (⊢), (=:), (≡), (??), (⁇), cases, hyp, hprf, qed ) where import Data.SBV@@ -44,10 +45,13 @@ import Data.SBV.Control hiding (getProof) +import Data.SBV.Core.Data(SolverContext)+ import Data.SBV.Tools.KD.Kernel import Data.SBV.Tools.KD.Utils -import Control.Monad.Trans (liftIO)+import Control.Monad (forM_)+import Control.Monad.Trans (liftIO, MonadIO) import qualified Data.SBV.List as SL @@ -61,11 +65,69 @@ import Data.SBV.Utils.TDiff import Data.Dynamic+import Data.Time (NominalDiffTime) -- | Bring an IO proof into current proof context. use :: IO Proof -> KD Proof use = liftIO +-- | Captures the steps for a calculationa proof+data CalcStrategy = CalcStrategy { calcIntros :: SBool+ , calcProofSteps :: [([Helper], SBool)]+ }++-- | Saturatable things in steps+proofStepSaturatables :: [([Helper], SBool)] -> [SBool]+proofStepSaturatables = concatMap getS+ where getS (hs, b) = b : concatMap getH hs+ getH (HelperProof p) = [getProof p]+ getH (HelperAssum b) = [b]+ getH (HelperCase _ ss) = ss++-- | Things that are inside calc-strategy that we have to saturate+getCalcStrategySaturatables :: CalcStrategy -> [SBool]+getCalcStrategySaturatables (CalcStrategy calcIntros calcProofSteps) = calcIntros : proofStepSaturatables calcProofSteps++-- | Based on the helpers given, construct the proofs we have to do in the given case+stepCases :: Int -> [Helper] -> Either (String, SBool) ([(String, SBool)], SBool)+stepCases i helpers+ | hasCase+ = Right (caseSplits, cover)+ | True+ = Left (show i, sAnd (map getBools helpers))+ where join :: [(String, SBool)] -> Helper -> [(String, SBool)]+ join sofar (HelperProof p) = map (\(n, cond) -> (n, cond .&& getProof p)) sofar+ join sofar (HelperAssum b) = map (\(n, cond) -> (n, cond .&& b)) sofar+ join sofar (HelperCase cn cs) = concatMap (\(n, cond) -> [ (dotN n ++ cn ++ "[" ++ show j ++ "]", cond .&& b)+ | (j, b) <- zip [(1::Int)..] cs+ ]) sofar++ -- Add a dot if we have a legit prefix+ dotN "" = ""+ dotN s = s ++ "."++ -- Used only when we have ano case splits:+ getBools (HelperProof p) = getProof p+ getBools (HelperAssum b) = b+ getBools (HelperCase{}) = error "Unexpected case in stepCases: Wasn't expecting to see a HelperCase here."++ -- All case-splits. If there isn't any, we'll get just one case+ caseSplits = foldl join [("", sTrue)] helpers++ -- If there were any cases, then we also need coverage+ isCase (HelperProof {}) = False+ isCase (HelperAssum {}) = False+ isCase (HelperCase {}) = True++ hasCase = any isCase helpers++ regulars = concatMap getHyp helpers+ where getHyp (HelperProof p) = [getProof p]+ getHyp (HelperAssum b) = [b]+ getHyp (HelperCase {}) = []++ cover = sAnd regulars .&& sNot (sOr [b | (_, b) <- caseSplits])+ -- | 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 CalcLemma a steps where@@ -103,7 +165,7 @@ -- | Internal, shouldn't be needed outside the library {-# MINIMAL calcSteps #-}- calcSteps :: a -> steps -> Symbolic (SBool, (SBool, [([Helper], SBool)]))+ calcSteps :: a -> steps -> Symbolic (SBool, CalcStrategy) calc nm p steps = getKDConfig >>= \cfg -> calcWith cfg nm p steps calcThm nm p steps = getKDConfig >>= \cfg -> calcThmWith cfg nm p steps@@ -122,25 +184,29 @@ mbStartTime <- getTimeStampIf measureTime - (goal, (calcIntros, proofSteps)) <- calcSteps result steps+ (calcGoal, strategy@CalcStrategy {calcIntros, calcProofSteps}) <- calcSteps result steps - let stepHelpers = concatMap fst proofSteps- (ros, modulo) = calculateRootOfTrust nm [p | HProof p <- stepHelpers]- finish = finishKD cfg ("Q.E.D." ++ modulo)+ let stepHelpers = concatMap fst calcProofSteps - mapM_ (qSaturateSavingObservables . getHelperBool) stepHelpers+ finish et helpers d = finishKD cfg ("Q.E.D." ++ modulo) d et+ where (_, modulo) = calculateRootOfTrust nm helpers + -- Collect all subterms and saturate them+ mapM_ qSaturateSavingObservables $ calcIntros : getCalcStrategySaturatables strategy+ let go :: Int -> SBool -> [([Helper], SBool)] -> Query Proof go _ accum [] = do queryDebug [nm ++ ": Proof end: proving the result:"] checkSatThen cfg kdSt "Result" True (Just (calcIntros .=> accum))- goal+ calcGoal [] ["", ""] (Just [nm, "Result"]) Nothing $ \d -> do mbElapsed <- getElapsedTime mbStartTime- finish d $ catMaybes [mbElapsed]+ let (ros, modulo) = calculateRootOfTrust nm (getHelperProofs stepHelpers)+ finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])+ pure Proof { rootOfTrust = ros , isUserAxiom = False , getProof = label nm (quantifiedBool result)@@ -151,7 +217,7 @@ go i accum ((by, s):ss) = do -- Prove that the assumptions follow, if any- case [a | HAssum a <- by] of+ case getHelperAssumes by of [] -> pure () as -> checkSatThen cfg kdSt "Asms " True@@ -159,30 +225,63 @@ (sAnd as) [] ["", show i]- (Just [nm, show i])+ (Just [nm, show i, "Assumptions"]) Nothing- (`finish` [])+ (finish [] []) queryDebug [nm ++ ": Proof step: " ++ show i ++ " to " ++ show (i+1) ++ ":"]- checkSatThen cfg kdSt "Step "- True- (Just (sAnd (map getHelperBool by)))- s- []- ["", show i]- (Just [nm, show i])- Nothing- (`finish` []) + proveAllCases i cfg kdSt (stepCases i by) "Step " s nm (finish [] (getHelperProofs by))+ go (i+1) (s .&& accum) ss - query $ go (1::Int) sTrue proofSteps+ query $ go (1::Int) sTrue calcProofSteps +proveAllCases :: (Monad m, SolverContext m, MonadIO m, MonadQuery m, Proposition a)+ => Int -> SMTConfig -> KDState+ -> Either (String, SBool) ([(String, SBool)], SBool)+ -> String -> a -> String -> ((Int, Maybe NominalDiffTime) -> IO ()) -> m ()+proveAllCases topStep cfg kdSt caseInfo stepTag s nm finalize+ | Left (stepName, asmp) <- caseInfo+ = checker stepTag asmp s ["", stepName] (Just [nm, stepName])+ | Right (proofCases, coverCond) <- caseInfo+ = do let len = length proofCases+ ways = case len of+ 1 -> "one way"+ n -> show n ++ " ways"++ slen = show len+ clen = length slen+ sh i = reverse . take clen $ reverse (show i) ++ repeat ' '++ _tab <- liftIO $ startKD cfg True ("Step " ++ show topStep) ["", "Case split " ++ ways ++ ":"]++ forM_ (zip [(1::Int)..] proofCases) $ \(c, (stepName, asmp)) ->+ checker ("Case [" ++ sh c ++ " of " ++ show len ++ "]") asmp s ["", "", stepName] (Just [nm, stepName])++ checker "Completeness" coverCond s ["", "", ""] (Just [nm, show topStep, "Completeness"])+ where+ checker tag caseAsmp cond cnm fnm = checkSatThen cfg kdSt tag True (Just caseAsmp) cond [] cnm fnm Nothing finalize+ -- | Turn a sequence of steps into a chain of equalities-mkCalcSteps :: EqSymbolic a => (SBool, [ProofStep a]) -> (SBool, [([Helper], SBool)])-mkCalcSteps (intros, xs) = (intros, zipWith merge xs (drop 1 xs))- where merge (ProofStep a by) (ProofStep b _) = (by, a .== b)+mkCalcSteps :: EqSymbolic a => (SBool, [ProofStep a]) -> CalcStrategy+mkCalcSteps (intros, xs) = case reverse xs of+ (SingleStep _ (_:_) : _) -> 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?"+ ]+ _ -> CalcStrategy { calcIntros = intros+ , calcProofSteps = zipWith merge xs (drop 1 xs)+ }+ where merge (SingleStep a by) (SingleStep b _) = (by, a .== b) +-- | Chaining lemmas that depend on no quantified variables+instance EqSymbolic z => CalcLemma SBool (SBool, [ProofStep z]) where+ calcSteps result steps = pure (result, mkCalcSteps steps)+ -- | Chaining lemmas that depend on a single quantified variable. instance (KnownSymbol na, SymVal a, EqSymbolic z) => CalcLemma (Forall na a -> SBool) (SBV a -> (SBool, [ProofStep z])) where calcSteps result steps = do a <- free (symbolVal (Proxy @na))@@ -224,65 +323,115 @@ , inductiveStep :: SBool } +-- | Are we doing strong induction or regular induction?+data InductionStyle = RegularInduction | StrongInduction++getInductionStrategySaturatables :: InductionStrategy -> [SBool]+getInductionStrategySaturatables (InductionStrategy inductionIntros+ inductionBaseCase+ inductionProofSteps+ _inductionBaseFailureMsg+ inductiveStep)+ = inductionIntros : inductionBaseCase : inductiveStep : proofStepSaturatables inductionProofSteps+ -- | A class for doing inductive proofs, with the possibility of explicit steps. class Inductive a steps where -- | Inductively prove a lemma, using the default config.- induct :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof+ -- 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 => String -> a -> (Proof -> steps) -> KD Proof + -- | Inductively prove a lemma, using strong 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 => String -> a -> (Proof -> steps) -> KD Proof+ -- | Inductively prove a theorem. Same as 'induct', but tagged as a theorem, 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. inductThm :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof + -- | Inductively prove a theorem, using strong induction. Same as 'sInduct', but tagged as a theorem, 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.+ sInductThm :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof+ -- | 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 => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof - -- | Same as 'inductiveTheorem, but with the given solver configuration.+ -- | 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 => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof++ -- | Same as 'inductThm', 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. inductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof + -- | Same as 'sInductThm', 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.+ sInductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof+ induct nm p steps = getKDConfig >>= \cfg -> inductWith cfg nm p steps inductThm nm p steps = getKDConfig >>= \cfg -> inductThmWith cfg nm p steps- inductWith = inductGeneric False- inductThmWith = inductGeneric True+ inductWith = inductGeneric RegularInduction False+ inductThmWith = inductGeneric RegularInduction True + sInduct nm p steps = getKDConfig >>= \cfg -> sInductWith cfg nm p steps+ sInductThm nm p steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p steps+ sInductWith = inductGeneric StrongInduction False+ sInductThmWith = inductGeneric StrongInduction True+ -- | Internal, shouldn't be needed outside the library {-# MINIMAL inductionStrategy #-}- inductionStrategy :: Proposition a => a -> (Proof -> steps) -> Symbolic InductionStrategy+ inductionStrategy :: Proposition a => InductionStyle -> a -> (Proof -> steps) -> Symbolic InductionStrategy - inductGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof- inductGeneric tagTheorem cfg@SMTConfig{kdOptions = KDOptions{measureTime}} nm result steps = do+ inductGeneric :: Proposition a => InductionStyle -> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof+ inductGeneric style tagTheorem cfg@SMTConfig{kdOptions = KDOptions{measureTime}} nm result steps = do kdSt <- getKDState liftIO $ runSMTWith cfg $ do qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out - message cfg $ "Inductive " ++ (if tagTheorem then "theorem" else "lemma") ++ ": " ++ nm ++ "\n"+ let strong = case style of+ RegularInduction -> ""+ StrongInduction -> " (strong)" + message cfg $ "Inductive " ++ (if tagTheorem then "theorem" else "lemma") ++ strong ++ ": " ++ nm ++ "\n"+ mbStartTime <- getTimeStampIf measureTime - InductionStrategy { inductionIntros- , inductionBaseCase- , inductionProofSteps- , inductionBaseFailureMsg- , inductiveStep- } <- inductionStrategy result steps+ strategy@InductionStrategy { inductionIntros+ , inductionBaseCase+ , inductionProofSteps+ , inductionBaseFailureMsg+ , inductiveStep+ } <- inductionStrategy style result steps - let stepHelpers = concatMap fst inductionProofSteps- (ros, modulo) = calculateRootOfTrust nm [p | HProof p <- stepHelpers]- finish et d = finishKD cfg ("Q.E.D." ++ modulo) d et+ let stepHelpers = concatMap fst inductionProofSteps - mapM_ (qSaturateSavingObservables . getHelperBool) stepHelpers+ finish et helpers d = finishKD cfg ("Q.E.D." ++ modulo) d et+ where (_, modulo) = calculateRootOfTrust nm helpers + -- Collect all subterms and saturate them+ mapM_ qSaturateSavingObservables $ getInductionStrategySaturatables strategy+ query $ do queryDebug [nm ++ ": Induction, proving base case:"] checkSatThen cfg kdSt "Base" True (Just inductionIntros) inductionBaseCase [] [nm, "Base"] Nothing (Just (liftIO (putStrLn inductionBaseFailureMsg)))- (finish [])+ (finish [] []) let loop i accum ((by, s):ss) = do -- Prove that the assumptions follow, if any- case [a | HAssum a <- by] of+ case getHelperAssumes by of [] -> pure () as -> checkSatThen cfg kdSt "Asms" True@@ -290,20 +439,14 @@ (sAnd as) [] ["", show i]- (Just [nm, show i])+ (Just [nm, show i, "Assumptions"]) Nothing- (finish [])+ (finish [] []) queryDebug [nm ++ ": Induction, proving step: " ++ show i]- checkSatThen cfg kdSt "Step"- True- (Just (sAnd (map getHelperBool by)))- s- []- ["", show i]- (Just [nm, show i])- Nothing- (finish [])++ proveAllCases i cfg kdSt (stepCases i by) "Step" s nm (finish [] (getHelperProofs by))+ loop (i+1) (accum .&& s) ss loop _ accum [] = pure accum@@ -321,8 +464,12 @@ [nm, "Step"] Nothing Nothing $ \d -> do+ mbElapsed <- getElapsedTime mbStartTime- finish (catMaybes [mbElapsed]) d++ let (ros, modulo) = calculateRootOfTrust nm (getHelperProofs stepHelpers)+ finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])+ pure $ Proof { rootOfTrust = ros , isUserAxiom = False , getProof = label nm $ quantifiedBool result@@ -332,19 +479,21 @@ -- | Induction over 'SInteger'. instance (KnownSymbol nk, EqSymbolic z) => Inductive (Forall nk Integer -> SBool) (SInteger -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate k = result (Forall k) nk = symbolVal (Proxy @nk) k <- free nk - let ih = internalAxiom "IH" $ predicate k- (intros, pSteps) = mkCalcSteps $ steps ih k+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ result (Forall k)+ StrongInduction -> internalAxiom "IH" $ \(Forall k' :: Forall nk Integer) -> k' .<= k .=> result (Forall k')+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k pure InductionStrategy {- inductionIntros = k .>= 0 .&& intros+ inductionIntros = k .>= 0 .&& calcIntros , inductionBaseCase = predicate 0- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0." , inductiveStep = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1)) }@@ -353,7 +502,7 @@ instance forall na a nk z. (KnownSymbol na, SymVal a, KnownSymbol nk, EqSymbolic z) => Inductive (Forall nk Integer -> Forall na a -> SBool) (SInteger -> SBV a -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate k a = result (Forall k) (Forall a) nk = symbolVal (Proxy @nk) na = symbolVal (Proxy @na)@@ -361,13 +510,15 @@ k <- free nk a <- free na - let ih = internalAxiom "IH" $ \a' -> result (Forall k) (a' :: Forall na a)- (intros, pSteps) = mkCalcSteps $ steps ih k a+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall k) (a' :: Forall na a)+ StrongInduction -> internalAxiom "IH" $ \(Forall k' :: Forall nk Integer) a' -> 0 .<= k' .&& k' .<= k .=> result (Forall k') (a' :: Forall na a)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a pure InductionStrategy {- inductionIntros = k .>= 0 .&& intros+ inductionIntros = k .>= 0 .&& calcIntros , inductionBaseCase = predicate 0 a- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0." , inductiveStep = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a) }@@ -376,7 +527,7 @@ instance forall na a nb b nk z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nk, EqSymbolic z) => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> SBool) (SInteger -> SBV a -> SBV b -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate k a b = result (Forall k) (Forall a) (Forall b) nk = symbolVal (Proxy @nk) na = symbolVal (Proxy @na)@@ -386,13 +537,15 @@ a <- free na b <- free nb - let ih = internalAxiom "IH" $ \a' b' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b)- (intros, pSteps) = mkCalcSteps $ steps ih k a b+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b)+ StrongInduction -> internalAxiom "IH" $ \(Forall k' :: Forall nk Integer) a' b' -> 0 .<= k' .&& k' .<= k .=> result (Forall k') (a' :: Forall na a) (b' :: Forall nb b)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b pure InductionStrategy {- inductionIntros = k .>= 0 .&& intros+ inductionIntros = k .>= 0 .&& calcIntros , inductionBaseCase = predicate 0 a b- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0." , inductiveStep = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b) }@@ -402,7 +555,7 @@ => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate k a b c = result (Forall k) (Forall a) (Forall b) (Forall c) nk = symbolVal (Proxy @nk) na = symbolVal (Proxy @na)@@ -414,13 +567,15 @@ b <- free nb c <- free nc - let ih = internalAxiom "IH" $ \a' b' c' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)- (intros, pSteps) = mkCalcSteps $ steps ih k a b c+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ StrongInduction -> internalAxiom "IH" $ \(Forall k' :: Forall nk Integer) a' b' c' -> 0 .<= k' .&& k' .<= k .=> result (Forall k') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b c pure InductionStrategy {- inductionIntros = k .>= 0 .&& intros+ inductionIntros = k .>= 0 .&& calcIntros , inductionBaseCase = predicate 0 a b c- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0." , inductiveStep = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b c) }@@ -429,7 +584,7 @@ instance forall na a nb b nc c nd d nk z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol nk, EqSymbolic z) => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate k a b c d = result (Forall k) (Forall a) (Forall b) (Forall c) (Forall d) nk = symbolVal (Proxy @nk) na = symbolVal (Proxy @na)@@ -443,13 +598,15 @@ c <- free nc d <- free nd - let ih = internalAxiom "IH" $ \a' b' c' d' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)- (intros, pSteps) = mkCalcSteps $ steps ih k a b c d+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall k) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ StrongInduction -> internalAxiom "IH" $ \(Forall k' :: Forall nk Integer) a' b' c' d' -> 0 .<= k' .&& k' .<= k .=> result (Forall k') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b c d pure InductionStrategy {- inductionIntros = k .>= 0 .&& intros+ inductionIntros = k .>= 0 .&& calcIntros , inductionBaseCase = predicate 0 a b c d- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0." , inductiveStep = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b c d) }@@ -463,28 +620,35 @@ 's':_:_ -> init n _ -> n ++ "Elt" +-- | Metric for induction. Currently we simply require the list we're assuming correctness for is shorter in length, which+-- is a measure that is guarenteed >= 0. -- Later on, we might want to generalize this to a user given measure.+smaller :: SymVal a => SList a -> SList a -> SBool+smaller xs ys = SL.length xs .<= SL.length ys+ -- | Induction over 'SList'.-instance (KnownSymbol nk, SymVal k, EqSymbolic z)- => Inductive (Forall nk [k] -> SBool)- (SBV k -> SList k -> (SBool, [ProofStep z]))+instance (KnownSymbol nx, SymVal x, EqSymbolic z)+ => Inductive (Forall nx [x] -> SBool)+ (SBV x -> SList x -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do- let predicate k = result (Forall k)- nks = symbolVal (Proxy @nk)- nk = singular nks+ inductionStrategy style result steps = do+ let predicate xs = result (Forall xs)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs - k <- free nk- ks <- free nks+ x <- free nx+ xs <- free nxs - let ih = internalAxiom "IH" $ predicate ks- (intros, pSteps) = mkCalcSteps $ steps ih k ks+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ result (Forall xs)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) -> xs' `smaller` xs .=> result (Forall xs')+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil- , inductionProofSteps = pSteps- , inductionBaseFailureMsg = "Property fails for " ++ nks ++ " = []."- , inductiveStep = observeIf not ("P(" ++ nk ++ ":" ++ nks ++ ")") (predicate (k SL..: ks))+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs)) } -- | Induction over 'SList' taking an extra argument@@ -492,7 +656,7 @@ => Inductive (Forall nx [x] -> Forall na a -> SBool) (SBV x -> SList x -> SBV a -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate xs a = result (Forall xs) (Forall a) na = symbolVal (Proxy @na) nxs = symbolVal (Proxy @nx)@@ -502,13 +666,15 @@ xs <- free nxs a <- free na - let ih = internalAxiom "IH" $ \a' -> result (Forall xs) (a' :: Forall na a)- (intros, pSteps) = mkCalcSteps $ steps ih x xs a+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (a' :: Forall na a)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil a- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []." , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a) }@@ -518,7 +684,7 @@ => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate xs a b = result (Forall xs) (Forall a) (Forall b) na = symbolVal (Proxy @na) nb = symbolVal (Proxy @nb)@@ -530,13 +696,15 @@ a <- free na b <- free nb - let ih = internalAxiom "IH" $ \a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b)- (intros, pSteps) = mkCalcSteps $ steps ih x xs a b+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil a b- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []." , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b) }@@ -546,7 +714,7 @@ => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate xs a b c = result (Forall xs) (Forall a) (Forall b) (Forall c) na = symbolVal (Proxy @na) nb = symbolVal (Proxy @nb)@@ -560,13 +728,15 @@ b <- free nb c <- free nc - let ih = internalAxiom "IH" $ \a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)- (intros, pSteps) = mkCalcSteps $ steps ih x xs a b c+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil a b c- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []." , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c) }@@ -576,7 +746,7 @@ => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate xs a b c d = result (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) na = symbolVal (Proxy @na) nb = symbolVal (Proxy @nb)@@ -592,13 +762,15 @@ c <- free nc d <- free nd - let ih = internalAxiom "IH" $ \a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)- (intros, pSteps) = mkCalcSteps $ steps ih x xs a b c d+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil a b c d- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []." , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c d) }@@ -608,7 +780,7 @@ => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z])) where- inductionStrategy result steps = do+ inductionStrategy style result steps = do let predicate xs a b c d e = result (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) na = symbolVal (Proxy @na) nb = symbolVal (Proxy @nb)@@ -626,17 +798,240 @@ d <- free nd e <- free ne - let ih = internalAxiom "IH" $ \a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)- (intros, pSteps) = mkCalcSteps $ steps ih x xs a b c d e+ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' e' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d e pure InductionStrategy {- inductionIntros = intros+ inductionIntros = calcIntros , inductionBaseCase = predicate SL.nil a b c d e- , inductionProofSteps = pSteps+ , inductionProofSteps = calcProofSteps , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []." , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c d e) } +-- | Induction over two lists, simultaneously+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [y] -> SBool)+ (SBV x -> SList x -> SBV y -> SList y -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys = result (Forall xs) (Forall ys)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ result (Forall xs) (Forall ys)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys')+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil .&& predicate SL.nil (y SL..: ys) .&& predicate (x SL..: xs) SL.nil+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys))+ }++-- | Induction over two lists, simultaneously, taking one extra argument+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool)+ (SBV x -> SList x -> SBV y -> SList y -> SBV a -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys a = result (Forall xs) (Forall ys) (Forall a)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys+ na = symbolVal (Proxy @na)++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ a <- free na++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (Forall ys) (a' :: Forall na a)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil a .&& predicate SL.nil (y SL..: ys) a .&& predicate (x SL..: xs) SL.nil a+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a)+ }++-- | Induction over two lists, simultaneously, taking two extra arguments+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)+ (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys a b = result (Forall xs) (Forall ys) (Forall a) (Forall b)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys+ na = symbolVal (Proxy @na)+ nb = symbolVal (Proxy @nb)++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ a <- free na+ b <- free nb++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil a b .&& predicate SL.nil (y SL..: ys) a b .&& predicate (x SL..: xs) SL.nil a b+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b)+ }++-- | Induction over two lists, simultaneously, taking three extra arguments+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> Forall nc c -> SBool)+ (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys a b c = result (Forall xs) (Forall ys) (Forall a) (Forall b) (Forall c)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys+ na = symbolVal (Proxy @na)+ nb = symbolVal (Proxy @nb)+ nc = symbolVal (Proxy @nc)++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ a <- free na+ b <- free nb+ c <- free nc++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil a b c .&& predicate SL.nil (y SL..: ys) a b c .&& predicate (x SL..: xs) SL.nil a b c+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c)+ }++-- | Induction over two lists, simultaneously, taking four extra arguments+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)+ (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys a b c d = result (Forall xs) (Forall ys) (Forall a) (Forall b) (Forall c) (Forall d)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys+ na = symbolVal (Proxy @na)+ nb = symbolVal (Proxy @nb)+ nc = symbolVal (Proxy @nc)+ nd = symbolVal (Proxy @nd)++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ a <- free na+ b <- free nb+ c <- free nc+ d <- free nd++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil a b c d .&& predicate SL.nil (y SL..: ys) a b c d .&& predicate (x SL..: xs) SL.nil a b c d+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c d)+ }++-- | Induction over two lists, simultaneously, taking four extra arguments+instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z)+ => Inductive (Forall nx [x] -> Forall ny [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 -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z]))+ where+ inductionStrategy style result steps = do+ let predicate xs ys a b c d e = result (Forall xs) (Forall ys) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)+ nxs = symbolVal (Proxy @nx)+ nx = singular nxs+ nys = symbolVal (Proxy @ny)+ ny = singular nys+ na = symbolVal (Proxy @na)+ nb = symbolVal (Proxy @nb)+ nc = symbolVal (Proxy @nc)+ nd = symbolVal (Proxy @nd)+ ne = symbolVal (Proxy @ne)++ x <- free nx+ xs <- free nxs++ y <- free ny+ ys <- free nys++ a <- free na+ b <- free nb+ c <- free nc+ d <- free nd+ e <- free ne++ let ih = case style of+ RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' e' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e)+ CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d e++ pure InductionStrategy {+ inductionIntros = calcIntros+ , inductionBaseCase = predicate SL.nil SL.nil a b c d e .&& predicate SL.nil (y SL..: ys) a b c d e .&& predicate (x SL..: xs) SL.nil a b c d e+ , inductionProofSteps = calcProofSteps+ , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"+ , inductiveStep = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c d e)+ }+ -- | Instantiation for a universally quantified variable newtype Inst (nm :: Symbol) a = Inst (SBV a) @@ -683,6 +1078,7 @@ ) => Instantiatable (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e) where 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 -> arg -> Proof instantiate ap p@Proof{getProp, proofName} a = case fromDynamic getProp of Nothing -> cantInstantiate@@ -711,57 +1107,71 @@ | True = '(' : s ++ ")" -- | Helpers for a step-data Helper = HProof Proof -- A previously proven theorem- | HAssum SBool -- A hypothesis+data Helper = HelperProof Proof -- A previously proven theorem+ | HelperAssum SBool -- A hypothesis+ | HelperCase String [SBool] -- Case split +-- | Get proofs from helpers+getHelperProofs :: [Helper] -> [Proof]+getHelperProofs = concatMap get+ where get (HelperProof p) = [p]+ get HelperAssum {} = []+ get HelperCase {} = []++-- | Get proofs from helpers+getHelperAssumes :: [Helper] -> [SBool]+getHelperAssumes = concatMap get+ where get HelperProof {} = []+ get (HelperAssum b) = [b]+ get HelperCase {} = []+ -- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're -- mixing proofs and booleans in one group of hints. hyp :: SBool -> Helper-hyp = HAssum+hyp = HelperAssum -- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're -- mixing proofs and booleans in one group of hints. hprf :: Proof -> Helper-hprf = HProof---- | Get the underlying boolean of a helper-getHelperBool :: Helper -> SBool-getHelperBool (HProof p) = getProof p-getHelperBool (HAssum b) = b+hprf = HelperProof -- | A proof-step with associated helpers-data ProofStep a = ProofStep a [Helper]+data ProofStep a = SingleStep a [Helper] -- | Class capturing giving a proof-step helper class ProofHint a b where -- | Specify a helper for the given proof step- (?) :: a -> b -> ProofStep a- infixl 2 ?+ (??) :: a -> b -> ProofStep a+ infixl 2 ?? -- | Giving just one proof as a helper. instance ProofHint a Proof where- a ? p = ProofStep a [HProof p]+ a ?? p = SingleStep a [HelperProof p] -- | Giving just one boolean as a helper. instance ProofHint a SBool where- a ? p = ProofStep a [HAssum p]+ a ?? p = SingleStep a [HelperAssum p] -- | Giving just one helper instance ProofHint a Helper where- a ? h = ProofStep a [h]+ a ?? h = SingleStep a [h] -- | Giving a bunch of proofs as a helper. instance ProofHint a [Proof] where- a ? ps = ProofStep a (map HProof ps)+ a ?? ps = SingleStep a (map HelperProof ps) -- | Giving a bunch of booleans as a helper. instance ProofHint a [SBool] where- a ? ps = ProofStep a (map HAssum ps)+ a ?? ps = SingleStep a (map HelperAssum ps) -- | Giving a set of helpers instance ProofHint a [Helper] where- a ? hs = ProofStep a hs+ a ?? hs = SingleStep a hs +-- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability+instance ProofHint a String where+ a ?? _ = SingleStep a []+ -- | 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.@@ -785,7 +1195,7 @@ -- | Chaining from a value without any annotation instance ChainStep a [ProofStep a] where- chain x y = ProofStep x [] : y+ chain x y = SingleStep x [] : y -- | Chaining from another proof step instance ChainStep (ProofStep a) [ProofStep a] where@@ -807,3 +1217,12 @@ (⊢) :: [SBool] -> [ProofStep a] -> (SBool, [ProofStep a]) (⊢) = (|-) infixl 0 ⊢++-- | Alternative unicode for `??`:+(⁇) :: ProofHint a b => a -> b -> ProofStep a+(⁇) = (??)+infixl 2 ⁇++-- | Specifying a case-split+cases :: String -> [SBool] -> Helper+cases = HelperCase
Data/SBV/Tools/KnuckleDragger.hs view
@@ -23,17 +23,17 @@ , axiom -- * Basic proofs- , lemma, lemmaWith- , theorem, theoremWith+ , lemma, lemmaWith, theorem, theoremWith -- * Reasoning via calculation- , calc, calcWith- , calcThm, calcThmWith+ , calc, calcWith, calcThm, calcThmWith - -- * Reasoning via induction- , induct, inductWith- , inductThm, inductThmWith+ -- * Reasoning via regular induction+ , induct, inductWith, inductThm, inductThmWith + -- * Reasoning via strong induction+ , sInduct, sInductWith, sInductThm, sInductThmWith+ -- * Creating instances of proofs , at, Inst(..) @@ -50,7 +50,10 @@ , (=:), (≡) -- * Supplying hints for a calculation step- , (?), hprf, hyp+ , (??), (⁇), hprf, hyp++ -- * Case splits+ , cases -- * Finishing up a calculational proof , qed
Data/SBV/Tools/Polynomial.hs view
@@ -47,7 +47,7 @@ -- For instance -- -- @polynomial [0, 1, 3] :: SWord8@- -- + -- -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicians would write this polynomial -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that. polynomial :: [Int] -> a
Data/SBV/Tuple.hs view
@@ -28,6 +28,10 @@ , tuple, untuple -- * Swapping, only for 2-tuples , swap+ -- * Extractors for 2-tuple+ , fst, snd+ -- * Extractors for 3-tuple+ , fst3, snd3, thd3 ) where import GHC.TypeLits@@ -36,6 +40,8 @@ import Data.SBV.Core.Symbolic import Data.SBV.Core.Model +import Prelude hiding (fst, snd)+ -- $setup -- >>> -- For doctest purposes only: -- >>> :set -XTypeApplications@@ -54,6 +60,26 @@ swap :: (SymVal a, SymVal b) => STuple a b -> STuple b a swap t = tuple (b, a) where (a, b) = untuple t++-- | First of a tuple+fst :: (SymVal a, SymVal b) => STuple a b -> SBV a+fst t = a where (a, _) = untuple t++-- | Second of a tuple+snd :: (SymVal a, SymVal b) => STuple a b -> SBV b+snd t = b where (_, b) = untuple t++-- | First of a 3-tuple+fst3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV a+fst3 t = a where (a, _, _) = untuple t++-- | Second of a 3-tuple+snd3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV b+snd3 t = b where (_, b, _) = untuple t++-- | Thirdd of a 3-tuple+thd3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV c+thd3 t = c where (_, _, c) = untuple t -- | Dynamic interface to exporting tuples, this function is not -- exported on purpose; use it only via the field functions '_1', '_2', etc.
Documentation/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -8,7 +8,7 @@ -- -- The PrefixSum algorithm over power-lists and proof of -- the Ladner-Fischer implementation.--- See <http://dl.acm.org/citation.cfm?id=197356>+-- See <https://www.cs.utexas.edu/~misra/psp.dir/powerlist.pdf> -- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>. ----------------------------------------------------------------------------- @@ -33,7 +33,7 @@ ---------------------------------------------------------------------- -- | A poor man's representation of powerlists and--- basic operations on them: <http://dl.acm.org/citation.cfm?id=197356>+-- basic operations on them: <https://www.cs.utexas.edu/~misra/psp.dir/powerlist.pdf>. -- We merely represent power-lists by ordinary lists. type PowerList a = [a] @@ -67,8 +67,7 @@ -- * The Ladner-Fischer parallel version ---------------------------------------------------------------------- --- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>--- or pg. 16 of <http://dl.acm.org/citation.cfm?id=197356>+-- | The Ladner-Fischer (@lf@) implementation of prefix-sum. lf :: (a, a -> a -> a) -> PowerList a -> PowerList a lf _ [] = error "lf: malformed (empty) powerlist" lf _ [x] = [x]
Documentation/SBV/Examples/CodeGeneration/Fibonacci.hs view
@@ -119,7 +119,7 @@ -} -- | Compute the fibonacci numbers statically at /code-generation/ time and--- put them in a table, accessed by the 'select' call. +-- put them in a table, accessed by the 'select' call. fib2 :: SWord64 -> SWord64 -> SWord64 fib2 top = select table 0 where table = map (fib1 top) [0 .. top]
Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -52,7 +53,13 @@ -- Step : 5 Q.E.D. -- Step : 6 Q.E.D. -- Result: Q.E.D.--- Lemma: notDiv3 Q.E.D.+-- Lemma: notDiv3+-- Step 1: Case split 3 ways:+-- Case [1 of 3]: n_mod_3[1] Q.E.D.+-- Case [2 of 3]: n_mod_3[2] Q.E.D.+-- Case [3 of 3]: n_mod_3[3] Q.E.D.+-- Completeness: Q.E.D.+-- Result: Q.E.D. -- [Proven] notDiv3 notDiv3 :: IO Proof notDiv3 = runKD $ do@@ -69,8 +76,8 @@ -- Case 0: n = 0 (mod 3) c0 <- calc "case_n_mod_3_eq_0"- (\(Forall @"n" n) -> n `sEMod` 3 .== 0 .=> p n) $- \n -> [case0 n] |- s n ? case0 n+ (\(Forall @"n" n) -> case0 n .=> p n) $+ \n -> [case0 n] |- s n ?? case0 n =: let w = some "witness" $ \k -> n .== 3*k -- Grab the witness for the case in s (3*w) =: s (3*w)@@ -81,8 +88,8 @@ -- Case 1: n = 1 (mod 3) c1 <- calc "case_n_mod_3_eq_1"- (\(Forall @"n" n) -> n `sEMod` 3 .== 1 .=> p n) $- \n -> [case1 n] |- s n ? case1 n+ (\(Forall @"n" n) -> case1 n .=> p n) $+ \n -> [case1 n] |- s n ?? case1 n =: let w = some "witness" $ \k -> n .== 3*k+1 -- Grab the witness for n being 1 modulo 3 in s (3*w+1) =: 2*(3*w+1)*(3*w+1) + (3*w+1) + 1@@ -94,8 +101,8 @@ -- Case 2: n = 2 (mod 3) c2 <- calc "case_n_mod_3_eq_2"- (\(Forall @"n" n) -> n `sEMod` 3 .== 2 .=> p n) $- \n -> [case2 n] |- s n ? case2 n+ (\(Forall @"n" n) -> case2 n .=> p n) $+ \n -> [case2 n] |- s n ?? case2 n =: let w = some "witness" $ \k -> n .== 3*k+2 -- Grab the witness for n being 2 modulo 3 in s (3*w+2) =: 2*(3*w+2)*(3*w+2) + (3*w+2) + 1@@ -105,6 +112,13 @@ =: 3*(6*w*w + 9*w + 3) + 2 =: qed - -- Note that z3 is smart enough to figure out the above cases are complete, so- -- no extra completeness helper is needed.- lemma "notDiv3" (\(Forall @"n" n) -> p n) [c0, c1, c2]+ calc "notDiv3"+ (\(Forall @"n" n) -> p n) $+ \n -> [] |- p n+ ?? [ cases "n_mod_3" [case0 n, case1 n, case2 n]+ , hprf $ c0 `at` Inst @"n" n+ , hprf $ c1 `at` Inst @"n" n+ , hprf $ c2 `at` Inst @"n" n+ ]+ =: sTrue+ =: qed
+ Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs view
@@ -0,0 +1,225 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.KnuckleDragger.InsertionSort+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Proving insertion-sort correct.+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.KnuckleDragger.InsertionSort where++import Data.SBV+import Data.SBV.Tools.KnuckleDragger++import Prelude hiding (null, length, head, tail, elem)+import Data.SBV.List++-- * Insertion sort++-- | Insert an element into an already sorted list in the correct place.+insert :: SInteger -> SList Integer -> SList Integer+insert = smtFunction "insert" $ \e l -> ite (null l) (singleton e)+ $ let (x, xs) = uncons l+ in ite (e .<= x) (e .: x .: xs) (x .: insert e xs)++-- | Insertion sort, using 'insert' above to successively insert the elements.+insertionSort :: SList Integer -> SList Integer+insertionSort = smtFunction "insertionSort" $ \l -> ite (null l) nil+ $ let (x, xs) = uncons l+ in insert x (insertionSort xs)+++-- * Helper functions++-- | A predicate testing whether a given list is non-decreasing.+nonDecreasing :: SList Integer -> SBool+nonDecreasing = smtFunction "nonDecreasing" $ \l -> null l .|| null (tail l)+ .|| let (x, l') = uncons l+ (y, _) = uncons l'+ in x .<= y .&& nonDecreasing l'++-- | Remove the first occurrence of an number from a list, if any.+removeFirst :: SInteger -> SList Integer -> SList Integer+removeFirst = smtFunction "removeFirst" $ \e l -> ite (null l)+ nil+ (let (x, xs) = uncons l+ in ite (e .== x) xs (x .: removeFirst e xs))++-- | Are two lists permutations of each other?+isPermutation :: SList Integer -> SList Integer -> SBool+isPermutation = smtFunction "isPermutation" $ \l r -> ite (null l)+ (null r)+ (let (x, xs) = uncons l+ in x `elem` r .&& isPermutation xs (removeFirst x r))++-- * Correctness proof++-- | Correctness of insertion-sort.+--+-- We have:+--+-- >>> correctness+-- Lemma: nonDecTail Q.E.D.+-- Inductive lemma: insertNonDecreasing+-- Base: insertNonDecreasing.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Asms: 4 Q.E.D.+-- Step: 4 Q.E.D.+-- Asms: 5 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: insertNonDecreasing.Step Q.E.D.+-- Lemma: insertionSort1 Q.E.D.+-- Inductive lemma: sortNonDecreasing+-- Base: sortNonDecreasing.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: sortNonDecreasing.Step Q.E.D.+-- Lemma: elemITE Q.E.D.+-- Inductive lemma: insertIsElem+-- Base: insertIsElem.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: insertIsElem.Step Q.E.D.+-- Inductive lemma: removeAfterInsert+-- Base: removeAfterInsert.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: removeAfterInsert.Step Q.E.D.+-- Inductive lemma: sortIsPermutation+-- Base: sortIsPermutation.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: sortIsPermutation.Step Q.E.D.+-- Lemma: insertionSortIsCorrect Q.E.D.+-- [Proven] insertionSortIsCorrect+correctness :: IO Proof+correctness = runKD $ do++ --------------------------------------------------------------------------------------------+ -- Part I. Prove that the output of insertion sort is non-decreasing.+ --------------------------------------------------------------------------------------------++ nonDecrTail <- lemma "nonDecTail"+ (\(Forall @"x" x) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs)+ []++ insertNonDecreasing <-+ induct "insertNonDecreasing"+ (\(Forall @"xs" xs) (Forall @"e" e) -> nonDecreasing xs .=> nonDecreasing (insert e xs)) $+ \ih x xs e -> [nonDecreasing (x .: xs)]+ |- nonDecreasing (insert e (x .: xs))+ ?? "unfold insert"+ =: nonDecreasing (ite (e .<= x) (e .: x .: xs) (x .: insert e xs))+ ?? "push nonDecreasing over the ite"+ =: ite (e .<= x) (nonDecreasing (e .: x .: xs))+ (nonDecreasing (x .: insert e xs))+ ?? "unfold nonDecreasing, simplify"+ =: ite (e .<= x)+ (nonDecreasing (x .: xs))+ (nonDecreasing (x .: insert e xs))+ ?? nonDecreasing (x .: xs)+ =: (e .> x .=> nonDecreasing (x .: insert e xs))+ ?? [ hyp (nonDecreasing (x .: xs))+ , hprf (nonDecrTail `at` (Inst @"x" x, Inst @"xs" (insert e xs)))+ , hprf ih+ ]+ =: sTrue+ =: qed+++ -- Unfolding insertion sort just once. This helps z3, which otherwise gets stuck in the following proof.+ is1 <- lemma "insertionSort1" (\(Forall @"x" x) (Forall @"xs" xs) -> insertionSort (x .: xs) .== insert x (insertionSort xs)) []++ sortNonDecreasing <-+ induct "sortNonDecreasing"+ (\(Forall @"xs" xs) -> nonDecreasing (insertionSort xs)) $+ \ih x xs -> [] |- nonDecreasing (insertionSort (x .: xs))+ -- Surprisingly, z3 really needs to be told how to instantiate is1 below so it doesn't get stuck.+ ?? is1 `at` (Inst @"x" x, Inst @"xs" xs)+ =: nonDecreasing (insert x (insertionSort xs))+ ?? [ hprf (insertNonDecreasing `at` (Inst @"xs" (insertionSort xs), Inst @"e" x))+ , hprf ih+ ]+ =: sTrue+ =: qed++ --------------------------------------------------------------------------------------------+ -- Part II. Prove that the output of insertion sort is a permuation of its input+ --------------------------------------------------------------------------------------------++ -- For whatever reason z3 can't figure this out in the below proof. This helper isn't needed for CVC5.+ -- Note that z3 is able to prove this out-of-the box without any helpers, but needs it in the next as a helper.+ elemITE <- lemma "elemITE" (\(Forall @"x" (x :: SInteger)) (Forall @"c" c) (Forall @"t" t) (Forall @"e" e)+ -> x `elem` ite c t e .== ite c (x `elem` t) (x `elem` e))+ []++ insertIsElem <-+ induct "insertIsElem"+ (\(Forall @"xs" xs) (Forall @"e" e) -> e `elem` insert e xs) $+ \ih x xs e -> [] |- e `elem` insert e (x .: xs)+ =: e `elem` ite (e .<= x) (e .: x .: xs) (x .: insert e xs)+ -- z3 has hard time making the following step (though cvc5 is OK with it)+ ?? elemITE `at` (Inst @"x" e, Inst @"c" (e .<= x), Inst @"t" (e .: x .: xs), Inst @"e" (x .: insert e xs))+ =: ite (e .<= x) (e `elem` (e .: x .: xs)) (e `elem` (x .: insert e xs))+ =: ite (e .<= x) sTrue (e `elem` insert e xs) ?? ih+ =: sTrue+ =: qed++ removeAfterInsert <-+ induct "removeAfterInsert"+ (\(Forall @"xs" xs) (Forall @"e" e) -> removeFirst e (insert e xs) .== xs) $+ \ih x xs e -> [] |- removeFirst e (insert e (x .: xs))+ ?? "expand insert"+ =: removeFirst e (ite (e .<= x) (e .: x .: xs) (x .: insert e xs))+ ?? "push removeFirst down the if-then-else"+ =: ite (e .<= x) (removeFirst e (e .: x .: xs)) (removeFirst e (x .: insert e xs))+ ?? "unfold removeFirst, then branch"+ =: ite (e .<= x) (x .: xs) (removeFirst e (x .: insert e xs))+ ?? "unfold removeFirst, else branch. Note that e .== x is False, due to the pre-condition"+ =: ite (e .<= x) (x .: xs) (x .: removeFirst e (insert e xs))+ ?? ih+ =: ite (e .<= x) (x .: xs) (x .: xs)+ ?? "simplify"+ =: x .: xs+ =: qed++ sortIsPermutation <-+ induct "sortIsPermutation"+ (\(Forall @"xs" xs) -> isPermutation xs (insertionSort xs)) $+ \ih x xs -> [] |- isPermutation (x .: xs) (insertionSort (x .: xs))+ =: isPermutation (x .: xs) (insert x (insertionSort xs))+ =: x `elem` insert x (insertionSort xs) .&& isPermutation xs (removeFirst x (insert x (insertionSort xs)))+ ?? insertIsElem+ =: isPermutation xs (removeFirst x (insert x (insertionSort xs)))+ ?? removeAfterInsert+ =: isPermutation xs (insertionSort xs)+ ?? ih+ =: sTrue+ =: qed++ --------------------------------------------------------------------------------------------+ -- Put the two parts together for the final proof+ --------------------------------------------------------------------------------------------+ lemma "insertionSortIsCorrect"+ (\(Forall @"xs" xs) -> let out = insertionSort xs in nonDecreasing out .&& isPermutation xs out)+ [sortNonDecreasing, sortIsPermutation]
Documentation/SBV/Examples/KnuckleDragger/Kleene.hs view
@@ -35,13 +35,13 @@ -- | Star operator over kleene algebras. We're leaving this uninterpreted. star :: SKleene -> SKleene-star = uninterpret "star"+star = uninterpret "STAR" -- | The 'Num' instance for Kleene makes it easy to write regular expressions -- in the more familiar form. instance Num SKleene where- (+) = uninterpret "par"- (*) = uninterpret "seq"+ (+) = uninterpret "PAR"+ (*) = uninterpret "SEQ" abs = error "SKleene: not defined: abs" signum = error "SKleene: not defined: signum"@@ -122,10 +122,10 @@ -- This one requires a chain of reasoning: x* x* == x* star_star_1 <- calc "star_star_1" (\(Forall @"x" (x :: SKleene)) -> star x * star x .== star x) $- \x -> [] |- star x * star x ? unfold- =: (1 + x * star x) * (1 + x * star x) ? kleene- =: (1 + 1) + (x * star x + x * star x) ? par_idem- =: 1 + x * star x ? unfold+ \x -> [] |- star x * star x ?? unfold+ =: (1 + x * star x) * (1 + x * star x) ?? kleene+ =: (1 + 1) + (x * star x + x * star x) ?? par_idem+ =: 1 + x * star x ?? unfold =: star x =: qed
Documentation/SBV/Examples/KnuckleDragger/Lists.hs view
@@ -21,21 +21,27 @@ {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-} -{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}+{-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.KnuckleDragger.Lists where -import Prelude (IO, ($), Integer, Num(..), pure, id, (.), flip)+import Prelude (IO, ($), Integer, Num(..), id, (.), flip) import Data.SBV import Data.SBV.List+import Data.SBV.Tuple import Data.SBV.Tools.KnuckleDragger +import Control.Monad (void)+import Data.Proxy+ #ifndef HADDOCK -- $setup -- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables+-- >>> :set -XTypeApplications -- >>> import Data.SBV+-- >>> import Data.Proxy -- >>> import Control.Exception #endif @@ -122,7 +128,7 @@ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) $ \ih (x :: SA) xs ys -> [] |- reverse ((x .: xs) ++ ys) =: reverse (x .: (xs ++ ys))- =: reverse (xs ++ ys) ++ singleton x ? ih+ =: reverse (xs ++ ys) ++ singleton x ?? ih =: (reverse ys ++ reverse xs) ++ singleton x =: reverse ys ++ (reverse xs ++ singleton x) =: reverse ys ++ reverse (x .: xs)@@ -159,8 +165,8 @@ induct "reverseReverse" (\(Forall @"xs" (xs :: SList A)) -> reverse (reverse xs) .== xs) $ \ih (x :: SA) xs -> [] |- reverse (reverse (x .: xs))- =: reverse (reverse xs ++ singleton x) ? ra- =: reverse (singleton x) ++ reverse (reverse xs) ? ih+ =: reverse (reverse xs ++ singleton x) ?? ra+ =: reverse (singleton x) ++ reverse (reverse xs) ?? ih =: singleton x ++ xs =: x .: xs =: qed@@ -194,9 +200,7 @@ let badLength :: SList Integer -> SInteger badLength xs = ite (length xs .> 5 .&& 42 `elem` xs) 42 (length xs) - lemma "badLengthProof" (\(Forall @"xs" xs) -> observe "imp" (badLength xs) .== observe "spec" (length xs)) []-- pure ()+ void $ lemma "badLengthProof" (\(Forall @"xs" xs) -> observe "imp" (badLength xs) .== observe "spec" (length xs)) [] -- | @length (xs ++ ys) == length xs + length ys@ --@@ -240,7 +244,7 @@ (\(Forall @"xs" xs) -> sNot (all id xs) .== any sNot xs) $ \ih x xs -> [] |- sNot (all id (x .: xs)) =: sNot (x .&& all id xs)- =: (sNot x .|| sNot (all id xs)) ? ih+ =: (sNot x .|| sNot (all id xs)) ?? ih =: sNot x .|| any sNot xs =: any sNot (x .: xs) =: qed@@ -262,7 +266,7 @@ (\(Forall @"xs" xs) -> (2 :: SInteger) `notElem` xs .=> (filter (.> 2) xs .== filter (.>= 2) xs)) $ \ih x xs -> let h = (2 :: SInteger) `notElem` (x .: xs) in [h] |- filter (.> 2) (x .: xs)- =: ite (x .> 2) (x .: filter (.> 2) xs) (filter (.> 2) xs) ? [hyp h, hprf ih]+ =: ite (x .> 2) (x .: filter (.> 2) xs) (filter (.> 2) xs) ?? [hyp h, hprf ih] =: ite (x .> 2) (x .: filter (.>= 2) xs) (filter (.>= 2) xs) =: qed @@ -275,13 +279,42 @@ -- Falsifiable. Counter-example: -- xs = [2] :: [Integer] filterEx2 :: IO ()-filterEx2 = runKD $ do- lemma "filterEx2" (\(Forall @"xs" xs) -> filter (.> (2 :: SInteger)) xs .== filter (.>= 2) xs) []-- pure ()+filterEx2 = runKD $+ void $ lemma "filterEx2" (\(Forall @"xs" xs) -> filter (.> (2 :: SInteger)) xs .== filter (.>= 2) xs) [] -- * Map, append, and reverse +-- | @f = g => map f xs = map g xs@+--+-- >>> mapEquiv+-- Inductive lemma: mapEquiv+-- Base: mapEquiv.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Asms: 2 Q.E.D.+-- Step: 2 Q.E.D.+-- Asms: 3 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: mapEquiv.Step Q.E.D.+-- [Proven] mapEquiv+mapEquiv :: IO Proof+mapEquiv = runKD $ do+ let f, g :: SA -> SB+ f = uninterpret "f"+ g = uninterpret "g"++ f'eq'g :: SBool+ f'eq'g = quantifiedBool $ \(Forall @"x" x) -> f x .== g x++ induct "mapEquiv"+ (\(Forall @"xs" xs) -> f'eq'g .=> map f xs .== map g xs) $+ \ih x xs -> [f'eq'g] |- map f (x .: xs) .== map g (x .: xs)+ =: f x .: map f xs .== g x .: map g xs ?? f'eq'g+ =: f x .: map f xs .== f x .: map g xs ?? [hyp f'eq'g, hprf ih]+ =: f x .: map f xs .== f x .: map f xs+ =: map f (x .: xs) .== map f (x .: xs)+ =: qed+ -- | @map f (xs ++ ys) == map f xs ++ map f ys@ -- -- >>> mapAppend (uninterpret "f")@@ -300,7 +333,7 @@ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" ys) -> map f (xs ++ ys) .== map f xs ++ map f ys) $ \ih x xs ys -> [] |- map f ((x .: xs) ++ ys) =: map f (x .: (xs ++ ys))- =: f x .: map f (xs ++ ys) ? ih+ =: f x .: map f (xs ++ ys) ?? ih =: f x .: (map f xs ++ map f ys) =: (f x .: map f xs) ++ map f ys =: map f (x .: xs) ++ map f ys@@ -339,9 +372,9 @@ (\(Forall @"xs" xs) -> reverse (map f xs) .== map f (reverse xs)) $ \ih x xs -> [] |- reverse (map f (x .: xs)) =: reverse (f x .: map f xs)- =: reverse (map f xs) ++ singleton (f x) ? ih+ =: reverse (map f xs) ++ singleton (f x) ?? ih =: map f (reverse xs) ++ singleton (f x)- =: map f (reverse xs) ++ map f (singleton x) ? mApp+ =: map f (reverse xs) ++ map f (singleton x) ?? mApp =: map f (reverse xs ++ singleton x) =: map f (reverse (x .: xs)) =: qed@@ -367,7 +400,7 @@ (\(Forall @"xs" (xs :: SList A)) -> length (reverse xs) .== length xs) $ \ih (x :: SA) xs -> [] |- length (reverse (x .: xs)) =: length (reverse xs ++ singleton x)- =: length (reverse xs) + length (singleton x) ? ih+ =: length (reverse xs) + length (singleton x) ?? ih =: length xs + 1 =: length (x .: xs) =: qed@@ -385,10 +418,8 @@ -- Falsifiable. Counter-example: -- xs = [A_1,A_2,A_1] :: [A] badRevLen :: IO ()-badRevLen = runKD $ do- lemma "badRevLen" (\(Forall @"xs" (xs :: SList A)) -> length (reverse xs) .== ite (length xs .== 3) 5 (length xs)) []-- pure ()+badRevLen = runKD $+ void $ lemma "badRevLen" (\(Forall @"xs" (xs :: SList A)) -> length (reverse xs) .== ite (length xs .== 3) 5 (length xs)) [] -- * Foldr-map fusion @@ -420,7 +451,7 @@ (\(Forall @"xs" xs) -> foldr f a (map g xs) .== foldr (f . g) a xs) $ \ih x xs -> [] |- foldr f a (map g (x .: xs)) =: foldr f a (g x .: map g xs)- =: g x `f` foldr f a (map g xs) ? ih+ =: g x `f` foldr f a (map g xs) ?? ih =: g x `f` foldr (f . g) a xs =: foldr (f . g) a (x .: xs) =: qed@@ -469,8 +500,8 @@ induct "foldrFusion" (\(Forall @"xs" xs) -> h1 .&& h2 .=> f (foldr g a xs) .== foldr h b xs) $ \ih x xs -> [h1, h2] |- f (foldr g a (x .: xs))- =: f (g x (foldr g a xs)) ? h2- =: h x (f (foldr g a xs)) ? [hyp h1, hyp h2, hprf ih]+ =: f (g x (foldr g a xs)) ?? h2+ =: h x (f (foldr g a xs)) ?? [hyp h1, hyp h2, hprf ih] =: h x (foldr h b xs) =: foldr h b (x .: xs) =: qed@@ -502,7 +533,7 @@ (\(Forall @"xs" xs) (Forall @"ys" ys) -> foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs) $ \ih x xs ys -> [] |- foldr f a ((x .: xs) ++ ys) =: foldr f a (x .: (xs ++ ys))- =: x `f` foldr f a (xs ++ ys) ? ih+ =: x `f` foldr f a (xs ++ ys) ?? ih =: x `f` foldr f (foldr f a ys) xs =: foldr f (foldr f a ys) (x .: xs) =: qed@@ -523,13 +554,14 @@ -- [Proven] foldlOverAppend foldlOverAppend :: (SB -> SA -> SB) -> IO Proof foldlOverAppend f = runKD $- -- z3 is smart enough to instantiate the IH correctly below, and the at clause isn't necessary. But we're being- -- explicit here to emphasize that the IH is used at a different value of a. induct "foldlOverAppend" (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"a" a) -> foldl f a (xs ++ ys) .== foldl f (foldl f a xs) ys) $ \ih x xs ys a -> [] |- foldl f a ((x .: xs) ++ ys) =: foldl f a (x .: (xs ++ ys))- =: foldl f (a `f` x) (xs ++ ys) ? ih `at` (Inst @"ys" ys, Inst @"a" (a `f` x))+ =: foldl f (a `f` x) (xs ++ ys)+ -- z3 is smart enough to instantiate the IH correctly below, but we're+ -- using an explicit instantiation to be clear about the use of @a@ at a different value+ ?? ih `at` (Inst @"ys" ys, Inst @"a" (a `f` x)) =: foldl f (foldl f (a `f` x) xs) ys =: qed @@ -568,10 +600,10 @@ \ih x xs e -> let ff = flip f rxs = reverse xs- in [] |- foldr f e (x .: xs) =: x `f` foldr f e xs ? ih+ in [] |- foldr f e (x .: xs) =: x `f` foldr f e xs ?? ih =: x `f` foldl ff e rxs =: foldl ff e rxs `ff` x- =: foldl ff (foldl ff e rxs) (singleton x) ? foa+ =: foldl ff (foldl ff e rxs) (singleton x) ?? foa =: foldl ff e (rxs ++ singleton x) =: foldl ff e (reverse (x .: xs)) =: qed@@ -637,8 +669,10 @@ helper <- induct "helper" (\(Forall @"xs" xs) (Forall @"y" y) (Forall @"z" z) -> assoc .=> foldl (@) (y @ z) xs .== y @ foldl (@) z xs) $ \ih x xs y z -> [assoc] |- foldl (@) (y @ z) (x .: xs)- =: foldl (@) ((y @ z) @ x) xs ? assoc- =: foldl (@) (y @ (z @ x)) xs ? [hyp assoc, hprf (ih `at` (Inst @"y" y, Inst @"z" (z @ x)))]+ =: foldl (@) ((y @ z) @ x) xs+ ?? assoc+ =: foldl (@) (y @ (z @ x)) xs+ ?? [hyp assoc, hprf (ih `at` (Inst @"y" y, Inst @"z" (z @ x)))] =: y @ foldl (@) (z @ x) xs =: y @ foldl (@) z (x .: xs) =: qed@@ -646,10 +680,10 @@ induct "foldrFoldlDuality" (\(Forall @"xs" xs) -> assoc .&& lunit .&& runit .=> foldr (@) e xs .== foldl (@) e xs) $ \ih x xs -> [assoc, lunit, runit] |- foldr (@) e (x .: xs)- =: x @ foldr (@) e xs ? [hyp assoc, hyp lunit, hyp runit, hprf ih]- =: x @ foldl (@) e xs ? [hyp assoc, hprf helper]- =: foldl (@) (x @ e) xs ? runit- =: foldl (@) x xs ? lunit+ =: x @ foldr (@) e xs ?? [hyp assoc, hyp lunit, hyp runit, hprf ih]+ =: x @ foldl (@) e xs ?? [hyp assoc, hprf helper]+ =: foldl (@) (x @ e) xs ?? runit+ =: foldl (@) x xs ?? lunit =: foldl (@) (e @ x) xs =: foldl (@) e (x .: xs) =: qed@@ -721,8 +755,8 @@ -- Using z to avoid confusion with the variable x already present, following Bird. -- z3 can figure out the proper instantiation of ih so the at call is unnecessary, but being explicit is helpful. \ih z xs x y -> [assoc] |- x <+> foldl (<*>) y (z .: xs)- =: x <+> foldl (<*>) (y <*> z) xs ? [hyp assoc, hprf (ih `at` (Inst @"x" x, Inst @"y" (y <*> z)))]- =: foldl (<*>) (x <+> (y <*> z)) xs ? assoc+ =: x <+> foldl (<*>) (y <*> z) xs ?? [hyp assoc, hprf (ih `at` (Inst @"x" x, Inst @"y" (y <*> z)))]+ =: foldl (<*>) (x <+> (y <*> z)) xs ?? assoc =: foldl (<*>) ((x <+> y) <*> z) xs =: foldl (<*>) (x <+> y) (z .: xs) =: qed@@ -731,9 +765,9 @@ induct "foldrFoldl" (\(Forall @"xs" xs) -> assoc .&& unit .=> foldr (<+>) e xs .== foldl (<*>) e xs) $ \ih x xs -> [assoc, unit] |- foldr (<+>) e (x .: xs)- =: x <+> foldr (<+>) e xs ? [hyp assoc, hyp unit, hprf ih]- =: x <+> foldl (<*>) e xs ? [hyp assoc, hprf helper]- =: foldl (<*>) (x <+> e) xs ? unit+ =: x <+> foldr (<+>) e xs ?? [hyp assoc, hyp unit, hprf ih]+ =: x <+> foldl (<*>) e xs ?? [hyp assoc, hprf helper]+ =: foldl (<*>) (x <+> e) xs ?? unit =: foldl (<*>) (e <*> x) xs =: foldl (<*>) e (x .: xs) =: qed@@ -823,8 +857,8 @@ helper <- induct "foldBase" (\(Forall @"xs" xs) (Forall @"y" y) -> lUnit .&& assoc .=> foldr f y xs .== foldr f a xs `f` y) $ \ih x xs y -> [lUnit, assoc] |- foldr f y (x .: xs)- =: x `f` foldr f y xs ? [hyp lUnit, hyp assoc, hprf ih]- =: x `f` (foldr f a xs `f` y) ? assoc+ =: x `f` foldr f y xs ?? [hyp lUnit, hyp assoc, hprf ih]+ =: x `f` (foldr f a xs `f` y) ?? assoc =: (x `f` foldr f a xs) `f` y =: foldr f a (x .: xs) `f` y =: qed@@ -834,9 +868,9 @@ induct "bookKeeping" (\(Forall @"xss" xss) -> assoc .&& rUnit .&& lUnit .=> foldr f a (concat xss) .== foldr f a (mapFoldr a xss)) $ \ih xs xss -> [assoc, rUnit, lUnit] |- foldr f a (concat (xs .: xss))- =: foldr f a (xs ++ concat xss) ? foa- =: foldr f (foldr f a (concat xss)) xs ? [hyp assoc, hyp rUnit, hyp lUnit, hprf ih]- =: foldr f (foldr f a (mapFoldr a xss)) xs ? [hyp lUnit, hyp assoc, hprf (helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (mapFoldr a xss))))]+ =: foldr f a (xs ++ concat xss) ?? foa+ =: foldr f (foldr f a (concat xss)) xs ?? [hyp assoc, hyp rUnit, hyp lUnit, hprf ih]+ =: foldr f (foldr f a (mapFoldr a xss)) xs ?? [hyp lUnit, hyp assoc, hprf (helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (mapFoldr a xss))))] =: foldr f a xs `f` foldr f a (mapFoldr a xss) =: foldr f a (foldr f a xs .: mapFoldr a xss) =: foldr f a (mapFoldr a (xs .: xss))@@ -864,7 +898,7 @@ (\(Forall @"xs" xs) (Forall @"ys" ys) -> filter p xs ++ filter p ys .== filter p (xs ++ ys)) $ \ih x xs ys -> [] |- filter p (x .: xs) ++ filter p ys =: ite (p x) (x .: filter p xs) (filter p xs) ++ filter p ys- =: ite (p x) (x .: filter p xs ++ filter p ys) (filter p xs ++ filter p ys) ? ih+ =: ite (p x) (x .: filter p xs ++ filter p ys) (filter p xs ++ filter p ys) ?? ih =: ite (p x) (x .: filter p (xs ++ ys)) (filter p (xs ++ ys)) =: filter p (x .: (xs ++ ys)) =: filter p ((x .: xs) ++ ys)@@ -913,8 +947,8 @@ induct "filterConcat" (\(Forall @"xss" xss) -> filter p (concat xss) .== concatMapFilter p xss) $ \ih xs xss -> [] |- filter p (concat (xs .: xss))- =: filter p (xs ++ concat xss) ? fa- =: filter p xs ++ filter p (concat xss) ? ih+ =: filter p (xs ++ concat xss) ?? fa+ =: filter p xs ++ filter p (concat xss) ?? ih =: filter p xs ++ concatMapFilter p xss =: concatMapFilter p (xs .: xss) =: qed@@ -950,13 +984,480 @@ p :: SA -> SBool p = uninterpret "p" - lemma "badMapFilter"- (\(Forall @"xs" xs) -> observe "lhs" (map f (filter p xs)) .== observe "rhs" (filter p (map f xs)))+ void $ lemma "badMapFilter"+ (\(Forall @"xs" xs) -> observe "lhs" (map f (filter p xs)) .== observe "rhs" (filter p (map f xs)))+ []++-- * Partition++-- | @fst (partition f xs) == filter f xs@+--+-- >>> partition1+-- Inductive lemma: partition1+-- Base: partition1.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: partition1.Step Q.E.D.+-- [Proven] partition1+partition1 :: IO Proof+partition1 = runKD $ do+ let f :: SA -> SBool+ f = uninterpret "f"++ induct "partition1"+ (\(Forall @"xs" xs) -> fst (partition f xs) .== filter f xs) $+ \ih x xs -> [] |- fst (partition f (x .: xs))+ =: fst (let res = partition f xs+ in ite (f x)+ (tuple (x .: fst res, snd res))+ (tuple (fst res, x .: snd res)))+ =: ite (f x) (x .: fst (partition f xs)) (fst (partition f xs)) ?? ih+ =: ite (f x) (x .: filter f xs) (filter f xs)+ =: filter f (x .: xs)+ =: qed++-- | @snd (partition f xs) == filter (not . f) xs@+--+-- >>> partition2+-- Inductive lemma: partition2+-- Base: partition2.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: partition2.Step Q.E.D.+-- [Proven] partition2+partition2 :: IO Proof+partition2 = runKD $ do+ let f :: SA -> SBool+ f = uninterpret "f"++ induct "partition2"+ (\(Forall @"xs" xs) -> snd (partition f xs) .== filter (sNot . f) xs) $+ \ih x xs -> [] |- snd (partition f (x .: xs))+ =: snd (let res = partition f xs+ in ite (f x)+ (tuple (x .: fst res, snd res))+ (tuple (fst res, x .: snd res)))+ =: ite (f x) (snd (partition f xs)) (x .: snd (partition f xs)) ?? ih+ =: ite (f x) (filter (sNot . f) xs) (x .: filter (sNot . f) xs)+ =: filter (sNot . f) (x .: xs)+ =: qed++-- * Take and drop++-- | @take n (take m xs) = take (n `smin` m) xs@+--+-- >>> take_take+-- Lemma: take_take Q.E.D.+-- [Proven] take_take+take_take :: IO Proof+take_take = runKD $+ lemma "take_take"+ (\(Forall @"xs" (xs :: SList A)) (Forall @"m" m) (Forall @"n" n) -> take n (take m xs) .== take (n `smin` m) xs)+ []+++-- | @n >= 0 && m >= 0 => drop n (drop m xs) = drop (n + m) xs@+--+-- >>> drop_drop+-- Lemma: drop_drop Q.E.D.+-- [Proven] drop_drop+drop_drop :: IO Proof+drop_drop = runKD $+ lemma "drop_drop"+ (\(Forall @"n" n) (Forall @"m" m) (Forall @"xs" (xs :: SList A)) ->+ n .>= 0 .&& m .>= 0 .=> drop n (drop m xs) .== drop (n + m) xs) [] - pure ()+-- | @take n xs ++ drop n xs == xs@+--+-- >>> take_drop+-- Lemma: take_drop Q.E.D.+-- [Proven] take_drop+take_drop :: IO Proof+take_drop = runKD $+ lemma "take_drop"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) -> take n xs ++ drop n xs .== xs)+ [] +-- | @n .> 0 => take n (x .: xs) = x .: take (n - 1) xs@+--+-- >>> take_cons+-- Lemma: take_cons Q.E.D.+-- [Proven] take_cons+take_cons :: IO Proof+take_cons = runKD $+ lemma "take_cons"+ (\(Forall @"n" n) (Forall @"x" x) (Forall @"xs" (xs :: SList A)) -> n .> 0 .=> take n (x .: xs) .== x .: take (n - 1) xs)+ []++-- | @take n (map f xs) == map f (take n xs)@+--+-- >>> take_map+-- Lemma: take_cons Q.E.D.+-- Lemma: map1 Q.E.D.+-- Lemma: take_map.n <= 0 Q.E.D.+-- Inductive lemma: take_map.n > 0+-- Base: take_map.n > 0.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Asms: 2 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Asms: 5 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: take_map.n > 0.Step Q.E.D.+-- Lemma: take_map Q.E.D.+-- [Proven] take_map+take_map :: IO Proof+take_map = runKD $ do+ let f :: SA -> SB+ f = uninterpret "f"++ tc <- use take_cons+ map1 <- lemma "map1" (\(Forall @"x" x) (Forall @"xs" xs) -> map f (x .: xs) .== f x .: map f xs) []++ h1 <- lemma "take_map.n <= 0"+ (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> take n (map f xs) .== map f (take n xs))+ []++ h2 <- induct "take_map.n > 0"+ (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> take n (map f xs) .== map f (take n xs)) $+ \ih x xs n -> [n .> 0] |- take n (map f (x .: xs))+ =: take n (f x .: map f xs) ?? n .> 0+ =: f x .: take (n - 1) (map f xs) ?? ih `at` Inst @"n" (n-1)+ =: f x .: map f (take (n - 1) xs) ?? map1 `at` (Inst @"x" x, Inst @"xs" (take (n - 1) xs))+ =: map f (x .: take (n - 1) xs) ?? [hyp (n .> 0), hprf tc]+ =: map f (take n (x .: xs))+ =: qed++ lemma "take_map" (\(Forall @"xs" xs) (Forall @"n" n) -> take n (map f xs) .== map f (take n xs)) [h1, h2]++-- | @n .> 0 => drop n (x .: xs) = drop (n - 1) xs@+--+-- >>> drop_cons (Proxy @A)+-- Lemma: drop_cons Q.E.D.+-- [Proven] drop_cons+drop_cons :: forall elt. SymVal elt => Proxy elt -> IO Proof+drop_cons _ = runKD $+ lemma "drop_cons"+ (\(Forall @"n" n) (Forall @"x" x) (Forall @"xs" (xs :: SList elt)) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs)+ []++-- | @drop n (map f xs) == map f (drop n xs)@+--+-- >>> drop_map+-- Lemma: drop_cons Q.E.D.+-- Lemma: drop_cons Q.E.D.+-- Lemma: drop_map.n <= 0 Q.E.D.+-- Inductive lemma: drop_map.n > 0+-- Base: drop_map.n > 0.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Asms: 2 Q.E.D.+-- Step: 2 Q.E.D.+-- Asms: 3 Q.E.D.+-- Step: 3 Q.E.D.+-- Asms: 4 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: drop_map.n > 0.Step Q.E.D.+-- Lemma: drop_map+-- Step : 1 Q.E.D.+-- Step : 2 Q.E.D.+-- Step : 3 Q.E.D.+-- Step : 4 Q.E.D.+-- Result: Q.E.D.+-- [Proven] drop_map+drop_map :: IO Proof+drop_map = runKD $ do+ let f :: SA -> SB+ f = uninterpret "f"++ dcA <- use $ drop_cons (Proxy @A)+ dcB <- use $ drop_cons (Proxy @B)++ h1 <- lemma "drop_map.n <= 0"+ (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> drop n (map f xs) .== map f (drop n xs))+ []++ h2 <- induct "drop_map.n > 0"+ (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> drop n (map f xs) .== map f (drop n xs)) $+ \ih x xs n -> [n .> 0] |- drop n (map f (x .: xs))+ =: drop n (f x .: map f xs)+ ?? [hyp (n .> 0), hprf (dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs)))]+ =: drop (n - 1) (map f xs)+ ?? [hyp (n .> 0), hprf (ih `at` Inst @"n" (n-1))]+ =: map f (drop (n - 1) xs)+ ?? [hyp (n .> 0), hprf (dcA `at` (Inst @"n" n, Inst @"x" x, Inst @"xs" xs))]+ =: map f (drop n (x .: xs))+ =: qed++ -- I'm a bit surprised that z3 can't deduce the following with a simple-lemma, which is essentially a simple case-split.+ -- But the good thing about calc is that it lets us direct the tool in precise ways that we'd like.+ calc "drop_map"+ (\(Forall @"xs" xs) (Forall @"n" n) -> drop n (map f xs) .== map f (drop n xs)) $+ \xs n -> [] |- let result = drop n (map f xs) .== map f (drop n xs)+ in result+ =: ite (n .<= 0) (n .<= 0 .=> result) (n .> 0 .=> result) ?? h1+ =: ite (n .<= 0) sTrue (n .> 0 .=> result) ?? h2+ =: ite (n .<= 0) sTrue sTrue+ =: sTrue+ =: qed++-- | @n >= 0 ==> length (take n xs) = length xs \`min\` n@+--+-- >>> length_take+-- Lemma: length_take Q.E.D.+-- [Proven] length_take+length_take :: IO Proof+length_take = runKD $+ lemma "length_take"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) -> n .>= 0 .=> length (take n xs) .== length xs `smin` n)+ []++-- | @n >= 0 ==> length (drop n xs) = (length xs - n) \`max\` 0@+--+-- >>> length_drop+-- Lemma: length_drop Q.E.D.+-- [Proven] length_drop+length_drop :: IO Proof+length_drop = runKD $+ lemma "length_drop"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) -> n .>= 0 .=> length (drop n xs) .== (length xs - n) `smax` 0)+ []++-- | @length xs \<= n ==\> take n xs == xs@+--+-- >>> take_all+-- Lemma: take_all Q.E.D.+-- [Proven] take_all+take_all :: IO Proof+take_all = runKD $+ lemma "take_all"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) -> length xs .<= n .=> take n xs .== xs)+ []++-- | @length xs \<= n ==\> drop n xs == nil@+--+-- >>> drop_all+-- Lemma: drop_all Q.E.D.+-- [Proven] drop_all+drop_all :: IO Proof+drop_all = runKD $+ lemma "drop_all"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) -> length xs .<= n .=> drop n xs .== nil)+ []++-- | @take n (xs ++ ys) = (take n xs ++ take (n - length xs) ys)@+--+-- >>> take_append+-- Lemma: take_append+-- Step : 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] take_append+take_append :: IO Proof+take_append = runKD $+ calc "take_append"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) (Forall @"ys" ys) -> take n (xs ++ ys) .== take n xs ++ take (n - length xs) ys) $++ -- z3 requires an explicit split here on xs. cvc5 actually proves this out-of-the-box without any helping steps.+ \n (xs :: SList A) ys -> [] |- take n (xs ++ ys)+ ?? "case split on xs"+ =: ite (null xs)+ (take n ys)+ (take n (head xs .: (tail xs ++ ys)))+ =: qed++-- | @drop n (xs ++ ys) = drop n xs ++ drop (n - length xs) ys@+--+-- NB. As of Feb 2025, z3 struggles to prove this, but cvc5 gets it out-of-the-box.+--+-- >>> drop_append+-- Lemma: drop_append Q.E.D.+-- [Proven] drop_append+drop_append :: IO Proof+drop_append = runKD $+ lemmaWith cvc5 "drop_append"+ (\(Forall @"n" n) (Forall @"xs" (xs :: SList A)) (Forall @"ys" ys) -> drop n (xs ++ ys) .== drop n xs ++ drop (n - length xs) ys)+ []++-- * Summing via halving++-- | We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses+-- strong induction. We have:+--+-- >>> sumHalves+-- Inductive lemma: sumAppend+-- Base: sumAppend.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: sumAppend.Step Q.E.D.+-- Inductive lemma (strong): sumHalves+-- Base: sumHalves.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: sumHalves.Step Q.E.D.+-- [Proven] sumHalves+sumHalves :: IO Proof+sumHalves = runKD $ do++ let halvingSum :: SList Integer -> SInteger+ halvingSum = smtFunction "halvingSum" $ \xs -> ite (null xs .|| null (tail xs))+ (sum xs)+ (let (f, s) = splitAt (length xs `sDiv` 2) xs+ in halvingSum f + halvingSum s)++ sum :: SList Integer -> SInteger+ sum = smtFunction "sum" $ \xs -> ite (null xs) 0 (head xs + sum (tail xs))++ helper <- induct "sumAppend"+ (\(Forall @"xs" xs) (Forall @"ys" ys) -> sum (xs ++ ys) .== sum xs + sum ys) $+ \ih x xs ys -> [] |- sum (x .: xs ++ ys)+ =: x + sum (xs ++ ys)+ ?? ih+ =: x + sum xs + sum ys+ =: sum (x .: xs) + sum ys+ =: qed++ -- Use strong induction to prove the theorem. CVC5 solves this with ease, but z3 struggles.+ sInductWith cvc5 "sumHalves"+ (\(Forall @"xs" xs) -> halvingSum xs .== sum xs) $+ \ih x xs -> [] |- halvingSum (x .: xs)+ =: let (f, s) = splitAt (length (x .: xs) `sDiv` 2) (x .: xs)+ in halvingSum f + halvingSum s+ ?? ih `at` Inst @"xs" f+ =: sum f + halvingSum s+ ?? ih `at` Inst @"xs" s+ =: sum f + sum s+ ?? helper `at` (Inst @"xs" f, Inst @"ys" s)+ =: sum (f ++ s)+ ?? "simplify"+ =: sum (x .: xs)+ =: qed++-- * Zip++-- | @length xs = length ys ⟹ map fst (zip xs ys) = xs@+--+-- >>> map_fst_zip+-- Inductive lemma: map_fst_zip+-- Base: map_fst_zip.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Asms: 4 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: map_fst_zip.Step Q.E.D.+-- [Proven] map_fst_zip+map_fst_zip :: IO Proof+map_fst_zip = runKD $+ induct "map_fst_zip"+ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" (ys :: SList B)) -> length xs .== length ys .=> map fst (zip xs ys) .== xs) $+ \ih (x :: SA) xs (y :: SB) ys -> [length (x .: xs) .== length (y .: ys)]+ |- map fst (zip (x .: xs) (y .: ys))+ =: map fst (tuple (x, y) .: zip xs ys)+ =: fst (tuple (x, y)) .: map fst (zip xs ys)+ =: x .: map fst (zip xs ys)+ ?? [hprf ih, hyp (length xs .== length ys)]+ =: x .: xs+ =: qed++-- | @length xs = length ys ⟹ map snd (zip xs ys) = xs@+--+-- >>> map_snd_zip+-- Inductive lemma: map_snd_zip+-- Base: map_snd_zip.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Asms: 4 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: map_snd_zip.Step Q.E.D.+-- [Proven] map_snd_zip+map_snd_zip :: IO Proof+map_snd_zip = runKD $+ induct "map_snd_zip"+ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" (ys :: SList B)) -> length xs .== length ys .=> map snd (zip xs ys) .== ys) $+ \ih (x :: SA) xs (y :: SB) ys -> [length (x .: xs) .== length (y .: ys)]+ |- map snd (zip (x .: xs) (y .: ys))+ =: map snd (tuple (x, y) .: zip xs ys)+ =: snd (tuple (x, y)) .: map snd (zip xs ys)+ =: y .: map snd (zip xs ys)+ ?? [hprf ih, hyp (length xs .== length ys)]+ =: y .: ys+ =: qed++-- | @map fst (zip xs ys) = take (min (length xs) (length ys)) xs@+--+-- >>> map_fst_zip_take+-- Lemma: take_cons Q.E.D.+-- Inductive lemma: map_fst_zip_take+-- Base: map_fst_zip_take.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: map_fst_zip_take.Step Q.E.D.+-- [Proven] map_fst_zip_take+map_fst_zip_take :: IO Proof+map_fst_zip_take = runKD $ do+ tc <- use take_cons++ induct "map_fst_zip_take"+ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" (ys :: SList B)) -> map fst (zip xs ys) .== take (length xs `smin` length ys) xs) $+ \ih (x :: SA) xs (y :: SB) ys -> []+ |- map fst (zip (x .: xs) (y .: ys))+ =: map fst (tuple (x, y) .: zip xs ys)+ =: x .: map fst (zip xs ys)+ ?? ih+ =: x .: take (length xs `smin` length ys) xs+ ?? tc+ =: take (1 + (length xs `smin` length ys)) (x .: xs)+ =: take (length (x .: xs) `smin` length (y .: ys)) (x .: xs)+ =: qed++-- | @map snd (zip xs ys) = take (min (length xs) (length ys)) xs@+--+-- >>> map_snd_zip_take+-- Lemma: take_cons Q.E.D.+-- Inductive lemma: map_snd_zip_take+-- Base: map_snd_zip_take.Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: map_snd_zip_take.Step Q.E.D.+-- [Proven] map_snd_zip_take+map_snd_zip_take :: IO Proof+map_snd_zip_take = runKD $ do+ tc <- use take_cons++ induct "map_snd_zip_take"+ (\(Forall @"xs" (xs :: SList A)) (Forall @"ys" (ys :: SList B)) -> map snd (zip xs ys) .== take (length xs `smin` length ys) ys) $+ \ih (x :: SA) xs (y :: SB) ys -> []+ |- map snd (zip (x .: xs) (y .: ys))+ =: map snd (tuple (x, y) .: zip xs ys)+ =: y .: map snd (zip xs ys)+ ?? ih+ =: y .: take (length xs `smin` length ys) ys+ ?? tc+ =: take (1 + (length xs `smin` length ys)) (y .: ys)+ =: take (length (x .: xs) `smin` length (y .: ys)) (y .: ys)+ =: qed+ {- HLint ignore reverseReverse "Redundant reverse" -} {- HLint ignore allAny "Use and" -} {- HLint ignore foldrMapFusion "Fuse foldr/map" -} {- HLint ignore filterConcat "Move filter" -}+{- HLint ignore module "Use camelCase" -}+{- HLint ignore module "Use first" -}+{- HLint ignore module "Use second" -}+{- HLint ignore module "Use zipWith" -}
Documentation/SBV/Examples/KnuckleDragger/Numeric.hs view
@@ -51,12 +51,12 @@ induct "sumConst_correct" (\(Forall @"n" n) -> n .>= 0 .=> sum n .== spec n) $- \ih k -> [k .>= 0] |- sum (k+1) ? k .>= 0- =: c + sum k ? [hprf ih, hyp (k .>= 0)]- =: c + spec k- =: c + c*k- =: c*(k+1)- =: spec (k+1)+ \ih n -> [n .>= 0] |- sum (n+1) ?? n .>= 0+ =: c + sum n ?? [hprf ih, hyp (n .>= 0)]+ =: c + spec n+ =: c + c*n+ =: c*(n+1)+ =: spec (n+1) =: qed -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@.@@ -86,10 +86,10 @@ inductWith cvc5 "sum_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $- \ih k -> [k .>= 0] |- sum (k+1) ? k .>= 0- =: k+1 + sum k ? [hprf ih, hyp (k .>= 0)]- =: k+1 + spec k- =: spec (k+1)+ \ih n -> [n .>= 0] |- sum (n+1) ?? n .>= 0+ =: n+1 + sum n ?? [hprf ih, hyp (n .>= 0)]+ =: n+1 + spec n+ =: spec (n+1) =: qed -- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@.@@ -119,10 +119,10 @@ inductWith cvc5 "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $- \ih k -> [k .>= 0] |- sumSquare (k+1) ? k .>= 0- =: (k+1)*(k+1) + sumSquare k ? [hprf ih, hyp (k .>= 0)]- =: (k+1)*(k+1) + spec k- =: spec (k+1)+ \ih n -> [n .>= 0] |- sumSquare (n+1) ?? n .>= 0+ =: (n+1)*(n+1) + sumSquare n ?? [hprf ih, hyp (n .>= 0)]+ =: (n+1)*(n+1) + spec n+ =: spec (n+1) =: qed -- | Prove that @11^n - 4^n@ is always divisible by 7.@@ -161,15 +161,18 @@ inductWith cvc5 "elevenMinusFour" (\(Forall @"n" n) -> n .>= 0 .=> emf n) $- \ih k -> [k .>= 0]- |- emf (k+1)- =: 7 `sDivides` (11 `pow` (k+1) - 4 `pow` (k+1)) ? [hyp (k .>= 0), hprf (powN `at` (Inst @"x" (11 :: SInteger), Inst @"n" k))]- =: 7 `sDivides` (11 * 11 `pow` k - 4 `pow` (k+1)) ? [hyp (k .>= 0), hprf (powN `at` (Inst @"x" ( 4 :: SInteger), Inst @"n" k))]- =: 7 `sDivides` (11 * 11 `pow` k - 4 * 4 `pow` k)- =: 7 `sDivides` (7 * 11 `pow` k + 4 * 11 `pow` k - 4 * 4 `pow` k)- =: 7 `sDivides` (7 * 11 `pow` k + 4 * (11 `pow` k - 4 `pow` k)) ? [hyp (k .>= 0), hprf ih]- =: let x = some "x" (\v -> 7*v .== 11 `pow` k - 4 `pow` k) -- Apply the IH and grab the witness for it- in 7 `sDivides` (7 * 11 `pow` k + 4 * 7 * x)- =: 7 `sDivides` (7 * (11 `pow` k + 4 * x))+ \ih n -> [n .>= 0]+ |- emf (n+1)+ =: 7 `sDivides` (11 `pow` (n+1) - 4 `pow` (n+1))+ ?? [hyp (n .>= 0), hprf (powN `at` (Inst @"x" (11 :: SInteger), Inst @"n" n))]+ =: 7 `sDivides` (11 * 11 `pow` n - 4 `pow` (n+1))+ ?? [hyp (n .>= 0), hprf (powN `at` (Inst @"x" ( 4 :: SInteger), Inst @"n" n))]+ =: 7 `sDivides` (11 * 11 `pow` n - 4 * 4 `pow` n)+ =: 7 `sDivides` (7 * 11 `pow` n + 4 * 11 `pow` n - 4 * 4 `pow` n)+ =: 7 `sDivides` (7 * 11 `pow` n + 4 * (11 `pow` n - 4 `pow` n))+ ?? [hyp (n .>= 0), hprf ih]+ =: let x = some "x" (\v -> 7*v .== 11 `pow` n - 4 `pow` n) -- Apply the IH and grab the witness for it+ in 7 `sDivides` (7 * 11 `pow` n + 4 * 7 * x)+ =: 7 `sDivides` (7 * (11 `pow` n + 4 * x)) =: sTrue =: qed
Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs view
@@ -382,22 +382,22 @@ sh3 <- sheffer3 commut <- calc "a | b = b | a" (\AB -> a ⏐ b .== b ⏐ a) $- \a b -> [] ⊢ a ⏐ b ? sh1- ≡ ﬧﬧ(a ⏐ b) ? sh1+ \a b -> [] ⊢ a ⏐ b ⁇ sh1+ ≡ ﬧﬧ(a ⏐ b) ⁇ sh1 ≡ ﬧﬧ(a ⏐ ﬧﬧ b)- ≡ ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b)) ? sh3+ ≡ ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b)) ⁇ sh3 ≡ ﬧ ((ﬧﬧ b ⏐ a) ⏐ (ﬧﬧ b ⏐ a))- ≡ ﬧﬧ(ﬧﬧ b ⏐ a) ? sh1- ≡ ﬧﬧ b ⏐ a ? sh1+ ≡ ﬧﬧ(ﬧﬧ b ⏐ a) ⁇ sh1+ ≡ ﬧﬧ b ⏐ a ⁇ sh1 ≡ b ⏐ a ≡ qed all_bot <- calc "a | a′ = b | b′" (\AB -> a ⏐ ﬧ a .== b ⏐ ﬧ b) $- \a b -> [] ⊢ a ⏐ ﬧ a ? sh1- ≡ ﬧﬧ(a ⏐ ﬧ a) ? sh2- ≡ ﬧ((a ⏐ ﬧ a) ⏐ (b ⏐ ﬧ b)) ? commut- ≡ ﬧ((b ⏐ ﬧ b) ⏐ (a ⏐ ﬧ a)) ? sh2- ≡ ﬧﬧ (b ⏐ ﬧ b) ? sh1+ \a b -> [] ⊢ a ⏐ ﬧ a ⁇ sh1+ ≡ ﬧﬧ(a ⏐ ﬧ a) ⁇ sh2+ ≡ ﬧ((a ⏐ ﬧ a) ⏐ (b ⏐ ﬧ b)) ⁇ commut+ ≡ ﬧ((b ⏐ ﬧ b) ⏐ (a ⏐ ﬧ a)) ⁇ sh2+ ≡ ﬧﬧ (b ⏐ ﬧ b) ⁇ sh1 ≡ b ⏐ ﬧ b ≡ qed @@ -414,62 +414,62 @@ compl2 <- lemma "a ⊓ aᶜ = ⲳ" (\A -> a ⨅ ﬧ a .== ⲳ) [sh1, commut, all_bot] bound1 <- calc "a ⊔ т = т" (\A -> a ⨆ т .== т) $- \(a :: SStroke) -> [] ⊢ a ⨆ т ? ident2- ≡ (a ⨆ т) ⨅ т ? commut2- ≡ т ⨅ (a ⨆ т) ? compl1- ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ т) ? distrib1- ≡ a ⨆ (ﬧ a ⨅ т) ? ident2- ≡ a ⨆ ﬧ a ? compl1+ \(a :: SStroke) -> [] ⊢ a ⨆ т ⁇ ident2+ ≡ (a ⨆ т) ⨅ т ⁇ commut2+ ≡ т ⨅ (a ⨆ т) ⁇ compl1+ ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ т) ⁇ distrib1+ ≡ a ⨆ (ﬧ a ⨅ т) ⁇ ident2+ ≡ a ⨆ ﬧ a ⁇ compl1 ≡ (т :: SStroke) ≡ qed bound2 <- calc "a ⊓ ⲳ = ⲳ" (\A -> a ⨅ ⲳ .== ⲳ) $- \(a :: SStroke) -> [] ⊢ a ⨅ ⲳ ? ident1- ≡ (a ⨅ ⲳ) ⨆ ⲳ ? commut1- ≡ ⲳ ⨆ (a ⨅ ⲳ) ? compl2- ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ? distrib2- ≡ a ⨅ (ﬧ a ⨆ ⲳ) ? ident1- ≡ a ⨅ ﬧ a ? compl2+ \(a :: SStroke) -> [] ⊢ a ⨅ ⲳ ⁇ ident1+ ≡ (a ⨅ ⲳ) ⨆ ⲳ ⁇ commut1+ ≡ ⲳ ⨆ (a ⨅ ⲳ) ⁇ compl2+ ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ⁇ distrib2+ ≡ a ⨅ (ﬧ a ⨆ ⲳ) ⁇ ident1+ ≡ a ⨅ ﬧ a ⁇ compl2 ≡ (ⲳ :: SStroke) ≡ qed absorb1 <- calc "a ⊔ (a ⊓ b) = a" (\AB -> a ⨆ (a ⨅ b) .== a) $- \(a :: SStroke) b -> [] ⊢ a ⨆ (a ⨅ b) ? ident2- ≡ (a ⨅ т) ⨆ (a ⨅ b) ? distrib2- ≡ a ⨅ (т ⨆ b) ? commut1- ≡ a ⨅ (b ⨆ т) ? bound1- ≡ a ⨅ т ? ident2+ \(a :: SStroke) b -> [] ⊢ a ⨆ (a ⨅ b) ⁇ ident2+ ≡ (a ⨅ т) ⨆ (a ⨅ b) ⁇ distrib2+ ≡ a ⨅ (т ⨆ b) ⁇ commut1+ ≡ a ⨅ (b ⨆ т) ⁇ bound1+ ≡ a ⨅ т ⁇ ident2 ≡ a ≡ qed absorb2 <- calc "a ⊓ (a ⊔ b) = a" (\AB -> a ⨅ (a ⨆ b) .== a) $- \(a :: SStroke) b -> [] ⊢ a ⨅ (a ⨆ b) ? ident1- ≡ (a ⨆ ⲳ) ⨅ (a ⨆ b) ? distrib1- ≡ a ⨆ (ⲳ ⨅ b) ? commut2- ≡ a ⨆ (b ⨅ ⲳ) ? bound2- ≡ a ⨆ ⲳ ? ident1+ \(a :: SStroke) b -> [] ⊢ a ⨅ (a ⨆ b) ⁇ ident1+ ≡ (a ⨆ ⲳ) ⨅ (a ⨆ b) ⁇ distrib1+ ≡ a ⨆ (ⲳ ⨅ b) ⁇ commut2+ ≡ a ⨆ (b ⨅ ⲳ) ⁇ bound2+ ≡ a ⨆ ⲳ ⁇ ident1 ≡ a ≡ qed idemp2 <- calc "a ⊓ a = a" (\A -> a ⨅ a .== a) $- \(a :: SStroke) -> [] ⊢ a ⨅ a ? ident1- ≡ a ⨅ (a ⨆ ⲳ) ? absorb2 + \(a :: SStroke) -> [] ⊢ a ⨅ a ⁇ ident1+ ≡ a ⨅ (a ⨆ ⲳ) ⁇ absorb2 ≡ a ≡ qed inv <- calc "a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ" (\AAp -> a ⨆ a' .== т .=> a ⨅ a' .== ⲳ .=> a' .== ﬧ a) $- \(a :: SStroke) a' -> [a ⨆ a' .== т, a ⨅ a' .== ⲳ] ⊢ a' ? ident2- ≡ a' ⨅ т ? compl1- ≡ a' ⨅ (a ⨆ ﬧ a) ? distrib2- ≡ (a' ⨅ a) ⨆ (a' ⨅ ﬧ a) ? commut2- ≡ (a' ⨅ a) ⨆ (ﬧ a ⨅ a') ? commut2- ≡ (a ⨅ a') ⨆ (ﬧ a ⨅ a') ? a ⨅ a' .== ⲳ- ≡ ⲳ ⨆ (ﬧ a ⨅ a') ? compl2- ≡ (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ? commut2- ≡ (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ? distrib2- ≡ ﬧ a ⨅ (a ⨆ a') ? a ⨆ a' .== т- ≡ ﬧ a ⨅ т ? ident2+ \(a :: SStroke) a' -> [a ⨆ a' .== т, a ⨅ a' .== ⲳ] ⊢ a' ⁇ ident2+ ≡ a' ⨅ т ⁇ compl1+ ≡ a' ⨅ (a ⨆ ﬧ a) ⁇ distrib2+ ≡ (a' ⨅ a) ⨆ (a' ⨅ ﬧ a) ⁇ commut2+ ≡ (a' ⨅ a) ⨆ (ﬧ a ⨅ a') ⁇ commut2+ ≡ (a ⨅ a') ⨆ (ﬧ a ⨅ a') ⁇ a ⨅ a' .== ⲳ+ ≡ ⲳ ⨆ (ﬧ a ⨅ a') ⁇ compl2+ ≡ (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ⁇ commut2+ ≡ (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ⁇ distrib2+ ≡ ﬧ a ⨅ (a ⨆ a') ⁇ a ⨆ a' .== т+ ≡ ﬧ a ⨅ т ⁇ ident2 ≡ ﬧ a ≡ qed @@ -479,22 +479,22 @@ cancel <- lemma "a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b" (\AB -> a ⨆ ﬧ b .== т .=> a ⨅ ﬧ b .== ⲳ .=> a .== b) [inv, inv_elim] a1 <- calc "a ⊔ (aᶜ ⊔ b) = т" (\AB -> a ⨆ (ﬧ a ⨆ b) .== т) $- \(a :: SStroke) b -> [] ⊢ a ⨆ (ﬧ a ⨆ b) ? ident2- ≡ (a ⨆ (ﬧ a ⨆ b)) ⨅ т ? commut2- ≡ т ⨅ (a ⨆ (ﬧ a ⨆ b)) ? compl1- ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ? distrib1- ≡ a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b)) ? absorb2- ≡ a ⨆ ﬧ a ? compl1+ \(a :: SStroke) b -> [] ⊢ a ⨆ (ﬧ a ⨆ b) ⁇ ident2+ ≡ (a ⨆ (ﬧ a ⨆ b)) ⨅ т ⁇ commut2+ ≡ т ⨅ (a ⨆ (ﬧ a ⨆ b)) ⁇ compl1+ ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ⁇ distrib1+ ≡ a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b)) ⁇ absorb2+ ≡ a ⨆ ﬧ a ⁇ compl1 ≡ (т :: SStroke) ≡ qed a2 <- calc "a ⊓ (aᶜ ⊓ b) = ⲳ" (\AB -> a ⨅ (ﬧ a ⨅ b) .== ⲳ) $- \(a :: SStroke) b -> [] ⊢ a ⨅ (ﬧ a ⨅ b) ? ident1- ≡ (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ ? commut1- ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b)) ? compl2- ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ? distrib2- ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b)) ? absorb1- ≡ a ⨅ ﬧ a ? compl2+ \(a :: SStroke) b -> [] ⊢ a ⨅ (ﬧ a ⨅ b) ⁇ ident1+ ≡ (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ ⁇ commut1+ ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b)) ⁇ compl2+ ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ⁇ distrib2+ ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b)) ⁇ absorb1+ ≡ a ⨅ ﬧ a ⁇ compl2 ≡ (ⲳ :: SStroke) ≡ qed @@ -513,30 +513,30 @@ e2 <- lemma "b ⊔ (a ⊓ (b ⊓ c)) = b" (\ABC -> b ⨆ (a ⨅ (b ⨅ c)) .== b) [distrib1, absorb1, absorb2, commut2] f1 <- calc "(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ b .== т) $- \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ b ? commut1- ≡ ﬧ b ⨆ (a ⨆ (b ⨆ c)) ? ident2- ≡ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т ? commut2- ≡ т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? compl1- ≡ (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? commut1- ≡ (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? distrib1- ≡ ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c))) ? e1- ≡ ﬧ b ⨆ b ? commut1- ≡ b ⨆ ﬧ b ? compl1+ \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ b ⁇ commut1+ ≡ ﬧ b ⨆ (a ⨆ (b ⨆ c)) ⁇ ident2+ ≡ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т ⁇ commut2+ ≡ т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⁇ compl1+ ≡ (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⁇ commut1+ ≡ (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⁇ distrib1+ ≡ ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c))) ⁇ e1+ ≡ ﬧ b ⨆ b ⁇ commut1+ ≡ b ⨆ ﬧ b ⁇ compl1 ≡ (т :: SStroke) ≡ qed g1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ cᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ c .== т) [commut1, f1] h1 <- calc "(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ a .== ⲳ) $- \(a :: SStroke) b c -> [] ⊢ ﬧ(a ⨆ b ⨆ c) ⨅ a ? commut2- ≡ a ⨅ ﬧ (a ⨆ b ⨆ c) ? dm1- ≡ a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? ident1- ≡ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ ? commut1- ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? compl2- ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? distrib2- ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? commut2- ≡ a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b))) ? e2- ≡ a ⨅ ﬧ a ? compl2+ \(a :: SStroke) b c -> [] ⊢ ﬧ(a ⨆ b ⨆ c) ⨅ a ⁇ commut2+ ≡ a ⨅ ﬧ (a ⨆ b ⨆ c) ⁇ dm1+ ≡ a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ⁇ ident1+ ≡ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ ⁇ commut1+ ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⁇ compl2+ ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⁇ distrib2+ ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⁇ commut2+ ≡ a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b))) ⁇ e2+ ≡ a ⨅ ﬧ a ⁇ compl2 ≡ (ⲳ :: SStroke) ≡ qed @@ -546,57 +546,57 @@ assoc1 <- do c1 <- calc "(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) .== т) $- \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) ? dm1- ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? distrib1- ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ? g1- ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т ? ident2- ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b) ? distrib1- ≡ ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? d1- ≡ т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? f1- ≡ т ⨅ (т :: SStroke) ? idemp2+ \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) ⁇ dm1+ ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ⁇ distrib1+ ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ⁇ g1+ ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т ⁇ ident2+ ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b) ⁇ distrib1+ ≡ ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ⁇ d1+ ≡ т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ⁇ f1+ ≡ т ⨅ (т :: SStroke) ⁇ idemp2 ≡ (т :: SStroke) ≡ qed c2 <- calc "(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ" (\ABC -> (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) .== ⲳ) $- \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) ? commut2- ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c)) ? distrib2- ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ? commut2- ≡ (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut2- ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? h1- ≡ ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut1- ≡ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ ? ident1- ≡ (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c) ? commut2- ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c) ? distrib2- ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c) ? j1- ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ ? i1- ≡ ⲳ ⨆ (ⲳ :: SStroke) ? ident1+ \(a :: SStroke) b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) ⁇ commut2+ ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c)) ⁇ distrib2+ ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ⁇ commut2+ ≡ (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⁇ commut2+ ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⁇ h1+ ≡ ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⁇ commut1+ ≡ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ ⁇ ident1+ ≡ (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c) ⁇ commut2+ ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c) ⁇ distrib2+ ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c) ⁇ j1+ ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ ⁇ i1+ ≡ ⲳ ⨆ (ⲳ :: SStroke) ⁇ ident1 ≡ (ⲳ :: SStroke) ≡ qed lemma "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c" (\ABC -> a ⨆ (b ⨆ c) .== (a ⨆ b) ⨆ c) [c1, c2, cancel] assoc2 <- calc "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c" (\ABC -> a ⨅ (b ⨅ c) .== (a ⨅ b) ⨅ c) $- \(a :: SStroke) b c -> [] ⊢ a ⨅ (b ⨅ c) ? dne- ≡ ﬧﬧ(a ⨅ (b ⨅ c)) ? assoc1- ≡ ﬧﬧ((a ⨅ b) ⨅ c) ? dne+ \(a :: SStroke) b c -> [] ⊢ a ⨅ (b ⨅ c) ⁇ dne+ ≡ ﬧﬧ(a ⨅ (b ⨅ c)) ⁇ assoc1+ ≡ ﬧﬧ((a ⨅ b) ⨅ c) ⁇ dne ≡ ((a ⨅ b) ⨅ c) ≡ qed le_antisymm <- calc "a ≤ b → b ≤ a → a = b" (\AB -> a ≤ b .=> b ≤ a .=> a .== b) $- \(a :: SStroke) b -> [a ≤ b, b ≤ a] ⊢ a ? a ≤ b- ≡ b ⨅ a ? commut2- ≡ a ⨅ b ? b ≤ a+ \(a :: SStroke) b -> [a ≤ b, b ≤ a] ⊢ a ⁇ a ≤ b+ ≡ b ⨅ a ⁇ commut2+ ≡ a ⨅ b ⁇ b ≤ a ≡ b ≡ qed le_refl <- lemma "a ≤ a" (\A -> a ≤ a) [idemp2] le_trans <- calc "a ≤ b → b ≤ c → a ≤ c" (\ABC -> a ≤ b .=> b ≤ c .=> a ≤ c) $- \(a :: SStroke) b c -> [a ≤ b, b ≤ c] ⊢ a ? a ≤ b- ≡ b ⨅ a ? b ≤ c- ≡ (c ⨅ b) ⨅ a ? assoc2- ≡ c ⨅ (b ⨅ a) ? a ≤ b+ \(a :: SStroke) b c -> [a ≤ b, b ≤ c] ⊢ a ⁇ a ≤ b+ ≡ b ⨅ a ⁇ b ≤ c+ ≡ (c ⨅ b) ⨅ a ⁇ assoc2+ ≡ c ⨅ (b ⨅ a) ⁇ a ≤ b ≡ (c ⨅ a) ≡ qed @@ -607,8 +607,8 @@ sup_le <- calc "a ≤ c → b ≤ c → a ⊔ b ≤ c" (\ABC -> a ≤ c .=> b ≤ c .=> a ⨆ b ≤ c) $- \(a :: SStroke) b c -> [a ≤ c, b ≤ c] ⊢ a ⨆ b ? [a ≤ c, b ≤ c]- ≡ (c ⨅ a) ⨆ (c ⨅ b) ? distrib2+ \(a :: SStroke) b c -> [a ≤ c, b ≤ c] ⊢ a ⨆ b ⁇ [a ≤ c, b ≤ c]+ ≡ (c ⨅ a) ⨆ (c ⨅ b) ⁇ distrib2 ≡ c ⨅ (a ⨆ b) ≡ qed @@ -617,9 +617,9 @@ le_inf <- calc "a ≤ b → a ≤ c → a ≤ b ⊓ c" (\ABC -> a ≤ b .=> a ≤ c .=> a ≤ b ⨅ c) $- \(a :: SStroke) b c -> [a ≤ b, a ≤ c] ⊢ a ? a ≤ b- ≡ b ⨅ a ? a ≤ c- ≡ b ⨅ (c ⨅ a) ? assoc2+ \(a :: SStroke) b c -> [a ≤ b, a ≤ c] ⊢ a ⁇ a ≤ b+ ≡ b ⨅ a ⁇ a ≤ c+ ≡ b ⨅ (c ⨅ a) ⁇ assoc2 ≡ (b ⨅ c ⨅ a) ≡ qed @@ -632,14 +632,14 @@ le_top <- calc "a ≤ ⊤" (\A -> a ≤ т) $ \(a :: SStroke)-> [] ⊢ a ≤ т- ≡ a .== т ⨅ a ? commut2- ≡ a .== a ⨅ т ? ident2+ ≡ a .== т ⨅ a ⁇ commut2+ ≡ a .== a ⨅ т ⁇ ident2 ≡ a .== a ≡ qed bot_le <- calc "⊥ ≤ a" (\A -> ⲳ ≤ a) $- \(a :: SStroke) -> [] ⊢ ⲳ ≤ a - ≡ ⲳ .== a ⨅ ⲳ ? bound2+ \(a :: SStroke) -> [] ⊢ ⲳ ≤ a+ ≡ ⲳ .== a ⨅ ⲳ ⁇ bound2 ≡ (ⲳ .== (ⲳ :: SStroke)) ≡ qed
Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs view
@@ -77,7 +77,7 @@ -- it to deduce that fact automatically. oddSquaredIsOdd <- calc "oddSquaredIsOdd" (\(Forall @"a" a) -> odd a .=> odd (sq a)) $- \a -> [odd a] |- sq a ? odd a+ \a -> [odd a] |- sq a ?? odd a =: sq (2 * ((a-1) `sEDiv` 2) + 1) =: qed @@ -90,7 +90,7 @@ -- Prove that if @a@ is an even number, then its square is four times the square of another. evenSquaredIsMult4 <- calc "evenSquaredIsMult4" (\(Forall @"a" a) -> even a .=> 4 `sDivides` sq a) $- \a -> [even a] |- sq a ? even a+ \a -> [even a] |- sq a ?? even a =: sq (2 * (a `sEDiv` 2)) =: qed
+ Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs view
@@ -0,0 +1,134 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.KnuckleDragger.StrongInduction+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Examples of strong induction on integers.+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.KnuckleDragger.StrongInduction where++import Prelude hiding (length, null, tail)++import Data.SBV+import Data.SBV.List+import Data.SBV.Tools.KnuckleDragger++#ifndef HADDOCK+-- $setup+-- >>> -- For doctest purposes only:+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Exception+#endif++-- | Prove that the sequence @1@, @3@, @S_{k-2} + 2 S_{k-1}@ is always odd.+--+-- We have:+--+-- >>> oddSequence1+-- Inductive lemma (strong): oddSequence+-- Base: oddSequence.Base Q.E.D.+-- Asms: 1 Q.E.D.+-- Step 1: Case split one way:+-- Case [1 of 1]: n[1] Q.E.D.+-- Completeness: Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: oddSequence.Step Q.E.D.+-- [Proven] oddSequence+oddSequence1 :: IO Proof+oddSequence1 = runKD $ do+ let s :: SInteger -> SInteger+ s = smtFunction "seq" $ \n -> ite (n .<= 0) 1+ $ ite (n .== 1) 3+ $ s (n-2) + 2 * s (n-1)++ -- z3 can't handle this, but CVC5 is proves it just fine.+ -- Note also that we do a "proof-by-contradiction," by deriving that+ -- the negation of the goal leads to falsehood.+ sInductWith cvc5 "oddSequence"+ (\(Forall @"n" n) -> n .>= 0 .=> sNot (2 `sDivides` s n)) $+ \ih n -> [n .>= 0] |- 2 `sDivides` s (n+1)+ ?? [cases "n" [n .< 2], hyp (n .>= 0)]+ =: 2 `sDivides` (s (n-1) + 2 * s n)+ =: 2 `sDivides` s (n-1)+ ?? ih `at` Inst @"n" (n - 1)+ =: sFalse+ =: qed++-- | Prove that the sequence @1@, @3@, @2 S_{k-1} - S_{k-2}@ generates sequence of odd numbers.+--+-- We have:+--+-- >>> oddSequence2+-- Inductive lemma (strong): oddSequence+-- Base: oddSequence.Base Q.E.D.+-- Asms: 1 Q.E.D.+-- Step 1: Case split one way:+-- Case [1 of 1]: n[1] Q.E.D.+-- Completeness: Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Step: 7 Q.E.D.+-- Step: oddSequence.Step Q.E.D.+-- [Proven] oddSequence+oddSequence2 :: IO Proof+oddSequence2 = runKD $ do+ let s :: SInteger -> SInteger+ s = smtFunction "seq" $ \n -> ite (n .<= 0) 1+ $ ite (n .== 1) 3+ $ 2 * s (n-1) - s (n-2)++ sInduct "oddSequence"+ (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $+ \ih n -> [n .>= 0] |- s (n+1)+ ?? [cases "n" [n+1 .< 2], hyp (n .>= 0)]+ =: let focus v = ite (n+1 .<= 0) 1 (ite (n + 1 .== 1) 3 v)+ in focus (2 * s n - s (n-1))+ ?? ih `at` Inst @"n" n+ =: focus (2 * (2 * n + 1) - s (n - 1))+ ?? ih `at` Inst @"n" (n-1)+ =: focus (2 * (2 * n + 1) - (2 * (n - 1) + 1))+ =: focus (4 * n + 2 - (2 * n - 1))+ =: focus (4 * n + 2 - 2 * n + 1)+ =: focus (2 * n + 2 + 1)+ =: focus (2 * (n + 1) + 1)+ =: qed++-- | For strong induction to work, We have to instantiate the proof at a "smaller" value. This+-- example demonstrates what happens if we don't. We have:+--+-- >>> won'tProve `catch` (\(_ :: SomeException) -> pure ())+-- Inductive lemma (strong): lengthGood+-- Base: lengthGood.Base Q.E.D.+-- Step: 1+-- *** Failed to prove lengthGood.1.+-- <BLANKLINE>+-- *** Solver reported: canceled+won'tProve :: IO ()+won'tProve = runKD $ do+ let len :: SList Integer -> SInteger+ len = smtFunction "len" $ \xs -> ite (null xs) 0 (1 + len (tail xs))++ -- Run it for 5 seconds, as otherwise z3 will hang as it can't prove make the inductive step+ _ <- sInductWith z3{extraArgs = ["-t:5000"]} "lengthGood"+ (\(Forall @"xs" xs) -> len xs .== length xs) $+ \ih x xs -> [] |- len (x .: xs)+ -- incorrectly instantiate the IH at x .: xs+ ?? ih `at` Inst @"xs" (x .: xs)+ =: length (x .: xs)+ =: qed+ pure ()
Documentation/SBV/Examples/Misc/ProgramPaths.hs view
@@ -8,7 +8,7 @@ -- -- A simple example of showing how to compute program paths. Consider the simple -- program:--- +-- -- @ -- d1 x y = if y < x - 2 then 7 else 2 -- d2 y = if y > 3 then 10 else 50@@ -42,7 +42,7 @@ d4 :: SInteger -> SInteger -> SInteger d4 x y = d1 x y + d2 y + d3 x y --- | Compute all possible program paths. Note the call to `partition`, which+-- | Compute all possible program paths. Note the call to `allSatPartition`, which -- causes `allSat` to find models that generate differing values for the given -- expression. We have: --@@ -80,4 +80,4 @@ paths = allSat $ do x <- sInteger "x" y <- sInteger "y"- partition "r" $ d4 x y+ allSatPartition "r" $ d4 x y
Documentation/SBV/Examples/Misc/SetAlgebra.hs view
@@ -243,13 +243,13 @@ {- $subsetChar There are multiple equivalent ways of characterizing the subset relationship: -\( A\subseteq B \iff A \cap B = A \) +\( A\subseteq B \iff A \cap B = A \) >>> prove $ \(a :: SI) b -> a `isSubsetOf` b .<=> a `intersection` b .== a Q.E.D. -\( A\subseteq B \iff A \cup B = B \) +\( A\subseteq B \iff A \cup B = B \) >>> prove $ \(a :: SI) b -> a `isSubsetOf` b .<=> a `union` b .== b Q.E.D.
Documentation/SBV/Examples/Misc/Tuple.hs view
@@ -38,7 +38,7 @@ -- | Create a dictionary of length 5, such that each element -- has an string key and each value is the length of the key.--- We impose a few more constraints to make the output interesting. +-- We impose a few more constraints to make the output interesting. -- For instance, you might get: -- -- @ ghci> example
Documentation/SBV/Examples/Puzzles/Birthday.hs view
@@ -22,7 +22,7 @@ -- -- "My birthday is one of these," she said. ----- Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday. To Bernard, she whispered the day, and only the day. +-- Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday. To Bernard, she whispered the day, and only the day. -- “Can you figure it out now?” she asked Albert. -- -- Albert: I don’t know when your birthday is, but I know Bernard doesn’t know, either.
Documentation/SBV/Examples/Puzzles/Coins.hs view
@@ -18,7 +18,7 @@ -- friend: No. -- you: How about a quarter? -- friend: Nope, and before you ask I cant make change for a dime or nickel either.--- you: Really? and these six coins are all US government coins currently in production? +-- you: Really? and these six coins are all US government coins currently in production? -- friend: Yes. -- you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back? -- friend: Sorry, I would like to but I cant with the coins I have.
Documentation/SBV/Examples/Puzzles/Sudoku.hs view
@@ -145,7 +145,7 @@ , [0, 0, 0, 0, 0, 0, 3, 0, 6] , [0, 0, 4, 0, 5, 0, 0, 0, 9] ] --- | According to the web, this is the toughest +-- | According to the web, this is the toughest. -- sudoku puzzle ever.. It even has a name: Al Escargot: -- <http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html> puzzle4 :: Puzzle
README.md view
@@ -17,8 +17,8 @@ ``` The function `prove` establishes theorem-hood, while `sat` finds a satisfying model if it exists.-All satisfying models can be computed using `allSat`. -SBV can also perform static assertion checks, such as absence of division-by-0, and other user given properties. +All satisfying models can be computed using `allSat`.+SBV can also perform static assertion checks, such as absence of division-by-0, and other user given properties. Furthermore, SBV can perform optimization, minimizing/maximizing arithmetic goals for their optimal values. SBV also allows for an incremental mode: Users are given a handle to the SMT solver as their programs execute, and they can issue SMTLib commands programmatically, query values, and direct the interaction using a high-level typed API. The incremental mode also allows for creation of constraints based on the current model, and access to internals of SMT solvers for advanced users. See the `runSMT` and `query` commands for details.@@ -54,7 +54,7 @@ - Uninterpreted sorts, and proofs over such sorts, potentially with axioms. - Ability to define SMTLib functions, generated directly from Haskell versions, including support for recursive and mutually recursive functions. - Reasoning with universal and existential quantifiers, including alternating quantifiers.- + The user can construct ordinary Haskell programs using these types, which behave like ordinary Haskell values when used concretely. However, when used with symbolic arguments, functions built out of these types can also be: - proven correct via an external SMT solver (the `prove` function),@@ -75,7 +75,8 @@ - [ABC](http://www.eecs.berkeley.edu/~alanmi/abc) from University of Berkeley - [Boolector](https://boolector.github.io/) from Johannes Kepler University - [Bitwuzla](https://bitwuzla.github.io/) from Stanford University- - [CVC4](http://cvc4.github.io/) and [CVC5](http://cvc5.github.io/) from Stanford University and the University of Iowa+ - [CVC4](http://cvc4.github.io/) from Stanford University and the University of Iowa+ - [CVC5](http://cvc5.github.io/) from Stanford University and the University of Iowa - [DReal](https://dreal.github.io/) from CMU - [MathSAT](http://mathsat.fbk.eu/) from FBK and DISI-University of Trento - [OpenSMT](https://verify.inf.usi.ch/opensmt) from Università della Svizzera italiana@@ -91,7 +92,7 @@ ## Using multiple solvers, simultaneously -SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. +SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. See `proveWithAny`/`proveWithAll` and `satWithAny`/`satWithAll` functions. The function `sbvAvailableSolvers` can be used to query the available solvers at run-time. ## Copyright, License@@ -120,7 +121,7 @@ Matthew Danish, Iavor Diatchki, Alex Dixon,-Robert Dockins, +Robert Dockins, Thomas DuBuisson, Trevor Elliott, Gergő Érdi,
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 907; Tried: 907; Skipped: 0; Success: 907; Errors: 0; Failures 0-Examples: 784; Tried: 784; Skipped: 0; Success: 784; Errors: 0; Failures 0-Setup: 123; Tried: 123; Skipped: 0; Success: 123; Errors: 0; Failures 0+Total: 937; Tried: 937; Skipped: 0; Success: 937; Errors: 0; Failures 0+Examples: 809; Tried: 809; Skipped: 0; Success: 809; Errors: 0; Failures 0+Setup: 128; Tried: 128; Skipped: 0; Success: 128; Errors: 0; Failures 0
SBVTestSuite/SBVConnectionTest.hs view
@@ -4,7 +4,7 @@ module Main (main) where -import Data.SBV hiding (partition)+import Data.SBV import Data.List import Control.Monad import System.Exit@@ -18,7 +18,7 @@ solverName = show . name . solver main :: IO ()-main = do let allSolvers = map (\s -> (solverName s, s)) [abc, boolector, bitwuzla, cvc4, cvc5, mathSAT, yices, z3, dReal, openSMT]+main = do let allSolvers = map ((\s -> (solverName s, s)) . defaultSolverConfig) [minBound .. maxBound] args <- getArgs
SBVTestSuite/TestSuite/Basics/Lambda.hs view
@@ -36,7 +36,7 @@ import Documentation.SBV.Examples.Misc.Definitions import Data.SBV.List-import Data.SBV.Tuple+import Data.SBV.Tuple hiding (fst, snd) import Data.Proxy
SBVTestSuite/TestSuite/Queries/Tuples.hs view
@@ -18,7 +18,7 @@ import Data.SBV import Data.SBV.Control-import Data.SBV.Tuple+import Data.SBV.Tuple hiding(fst) import Utils.SBVTestFramework
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 11.1+Version : 11.2 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT@@ -155,11 +155,13 @@ , Documentation.SBV.Examples.Lists.CountOutAndTransfer , Documentation.SBV.Examples.KnuckleDragger.Basics , Documentation.SBV.Examples.KnuckleDragger.CaseSplit+ , Documentation.SBV.Examples.KnuckleDragger.InsertionSort , Documentation.SBV.Examples.KnuckleDragger.Kleene , Documentation.SBV.Examples.KnuckleDragger.Lists , Documentation.SBV.Examples.KnuckleDragger.Numeric , Documentation.SBV.Examples.KnuckleDragger.ShefferStroke , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational+ , Documentation.SBV.Examples.KnuckleDragger.StrongInduction , Documentation.SBV.Examples.KnuckleDragger.Tao , Documentation.SBV.Examples.Misc.Definitions , Documentation.SBV.Examples.Misc.Enumerate