sbv 13.3 → 13.4
raw patch · 55 files changed
+2917/−2284 lines, 55 files
Files
- CHANGES.md +29/−0
- COPYRIGHT +1/−1
- Data/SBV.hs +1/−1
- Data/SBV/Control/Query.hs +3/−140
- Data/SBV/Control/Utils.hs +220/−6
- Data/SBV/Core/Concrete.hs +2/−2
- Data/SBV/Core/Model.hs +23/−4
- Data/SBV/List.hs +14/−4
- Data/SBV/Provers/Prover.hs +13/−50
- Data/SBV/SMT/SMT.hs +14/−2
- Data/SBV/TP.hs +1/−1
- Data/SBV/TP/Kernel.hs +29/−21
- Data/SBV/TP/List.hs +0/−1948
- Data/SBV/TP/TP.hs +22/−16
- Documentation/SBV/Examples/ADT/Expr.hs +2/−0
- Documentation/SBV/Examples/ADT/Param.hs +2/−0
- Documentation/SBV/Examples/Crypto/AES.hs +4/−3
- Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +1/−4
- Documentation/SBV/Examples/Misc/LambdaArray.hs +2/−0
- Documentation/SBV/Examples/Puzzles/SquareBirthday.hs +202/−0
- Documentation/SBV/Examples/TP/Basics.hs +11/−10
- Documentation/SBV/Examples/TP/BinarySearch.hs +2/−0
- Documentation/SBV/Examples/TP/GCD.hs +33/−11
- Documentation/SBV/Examples/TP/Lists.hs +1948/−0
- Documentation/SBV/Examples/TP/Majority.hs +1/−1
- Documentation/SBV/Examples/TP/MergeSort.hs +1/−1
- Documentation/SBV/Examples/TP/Primes.hs +18/−9
- Documentation/SBV/Examples/TP/QuickSort.hs +1/−1
- Documentation/SBV/Examples/TP/Reverse.hs +1/−1
- Documentation/SBV/Examples/TP/SortHelpers.hs +1/−1
- LICENSE +1/−1
- README.md +1/−1
- SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs +2/−0
- SBVBenchSuite/BenchSuite/Crypto/AES.hs +2/−0
- SBVBenchSuite/BenchSuite/Misc/Enumerate.hs +2/−0
- SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs +2/−0
- SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs +1/−4
- SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs +3/−0
- SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs +2/−0
- SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs +2/−0
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/GoldFiles/lambda70.gold +6/−4
- SBVTestSuite/GoldFiles/qOpt_1.gold +109/−0
- SBVTestSuite/GoldFiles/qOpt_2.gold +119/−0
- SBVTestSuite/GoldFiles/set_uninterp1.gold +15/−15
- SBVTestSuite/TestSuite/ADT/MutRec.hs +1/−1
- SBVTestSuite/TestSuite/Arrays/Query.hs +2/−0
- SBVTestSuite/TestSuite/Basics/Lambda.hs +11/−0
- SBVTestSuite/TestSuite/Basics/Quantifiers.hs +0/−4
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr +1/−1
- SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr +1/−1
- SBVTestSuite/TestSuite/Optimization/Basics.hs +23/−0
- SBVTestSuite/TestSuite/Puzzles/Sudoku.hs +1/−2
- SBVTestSuite/TestSuite/Queries/UISatEx.hs +1/−4
- sbv.cabal +4/−5
CHANGES.md view
@@ -1,6 +1,35 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 13.4, 2026-01-09++ * Remove Eq constraint on readArray, generalizing it to arbitrary types for array-reads.++ * Addded 'freeArray', which creates an array with no constraints at all. (Compare to 'constArray'.)+ Note that this is useful for expression contexts. If you're in a symbolic context (i.e., in+ the Symbolic monad), you can just use 'free' or 'sArray' as usual.)++ * Add missing instance of SatModel for Arrays. Thanks to Robin Webbers for the patch.++ * Export ArrayModel, so it can be programmatically processed after a call.++ * Moved Data/SBV/TP/List.hs to Documentation/SBV/Examples/TP/Lists.hs, which aligns better with the+ haddock documentation.++ * Fixed closure-version implementations of list functions filter, partition, takeWhile, and dropWhile.+ Thanks to amigalemming on github for the bug report.++ * Query mode now works with optimization directives. In this case, we perform lexicographic+ optimization. (Let me know if you need other methods.) The advantage of this is that calls+ to getValue works in this mode, so it is easier to access optimized model values. In case+ the optimal value is in an extension field (i.e., involves epsilon or infinity values),+ then calls to getValue will throw an error and alert the user. In this latter case, you+ should resort back to using the regular optimize calls.++ * Added new puzzle example: Documentation.SBV.Examples.Puzzles.SquareBirthday++ * Add recallWith to Data.SBV.TP, which allows you to change the solver in a recalled proof.+ ### Version 13.3, 2025-12-05 * Added 'constArray', which allows creation of constant valued symbolic arrays. The definition
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2010-2025, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2026, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV.hs view
@@ -249,7 +249,7 @@ -- ** Sets , RCSet(..), SSet -- * Arrays of symbolic values- , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, constArray, listArray, ArrayModel+ , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, constArray, freeArray, listArray, ArrayModel(..) -- * Creating symbolic values -- ** Single value
Data/SBV/Control/Query.hs view
@@ -9,13 +9,9 @@ -- Querying a solver interactively. ----------------------------------------------------------------------------- -{-# LANGUAGE BangPatterns #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -40,21 +36,18 @@ import Data.IORef (readIORef) import qualified Data.Map.Strict as M-import qualified Data.Sequence as S import qualified Data.Text as T import qualified Data.Foldable as F import Data.Char (toLower)-import Data.List (intercalate, nubBy, sortOn)-import Data.Maybe (listToMaybe, catMaybes, fromMaybe)+import Data.List (intercalate, nubBy)+import Data.Maybe (fromMaybe) import Data.Function (on)-import Data.Bifunctor (first)-import Data.Foldable (toList) import Data.SBV.Core.Data -import Data.SBV.Core.Symbolic (MonadQuery(..), State(..), incrementInternalCounter, validationRequested, getSV, lookupInput, mustIgnoreVar)+import Data.SBV.Core.Symbolic (MonadQuery(..), State(..), incrementInternalCounter, getSV) import Data.SBV.Utils.SExpr @@ -67,17 +60,6 @@ -- | An Assignment of a model binding data Assignment = Assign SVal CV --- | Remove the bars from model names; these are (mostly!) automatically inserted-unBarModel :: SMTModel -> SMTModel-unBarModel SMTModel {modelObjectives, modelBindings, modelAssocs, modelUIFuns}- = SMTModel { modelObjectives = ubf <$> modelObjectives- , modelBindings = (ubn <$>) <$> modelBindings- , modelAssocs = ubf <$> modelAssocs- , modelUIFuns = ubf <$> modelUIFuns- }- where ubf (n, a) = (unBar n, a)- ubn (NamedSymVar sv nm, a) = (NamedSymVar sv (T.pack (unBar (T.unpack nm))), a)- -- Is this a string? If so, return it, otherwise fail in the Maybe monad. fromECon :: SExpr -> Maybe String fromECon (ECon s) = Just s@@ -300,123 +282,6 @@ DSat{} -> more Unk -> more --- | Generalization of 'Data.SBV.Control.getModel'-getModel :: (MonadIO m, MonadQuery m) => m SMTModel-getModel = getModelAtIndex Nothing---- | Get a model stored at an index. This is likely very Z3 specific!-getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel-getModelAtIndex mbi = do- State{runMode} <- queryState- rm <- io $ readIORef runMode- case rm of- m@CodeGen -> error $ "SBV.getModel: Model is not available in mode: " ++ show m- m@LambdaGen{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m- m@Concrete{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m- SMTMode{} -> do- cfg <- getConfig- uis <- getUIs-- allModelInputs <- getTopLevelInputs- obsvs <- getObservables-- inputAssocs <- let grab (NamedSymVar sv nm) = let wrap !c = (sv, (nm, c)) in wrap <$> getValueCV mbi sv- in mapM grab allModelInputs-- let name = fst . snd- removeSV = snd- prepare = S.unstableSort . S.filter (not . mustIgnoreVar cfg . T.unpack . name)- assocs = fmap removeSV (prepare inputAssocs) <> S.fromList (sortOn fst obsvs)-- -- collect UIs, and UI functions if requested- let uiFuns = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as > 1, allSatTrackUFs cfg, not (mustIgnoreVar cfg nm)] -- functions have at least two things in their type!- uiRegs = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as == 1, not (mustIgnoreVar cfg nm)]-- -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out- -- as cex's tend to get larger- unless (null uiFuns) $- let solverCaps = capabilities (solver cfg)- in case supportsFlattenedModels solverCaps of- Nothing -> return ()- Just cmds -> mapM_ (send True) cmds-- bindings <- let get i@(getSV -> sv) = case lookupInput fst sv inputAssocs of- Just (_, (_, cv)) -> return (i, cv)- Nothing -> do cv <- getValueCV mbi sv- return (i, cv)-- in if validationRequested cfg- then Just <$> mapM get allModelInputs- else return Nothing-- uiFunVals <- mapM (\ui@(nm, (c, _, t)) -> (\a -> (nm, (c, t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns-- uiVals <- mapM (\ui@(nm, (_, _, _)) -> (nm,) <$> getUICVal mbi ui) uiRegs-- return $ unBarModel $ SMTModel { modelObjectives = []- , modelBindings = toList <$> bindings- , modelAssocs = uiVals ++ toList (first T.unpack <$> assocs)- , modelUIFuns = uiFunVals- }---- | Just after a check-sat is issued, collect objective values. Used--- internally only, not exposed to the user.-getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]-getObjectiveValues = do let cmd = "(get-objectives)"-- bad = unexpected "getObjectiveValues" cmd "a list of objective values" Nothing-- r <- ask cmd-- si <- queryState >>= getSInfo-- inputs <- F.toList <$> getTopLevelInputs-- parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue si (bad r) inputs) es- _ -> bad r Nothing-- where -- | Parse an objective value out.- getObjValue :: SInfo -> (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))- getObjValue si bailOut inputs expr =- case expr of- EApp [_] -> return Nothing -- Happens when a soft-assertion has no associated group.- EApp [ECon nm, v] -> locate nm v -- Regular case- _ -> dontUnderstand (show expr)-- where locate nm v = case listToMaybe [p | p@(NamedSymVar sv _) <- inputs, show sv == nm] of- Nothing -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names- Just (NamedSymVar sv actualName) -> grab sv v >>= \val -> return $ Just (T.unpack actualName, val)-- dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."- , "While trying to process: " ++ s- ]-- grab :: SV -> SExpr -> m GeneralizedCV- grab s topExpr- | Just v <- recoverKindedValue si k topExpr = return $ RegularCV v- | True = ExtendedCV <$> cvt (simplify topExpr)- where k = kindOf s-- -- Convert to an extended expression. Hopefully complete!- cvt :: SExpr -> m ExtCV- cvt (ECon "oo") = return $ Infinite k- cvt (ECon "epsilon") = return $ Epsilon k- cvt (EApp [ECon "interval", x, y]) = Interval <$> cvt x <*> cvt y- cvt (ENum (i, _, _)) = return $ BoundedCV $ mkConstCV k i- cvt (EReal r) = return $ BoundedCV $ CV k $ CAlgReal r- cvt (EFloat f) = return $ BoundedCV $ CV k $ CFloat f- cvt (EDouble d) = return $ BoundedCV $ CV k $ CDouble d- cvt (EApp [ECon "+", x, y]) = AddExtCV <$> cvt x <*> cvt y- cvt (EApp [ECon "*", x, y]) = MulExtCV <$> cvt x <*> cvt y- -- Nothing else should show up, hopefully!- cvt e = dontUnderstand (show e)-- -- drop the pesky to_real's that Z3 produces.. Cool but useless.- simplify :: SExpr -> SExpr- simplify (EApp [ECon "to_real", n]) = n- simplify (EApp xs) = EApp (map simplify xs)- simplify e = e- -- | Generalization of 'Data.SBV.Control.checkSatAssuming' checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult checkSatAssuming sBools = fst <$> checkSatAssumingHelper False sBools@@ -833,5 +698,3 @@ } return $ Satisfiable queryConfig m--{- HLint ignore getModelAtIndex "Use forM_" -}
Data/SBV/Control/Utils.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-}@@ -33,6 +34,7 @@ , inNewContext, freshVar, freshVar_ , getTopLevelInputs, parse, unexpected , timeout, queryDebug, retrieveResponse, recoverKindedValue, runProofOn, executeQuery+ , startOptimizer, getObjectiveValues, getModel, getModelAtIndex ) where import Data.List (sortBy, sortOn, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf, isSuffixOf)@@ -53,7 +55,7 @@ import Control.Monad.Trans (lift) import Control.Monad.Reader (runReaderT) -import Data.Maybe (isNothing, isJust)+import Data.Maybe (isNothing, isJust, catMaybes, listToMaybe) import Data.IORef (readIORef, writeIORef, IORef, newIORef, modifyIORef') @@ -69,6 +71,7 @@ , Result(..), SMTProblem(..), trueSV, SymVal(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..) , SBVType(..), forceSVArg, RoundingMode(RoundNearestTiesToEven), (.=>) , RCSet(..), QuantifiedBool(..), ArrayModel(..), SInfo(..), getSInfo+ , OptimizeStyle(..), GeneralizedCV(..), ExtCV(..) ) import Data.SBV.Core.Symbolic ( IncState(..), withNewIncState, State(..), svToSV, symbolicEnv, SymbolicT@@ -78,7 +81,7 @@ , extractSymbolicSimulationState, MonadSymbolic(..) , UserInputs, getSV, NamedSymVar(..), lookupInput, getUserName' , Name, CnstMap, Inputs(..), ProgInfo(..)- , mustIgnoreVar, newInternalVariable+ , mustIgnoreVar, newInternalVariable, Penalty(..) ) import Data.SBV.Core.AlgReals (mergeAlgReals, AlgReal(..), RealPoint(..))@@ -86,7 +89,7 @@ import Data.SBV.Core.Kind (smtType, hasUninterpretedSorts, expandKinds, isSomeKindOfFloat, substituteADTVars) import Data.SBV.Core.Operations (svNot, svNotEqual, svOr, svEqual) -import Data.SBV.SMT.SMT (showModel, parseCVs, SatModel, AllSatResult(..))+import Data.SBV.SMT.SMT (showModel, parseCVs, SatModel, AllSatResult(..), OptimizeResult(..)) import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib) import Data.SBV.SMT.SMTLib2 (setSMTOption) import Data.SBV.SMT.Utils ( showTimeoutValue, addAnnotations, alignPlain, debug@@ -94,7 +97,7 @@ ) import Data.SBV.Utils.ExtractIO-import Data.SBV.Utils.Lib (qfsToString)+import Data.SBV.Utils.Lib (qfsToString, unBar) import Data.SBV.Utils.SExpr import Data.SBV.Utils.PrettyNum (cvToSMTLib) @@ -357,6 +360,32 @@ Unk -> bad Unsat -> bad + -- Are we in an optimization context? If so, we must ensure that the model is not in an extended field+ objs <- getObjectives+ unless (null objs) $ do+ ovs <- getObjectiveValues+ case [() | (_, ExtendedCV _) <- ovs] of+ [] -> pure () -- We're good, all objectives are within the domain+ _ -> do cfg <- getConfig+ m <- getModel+ ov <- getObjectiveValues++ let mdl = LexicographicResult (SatExtField cfg m{modelObjectives = ov})++ align "" = "***"+ align l = "*** " ++ l++ error $ unlines $ "" : map align ([+ "Data.SBV.getValue: The current solver state is satisfiable in an extension field."+ , "That is, the optimized values assume epsilon/infinity values."+ , ""+ , "Calls to getValue is not supported in this context. Instead, use the 'optimize' method"+ , "directly and inspect the objective values explicitly."+ , ""+ , "The current model is:"+ , ""+ ] ++ map (" " ++) (lines (show mdl)))+ cv <- getValueCV Nothing sv return $ fromCV cv @@ -1858,7 +1887,7 @@ -- | Generalization of 'Data.SBV.Control.executeQuery' executeQuery :: forall m a. ExtractIO m => QueryContext -> QueryT m a -> SymbolicT m a-executeQuery queryContext (QueryT userQuery) = do+executeQuery queryContext originalQuery = do st <- symbolicEnv rm <- liftIO $ readIORef (runMode st) @@ -1901,8 +1930,18 @@ Nothing -> return () Just QueryState{queryTerminate} -> queryTerminate maybeForwardedException + -- If this is an extrnal query and there are objectives, let's add those to the list before we run+ -- Here we only allow Lexicographic; we might want to make that configurable later.+ let userQuery = case queryContext of+ QueryInternal -> originalQuery+ QueryExternal -> do mbDirs <- startOptimizer cfg Lexicographic+ case mbDirs of+ Nothing -> pure ()+ Just (_, cmds) -> mapM_ (send True) cmds+ originalQuery+ lift $ join $ liftIO $ C.mask $ \restore -> do- r <- restore (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery)+ r <- restore (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT (runQueryT userQuery)) `C.catch` \e -> terminateSolver (Just e) >> C.throwIO (e :: C.SomeException) terminateSolver Nothing return r@@ -1966,5 +2005,180 @@ , "*** and each call to runSMT should have only one query call inside." ] +-- | Preparing for optimization. If we have objectives, returns the directives for the solver. If not, it returns nothing.+startOptimizer :: (MonadIO m, MonadQuery m) => SMTConfig -> OptimizeStyle -> m (Maybe ([Objective (SV, SV)], [String]))+startOptimizer config style = do+ objectives <- getObjectives++ if null objectives+ then return Nothing+ else do unless (supportsOptimization (capabilities (solver config))) $+ error $ unlines [ ""+ , "*** Data.SBV: The backend solver " ++ show (name (solver config)) ++ "does not support optimization goals."+ , "*** Please use a solver that has support, such as z3"+ ]++ when (validateModel config && not (optimizeValidateConstraints config)) $+ error $ unlines [ ""+ , "*** Data.SBV: Model validation is not supported in optimization calls."+ , "***"+ , "*** Instead, use `cfg{optimizeValidateConstraints = True}`"+ , "***"+ , "*** which checks that the results satisfy the constraints but does"+ , "*** NOT ensure that they are optimal."+ ]+++ let optimizerDirectives = concatMap minmax objectives ++ priority style+ where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"++ minmax (Minimize _ xy@(_, v)) = [mkEq xy, "(minimize " ++ show v ++ ")"]+ minmax (Maximize _ xy@(_, v)) = [mkEq xy, "(maximize " ++ show v ++ ")"]+ minmax (AssertWithPenalty nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ show v ++ penalize mbp ++ ")"]+ where penalize DefaultPenalty = ""+ penalize (Penalty w mbGrp)+ | w <= 0 = error $ unlines [ "SBV.AssertWithPenalty: Goal " ++ show nm ++ " is assigned a non-positive penalty: " ++ shw+ , "All soft goals must have > 0 penalties associated."+ ]+ | True = " :weight " ++ shw ++ maybe "" group mbGrp+ where shw = show (fromRational w :: Double)++ group g = " :id " ++ g++ priority Lexicographic = [] -- default, no option needed+ priority Independent = ["(set-option :opt.priority box)"]+ priority (Pareto _) = ["(set-option :opt.priority pareto)"]++ pure $ Just (objectives, optimizerDirectives)++-- | Just after a check-sat is issued, collect objective values. Used+-- internally only, not exposed to the user.+getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]+getObjectiveValues = do let cmd = "(get-objectives)"++ bad = unexpected "getObjectiveValues" cmd "a list of objective values" Nothing++ r <- ask cmd++ si <- queryState >>= getSInfo++ inputs <- F.toList <$> getTopLevelInputs++ parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue si (bad r) inputs) es+ _ -> bad r Nothing++ where -- | Parse an objective value out.+ getObjValue :: SInfo -> (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))+ getObjValue si bailOut inputs expr =+ case expr of+ EApp [_] -> return Nothing -- Happens when a soft-assertion has no associated group.+ EApp [ECon nm, v] -> locate nm v -- Regular case+ _ -> dontUnderstand (show expr)++ where locate nm v = case listToMaybe [p | p@(NamedSymVar sv _) <- inputs, show sv == nm] of+ Nothing -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names+ Just (NamedSymVar sv actualName) -> grab sv v >>= \val -> return $ Just (T.unpack actualName, val)++ dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."+ , "While trying to process: " ++ s+ ]++ grab :: SV -> SExpr -> m GeneralizedCV+ grab s topExpr+ | Just v <- recoverKindedValue si k topExpr = return $ RegularCV v+ | True = ExtendedCV <$> cvt (simplify topExpr)+ where k = kindOf s++ -- Convert to an extended expression. Hopefully complete!+ cvt :: SExpr -> m ExtCV+ cvt (ECon "oo") = return $ Infinite k+ cvt (ECon "epsilon") = return $ Epsilon k+ cvt (EApp [ECon "interval", x, y]) = Interval <$> cvt x <*> cvt y+ cvt (ENum (i, _, _)) = return $ BoundedCV $ mkConstCV k i+ cvt (EReal r) = return $ BoundedCV $ CV k $ CAlgReal r+ cvt (EFloat f) = return $ BoundedCV $ CV k $ CFloat f+ cvt (EDouble d) = return $ BoundedCV $ CV k $ CDouble d+ cvt (EApp [ECon "+", x, y]) = AddExtCV <$> cvt x <*> cvt y+ cvt (EApp [ECon "*", x, y]) = MulExtCV <$> cvt x <*> cvt y+ -- Nothing else should show up, hopefully!+ cvt e = dontUnderstand (show e)++ -- drop the pesky to_real's that Z3 produces.. Cool but useless.+ simplify :: SExpr -> SExpr+ simplify (EApp [ECon "to_real", n]) = n+ simplify (EApp xs) = EApp (map simplify xs)+ simplify e = e++-- | Generalization of 'Data.SBV.Control.getModel'+getModel :: (MonadIO m, MonadQuery m) => m SMTModel+getModel = getModelAtIndex Nothing++-- | Get a model stored at an index. This is likely very Z3 specific!+getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel+getModelAtIndex mbi = do+ State{runMode} <- queryState+ rm <- io $ readIORef runMode+ case rm of+ m@CodeGen -> error $ "SBV.getModel: Model is not available in mode: " ++ show m+ m@LambdaGen{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m+ m@Concrete{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m+ SMTMode{} -> do+ cfg <- getConfig+ uis <- getUIs++ allModelInputs <- getTopLevelInputs+ obsvs <- getObservables++ inputAssocs <- let grab (NamedSymVar sv nm) = let wrap !c = (sv, (nm, c)) in wrap <$> getValueCV mbi sv+ in mapM grab allModelInputs++ let name = fst . snd+ removeSV = snd+ prepare = S.unstableSort . S.filter (not . mustIgnoreVar cfg . T.unpack . name)+ assocs = fmap removeSV (prepare inputAssocs) <> S.fromList (sortOn fst obsvs)++ -- collect UIs, and UI functions if requested+ let uiFuns = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as > 1, allSatTrackUFs cfg, not (mustIgnoreVar cfg nm)] -- functions have at least two things in their type!+ uiRegs = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as == 1, not (mustIgnoreVar cfg nm)]++ -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out+ -- as cex's tend to get larger+ unless (null uiFuns) $+ let solverCaps = capabilities (solver cfg)+ in case supportsFlattenedModels solverCaps of+ Nothing -> return ()+ Just cmds -> mapM_ (send True) cmds++ bindings <- let get i@(getSV -> sv) = case lookupInput fst sv inputAssocs of+ Just (_, (_, cv)) -> return (i, cv)+ Nothing -> do cv <- getValueCV mbi sv+ return (i, cv)++ in if validationRequested cfg+ then Just <$> mapM get allModelInputs+ else return Nothing++ uiFunVals <- mapM (\ui@(nm, (c, _, t)) -> (\a -> (nm, (c, t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns++ uiVals <- mapM (\ui@(nm, (_, _, _)) -> (nm,) <$> getUICVal mbi ui) uiRegs++ return $ unBarModel $ SMTModel { modelObjectives = []+ , modelBindings = F.toList <$> bindings+ , modelAssocs = uiVals ++ F.toList (first T.unpack <$> assocs)+ , modelUIFuns = uiFunVals+ }++-- | Remove the bars from model names; these are (mostly!) automatically inserted+unBarModel :: SMTModel -> SMTModel+unBarModel SMTModel {modelObjectives, modelBindings, modelAssocs, modelUIFuns}+ = SMTModel { modelObjectives = ubf <$> modelObjectives+ , modelBindings = (ubn <$>) <$> modelBindings+ , modelAssocs = ubf <$> modelAssocs+ , modelUIFuns = ubf <$> modelUIFuns+ }+ where ubf (n, a) = (unBar n, a)+ ubn (NamedSymVar sv nm, a) = (NamedSymVar sv (T.pack (unBar (T.unpack nm))), a)+ {- HLint ignore module "Reduce duplication" -} {- HLint ignore getAllSatResult "Use forM_" -}+{- HLint ignore getModelAtIndex "Use forM_" -}
Data/SBV/Core/Concrete.hs view
@@ -90,7 +90,7 @@ -- That is, we store the history of the writes. The earlier a pair is in the list, the "later" it -- is done, i.e., it takes precedence over the latter entries. data ArrayModel a b = ArrayModel [(a, b)] b- deriving (G.Data, Generic, NFData)+ deriving (G.Data, Generic, NFData, Show) -- | The kind of an ArrayModel instance (HasKind a, HasKind b) => HasKind (ArrayModel a b) where@@ -425,7 +425,7 @@ -- | Create a constant word from an integral. mkConstCV :: Integral a => Kind -> a -> CV-mkConstCV k@(KVar{}) _ = error $ "mkConstCV: Unexpected kind: " ++ show k+mkConstCV k@KVar{} _ = error $ "mkConstCV: Unexpected kind: " ++ show k mkConstCV KBool a = normCV $ CV KBool (CInteger (toInteger a)) mkConstCV k@KBounded{} a = normCV $ CV k (CInteger (toInteger a)) mkConstCV KUnbounded a = normCV $ CV KUnbounded (CInteger (toInteger a))
Data/SBV/Core/Model.hs view
@@ -57,7 +57,7 @@ , genLiteral, genFromCV, genMkSymVar , zeroExtend, signExtend , sbvQuickCheck- , readArray, writeArray, constArray, lambdaArray, listArray+ , readArray, writeArray, constArray, freeArray, lambdaArray, listArray , FromSized, ToSized, FromSizedBV(..), ToSizedBV(..) , smtHOFunction, Closure(..) )@@ -3224,10 +3224,10 @@ k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g) -- | Reading a value from an array.-readArray :: forall key val. (Eq key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val+readArray :: forall key val. (SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val readArray array key- | eqCheckIsObjectEq ka, Just (ArrayModel tbl def) <- unliteral array, Just k <- unliteral key- = literal $ fromMaybe def (k `lookup` tbl) -- return the first value, since we don't bother deleting previous writes+ | eqCheckIsObjectEq ka, Just (ArrayModel tbl def) <- unliteral array, Just _ <- unliteral key, Just r <- locate (unSBV key) def tbl+ = r | True = symRes where symRes = SBV . SVal kb . Right $ cache g@@ -3237,6 +3237,15 @@ k <- sbvToSV st key newExpr st kb (SBVApp ReadArray [f, k]) + -- return the first value, since we don't bother deleting previous writes. Note that this might+ -- fail if we don't have equality; but that's OK; in that case we'll go symbolic.+ locate skey def vals = go vals+ where go [] = Just $ literal def+ go ((k, v) : rest) = case unliteral (SBV (svStrongEqual skey (unSBV (literal k)))) of+ Nothing -> Nothing+ Just True -> Just $ literal v+ Just False -> go rest+ -- | Writing a value to an array. For the concrete case, we don't bother deleting earlier entries, we keep a history. The earlier a value is in the list, the "later" it happened; in a stack fashion. writeArray :: forall key val. (HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val writeArray array key value@@ -3265,6 +3274,16 @@ g st = do sv <- sbvToSV st v newExpr st k (SBVApp (ArrayInit (Left (ka, kb))) [sv])++-- | Create a completely free array, with no constraints on it, as an expression.+-- Note that you can create an array in the symbolic context with the regular 'free'+-- calls. (Or 'sArray' if you prefer.) This variant creates it as an expression, i.e.,+-- without having to be in the monadic context. We take a name identifier here as an+-- argument which uniquely identifies this array. Note that this is necessary, as otherwise+-- there would be no way to distinguish two different calls in the pure context. If you+-- use the same name, then you'll get the same array, much like uninterpreted functions.+freeArray :: forall key val. (SymVal key, SymVal val) => String -> SArray key val+freeArray = lambdaArray . uninterpret -- | Using a lambda as an array. We can turn a function into an array, relating indexes -- to their values. (That is, passing @f@ would create an array where entry @i@
Data/SBV/List.hs view
@@ -1046,7 +1046,10 @@ $ \envxs -> let (cEnv, xs) = untuple envxs (h, t) = uncons xs r = sbvFilter (tuple (cEnv, t))- in ite (closureFun cEnv h) (h .: r) r+ in ite (null xs) []+ $ ite (closureFun cEnv h)+ (h .: r)+ r partition cls@Closure{closureEnv, closureFun} l | Just concResult <- concretePartition cls (closureFun closureEnv) l@@ -1057,7 +1060,8 @@ $ \envxs -> let (cEnv, xs) = untuple envxs (h, t) = uncons xs (as, bs) = untuple $ sbvPartition (tuple (cEnv, t))- in ite (closureFun cEnv h)+ in ite (null xs) (tuple ([], []))+ $ ite (closureFun cEnv h) (tuple (h .: as, bs)) (tuple (as, h .: bs)) @@ -1069,7 +1073,10 @@ where sbvTakeWhile = smtHOFunction "sbv.closureTakeWhile" closureFun $ \envxs -> let (cEnv, xs) = untuple envxs (h, t) = uncons xs- in ite (closureFun cEnv h) (h .: sbvTakeWhile (tuple (cEnv, t))) []+ in ite (null xs) []+ $ ite (closureFun cEnv h)+ (h .: sbvTakeWhile (tuple (cEnv, t)))+ [] dropWhile cls@Closure{closureEnv, closureFun} l | Just concResult <- concreteDropWhile cls (closureFun closureEnv) l@@ -1079,7 +1086,10 @@ where sbvDropWhile = smtHOFunction "sbv.closureDropWhile" closureFun $ \envxs -> let (cEnv, xs) = untuple envxs (h, t) = uncons xs- in ite (closureFun cEnv h) (sbvDropWhile (tuple (cEnv, t))) xs+ in ite (null xs) []+ $ ite (closureFun cEnv h)+ (sbvDropWhile (tuple (cEnv, t)))+ xs -- | @`sum` s@. Sum the given sequence. --
Data/SBV/Provers/Prover.hs view
@@ -35,7 +35,7 @@ ) where -import Control.Monad (when, unless)+import Control.Monad (unless) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.DeepSeq (rnf, NFData(..)) @@ -263,57 +263,20 @@ in IndependentResult <$> w xs [] ParetoResult (b, rs) -> ParetoResult . (b, ) <$> mapM v rs - where opt = do objectives <- Control.getObjectives-- when (null objectives) $- error $ unlines [ ""- , "*** Data.SBV: Unsupported call to optimize when no objectives are present."- , "*** Use \"sat\" for plain satisfaction"- ]-- unless (supportsOptimization (capabilities (solver config))) $- error $ unlines [ ""- , "*** Data.SBV: The backend solver " ++ show (name (solver config)) ++ "does not support optimization goals."- , "*** Please use a solver that has support, such as z3"- ]-- when (validateModel config && not (optimizeValidateConstraints config)) $- error $ unlines [ ""- , "*** Data.SBV: Model validation is not supported in optimization calls."- , "***"- , "*** Instead, use `cfg{optimizeValidateConstraints = True}`"- , "***"- , "*** which checks that the results satisfy the constraints but does"- , "*** NOT ensure that they are optimal."- ]--- let optimizerDirectives = concatMap minmax objectives ++ priority style- where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"-- minmax (Minimize _ xy@(_, v)) = [mkEq xy, "(minimize " ++ show v ++ ")"]- minmax (Maximize _ xy@(_, v)) = [mkEq xy, "(maximize " ++ show v ++ ")"]- minmax (AssertWithPenalty nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ show v ++ penalize mbp ++ ")"]- where penalize DefaultPenalty = ""- penalize (Penalty w mbGrp)- | w <= 0 = error $ unlines [ "SBV.AssertWithPenalty: Goal " ++ show nm ++ " is assigned a non-positive penalty: " ++ shw- , "All soft goals must have > 0 penalties associated."- ]- | True = " :weight " ++ shw ++ maybe "" group mbGrp- where shw = show (fromRational w :: Double)-- group g = " :id " ++ g-- priority Lexicographic = [] -- default, no option needed- priority Independent = ["(set-option :opt.priority box)"]- priority (Pareto _) = ["(set-option :opt.priority pareto)"]+ where opt = do mbDirs <- Control.startOptimizer config style - mapM_ (Control.send True) optimizerDirectives+ case mbDirs of+ Nothing -> error $ unlines [ ""+ , "*** Data.SBV: Unsupported call to optimize when no objectives are present."+ , "*** Use \"sat\" for plain satisfaction"+ ]+ Just (objectives, optimizerDirectives) -> do+ mapM_ (Control.send True) optimizerDirectives - case style of- Lexicographic -> LexicographicResult <$> Control.getLexicographicOptResults- Independent -> IndependentResult <$> Control.getIndependentOptResults (map objectiveName objectives)- Pareto mbN -> ParetoResult <$> Control.getParetoOptResults mbN+ case style of+ Lexicographic -> LexicographicResult <$> Control.getLexicographicOptResults+ Independent -> IndependentResult <$> Control.getIndependentOptResults (map objectiveName objectives)+ Pareto mbN -> ParetoResult <$> Control.getParetoOptResults mbN -- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The -- results will be returned in the order produced.
Data/SBV/SMT/SMT.hs view
@@ -231,11 +231,11 @@ -- | Given a sequence of constant-words, extract one instance of the type @a@, returning -- the remaining elements untouched. If the next element is not what's expected for this -- type you should return 'Nothing'- parseCVs :: [CV] -> Maybe (a, [CV])+ parseCVs :: [CV] -> Maybe (a, [CV]) -- | Given a parsed model instance, transform it using @f@, and return the result. -- The default definition for this method should be sufficient in most use cases.- cvtModel :: (a -> Maybe b) -> Maybe (a, [CV]) -> Maybe (b, [CV])+ cvtModel :: (a -> Maybe b) -> Maybe (a, [CV]) -> Maybe (b, [CV]) cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r) {-# MINIMAL parseCVs #-}@@ -318,6 +318,18 @@ -- | Constructing models for 'IntN' instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where parseCVs = genParse (kindOf (undefined :: IntN n))++-- | Constructing models for t'ArrayModel'+instance (SatModel k, SatModel v) => SatModel (ArrayModel k v) where+ parseCVs (CV (KArray kk kv) (CArray (ArrayModel tbl def)) : r)+ | Just (def', _) <- parseCVs @v [CV kv def]+ , let convert (k, v) = do+ (k', _) <- parseCVs @k [CV kk k]+ (v', _) <- parseCVs @v [CV kv v]+ pure (k', v')+ , Just tbl' <- traverse convert tbl+ = Just (ArrayModel tbl' def', r)+ parseCVs _ = Nothing -- | @CV@ as extracted from a model; trivial definition instance SatModel CV where
Data/SBV/TP.hs view
@@ -72,7 +72,7 @@ , disp -- * Recall an old proof, quietly proving it- , recall+ , recall, recallWith ) where import Data.SBV.TP.TP
Data/SBV/TP/Kernel.hs view
@@ -25,6 +25,7 @@ , inductiveLemma, inductiveLemmaWith , internalAxiom , TPProofContext (..), smtProofStep, HasInductionSchema(..)+ , tpMergeCfg ) where import Control.Monad.Trans (liftIO, MonadIO)@@ -186,32 +187,39 @@ , isCached = False } --- | Prove a lemma, using the given configuration-lemmaWith :: Proposition a => SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)-lemmaWith cfg@SMTConfig{tpOptions = TPOptions{printStats}} nm inputProp by = withProofCache nm $ do- tpSt <- getTPState- u <- tpGetNextUnique- liftIO $ getTimeStampIf printStats >>= runSMTWith cfg . go tpSt u- where go tpSt u mbStartTime = do qSaturateSavingObservables inputProp- mapM_ (constrain . getObjProof) by- query $ smtProofStep cfg tpSt "Lemma" 0 (TPProofOneShot nm by) Nothing inputProp [] (good mbStartTime u)-- -- What to do if all goes well- good mbStart u d = do mbElapsed <- getElapsedTime mbStart- liftIO $ finishTP cfg ("Q.E.D." ++ concludeModulo by) d $ catMaybes [mbElapsed]- pure $ Proof $ ProofObj { dependencies = by- , isUserAxiom = False- , getObjProof = label nm (quantifiedBool inputProp)- , getProp = toDyn inputProp- , proofName = nm- , uniqId = u- , isCached = False- }+-- | Propagate the settings for ribbon/timing from top to current. Because in any subsequent configuration+-- in a lemmaWith, inductWith etc., we just want to change the solver, not the actual settings for TP.+tpMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig+tpMergeCfg cur top = cur{tpOptions = tpOptions top} -- | Prove a given statement, using auxiliaries as helpers. Using the default solver. lemma :: Proposition a => String -> a -> [ProofObj] -> TP (Proof a) lemma nm f by = do cfg <- getTPConfig lemmaWith cfg nm f by++-- | Prove a lemma, using the given configuration.+lemmaWith :: Proposition a => SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)+lemmaWith cfgIn nm inputProp by = withProofCache nm $ do+ topCfg <- getTPConfig+ let cfg@SMTConfig{tpOptions = TPOptions{printStats}} = cfgIn `tpMergeCfg` topCfg+ tpSt <- getTPState+ u <- tpGetNextUnique+ liftIO $ getTimeStampIf printStats >>= runSMTWith cfg . go tpSt cfg u+ where go tpSt cfg u mbStartTime = do qSaturateSavingObservables inputProp+ mapM_ (constrain . getObjProof) by+ query $ smtProofStep cfg tpSt "Lemma" 0 (TPProofOneShot nm by) Nothing inputProp [] (good cfg mbStartTime u)++ -- What to do if all goes well+ good cfg mbStart u d = do mbElapsed <- getElapsedTime mbStart+ liftIO $ finishTP cfg ("Q.E.D." ++ concludeModulo by) d $ catMaybes [mbElapsed]+ pure $ Proof $ ProofObj { dependencies = by+ , isUserAxiom = False+ , getObjProof = label nm (quantifiedBool inputProp)+ , getProp = toDyn inputProp+ , proofName = nm+ , uniqId = u+ , isCached = False+ } -- | Prove a given statement, using the induction schema for the proposition. Using the default solver. inductiveLemma :: Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
− Data/SBV/TP/List.hs
@@ -1,1948 +0,0 @@--------------------------------------------------------------------------------- |--- Module : Data.SBV.TP.List--- Copyright : (c) Levent Erkok--- License : BSD3--- Maintainer: erkokl@gmail.com--- Stability : experimental------ A variety of TP proofs on list processing functions. Note that--- these proofs only hold for finite lists. SMT-solvers do not model infinite--- lists, and hence all claims are for finite (but arbitrary-length) lists.--------------------------------------------------------------------------------{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE OverloadedLists #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeAbstractions #-}-{-# LANGUAGE TypeApplications #-}--{-# OPTIONS_GHC -Wall -Werror #-}--module Data.SBV.TP.List (- -- * Append- appendNull, consApp, appendAssoc, initsLength, tailsLength, tailsAppend-- -- * Reverse- , revLen, revApp, revCons, revSnoc, revRev, enumLen, revNM-- -- * Length- , lengthTail, lenAppend, lenAppend2-- -- * Replicate- , replicateLength-- -- * All and any- , allAny-- -- * Map- , mapEquiv, mapAppend, mapReverse, mapCompose-- -- * Foldr and foldl- , foldrMapFusion, foldrFusion, foldrOverAppend, foldlOverAppend, foldrFoldlDuality, foldrFoldlDualityGeneralized, foldrFoldl- , bookKeeping-- -- * Filter- , filterAppend, filterConcat, takeDropWhile-- -- * Stutter removal- , destutter, destutterIdempotent-- -- * Difference- , appendDiff, diffAppend, diffDiff-- -- * Partition- , partition1, partition2-- -- * Take and drop- , take_take, drop_drop, take_drop, take_cons, take_map, drop_cons, drop_map, length_take, length_drop, take_all, drop_all- , take_append, drop_append-- -- * Zip- , map_fst_zip- , map_snd_zip- , map_fst_zip_take- , map_snd_zip_take-- -- * Counting elements- , count, countAppend, takeDropCount, countNonNeg, countElem, elemCount-- -- * Disjointness- , disjoint, disjointDiff-- -- * Interleaving- , interleave, uninterleave, interleaveLen, interleaveRoundTrip- ) where--import Prelude (Integer, Bool, Eq, ($), Num(..), id, (.), flip)--import Data.SBV-import Data.SBV.List-import Data.SBV.Tuple-import Data.SBV.TP--#ifdef DOCTEST--- $setup--- >>> :set -XScopedTypeVariables--- >>> :set -XTypeApplications--- >>> import Data.SBV--- >>> import Data.SBV.TP--- >>> import Control.Exception-#endif---- | @xs ++ [] == xs@------ >>> runTP $ appendNull @Integer--- Lemma: appendNull Q.E.D.--- [Proven] appendNull :: Ɐxs ∷ [Integer] → Bool-appendNull :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-appendNull = lemma "appendNull"- (\(Forall xs) -> xs ++ nil .== xs)- []---- | @(x : xs) ++ ys == x : (xs ++ ys)@------ >>> runTP $ consApp @Integer--- Lemma: consApp Q.E.D.--- [Proven] consApp :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-consApp :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))-consApp = lemma "consApp"- (\(Forall x) (Forall xs) (Forall ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))- []---- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@------ >>> runTP $ appendAssoc @Integer--- Lemma: appendAssoc Q.E.D.--- [Proven] appendAssoc :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐzs ∷ [Integer] → Bool------ Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to--- the concatenation of sequences in SMTLib, it must trigger an internal heuristic in z3--- that proves it right out-of-the-box!)-appendAssoc :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "zs" [a] -> SBool))-appendAssoc =- lemma "appendAssoc"- (\(Forall xs) (Forall ys) (Forall zs) -> xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs)- []---- | @length (inits xs) == 1 + length xs@------ >>> runTP $ initsLength @Integer--- Inductive lemma (strong): initsLength--- Step: Measure is non-negative Q.E.D.--- Step: 1 Q.E.D.--- Result: Q.E.D.--- [Proven] initsLength :: Ɐxs ∷ [Integer] → Bool-initsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-initsLength =- sInduct "initsLength"- (\(Forall xs) -> length (inits xs) .== 1 + length xs)- (length @a, []) $- \ih xs -> [] |- length (inits xs)- ?? ih- =: 1 + length xs- =: qed---- | @length (tails xs) == 1 + length xs@------ >>> runTP $ tailsLength @Integer--- Inductive lemma: tailsLength--- Step: Base Q.E.D.--- 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] tailsLength :: Ɐxs ∷ [Integer] → Bool-tailsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-tailsLength =- induct "tailsLength"- (\(Forall xs) -> length (tails xs) .== 1 + length xs) $- \ih (x, xs) -> [] |- length (tails (x .: xs))- =: length (tails xs ++ [x .: xs])- =: length (tails xs) + 1- ?? ih- =: 1 + length xs + 1- =: 1 + length (x .: xs)- =: qed---- | @tails (xs ++ ys) == map (++ ys) (tails xs) ++ tail (tails ys)@------ This property comes from Richard Bird's "Pearls of functional Algorithm Design" book, chapter 2.--- Note that it is not exactly as stated there, as the definition of @tail@ Bird uses is different--- than the standard Haskell function @tails@: Bird's version does not return the empty list as the--- tail. So, we slightly modify it to fit the standard definition. (NB. z3 is finicky on this--- problem, while cvc5 works much better.)------ >>> runTPWith cvc5 $ tailsAppend @Integer--- Inductive lemma: base case--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- Lemma: helper--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: tailsAppend--- Step: Base Q.E.D.--- 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] tailsAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-tailsAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-tailsAppend = do-- let -- Ideally, we would like to define appendEach like this:- --- -- appendEach xs ys = map (++ ys) xs- --- -- But capture of ys is not allowed when we use the higher-order- -- function map in SBV. So, we create a closure instead.- appendEach :: SList a -> SList [a] -> SList [a]- appendEach ys = map $ Closure { closureEnv = ys- , closureFun = \env xs -> xs ++ env- }-- -- Even proving the base case of induction is hard due to recursive definition. So we first prove the base case by induction.- bc <- induct "base case"- (\(Forall @"ys" (ys :: SList a)) -> tails ys .== [ys] ++ tail (tails ys)) $- \ih (y, ys) -> [] |- tails (y .: ys)- =: [y .: ys] ++ tails ys- ?? ih- =: [y .: ys] ++ [ys] ++ tail (tails ys)- =: [y .: ys] ++ tail (tails (y .: ys))- =: qed-- -- Also need a helper to relate how appendEach and tails work together- helper <- calc "helper"- (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"x" x) ->- appendEach ys (tails (x .: xs)) .== [(x .: xs) ++ ys] ++ appendEach ys (tails xs)) $- \xs ys x -> [] |- appendEach ys (tails (x .: xs))- =: appendEach ys ([x .: xs] ++ tails xs)- =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs)- =: qed-- induct "tailsAppend"- (\(Forall xs) (Forall ys) -> tails (xs ++ ys) .== appendEach ys (tails xs) ++ tail (tails ys)) $- \ih (x, xs) ys -> [assumptionFromProof bc]- |- tails ((x .: xs) ++ ys)- =: tails (x .: (xs ++ ys))- =: [x .: (xs ++ ys)] ++ tails (xs ++ ys)- ?? ih- =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs) ++ tail (tails ys)- ?? helper- =: appendEach ys (tails (x .: xs)) ++ tail (tails ys)- =: qed---- | @length xs == length (reverse xs)@------ >>> runTP $ revLen @Integer--- Inductive lemma: revLen--- Step: Base Q.E.D.--- 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] revLen :: Ɐxs ∷ [Integer] → Bool-revLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-revLen = induct "revLen"- (\(Forall xs) -> length (reverse xs) .== length xs) $- \ih (x, xs) -> [] |- length (reverse (x .: xs))- =: length (reverse xs ++ [x])- =: length (reverse xs) + length [x]- ?? ih- =: length xs + 1- =: length (x .: xs)- =: qed---- | @reverse (xs ++ ys) .== reverse ys ++ reverse xs@------ >>> runTP $ revApp @Integer--- Inductive lemma: revApp--- Step: 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.--- Result: Q.E.D.--- [Proven] revApp :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-revApp :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-revApp = induct "revApp"- (\(Forall xs) (Forall ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) $- \ih (x, xs) ys -> [] |- reverse ((x .: xs) ++ ys)- =: reverse (x .: (xs ++ ys))- =: reverse (xs ++ ys) ++ [x]- ?? ih- =: (reverse ys ++ reverse xs) ++ [x]- =: reverse ys ++ (reverse xs ++ [x])- =: reverse ys ++ reverse (x .: xs)- =: qed---- | @reverse (x:xs) == reverse xs ++ [x]@------ >>> runTP $ revCons @Integer--- Lemma: revCons Q.E.D.--- [Proven] revCons :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-revCons :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))-revCons = lemma "revCons"- (\(Forall x) (Forall xs) -> reverse (x .: xs) .== reverse xs ++ [x])- []---- | @reverse (xs ++ [x]) == x : reverse xs@------ >>> runTP $ revSnoc @Integer--- Inductive lemma: revApp--- Step: 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.--- Result: Q.E.D.--- Lemma: revSnoc Q.E.D.--- [Proven] revSnoc :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-revSnoc :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))-revSnoc = do- ra <- revApp @a-- lemma "revSnoc"- (\(Forall x) (Forall xs) -> reverse (xs ++ [x]) .== x .: reverse xs)- [proofOf ra]---- | @reverse (reverse xs) == xs@------ >>> runTP $ revRev @Integer--- Inductive lemma: revApp--- Step: 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.--- Result: Q.E.D.--- Inductive lemma: revRev--- Step: Base Q.E.D.--- 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] revRev :: Ɐxs ∷ [Integer] → Bool-revRev :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-revRev = do-- ra <- revApp @a-- induct "revRev"- (\(Forall xs) -> reverse (reverse xs) .== xs) $- \ih (x, xs) -> [] |- reverse (reverse (x .: xs))- =: reverse (reverse xs ++ [x])- ?? ra- =: reverse [x] ++ reverse (reverse xs)- ?? ih- =: [x] ++ xs- =: x .: xs- =: qed---- | \(\text{length } [n \dots m] = \max(0,\; m - n + 1)\)------ The proof uses the metric @|m-n|@.------ >>> runTP enumLen--- Inductive lemma (strong): enumLen--- Step: Measure is non-negative Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.2.3 Q.E.D.--- Step: 1.2.4 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool-enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))-enumLen =- sInduct "enumLen"- (\(Forall n) (Forall m) -> length [sEnum|n .. m|] .== 0 `smax` (m - n + 1))- (\n m -> abs (m - n), []) $- \ih n m -> [] |- length [sEnum|n+1 .. m|]- =: cases [ n+1 .> m ==> trivial- , n+1 .<= m ==> length (n+1 .: [sEnum|n+2 .. m|])- =: 1 + length [sEnum|n+2 .. m|]- ?? ih- =: 1 + (0 `smax` (m - (n+2) + 1))- =: 0 `smax` (m - (n+1) + 1)- =: qed- ]---- | @reverse [n .. m] == [m, m-1 .. n]@------ The proof uses the metric @|m-n|@.------ >>> runTP $ revNM--- Inductive lemma (strong): helper--- Step: Measure is non-negative Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- Inductive lemma (strong): revNM--- Step: Measure is non-negative Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.2.3 Q.E.D.--- Step: 1.2.4 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] revNM :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool-revNM :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))-revNM = do-- helper <- sInduct "helper"- (\(Forall @"m" (m :: SInteger)) (Forall @"n" n) ->- n .< m .=> [sEnum|m, m-1 .. n+1|] ++ [n] .== [sEnum|m, m-1 .. n|])- (\m n -> abs (m - n), []) $- \ih m n -> [n .< m] |- [sEnum|m, m-1 .. n+1|] ++ [n]- =: m .: [sEnum|m-1, m-2 .. n+1|] ++ [n]- ?? ih- =: m .: [sEnum|m-1, m-2 .. n|]- =: [sEnum|m, m-1 .. n|]- =: qed-- sInduct "revNM"- (\(Forall n) (Forall m) -> reverse [sEnum|n .. m|] .== [sEnum|m, m-1 .. n|])- (\n m -> abs (m - n), []) $- \ih n m -> [] |- reverse [sEnum|n .. m|]- =: cases [ n .> m ==> trivial- , n .<= m ==> reverse (n .: [sEnum|(n+1) .. m|])- =: reverse [sEnum|(n+1) .. m|] ++ [n]- ?? ih- =: [sEnum|m, m-1 .. n+1|] ++ [n]- ?? helper- =: [sEnum|m, m-1 .. n|]- =: qed- ]---- | @length (x : xs) == 1 + length xs@------ >>> runTP $ lengthTail @Integer--- Lemma: lengthTail Q.E.D.--- [Proven] lengthTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-lengthTail :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))-lengthTail = lemma "lengthTail"- (\(Forall x) (Forall xs) -> length (x .: xs) .== 1 + length xs)- []---- | @length (xs ++ ys) == length xs + length ys@------ >>> runTP $ lenAppend @Integer--- Lemma: lenAppend Q.E.D.--- [Proven] lenAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-lenAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-lenAppend = lemma "lenAppend"- (\(Forall xs) (Forall ys) -> length (xs ++ ys) .== length xs + length ys)- []---- | @length xs == length ys -> length (xs ++ ys) == 2 * length xs@------ >>> runTP $ lenAppend2 @Integer--- Lemma: lenAppend2 Q.E.D.--- [Proven] lenAppend2 :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-lenAppend2 :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-lenAppend2 = lemma "lenAppend2"- (\(Forall xs) (Forall ys) -> length xs .== length ys .=> length (xs ++ ys) .== 2 * length xs)- []---- | @length (replicate k x) == max (0, k)@------ >>> runTP $ replicateLength @Integer--- Inductive lemma: replicateLength--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.2.3 Q.E.D.--- Step: 1.2.4 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] replicateLength :: Ɐk ∷ Integer → Ɐx ∷ Integer → Bool-replicateLength :: forall a. SymVal a => TP (Proof (Forall "k" Integer -> Forall "x" a -> SBool))-replicateLength = induct "replicateLength"- (\(Forall k) (Forall x) -> length (replicate k x) .== 0 `smax` k) $- \ih k x -> [] |- length (replicate (k+1) x)- =: cases [ k .< 0 ==> trivial- , k .>= 0 ==> length (x .: replicate k x)- =: 1 + length (replicate k x)- ?? ih- =: 1 + 0 `smax` k- =: 0 `smax` (k+1)- =: qed- ]---- | @not (all id xs) == any not xs@------ A list of booleans is not all true, if any of them is false.------ >>> runTP allAny--- Inductive lemma: allAny--- Step: Base Q.E.D.--- 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] allAny :: Ɐxs ∷ [Bool] → Bool-allAny :: TP (Proof (Forall "xs" [Bool] -> SBool))-allAny = induct "allAny"- (\(Forall 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 .|| any sNot xs- =: any sNot (x .: xs)- =: qed---- | @f == g ==> map f xs == map g xs@------ >>> runTP $ mapEquiv @Integer @Integer (uninterpret "f") (uninterpret "g")--- Inductive lemma: mapEquiv--- Step: Base Q.E.D.--- 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] mapEquiv :: Ɐxs ∷ [Integer] → Bool-mapEquiv :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))-mapEquiv f g = do- let f'eq'g :: SBool- f'eq'g = quantifiedBool $ \(Forall x) -> f x .== g x-- induct "mapEquiv"- (\(Forall 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 x .: map f xs .== f x .: map g xs- ?? 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@------ >>> runTP $ mapAppend @Integer @Integer (uninterpret "f")--- Inductive lemma: mapAppend--- Step: 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.--- Result: Q.E.D.--- [Proven] mapAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-mapAppend :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-mapAppend f =- induct "mapAppend"- (\(Forall xs) (Forall 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 ++ map f ys)- =: (f x .: map f xs) ++ map f ys- =: map f (x .: xs) ++ map f ys- =: qed---- | @map f . reverse == reverse . map f@------ >>> runTP $ mapReverse @Integer @String (uninterpret "f")--- Inductive lemma: mapAppend--- Step: 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.--- Result: Q.E.D.--- Inductive lemma: mapReverse--- Step: 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.--- Result: Q.E.D.--- [Proven] mapReverse :: Ɐxs ∷ [Integer] → Bool-mapReverse :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))-mapReverse f = do- mApp <- mapAppend f-- induct "mapReverse"- (\(Forall 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) ++ [f x]- ?? ih- =: map f (reverse xs) ++ [f x]- =: map f (reverse xs) ++ map f [x]- ?? mApp- =: map f (reverse xs ++ [x])- =: map f (reverse (x .: xs))- =: qed---- | @map f . map g == map (f . g)@------ >>> runTP $ mapCompose @Integer @Bool @String (uninterpret "f") (uninterpret "g")--- Inductive lemma: mapCompose--- Step: 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.--- Result: Q.E.D.--- [Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool-mapCompose :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))-mapCompose f g =- induct "mapCompose"- (\(Forall xs) -> map g (map f xs) .== map (g . f) xs) $- \ih (x, xs) -> [] |- map g (map f (x .: xs))- =: map g (f x .: map f xs)- =: g (f x) .: map g (map f xs)- ?? ih- =: g (f x) .: map (g . f) xs- =: (g . f) x .: map (g . f) xs- =: map (g . f) (x .: xs)- =: qed---- | @foldr f a . map g == foldr (f . g) a@------ >>> runTP $ foldrMapFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "c")--- Inductive lemma: foldrMapFusion--- Step: Base Q.E.D.--- 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] foldrMapFusion :: Ɐxs ∷ [[Char]] → Bool-foldrMapFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> (SBV a -> SBV b) -> (SBV b -> SBV c -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))-foldrMapFusion a g f =- induct "foldrMapFusion"- (\(Forall 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 . g) a xs- =: foldr (f . g) a (x .: xs)- =: qed---- |------ @--- f . foldr g a == foldr h b--- provided, f a = b and for all x and y, f (g x y) == h x (f y).--- @------ >>> runTP $ foldrFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "f") (uninterpret "g") (uninterpret "h")--- Inductive lemma: foldrFusion--- Step: Base Q.E.D.--- 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] foldrFusion :: Ɐxs ∷ [[Char]] → Bool-foldrFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> SBV b -> (SBV c -> SBV b) -> (SBV a -> SBV c -> SBV c) -> (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))-foldrFusion a b f g h = do- let -- Assumptions under which the equality holds- h1 = f a .== b- h2 = quantifiedBool $ \(Forall x) (Forall y) -> f (g x y) .== h x (f y)-- induct "foldrFusion"- (\(Forall 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))- =: h x (f (foldr g a xs))- ?? ih- =: h x (foldr h b xs)- =: foldr h b (x .: xs)- =: qed---- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@------ >>> runTP $ foldrOverAppend @Integer (uninterpret "a") (uninterpret "f")--- Inductive lemma: foldrOverAppend--- Step: Base Q.E.D.--- 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] foldrOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-foldrOverAppend :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-foldrOverAppend a f =- induct "foldrOverAppend"- (\(Forall xs) (Forall 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 (foldr f a ys) xs- =: foldr f (foldr f a ys) (x .: xs)- =: qed---- | @foldl f e (xs ++ ys) == foldl f (foldl f e xs) ys@------ >>> runTP $ foldlOverAppend @Integer @Bool (uninterpret "f")--- Inductive lemma: foldlOverAppend--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- [Proven] foldlOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Bool → Bool-foldlOverAppend :: forall a b. (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" b -> SBool))-foldlOverAppend f =- induct "foldlOverAppend"- (\(Forall xs) (Forall ys) (Forall 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)- -- 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 @"e" (a `f` x))- =: foldl f (foldl f (a `f` x) xs) ys- =: qed---- | @foldr f e xs == foldl (flip f) e (reverse xs)@------ >>> runTP $ foldrFoldlDuality @Integer @String (uninterpret "f")--- Inductive lemma: foldlOverAppend--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: foldrFoldlDuality--- Step: 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.--- Result: Q.E.D.--- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Ɐe ∷ [Char] → Bool-foldrFoldlDuality :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "e" b -> SBool))-foldrFoldlDuality f = do- foa <- foldlOverAppend (flip f)-- induct "foldrFoldlDuality"- (\(Forall xs) (Forall e) -> foldr f e xs .== foldl (flip f) e (reverse xs)) $- \ih (x, xs) e -> [] |- let ff = flip f- rxs = reverse xs- 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) [x]- ?? foa- =: foldl ff e (rxs ++ [x])- =: foldl ff e (reverse (x .: xs))- =: qed---- | Given:------ @--- x \@ (y \@ z) = (x \@ y) \@ z (associativity of @)--- and e \@ x = x (left unit)--- and x \@ e = x (right unit)--- @------ Proves:------ @--- foldr (\@) e xs == foldl (\@) e xs--- @------ >>> runTP $ foldrFoldlDualityGeneralized @Integer (uninterpret "e") (uninterpret "|@|")--- Inductive lemma: helper--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: foldrFoldlDuality--- Step: 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.--- Result: Q.E.D.--- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Bool-foldrFoldlDualityGeneralized :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> SBool))-foldrFoldlDualityGeneralized e (@) = do- -- Assumptions under which the equality holds- let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x @ (y @ z) .== (x @ y) @ z- lunit = quantifiedBool $ \(Forall x) -> e @ x .== x- runit = quantifiedBool $ \(Forall x) -> x @ e .== x-- -- Helper: foldl (@) (y @ z) xs = y @ foldl (@) z xs- -- Note the instantiation of the IH at a different value for z. It turns out- -- we don't have to actually specify this since z3 can figure it out by itself, but we're being explicit.- 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- ?? ih `at` (Inst @"y" y, Inst @"z" (z @ x))- =: y @ foldl (@) (z @ x) xs- =: y @ foldl (@) z (x .: xs)- =: qed-- induct "foldrFoldlDuality"- (\(Forall xs) -> assoc .&& lunit .&& runit .=> foldr (@) e xs .== foldl (@) e xs) $- \ih (x, xs) -> [assoc, lunit, runit] |- foldr (@) e (x .: xs)- =: x @ foldr (@) e xs- ?? ih- =: x @ foldl (@) e xs- ?? helper- =: foldl (@) (x @ e) xs- ?? runit- =: foldl (@) x xs- ?? lunit- =: foldl (@) (e @ x) xs- =: foldl (@) e (x .: xs)- =: qed---- | Given:------ @--- (x \<+> y) \<*> z = x \<+> (y \<*> z)--- and x \<+> e = e \<*> x--- @------ Proves:------ @--- foldr (\<+>) e xs = foldl (\<*>) e xs--- @------ In Bird's Introduction to Functional Programming book (2nd edition) this is called the second duality theorem:------ >>> runTP $ foldrFoldl @Integer @String (uninterpret "<+>") (uninterpret "<*>") (uninterpret "e")--- Inductive lemma: foldl over <*>/<+>--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: foldrFoldl--- Step: 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.--- Result: Q.E.D.--- [Proven] foldrFoldl :: Ɐxs ∷ [Integer] → Bool-foldrFoldl :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool))-foldrFoldl (<+>) (<*>) e = do- -- Assumptions about the operators- let -- (x <+> y) <*> z == x <+> (y <*> z)- assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> (x <+> y) <*> z .== x <+> (y <*> z)-- -- x <+> e == e <*> x- unit = quantifiedBool $ \(Forall x) -> x <+> e .== e <*> x-- -- Helper: x <+> foldl (<*>) y xs == foldl (<*>) (x <+> y) xs- helper <-- induct "foldl over <*>/<+>"- (\(Forall @"xs" xs) (Forall @"x" x) (Forall @"y" y) -> assoc .=> x <+> foldl (<*>) y xs .== foldl (<*>) (x <+> y) xs) $-- -- 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- ?? 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-- -- Final proof:- induct "foldrFoldl"- (\(Forall xs) -> assoc .&& unit .=> foldr (<+>) e xs .== foldl (<*>) e xs) $- \ih (x, xs) -> [assoc, unit] |- foldr (<+>) e (x .: xs)- =: x <+> foldr (<+>) e xs- ?? ih- =: x <+> foldl (<*>) e xs- ?? helper- =: foldl (<*>) (x <+> e) xs- =: foldl (<*>) (e <*> x) xs- =: foldl (<*>) e (x .: xs)- =: qed---- | Provided @f@ is associative and @a@ is its both left and right-unit:------ @foldr f a . concat == foldr f a . map (foldr f a)@------ >>> runTP $ bookKeeping @Integer (uninterpret "a") (uninterpret "f")--- Inductive lemma: foldBase--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: foldrOverAppend--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: Q.E.D.--- Inductive lemma: bookKeeping--- Step: 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.--- Result: Q.E.D.--- [Proven] bookKeeping :: Ɐxss ∷ [[Integer]] → Bool------ NB. This theorem does not hold if @f@ does not have a left-unit! Consider the input @[[], [x]]@. Left hand side reduces to--- @x@, while the right hand side reduces to: @f a x@. And unless @f@ is commutative or @a@ is not also a left-unit,--- then one can find a counter-example. (Aside: if both left and right units exist for a binary operator, then they--- are necessarily the same element, since @l = f l r = r@. So, an equivalent statement could simply say @f@ has--- both left and right units.) A concrete counter-example is:------ @--- data T = A | B | C------ f :: T -> T -> T--- f C A = A--- f C B = A--- f x _ = x--- @------ You can verify @f@ is associative. Also note that @C@ is the right-unit for @f@, but it isn't the left-unit.--- In fact, @f@ has no-left unit by the above argument. In this case, the bookkeeping law produces @B@ for--- the left-hand-side, and @A@ for the right-hand-side for the input @[[], [B]]@.-bookKeeping :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xss" [[a]] -> SBool))-bookKeeping a f = do-- -- Assumptions about f- let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x `f` (y `f` z) .== (x `f` y) `f` z- rUnit = quantifiedBool $ \(Forall x) -> x `f` a .== x- lUnit = quantifiedBool $ \(Forall x) -> a `f` x .== x-- -- Helper: @foldr f y xs = foldr f a xs `f` y@- helper <- induct "foldBase"- (\(Forall xs) (Forall 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- ?? ih- =: x `f` (foldr f a xs `f` y)- =: (x `f` foldr f a xs) `f` y- =: foldr f a (x .: xs) `f` y- =: qed-- foa <- foldrOverAppend a f-- induct "bookKeeping"- (\(Forall xss) -> assoc .&& rUnit .&& lUnit .=> foldr f a (concat xss) .== foldr f a (map (foldr f 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- ?? ih- =: foldr f (foldr f a (map (foldr f a) xss)) xs- ?? helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (map (foldr f a) xss)))- =: foldr f a xs `f` foldr f a (map (foldr f a) xss)- =: foldr f a (foldr f a xs .: map (foldr f a) xss)- =: foldr f a (map (foldr f a) (xs .: xss))- =: qed---- | @filter p (xs ++ ys) == filter p xs ++ filter p ys@------ >>> runTP $ filterAppend @Integer (uninterpret "p")--- Inductive lemma: filterAppend--- Step: 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.--- Result: Q.E.D.--- [Proven] filterAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-filterAppend :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-filterAppend p =- induct "filterAppend"- (\(Forall xs) (Forall 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 ++ ys)) (filter p (xs ++ ys))- =: filter p (x .: (xs ++ ys))- =: filter p ((x .: xs) ++ ys)- =: qed---- | @filter p (concat xss) == concatMap (filter p xss)@------ >>> runTP $ filterConcat @Integer (uninterpret "f")--- Inductive lemma: filterAppend--- Step: 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.--- Result: Q.E.D.--- Inductive lemma: filterConcat--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- [Proven] filterConcat :: Ɐxss ∷ [[Integer]] → Bool-filterConcat :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xss" [[a]] -> SBool))-filterConcat p = do- fa <- filterAppend p-- inductWith cvc5 "filterConcat"- (\(Forall xss) -> filter p (concat xss) .== concatMap (filter p) xss) $- \ih (xs, xss) -> [] |- filter p (concat (xs .: xss))- =: filter p (xs ++ concat xss)- ?? fa- =: filter p xs ++ filter p (concat xss)- ?? ih- =: concatMap (filter p) (xs .: xss)- =: qed---- | @takeWhile f xs ++ dropWhile f xs == xs@------ >>> runTP $ takeDropWhile @Integer (uninterpret "f")--- Inductive lemma: takeDropWhile--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1.1 Q.E.D.--- Step: 1.1.2 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] takeDropWhile :: Ɐxs ∷ [Integer] → Bool-takeDropWhile :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))-takeDropWhile f =- induct "takeDropWhile"- (\(Forall xs) -> takeWhile f xs ++ dropWhile f xs .== xs) $- \ih (x, xs) -> [] |- takeWhile f (x .: xs) ++ dropWhile f (x .: xs)- =: cases [ f x ==> x .: takeWhile f xs ++ dropWhile f xs- ?? ih- =: x .: xs- =: qed- , sNot (f x) ==> [] ++ x .: xs- =: x .: xs- =: qed- ]--- | Remove adjacent duplicates.-destutter :: SymVal a => SList a -> SList a-destutter = smtFunction "destutter" $ \xs -> ite (null xs .|| null (tail xs))- xs- (let (a, as) = uncons xs- r = destutter as- in ite (a .== head as) r (a .: r))---- | @destutter (destutter xs) == destutter xs@------ >>> runTP $ destutterIdempotent @Integer--- Inductive lemma: helper1--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- Inductive lemma: helper2--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Result: Q.E.D.--- Inductive lemma (strong): helper3--- Step: Measure is non-negative Q.E.D.--- Step: 1 (2 way full case split)--- Step: 1.1 Q.E.D.--- Step: 1.2 (2 way full case split)--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2.1 Q.E.D.--- Step: 1.2.2.2 (2 way case split)--- Step: 1.2.2.2.1.1 Q.E.D.--- Step: 1.2.2.2.1.2 Q.E.D.--- Step: 1.2.2.2.2.1 Q.E.D.--- Step: 1.2.2.2.2.2 Q.E.D.--- Step: 1.2.2.2.Completeness Q.E.D.--- Result: Q.E.D.--- Lemma: destutterIdempotent Q.E.D.--- [Proven] destutterIdempotent :: Ɐxs ∷ [Integer] → Bool-destutterIdempotent :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))-destutterIdempotent = do-- -- No adjacent duplicates- let noAdd = smtFunction "noAdd" $ \xs -> null xs .|| null (tail xs) .|| (head xs ./= head (tail xs) .&& noAdd (tail xs))-- -- Helper: The head of a destuttered non-empty list does not change- helper1 <- induct "helper1"- (\(Forall @"xs" (xs :: SList a)) (Forall @"h" h) -> head (destutter (h .: xs)) .== h) $- \ih (x, xs) h -> []- |- head (destutter (h .: x .: xs))- =: cases [ h ./= x ==> trivial- , h .== x ==> head (destutter (x .: xs))- ?? ih- =: x- =: qed- ]-- -- Helper: show that if a list has no adjacent duplicates, then destutter leaves it unchanged:- helper2 <- induct "helper2"- (\(Forall @"xs" (xs :: SList a)) -> noAdd xs .=> destutter xs .== xs) $- \ih (x, xs) -> [noAdd (x .: xs)]- |- destutter (x .: xs)- ?? ih- =: x .: xs- =: qed-- -- Helper: prove that noAdd is true for the result of destutter- helper3 <- sInductWith cvc5 "helper3"- (\(Forall @"xs" (xs :: SList a)) -> noAdd (destutter xs))- (length, []) $- \ih xs -> []- |- noAdd (destutter xs)- =: split xs- trivial- (\a as -> split as- trivial- (\b bs -> noAdd (destutter (a .: b .: bs))- =: cases [a .== b ==> noAdd (destutter (b .: bs))- ?? ih- =: sTrue- =: qed- , a ./= b ==> noAdd (a .: destutter (b .: bs))- ?? helper1 `at` (Inst @"xs" bs, Inst @"h" b)- ?? ih- =: sTrue- =: qed- ]))-- -- Now we can prove idempotency easily:- lemma "destutterIdempotent"- (\(Forall xs) -> destutter (destutter xs) .== destutter xs)- [proofOf helper2, proofOf helper3]---- | @(as ++ bs) \\ cs == (as \\ cs) ++ (bs \\ cs)@------ >>> runTP $ appendDiff @Integer--- Inductive lemma: appendDiff--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Result: Q.E.D.--- [Proven] appendDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool-appendDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))-appendDiff = induct "appendDiff"- (\(Forall as) (Forall bs) (Forall cs) -> (as ++ bs) \\ cs .== (as \\ cs) ++ (bs \\ cs)) $- \ih (a, as) bs cs -> [] |- (a .: as ++ bs) \\ cs- =: (a .: (as ++ bs)) \\ cs- =: ite (a `elem` cs) ((as ++ bs) \\ cs) (a .: ((as ++ bs) \\ cs))- ?? ih- =: ((a .: as) \\ cs) ++ (bs \\ cs)- =: qed---- | @as \\ (bs ++ cs) == (as \\ bs) \\ cs@------ >>> runTP $ diffAppend @Integer--- Inductive lemma: diffAppend--- Step: Base Q.E.D.--- 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] diffAppend :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool-diffAppend :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))-diffAppend = induct "diffAppend"- (\(Forall as) (Forall bs) (Forall cs) -> as \\ (bs ++ cs) .== (as \\ bs) \\ cs) $- \ih (a, as) bs cs -> [] |- (a .: as) \\ (bs ++ cs)- =: ite (a `elem` (bs ++ cs)) (as \\ (bs ++ cs)) (a .: (as \\ (bs ++ cs)))- ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)- =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: (as \\ (bs ++ cs)))- ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)- =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: ((as \\ bs) \\ cs))- =: ((a .: as) \\ bs) \\ cs- =: qed---- | @(as \\ bs) \\ cs == (as \\ cs) \\ bs@------ >>> runTP $ diffDiff @Integer--- Inductive lemma: diffDiff--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1.1 Q.E.D.--- Step: 1.1.2 Q.E.D.--- Step: 1.1.3 (2 way case split)--- Step: 1.1.3.1 Q.E.D.--- Step: 1.1.3.2.1 Q.E.D.--- Step: 1.1.3.2.2 (a ∉ cs) Q.E.D.--- Step: 1.1.3.Completeness Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 (2 way case split)--- Step: 1.2.2.1.1 Q.E.D.--- Step: 1.2.2.1.2 Q.E.D.--- Step: 1.2.2.1.3 (a ∈ cs) Q.E.D.--- Step: 1.2.2.2.1 Q.E.D.--- Step: 1.2.2.2.2 Q.E.D.--- Step: 1.2.2.2.3 (a ∉ bs) Q.E.D.--- Step: 1.2.2.2.4 (a ∉ cs) Q.E.D.--- Step: 1.2.2.Completeness Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] diffDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool-diffDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))-diffDiff = induct "diffDiff"- (\(Forall as) (Forall bs) (Forall cs) -> (as \\ bs) \\ cs .== (as \\ cs) \\ bs) $- \ih (a, as) bs cs ->- [] |- ((a .: as) \\ bs) \\ cs- =: cases [ a `elem` bs ==> (as \\ bs) \\ cs- ?? ih- =: (as \\ cs) \\ bs- =: cases [ a `elem` cs ==> ((a .: as) \\ cs) \\ bs- =: qed- , a `notElem` cs ==> (a .: (as \\ cs)) \\ bs- ?? "a ∉ cs"- =: ((a .: as) \\ cs) \\ bs- =: qed- ]- , a `notElem` bs ==> (a .: (as \\ bs)) \\ cs- =: cases [ a `elem` cs ==> (as \\ bs) \\ cs- ?? ih- =: (as \\ cs) \\ bs- ?? "a ∈ cs"- =: ((a .: as) \\ cs) \\ bs- =: qed- , a `notElem` cs ==> a .: ((as \\ bs) \\ cs)- ?? ih- =: a .: ((as \\ cs) \\ bs)- ?? "a ∉ bs"- =: (a .: (as \\ cs)) \\ bs- ?? "a ∉ cs"- =: ((a .: as) \\ cs) \\ bs- =: qed- ]- ]---- | Are the two lists disjoint?-disjoint :: (Eq a, SymVal a) => SList a -> SList a -> SBool-disjoint = smtFunction "disjoint" $ \xs ys -> null xs .|| head xs `notElem` ys .&& disjoint (tail xs) ys---- | @disjoint as bs .=> as \\ bs == as@------ >>> runTP $ disjointDiff @Integer--- Inductive lemma: disjointDiff--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Result: Q.E.D.--- [Proven] disjointDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Bool-disjointDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> SBool))-disjointDiff = induct "disjointDiff"- (\(Forall as) (Forall bs) -> disjoint as bs .=> as \\ bs .== as) $- \ih (a, as) bs -> [disjoint (a .: as) bs]- |- (a .: as) \\ bs- =: a .: (as \\ bs)- ?? ih- =: a .: as- =: qed---- | @fst (partition f xs) == filter f xs@------ >>> runTP $ partition1 @Integer (uninterpret "f")--- Inductive lemma: partition1--- Step: Base Q.E.D.--- 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] partition1 :: Ɐxs ∷ [Integer] → Bool-partition1 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))-partition1 f =- induct "partition1"- (\(Forall 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@------ >>> runTP $ partition2 @Integer (uninterpret "f")--- Inductive lemma: partition2--- Step: Base Q.E.D.--- 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] partition2 :: Ɐxs ∷ [Integer] → Bool-partition2 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))-partition2 f =- induct "partition2"- (\(Forall 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 n (take m xs) == take (n `smin` m) xs@------ >>> runTP $ take_take @Integer--- Lemma: take_take Q.E.D.--- [Proven] take_take :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-take_take :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))-take_take = lemma "take_take"- (\(Forall m) (Forall n) (Forall xs) -> take n (take m xs) .== take (n `smin` m) xs)- []---- | @n >= 0 && m >= 0 ==> drop n (drop m xs) == drop (n + m) xs@------ >>> runTP $ drop_drop @Integer--- Lemma: drop_drop Q.E.D.--- [Proven] drop_drop :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-drop_drop :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))-drop_drop = lemma "drop_drop"- (\(Forall m) (Forall n) (Forall xs) -> n .>= 0 .&& m .>= 0 .=> drop n (drop m xs) .== drop (n + m) xs)- []---- | @take n xs ++ drop n xs == xs@------ >>> runTP $ take_drop @Integer--- Lemma: take_drop Q.E.D.--- [Proven] take_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-take_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-take_drop = lemma "take_drop"- (\(Forall n) (Forall xs) -> take n xs ++ drop n xs .== xs)- []---- | @n .> 0 ==> take n (x .: xs) == x .: take (n - 1) xs@------ >>> runTP $ take_cons @Integer--- Lemma: take_cons Q.E.D.--- [Proven] take_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-take_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))-take_cons = lemma "take_cons"- (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> take n (x .: xs) .== x .: take (n - 1) xs)- []---- | @take n (map f xs) == map f (take n xs)@------ >>> runTP $ take_map @Integer @Integer (uninterpret "f")--- 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--- Step: 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.--- Result: Q.E.D.--- Lemma: take_map--- Step: 1 Q.E.D.--- Result: Q.E.D.--- [Proven] take_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-take_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-take_map f = do- tc <- take_cons @a-- map1 <- lemma "map1"- (\(Forall x) (Forall 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)- =: 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)- ?? tc- =: map f (take n (x .: xs))- =: qed-- calc "take_map"- (\(Forall n) (Forall xs) -> take n (map f xs) .== map f (take n xs)) $- \n xs -> [] |- take n (map f xs)- ?? h1- ?? h2- =: map f (take n xs)- =: qed---- | @n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs@------ >>> runTP $ drop_cons @Integer--- Lemma: drop_cons Q.E.D.--- [Proven] drop_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool-drop_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))-drop_cons = lemma "drop_cons"- (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs)- []---- | @drop n (map f xs) == map f (drop n xs)@------ >>> runTP $ drop_map @Integer @String (uninterpret "f")--- 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--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Result: 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 :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-drop_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-drop_map f = do- dcA <- drop_cons @a- dcB <- drop_cons @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)- ?? dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs))- =: drop (n - 1) (map f xs)- ?? ih `at` Inst @"n" (n-1)- =: map f (drop (n - 1) xs)- ?? 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 n) (Forall xs) -> drop n (map f xs) .== map f (drop n xs)) $- \n xs -> [] |- 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@------ >>> runTP $ length_take @Integer--- Lemma: length_take Q.E.D.--- [Proven] length_take :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-length_take :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-length_take = lemma "length_take"- (\(Forall n) (Forall xs) -> n .>= 0 .=> length (take n xs) .== length xs `smin` n)- []---- | @n >= 0 ==> length (drop n xs) == (length xs - n) \`max\` 0@------ >>> runTP $ length_drop @Integer--- Lemma: length_drop Q.E.D.--- [Proven] length_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-length_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-length_drop = lemma "length_drop"- (\(Forall n) (Forall xs) -> n .>= 0 .=> length (drop n xs) .== (length xs - n) `smax` 0)- []---- | @length xs \<= n ==\> take n xs == xs@------ >>> runTP $ take_all @Integer--- Lemma: take_all Q.E.D.--- [Proven] take_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-take_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-take_all = lemma "take_all"- (\(Forall n) (Forall xs) -> length xs .<= n .=> take n xs .== xs)- []---- | @length xs \<= n ==\> drop n xs == nil@------ >>> runTP $ drop_all @Integer--- Lemma: drop_all Q.E.D.--- [Proven] drop_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool-drop_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))-drop_all = lemma "drop_all"- (\(Forall n) (Forall xs) -> length xs .<= n .=> drop n xs .== nil)- []---- | @take n (xs ++ ys) == (take n xs ++ take (n - length xs) ys)@------ >>> runTP $ take_append @Integer--- Lemma: take_append Q.E.D.--- [Proven] take_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-take_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))-take_append = lemmaWith cvc5 "take_append"- (\(Forall n) (Forall xs) (Forall ys) -> take n (xs ++ ys) .== take n xs ++ take (n - length xs) ys)- []---- | @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.------ >>> runTP $ drop_append @Integer--- Lemma: drop_append Q.E.D.--- [Proven] drop_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-drop_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))-drop_append = lemmaWith cvc5 "drop_append"- (\(Forall n) (Forall xs) (Forall ys) -> drop n (xs ++ ys) .== drop n xs ++ drop (n - length xs) ys)- []---- | @length xs == length ys ==> map fst (zip xs ys) = xs@------ >>> runTP $ map_fst_zip @Integer @Integer--- Inductive lemma: map_fst_zip--- Step: Base Q.E.D.--- 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] map_fst_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool-map_fst_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))-map_fst_zip = induct "map_fst_zip"- (\(Forall xs, Forall ys) -> length xs .== length ys .=> map fst (zip xs ys) .== xs) $- \ih (x, xs, y, 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)- ?? ih- =: x .: xs- =: qed---- | @length xs == length ys ==> map snd (zip xs ys) = xs@------ >>> runTP $ map_snd_zip @Integer @Integer--- Inductive lemma: map_snd_zip--- Step: Base Q.E.D.--- 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] map_snd_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool-map_snd_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))-map_snd_zip = induct "map_snd_zip"- (\(Forall xs, Forall ys) -> length xs .== length ys .=> map snd (zip xs ys) .== ys) $- \ih (x, xs, y, 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)- ?? ih- =: y .: ys- =: qed---- | @map fst (zip xs ys) == take (min (length xs) (length ys)) xs@------ >>> runTP $ map_fst_zip_take @Integer @Integer--- Lemma: take_cons Q.E.D.--- Inductive lemma: map_fst_zip_take--- Step: 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.--- Result: Q.E.D.--- [Proven] map_fst_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool-map_fst_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))-map_fst_zip_take = do- tc <- take_cons @a-- induct "map_fst_zip_take"- (\(Forall xs, Forall ys) -> map fst (zip xs ys) .== take (length xs `smin` length ys) xs) $- \ih (x, xs, y, 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@------ >>> runTP $ map_snd_zip_take @Integer @Integer--- Lemma: take_cons Q.E.D.--- Inductive lemma: map_snd_zip_take--- Step: 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.--- Result: Q.E.D.--- [Proven] map_snd_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool-map_snd_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))-map_snd_zip_take = do- tc <- take_cons @a-- induct "map_snd_zip_take"- (\(Forall xs, Forall ys) -> map snd (zip xs ys) .== take (length xs `smin` length ys) ys) $- \ih (x, xs, y, 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---- | Count the number of occurrences of an element in a list-count :: SymVal a => SBV a -> SList a -> SInteger-count = smtFunction "count" $ \e l -> ite (null l)- 0- (let (x, xs) = uncons l- cxs = count e xs- in ite (e .== x) (1 + cxs) cxs)---- | Interleave the elements of two lists. If one ends, we take the rest from the other.-interleave :: SymVal a => SList a -> SList a -> SList a-interleave = smtFunction "interleave" (\xs ys -> ite (null xs) ys (head xs .: interleave ys (tail xs)))---- | Prove that interleave preserves total length.------ The induction here is on the total length of the lists, and hence--- we use the generalized induction principle. We have:------ >>> runTP $ interleaveLen @Integer--- Inductive lemma (strong): interleaveLen--- Step: Measure is non-negative Q.E.D.--- Step: 1 (2 way full case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.2.3 Q.E.D.--- Result: Q.E.D.--- [Proven] interleaveLen :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-interleaveLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-interleaveLen = sInduct "interleaveLen"- (\(Forall xs) (Forall ys) -> length xs + length ys .== length (interleave xs ys))- (\xs ys -> length xs + length ys, []) $- \ih xs ys -> [] |- length xs + length ys .== length (interleave xs ys)- =: split xs- trivial- (\a as -> length (a .: as) + length ys .== length (interleave (a .: as) ys)- =: 1 + length as + length ys .== 1 + length (interleave ys as)- ?? ih `at` (Inst @"xs" ys, Inst @"ys" as)- =: sTrue- =: qed)---- | Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.-uninterleave :: SymVal a => SList a -> STuple [a] [a]-uninterleave lst = uninterleaveGen lst (tuple (nil, nil))---- | Generalized form of uninterleave with the auxilary lists made explicit.-uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]-uninterleaveGen = smtFunction "uninterleave" (\xs alts -> let (es, os) = untuple alts- in ite (null xs)- (tuple (reverse es, reverse os))- (uninterleaveGen (tail xs) (tuple (os, head xs .: es))))---- | The functions 'uninterleave' and 'interleave' are inverses so long as the inputs are of the same length. (The equality--- would even hold if the first argument has one extra element, but we keep things simple here.)------ We have:------ >>> runTP $ interleaveRoundTrip @Integer--- Lemma: revCons Q.E.D.--- Inductive lemma (strong): roundTripGen--- Step: Measure is non-negative Q.E.D.--- Step: 1 (4 way full case split)--- Step: 1.1 Q.E.D.--- Step: 1.2 Q.E.D.--- Step: 1.3 Q.E.D.--- Step: 1.4.1 Q.E.D.--- Step: 1.4.2 Q.E.D.--- Step: 1.4.3 Q.E.D.--- Step: 1.4.4 Q.E.D.--- Step: 1.4.5 Q.E.D.--- Step: 1.4.6 Q.E.D.--- Step: 1.4.7 Q.E.D.--- Step: 1.4.8 Q.E.D.--- Result: Q.E.D.--- Lemma: interleaveRoundTrip--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Result: Q.E.D.--- [Proven] interleaveRoundTrip :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool-interleaveRoundTrip :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))-interleaveRoundTrip = do-- revHelper <- lemma "revCons" (\(Forall a) (Forall as) (Forall bs) -> reverse @a (a .: as) ++ bs .== reverse as ++ (a .: bs)) []-- -- Generalize the theorem first to take the helper lists explicitly- roundTripGen <- sInductWith cvc5- "roundTripGen"- (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"alts" alts) ->- length xs .== length ys .=> let (es, os) = untuple alts- in uninterleaveGen (interleave xs ys) alts .== tuple (reverse es ++ xs, reverse os ++ ys))- (\xs ys _alts -> length xs + length ys, []) $- \ih xs ys alts -> [length xs .== length ys]- |- let (es, os) = untuple alts- in uninterleaveGen (interleave xs ys) alts- =: split2 (xs, ys)- trivial- trivial- trivial- (\(a, as) (b, bs) -> uninterleaveGen (interleave (a .: as) (b .: bs)) alts- =: uninterleaveGen (a .: interleave (b .: bs) as) alts- =: uninterleaveGen (a .: b .: interleave as bs) alts- =: uninterleaveGen (interleave as bs) (tuple (a .: es, b .: os))- ?? ih `at` (Inst @"xs" as, Inst @"ys" bs, Inst @"alts" (tuple (a .: es, b .: os)))- =: tuple (reverse (a .: es) ++ as, reverse (b .: os) ++ bs)- ?? revHelper `at` (Inst @"a" a, Inst @"as" es, Inst @"bs" as)- =: tuple (reverse es ++ (a .: as), reverse (b .: os) ++ bs)- ?? revHelper `at` (Inst @"a" b, Inst @"as" os, Inst @"bs" bs)- =: tuple (reverse es ++ (a .: as), reverse os ++ (b .: bs))- =: tuple (reverse es ++ xs, reverse os ++ ys)- =: qed)-- -- Round-trip theorem:- calc "interleaveRoundTrip"- (\(Forall xs) (Forall ys) -> length xs .== length ys .=> uninterleave (interleave xs ys) .== tuple (xs, ys)) $- \xs ys -> [length xs .== length ys]- |- uninterleave (interleave xs ys)- =: uninterleaveGen (interleave xs ys) (tuple (nil, nil))- ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple (nil, nil)))- =: tuple (reverse nil ++ xs, reverse nil ++ ys)- =: qed---- | @count e (xs ++ ys) == count e xs + count e ys@------ >>> runTP $ countAppend @Integer--- Inductive lemma: countAppend--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 (unfold count) Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 (simplify) Q.E.D.--- Result: Q.E.D.--- [Proven] countAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Integer → Bool-countAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))-countAppend =- induct "countAppend"- (\(Forall xs) (Forall ys) (Forall e) -> count e (xs ++ ys) .== count e xs + count e ys) $- \ih (x, xs) ys e -> [] |- count e ((x .: xs) ++ ys)- =: count e (x .: (xs ++ ys))- ?? "unfold count"- =: (let r = count e (xs ++ ys) in ite (e .== x) (1+r) r)- ?? ih `at` (Inst @"ys" ys, Inst @"e" e)- =: (let r = count e xs + count e ys in ite (e .== x) (1+r) r)- ?? "simplify"- =: count e (x .: xs) + count e ys- =: qed---- | @count e (take n xs) + count e (drop n xs) == count e xs@------ >>> runTP $ takeDropCount @Integer--- Inductive lemma: countAppend--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 (unfold count) Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 (simplify) Q.E.D.--- Result: Q.E.D.--- Lemma: take_drop Q.E.D.--- Lemma: takeDropCount--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Result: Q.E.D.--- [Proven] takeDropCount :: Ɐxs ∷ [Integer] → Ɐn ∷ Integer → Ɐe ∷ Integer → Bool-takeDropCount :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool))-takeDropCount = do- capp <- countAppend @a- takeDrop <- take_drop @a-- calc "takeDropCount"- (\(Forall xs) (Forall n) (Forall e) -> count e (take n xs) + count e (drop n xs) .== count e xs) $- \xs n e -> [] |- count e (take n xs) + count e (drop n xs)- ?? capp `at` (Inst @"xs" (take n xs), Inst @"ys" (drop n xs), Inst @"e" e)- =: count e (take n xs ++ drop n xs)- ?? takeDrop- =: count e xs- =: qed---- | @count e xs >= 0@------ >>> runTP $ countNonNeg @Integer--- Inductive lemma: countNonNeg--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1.1 Q.E.D.--- Step: 1.1.2 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] countNonNeg :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool-countNonNeg :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))-countNonNeg =- induct "countNonNeg"- (\(Forall xs) (Forall e) -> count e xs .>= 0) $- \ih (x, xs) e -> [] |- count e (x .: xs) .>= 0- =: cases [ e .== x ==> 1 + count e xs .>= 0- ?? ih- =: sTrue- =: qed- , e ./= x ==> count e xs .>= 0- ?? ih- =: sTrue- =: qed- ]---- | @e \`elem\` xs ==> count e xs .> 0@------ >>> runTP $ countElem @Integer--- Inductive lemma: countNonNeg--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1.1 Q.E.D.--- Step: 1.1.2 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- Inductive lemma: countElem--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1.1 Q.E.D.--- Step: 1.1.2 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] countElem :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool-countElem :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))-countElem = do-- cnn <- countNonNeg @a-- induct "countElem"- (\(Forall xs) (Forall e) -> e `elem` xs .=> count e xs .> 0) $- \ih (x, xs) e -> [e `elem` (x .: xs)]- |- count e (x .: xs) .> 0- =: cases [ e .== x ==> 1 + count e xs .> 0- ?? cnn- =: sTrue- =: qed- , e ./= x ==> count e xs .> 0- ?? ih- =: sTrue- =: qed- ]---- | @count e xs .> 0 .=> e \`elem\` xs@------ >>> runTP $ elemCount @Integer--- Inductive lemma: elemCount--- Step: Base Q.E.D.--- Step: 1 (2 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2.1 Q.E.D.--- Step: 1.2.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.--- [Proven] elemCount :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool-elemCount :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))-elemCount =- induct "elemCount"- (\(Forall xs) (Forall e) -> count e xs .> 0 .=> e `elem` xs) $- \ih (x, xs) e -> [count e xs .> 0]- |- e `elem` (x .: xs)- =: cases [ e .== x ==> trivial- , e ./= x ==> e `elem` xs- ?? ih- =: sTrue- =: qed- ]--{- HLint ignore revRev "Redundant reverse" -}-{- HLint ignore allAny "Use and" -}-{- HLint ignore bookKeeping "Fuse foldr/map" -}-{- 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" -}-{- HLint ignore mapCompose "Use map once" -}-{- HLint ignore tailsAppend "Avoid lambda" -}-{- HLint ignore tailsAppend "Use :" -}-{- HLint ignore mapReverse "Evaluate" -}-{- HLint ignore takeDropWhile "Evaluate" -}
Data/SBV/TP/TP.hs view
@@ -34,7 +34,7 @@ , (|-), (|->), (⊢), (=:), (≡), (??), (∵), split, split2, cases, (==>), (⟹), qed, trivial, contradiction , qc, qcWith , disp- , recall+ , recall, recallWith ) where import Data.SBV@@ -91,11 +91,6 @@ getCalcStrategySaturatables :: CalcStrategy -> [SBool] getCalcStrategySaturatables (CalcStrategy calcIntros calcProofTree _calcQCInstance) = calcIntros : proofTreeSaturatables calcProofTree --- | Propagate the settings for ribbon/timing from top to current. Because in any subsequent configuration--- in a lemmaWith, inductWith etc., we just want to change the solver, not the actual settings for TP.-tpMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig-tpMergeCfg cur top = cur{tpOptions = tpOptions top}- -- | Use an injective type family to allow for curried use of calc and strong induction steps. type family StepArgs a t = result | result -> t where StepArgs SBool t = (SBool, TPProofRaw (SBV t))@@ -1525,15 +1520,26 @@ -- | Recalling a proof. This essentially sets the verbose output off during this proof. Note that -- if we're doing stats, we ignore this as the whole point of doing stats is to see steps in detail. recall :: String -> TP (Proof a) -> TP (Proof a)-recall nm prf = do- cfg <- getTPConfig- if printStats (tpOptions cfg)- then prf+recall nm prf = getTPConfig >>= \cfg -> recallWith cfg nm prf++-- | Recalling a proof, using a given config. We keep the stat field as the or of the current and the context+-- configuration.+recallWith :: SMTConfig -> String -> TP (Proof a) -> TP (Proof a)+recallWith cfgIn nm prf = do+ topCfg <- getTPConfig+ let cfg@SMTConfig{tpOptions = TPOptions{printStats}} = cfgIn `tpMergeCfg` topCfg+ if printStats+ then do restoring cfg topCfg prf else do tab <- liftIO $ startTP cfg (verbose cfg) "Lemma" 0 (TPProofOneShot nm [])- setTPConfig cfg{tpOptions = (tpOptions cfg) {quiet = True}}- r@Proof{proofOf = ProofObj{dependencies}} <- prf- setTPConfig cfg- liftIO $ finishTP cfg ("Q.E.D." ++ concludeModulo dependencies) (tab, Nothing) []- pure r+ let new = cfg{tpOptions = (tpOptions cfg) {quiet = True}}+ restoring new topCfg $ do+ r@Proof{proofOf = ProofObj{dependencies}} <- prf+ liftIO $ finishTP cfg ("Q.E.D." ++ concludeModulo dependencies) (tab, Nothing) []+ pure r+ where restoring new old act = do setTPConfig new+ res <- act+ setTPConfig old+ pure res -{- HLint ignore module "Eta reduce" -}+{- HLint ignore module "Eta reduce" -}+{- HLint ignore module "Reduce duplication" -}
Documentation/SBV/Examples/ADT/Expr.hs view
@@ -162,3 +162,5 @@ io $ putStrLn $ "e1: " ++ show e1v io $ putStrLn $ "e2: " ++ show e2v _ -> error $ "Unexpected result: " ++ show cs++{- HLint ignore module "Reduce duplication" -}
Documentation/SBV/Examples/ADT/Param.hs view
@@ -181,3 +181,5 @@ io $ putStrLn $ "e2: " ++ show e2v io $ putStrLn $ "e3: " ++ show e3v _ -> error $ "Unexpected result: " ++ show cs++{- HLint ignore module "Reduce duplication" -}
Documentation/SBV/Examples/Crypto/AES.hs view
@@ -908,6 +908,7 @@ chop4 [] = [] chop4 xs = let (f, r) = splitAt 4 xs in f : chop4 r -{- HLint ignore aesRound "Use head" -}-{- HLint ignore aesInvRound "Use head" -}-{- HLint ignore aesDecryptUnwoundKey "Use head" -}+{- HLint ignore aesRound "Use head" -}+{- HLint ignore aesInvRound "Use head" -}+{- HLint ignore aesDecryptUnwoundKey "Use head" -}+{- HLint ignore module "Reduce duplication" -}
Documentation/SBV/Examples/Misc/FirstOrderLogic.hs view
@@ -15,11 +15,8 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}--#if MIN_VERSION_base(4,19,0) {-# LANGUAGE TypeAbstractions #-}-#endif+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-}
Documentation/SBV/Examples/Misc/LambdaArray.hs view
@@ -66,3 +66,5 @@ -- Let read produce non-zero constrain $ observe "Read" (readArray (memset mem lo hi zero) idx) ./= zero++{- HLint ignore module "Reduce duplication" -}
+ Documentation/SBV/Examples/Puzzles/SquareBirthday.hs view
@@ -0,0 +1,202 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.Puzzles.SquareBirthday+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- As of January 2026, to access the careers link at <http://math.inc>, you need to solve the following+-- puzzle:+--+-- @+-- Suppose that today is June 1, 2025. We call a date "square" if all of its components (day, month, and year) are+-- perfect squares. I was born in the last millennium, and my next birthday (relative to that date) will be the last+-- square date in my life. If you sum the square roots of the components of that upcoming square birthday+-- (day, month, year), you obtain my age on June 1, 2025. My mother would have been born on a square date if the month+-- were a square number; in reality it is not a square date, but both the month and day are perfect cubes. When was+-- I born, and when was my mother born?+-- @+--+-- So, let's solve it using SBV.+-----------------------------------------------------------------------------++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE OverloadedRecordDot #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.Puzzles.SquareBirthday where++import Prelude hiding (fromEnum, toEnum)++import Data.SBV+import Data.SBV.Control++import qualified Data.SBV.List as SL+import qualified Data.SBV.Tuple as ST++-- | Months in a year.+data Month = Jan | Feb | Mar | Apr | May | Jun+ | Jul | Aug | Sep | Oct | Nov | Dec+ deriving Show++-- | A date. We use unbounded integers for day and year, which simplifies coding,+-- though one can also enumerate the possible values from the problem itself.+data Date = MkDate { day :: Integer+ , month :: Month+ , year :: Integer+ }++-- | Make 'Month' and 'Date' usable in symbolic contexts.+mkSymbolic [''Month, ''Date]++-- | Show instance for date, for pretty-printing.+instance Show Date where+ show (MkDate d m y) = show m ++ " " ++ pad ++ show d ++ ", " ++ show y+ where pad | d < 10 = " "+ | True = ""++-- | Get a symbolic date with the given name. Since we used+-- integers for the day and year fields, we constrain them+-- appropriately. Note that one can further constrain days+-- based on the year and month; but that level detail isn't+-- necessary for the current problem.+symDate :: String -> Symbolic SDate+symDate nm = do dt <- free nm++ constrain [sCase|Date dt of+ MkDate d _ y -> sAnd [ 1 .<= d, d .<= 31+ , 0 .<= y+ ]+ |]++ pure dt++-- | Encode today as a symbolic value. The puzzle says today is June 1st, 2025.+today :: SDate+today = literal $ MkDate { day = 1+ , month = Jun+ , year = 2025+ }++-- | A date is on or after another, if the month-day combo is+-- lexicographically later. Note that we ignore the year for this+-- comparison, as we're interested if the anniversary of a date is after or not.+onOrAfter :: SDate -> SDate -> SBool+d1 `onOrAfter` d2 = (smonth d1, sday d1) .>= (smonth d2, sday d2)++-- | Similar to 'onOrAfter', except we require strictly later.+after :: SDate -> SDate -> SBool+d1 `after` d2 = (smonth d1, sday d1) .> (smonth d2, sday d2)++-- | The age based on a given date is the difference between years less than one.+-- We have to adjust by 1 if today happens to be after the given date.+age :: SDate -> SInteger+age d = syear today - syear d - 1 + oneIf (today `after` d)++-- | We can let years to range over arbitrary integers. But that complicates the+-- job of the solver. So, based on what we know from the problem, we restrict+-- our attention to years betweek 1900 and 2100. Note that there are only+-- two years that satisfy this in that range: 1936 and 2025. (Any other square+-- year makes no sense for the setting of the problem.) To simplify the square-root+-- computation, we also store the square root in this list as the second component:+--+-- >>> squareYears+-- [(1936,44),(2025,45)]+squareYears :: [(Integer, Integer)]+squareYears = takeWhile (\(y, _) -> y < 2100)+ $ dropWhile (\(y, _) -> y < 1900)+ $ [(i * i, i) | i <- [1::Integer ..]]++-- | A date is square if all its components are.+squareDate :: SDate -> SBool+squareDate dt = [sCase|Date dt of+ MkDate d m y -> squareDay d .&& squareMonth m .&& squareYear y+ |]+ where squareDay d = d `sElem` [1, 4, 9, 16, 25]+ squareMonth m = m `sElem` [sJan, sApr, sSep]+ squareYear y = y `sElem` map (literal . fst) squareYears+++-- | Summing the square-roots of the components of a date.+sqrSum :: SDate -> SInteger+sqrSum dt = [sCase|Date dt of+ MkDate d m y -> r d + mr m + r y+ |]+ where r v = v `SL.lookup` literal ([(i * i, i) | i <- [1, 2, 3, 4, 5]] ++ squareYears)++ mr :: SMonth -> SInteger+ mr m = [sCase|Month m of+ Jan -> 1+ Apr -> 2+ Sep -> 3+ _ -> some "Non-Square Month" (const sTrue)+ |]++-- | Formalizing the puzzle. We literally write down the description in+-- SBV notation. As with any formalization, this step is subjective; there+-- could be many different ways to express the same problem. The description+-- below is quite faithful to the problem description given. We have:+--+-- >>> puzzle+-- Me : Sep 25, 1971+-- Mom: Aug 1, 1936+puzzle :: IO ()+puzzle = runSMT $ do++ -----------------------------------+ -- Constraints about my birthday+ -----------------------------------+ myBirthday <- symDate "My Birthday"++ -- I was born in the last millenium+ constrain $ syear myBirthday .< 2000 .&& syear myBirthday .>= 1900++ -- My next birthday will be a square+ let next = [sCase|Date myBirthday of+ MkDate d m _ -> sMkDate d m (syear today + oneIf (today `onOrAfter` myBirthday))+ |]++ constrain $ squareDate next++ -- And it'll be the last square day of my life, so we maximize the metric corresponding to the+ -- date. We turn it into a 3-tuple of year, month, date over integers, which preserves the+ -- order of the dates.+ maximize "Next Birthday Latest" $ ST.tuple (syear next, fromEnum (smonth next), sday next)++ -- If you square the components of my next birthday, it gives me my current age on Jun 1, 2025+ constrain $ sqrSum next .== age myBirthday++ -----------------------------------+ -- Constraints about mom's birthday+ -----------------------------------+ momBirthday <- symDate "Mom's Birthday"++ -- Mom has a square birth-date, except for the month:+ constrain [sCase|Date momBirthday of+ MkDate d _ y -> squareDate (sMkDate d sJan y)+ |]++ -- Mom's day and month are perfect cubes+ constrain [sCase|Date momBirthday of+ MkDate d m _ -> sAnd [ d `sElem` [1, 8, 27]+ , m `sElem` [sJan, sAug]+ ]+ |]++ -- Extract the results:+ query $ do cs <- checkSat+ case cs of+ Sat -> do me <- getValue myBirthday+ mom <- getValue momBirthday++ io $ do putStrLn $ "Me : " ++ show me+ putStrLn $ "Mom: " ++ show mom++ _ -> error $ "Unexpected result: " ++ show cs
Documentation/SBV/Examples/TP/Basics.hs view
@@ -115,18 +115,18 @@ -- *** Failed to prove forallConjunctionNot. -- Falsifiable. Counter-example: -- p :: Integer -> Bool--- p 2 = True--- p 1 = False+-- p 4 = True+-- p 3 = False -- p _ = True -- <BLANKLINE> -- q :: Integer -> Bool--- q 2 = False--- q 1 = True+-- q 4 = False+-- q 3 = True -- q _ = True ----- Note how @p@ assigns two selected values to @True@ and everything else to @False@, while @q@ does the exact opposite.--- So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds--- a model with two distinct values, as one would have sufficed. But it is still a valud model.)+-- Note how @p@ and @q@ differ in their treatment of the inputs 3 and 4, but agree everywhere else. So, for each+-- input, at least one of @p@ or @q@ is @True@, making the disjunction @True@ for all inputs. But the predicates+-- @p@ and @q@ are not universally true themselves, constituting a counter-example. forallDisjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO () forallDisjunctionNot p q = runTP $ do let qb = quantifiedBool@@ -148,14 +148,15 @@ -- *** Failed to prove existsConjunctionNot. -- Falsifiable. Counter-example: -- p :: Integer -> Bool--- p 1 = False+-- p 3 = False -- p _ = True -- <BLANKLINE> -- q :: Integer -> Bool--- q 1 = True+-- q 3 = True -- q _ = False ----- In this case, we again have a predicate That disagree at every point, providing a counter-example.+-- In this case, both @p@ and @q@ have a satisfying input (for @p@ everything but 3, for @q@, only 3), but+-- there is no single value that satisfies both, thus giving us our counter-example. existsConjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO () existsConjunctionNot p q = runTP $ do let qb = quantifiedBool
Documentation/SBV/Examples/TP/BinarySearch.hs view
@@ -263,3 +263,5 @@ =: sTrue =: qed ]++{- HLint ignore module "Reduce duplication" -}
Documentation/SBV/Examples/TP/GCD.hs view
@@ -31,6 +31,7 @@ #ifdef DOCTEST -- $setup+-- >>> import Data.SBV -- >>> import Data.SBV.TP #endif @@ -237,7 +238,9 @@ -- Lemma: dvdMul -- Step: 1 (2 way case split) -- Step: 1.1 Q.E.D.--- Step: 1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D. -- Step: 1.Completeness Q.E.D. -- Result: Q.E.D. -- [Proven] dvdMul :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐk ∷ Integer → Bool@@ -251,7 +254,9 @@ =: qed , d ./= 0 ==> d `dvd` (k*a) ?? a .== d * a `sEDiv` d- =: d `dvd` (k * d * a `sEDiv` d)+ =: d `dvd` ((d * a `sEDiv` d) * k)+ =: d `dvd` (d * ((a `sEDiv` d) * k))+ =: sTrue =: qed ] @@ -308,7 +313,7 @@ -- Arithmetic gives us =: 2*a .== 2*t*m + m .&& 2*(a-t*m) .== m - -- So, we now now m is even+ -- So, we now know m is even =: 2 `sDivides` m -- Give that divisor a name:@@ -676,8 +681,14 @@ -- | \(\gcd\, (2a)\, (2b) = 2 (\gcd\,a\, b)\) -- -- ==== __Proof__--- >>> runTP gcdEvenEven--- Lemma: modEE Q.E.D.+-- >>> runTPWith cvc5 gcdEvenEven+-- Lemma: red2 Q.E.D.+-- Lemma: modEE+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D. -- Inductive lemma (strong): nGCDEvenEven -- Step: Measure is non-negative Q.E.D. -- Step: 1 (2 way case split)@@ -698,10 +709,21 @@ gcdEvenEven :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) gcdEvenEven = do - modEE <- lemma "modEE"- (\(Forall @"a" a) (Forall @"b" b) -> b ./= 0 .=> (2 * a) `sEMod` (2 * b) .== 2 * (a `sEMod` b))+ red2 <- lemma "red2"+ (\(Forall @"a" a) (Forall @"b" b) -> b ./= 0 .=> (2*a) `sEDiv` (2*b) .== a `sEDiv` b) [] + modEE <- calc "modEE"+ (\(Forall @"a" a) (Forall @"b" b) -> b ./= 0 .=> (2*a) `sEMod` (2*b) .== 2 * (a `sEMod` b)) $+ \a b -> [b ./= 0]+ |- (2*a) `sEMod` (2*b)+ =: 2*a - 2*b * ((2*a) `sEDiv` (2*b))+ ?? red2 `at` (Inst @"a" a, Inst @"b" b)+ =: 2*a - 2*b * (a `sEDiv` b)+ =: 2 * (a - b * (a `sEDiv` b))+ =: 2 * (a `sEMod` b)+ =: qed+ nGCDEvenEven <- sInduct "nGCDEvenEven" (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCD (2*a) (2*b) .== 2 * nGCD a b) (\_a b -> b, []) $@@ -944,10 +966,10 @@ -- [Proven] gcdBinEquiv :: Ɐa ∷ Integer → Ɐb ∷ Integer → Bool gcdBinEquiv :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> SBool)) gcdBinEquiv = do- gEvenEven <- recall "gcdEvenEven" gcdEvenEven- gOddEven <- recall "gcdOddEven" gcdOddEven- gAdd <- recall "gcdAdd" gcdAdd- comm <- recall "commutative" commutative+ gEvenEven <- recallWith cvc5 "gcdEvenEven" gcdEvenEven+ gOddEven <- recall "gcdOddEven" gcdOddEven+ gAdd <- recall "gcdAdd" gcdAdd+ comm <- recall "commutative" commutative -- First prove over the non-negative numbers: nEq <- sInduct "nGCDBinEquiv"
+ Documentation/SBV/Examples/TP/Lists.hs view
@@ -0,0 +1,1948 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.TP.Lists+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- A variety of TP proofs on list processing functions. Note that+-- these proofs only hold for finite lists. SMT-solvers do not model infinite+-- lists, and hence all claims are for finite (but arbitrary-length) lists.+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE OverloadedLists #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.TP.Lists (+ -- * Append+ appendNull, consApp, appendAssoc, initsLength, tailsLength, tailsAppend++ -- * Reverse+ , revLen, revApp, revCons, revSnoc, revRev, enumLen, revNM++ -- * Length+ , lengthTail, lenAppend, lenAppend2++ -- * Replicate+ , replicateLength++ -- * All and any+ , allAny++ -- * Map+ , mapEquiv, mapAppend, mapReverse, mapCompose++ -- * Foldr and foldl+ , foldrMapFusion, foldrFusion, foldrOverAppend, foldlOverAppend, foldrFoldlDuality, foldrFoldlDualityGeneralized, foldrFoldl+ , bookKeeping++ -- * Filter+ , filterAppend, filterConcat, takeDropWhile++ -- * Stutter removal+ , destutter, destutterIdempotent++ -- * Difference+ , appendDiff, diffAppend, diffDiff++ -- * Partition+ , partition1, partition2++ -- * Take and drop+ , take_take, drop_drop, take_drop, take_cons, take_map, drop_cons, drop_map, length_take, length_drop, take_all, drop_all+ , take_append, drop_append++ -- * Zip+ , map_fst_zip+ , map_snd_zip+ , map_fst_zip_take+ , map_snd_zip_take++ -- * Counting elements+ , count, countAppend, takeDropCount, countNonNeg, countElem, elemCount++ -- * Disjointness+ , disjoint, disjointDiff++ -- * Interleaving+ , interleave, uninterleave, interleaveLen, interleaveRoundTrip+ ) where++import Prelude (Integer, Bool, Eq, ($), Num(..), id, (.), flip)++import Data.SBV+import Data.SBV.List+import Data.SBV.Tuple+import Data.SBV.TP++#ifdef DOCTEST+-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> :set -XTypeApplications+-- >>> import Data.SBV+-- >>> import Data.SBV.TP+-- >>> import Control.Exception+#endif++-- | @xs ++ [] == xs@+--+-- >>> runTP $ appendNull @Integer+-- Lemma: appendNull Q.E.D.+-- [Proven] appendNull :: Ɐxs ∷ [Integer] → Bool+appendNull :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+appendNull = lemma "appendNull"+ (\(Forall xs) -> xs ++ nil .== xs)+ []++-- | @(x : xs) ++ ys == x : (xs ++ ys)@+--+-- >>> runTP $ consApp @Integer+-- Lemma: consApp Q.E.D.+-- [Proven] consApp :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+consApp :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))+consApp = lemma "consApp"+ (\(Forall x) (Forall xs) (Forall ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))+ []++-- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@+--+-- >>> runTP $ appendAssoc @Integer+-- Lemma: appendAssoc Q.E.D.+-- [Proven] appendAssoc :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐzs ∷ [Integer] → Bool+--+-- Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to+-- the concatenation of sequences in SMTLib, it must trigger an internal heuristic in z3+-- that proves it right out-of-the-box!)+appendAssoc :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "zs" [a] -> SBool))+appendAssoc =+ lemma "appendAssoc"+ (\(Forall xs) (Forall ys) (Forall zs) -> xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs)+ []++-- | @length (inits xs) == 1 + length xs@+--+-- >>> runTP $ initsLength @Integer+-- Inductive lemma (strong): initsLength+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] initsLength :: Ɐxs ∷ [Integer] → Bool+initsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+initsLength =+ sInduct "initsLength"+ (\(Forall xs) -> length (inits xs) .== 1 + length xs)+ (length @a, []) $+ \ih xs -> [] |- length (inits xs)+ ?? ih+ =: 1 + length xs+ =: qed++-- | @length (tails xs) == 1 + length xs@+--+-- >>> runTP $ tailsLength @Integer+-- Inductive lemma: tailsLength+-- Step: Base Q.E.D.+-- 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] tailsLength :: Ɐxs ∷ [Integer] → Bool+tailsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+tailsLength =+ induct "tailsLength"+ (\(Forall xs) -> length (tails xs) .== 1 + length xs) $+ \ih (x, xs) -> [] |- length (tails (x .: xs))+ =: length (tails xs ++ [x .: xs])+ =: length (tails xs) + 1+ ?? ih+ =: 1 + length xs + 1+ =: 1 + length (x .: xs)+ =: qed++-- | @tails (xs ++ ys) == map (++ ys) (tails xs) ++ tail (tails ys)@+--+-- This property comes from Richard Bird's "Pearls of functional Algorithm Design" book, chapter 2.+-- Note that it is not exactly as stated there, as the definition of @tails@ Bird uses is different+-- than the standard Haskell function @tails@: Bird's version does not return the empty list as the+-- tail. So, we slightly modify it to fit the standard definition. (NB. z3 is finicky on this+-- problem, while cvc5 works much better.)+--+-- >>> runTPWith cvc5 $ tailsAppend @Integer+-- Inductive lemma: base case+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Lemma: helper+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: tailsAppend+-- Step: Base Q.E.D.+-- 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] tailsAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+tailsAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+tailsAppend = do++ let -- Ideally, we would like to define appendEach like this:+ --+ -- appendEach xs ys = map (++ ys) xs+ --+ -- But capture of ys is not allowed when we use the higher-order+ -- function map in SBV. So, we create a closure instead.+ appendEach :: SList a -> SList [a] -> SList [a]+ appendEach ys = map $ Closure { closureEnv = ys+ , closureFun = \env xs -> xs ++ env+ }++ -- Even proving the base case of induction is hard due to recursive definition. So we first prove the base case by induction.+ bc <- induct "base case"+ (\(Forall @"ys" (ys :: SList a)) -> tails ys .== [ys] ++ tail (tails ys)) $+ \ih (y, ys) -> [] |- tails (y .: ys)+ =: [y .: ys] ++ tails ys+ ?? ih+ =: [y .: ys] ++ [ys] ++ tail (tails ys)+ =: [y .: ys] ++ tail (tails (y .: ys))+ =: qed++ -- Also need a helper to relate how appendEach and tails work together+ helper <- calc "helper"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"x" x) ->+ appendEach ys (tails (x .: xs)) .== [(x .: xs) ++ ys] ++ appendEach ys (tails xs)) $+ \xs ys x -> [] |- appendEach ys (tails (x .: xs))+ =: appendEach ys ([x .: xs] ++ tails xs)+ =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs)+ =: qed++ induct "tailsAppend"+ (\(Forall xs) (Forall ys) -> tails (xs ++ ys) .== appendEach ys (tails xs) ++ tail (tails ys)) $+ \ih (x, xs) ys -> [assumptionFromProof bc]+ |- tails ((x .: xs) ++ ys)+ =: tails (x .: (xs ++ ys))+ =: [x .: (xs ++ ys)] ++ tails (xs ++ ys)+ ?? ih+ =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs) ++ tail (tails ys)+ ?? helper+ =: appendEach ys (tails (x .: xs)) ++ tail (tails ys)+ =: qed++-- | @length xs == length (reverse xs)@+--+-- >>> runTP $ revLen @Integer+-- Inductive lemma: revLen+-- Step: Base Q.E.D.+-- 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] revLen :: Ɐxs ∷ [Integer] → Bool+revLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+revLen = induct "revLen"+ (\(Forall xs) -> length (reverse xs) .== length xs) $+ \ih (x, xs) -> [] |- length (reverse (x .: xs))+ =: length (reverse xs ++ [x])+ =: length (reverse xs) + length [x]+ ?? ih+ =: length xs + 1+ =: length (x .: xs)+ =: qed++-- | @reverse (xs ++ ys) .== reverse ys ++ reverse xs@+--+-- >>> runTP $ revApp @Integer+-- Inductive lemma: revApp+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] revApp :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+revApp :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+revApp = induct "revApp"+ (\(Forall xs) (Forall ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) $+ \ih (x, xs) ys -> [] |- reverse ((x .: xs) ++ ys)+ =: reverse (x .: (xs ++ ys))+ =: reverse (xs ++ ys) ++ [x]+ ?? ih+ =: (reverse ys ++ reverse xs) ++ [x]+ =: reverse ys ++ (reverse xs ++ [x])+ =: reverse ys ++ reverse (x .: xs)+ =: qed++-- | @reverse (x:xs) == reverse xs ++ [x]@+--+-- >>> runTP $ revCons @Integer+-- Lemma: revCons Q.E.D.+-- [Proven] revCons :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool+revCons :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))+revCons = lemma "revCons"+ (\(Forall x) (Forall xs) -> reverse (x .: xs) .== reverse xs ++ [x])+ []++-- | @reverse (xs ++ [x]) == x : reverse xs@+--+-- >>> runTP $ revSnoc @Integer+-- Inductive lemma: revApp+-- Step: 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.+-- Result: Q.E.D.+-- Lemma: revSnoc Q.E.D.+-- [Proven] revSnoc :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool+revSnoc :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))+revSnoc = do+ ra <- revApp @a++ lemma "revSnoc"+ (\(Forall x) (Forall xs) -> reverse (xs ++ [x]) .== x .: reverse xs)+ [proofOf ra]++-- | @reverse (reverse xs) == xs@+--+-- >>> runTP $ revRev @Integer+-- Inductive lemma: revApp+-- Step: 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.+-- Result: Q.E.D.+-- Inductive lemma: revRev+-- Step: Base Q.E.D.+-- 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] revRev :: Ɐxs ∷ [Integer] → Bool+revRev :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+revRev = do++ ra <- revApp @a++ induct "revRev"+ (\(Forall xs) -> reverse (reverse xs) .== xs) $+ \ih (x, xs) -> [] |- reverse (reverse (x .: xs))+ =: reverse (reverse xs ++ [x])+ ?? ra+ =: reverse [x] ++ reverse (reverse xs)+ ?? ih+ =: [x] ++ xs+ =: x .: xs+ =: qed++-- | \(\text{length } [n \dots m] = \max(0,\; m - n + 1)\)+--+-- The proof uses the metric @|m-n|@.+--+-- >>> runTP enumLen+-- Inductive lemma (strong): enumLen+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool+enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))+enumLen =+ sInduct "enumLen"+ (\(Forall n) (Forall m) -> length [sEnum|n .. m|] .== 0 `smax` (m - n + 1))+ (\n m -> abs (m - n), []) $+ \ih n m -> [] |- length [sEnum|n+1 .. m|]+ =: cases [ n+1 .> m ==> trivial+ , n+1 .<= m ==> length (n+1 .: [sEnum|n+2 .. m|])+ =: 1 + length [sEnum|n+2 .. m|]+ ?? ih+ =: 1 + (0 `smax` (m - (n+2) + 1))+ =: 0 `smax` (m - (n+1) + 1)+ =: qed+ ]++-- | @reverse [n .. m] == [m, m-1 .. n]@+--+-- The proof uses the metric @|m-n|@.+--+-- >>> runTP $ revNM+-- Inductive lemma (strong): helper+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): revNM+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] revNM :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool+revNM :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))+revNM = do++ helper <- sInduct "helper"+ (\(Forall @"m" (m :: SInteger)) (Forall @"n" n) ->+ n .< m .=> [sEnum|m, m-1 .. n+1|] ++ [n] .== [sEnum|m, m-1 .. n|])+ (\m n -> abs (m - n), []) $+ \ih m n -> [n .< m] |- [sEnum|m, m-1 .. n+1|] ++ [n]+ =: m .: [sEnum|m-1, m-2 .. n+1|] ++ [n]+ ?? ih+ =: m .: [sEnum|m-1, m-2 .. n|]+ =: [sEnum|m, m-1 .. n|]+ =: qed++ sInduct "revNM"+ (\(Forall n) (Forall m) -> reverse [sEnum|n .. m|] .== [sEnum|m, m-1 .. n|])+ (\n m -> abs (m - n), []) $+ \ih n m -> [] |- reverse [sEnum|n .. m|]+ =: cases [ n .> m ==> trivial+ , n .<= m ==> reverse (n .: [sEnum|(n+1) .. m|])+ =: reverse [sEnum|(n+1) .. m|] ++ [n]+ ?? ih+ =: [sEnum|m, m-1 .. n+1|] ++ [n]+ ?? helper+ =: [sEnum|m, m-1 .. n|]+ =: qed+ ]++-- | @length (x : xs) == 1 + length xs@+--+-- >>> runTP $ lengthTail @Integer+-- Lemma: lengthTail Q.E.D.+-- [Proven] lengthTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool+lengthTail :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))+lengthTail = lemma "lengthTail"+ (\(Forall x) (Forall xs) -> length (x .: xs) .== 1 + length xs)+ []++-- | @length (xs ++ ys) == length xs + length ys@+--+-- >>> runTP $ lenAppend @Integer+-- Lemma: lenAppend Q.E.D.+-- [Proven] lenAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+lenAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+lenAppend = lemma "lenAppend"+ (\(Forall xs) (Forall ys) -> length (xs ++ ys) .== length xs + length ys)+ []++-- | @length xs == length ys -> length (xs ++ ys) == 2 * length xs@+--+-- >>> runTP $ lenAppend2 @Integer+-- Lemma: lenAppend2 Q.E.D.+-- [Proven] lenAppend2 :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+lenAppend2 :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+lenAppend2 = lemma "lenAppend2"+ (\(Forall xs) (Forall ys) -> length xs .== length ys .=> length (xs ++ ys) .== 2 * length xs)+ []++-- | @length (replicate k x) == max (0, k)@+--+-- >>> runTP $ replicateLength @Integer+-- Inductive lemma: replicateLength+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] replicateLength :: Ɐk ∷ Integer → Ɐx ∷ Integer → Bool+replicateLength :: forall a. SymVal a => TP (Proof (Forall "k" Integer -> Forall "x" a -> SBool))+replicateLength = induct "replicateLength"+ (\(Forall k) (Forall x) -> length (replicate k x) .== 0 `smax` k) $+ \ih k x -> [] |- length (replicate (k+1) x)+ =: cases [ k .< 0 ==> trivial+ , k .>= 0 ==> length (x .: replicate k x)+ =: 1 + length (replicate k x)+ ?? ih+ =: 1 + 0 `smax` k+ =: 0 `smax` (k+1)+ =: qed+ ]++-- | @not (all id xs) == any not xs@+--+-- A list of booleans is not all true, if any of them is false.+--+-- >>> runTP allAny+-- Inductive lemma: allAny+-- Step: Base Q.E.D.+-- 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] allAny :: Ɐxs ∷ [Bool] → Bool+allAny :: TP (Proof (Forall "xs" [Bool] -> SBool))+allAny = induct "allAny"+ (\(Forall 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 .|| any sNot xs+ =: any sNot (x .: xs)+ =: qed++-- | @f == g ==> map f xs == map g xs@+--+-- >>> runTP $ mapEquiv @Integer @Integer (uninterpret "f") (uninterpret "g")+-- Inductive lemma: mapEquiv+-- Step: Base Q.E.D.+-- 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] mapEquiv :: Ɐxs ∷ [Integer] → Bool+mapEquiv :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))+mapEquiv f g = do+ let f'eq'g :: SBool+ f'eq'g = quantifiedBool $ \(Forall x) -> f x .== g x++ induct "mapEquiv"+ (\(Forall 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 x .: map f xs .== f x .: map g xs+ ?? 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@+--+-- >>> runTP $ mapAppend @Integer @Integer (uninterpret "f")+-- Inductive lemma: mapAppend+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] mapAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+mapAppend :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+mapAppend f =+ induct "mapAppend"+ (\(Forall xs) (Forall 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 ++ map f ys)+ =: (f x .: map f xs) ++ map f ys+ =: map f (x .: xs) ++ map f ys+ =: qed++-- | @map f . reverse == reverse . map f@+--+-- >>> runTP $ mapReverse @Integer @String (uninterpret "f")+-- Inductive lemma: mapAppend+-- Step: 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.+-- Result: Q.E.D.+-- Inductive lemma: mapReverse+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] mapReverse :: Ɐxs ∷ [Integer] → Bool+mapReverse :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))+mapReverse f = do+ mApp <- mapAppend f++ induct "mapReverse"+ (\(Forall 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) ++ [f x]+ ?? ih+ =: map f (reverse xs) ++ [f x]+ =: map f (reverse xs) ++ map f [x]+ ?? mApp+ =: map f (reverse xs ++ [x])+ =: map f (reverse (x .: xs))+ =: qed++-- | @map f . map g == map (f . g)@+--+-- >>> runTP $ mapCompose @Integer @Bool @String (uninterpret "f") (uninterpret "g")+-- Inductive lemma: mapCompose+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool+mapCompose :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))+mapCompose f g =+ induct "mapCompose"+ (\(Forall xs) -> map g (map f xs) .== map (g . f) xs) $+ \ih (x, xs) -> [] |- map g (map f (x .: xs))+ =: map g (f x .: map f xs)+ =: g (f x) .: map g (map f xs)+ ?? ih+ =: g (f x) .: map (g . f) xs+ =: (g . f) x .: map (g . f) xs+ =: map (g . f) (x .: xs)+ =: qed++-- | @foldr f a . map g == foldr (f . g) a@+--+-- >>> runTP $ foldrMapFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "c")+-- Inductive lemma: foldrMapFusion+-- Step: Base Q.E.D.+-- 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] foldrMapFusion :: Ɐxs ∷ [[Char]] → Bool+foldrMapFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> (SBV a -> SBV b) -> (SBV b -> SBV c -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))+foldrMapFusion a g f =+ induct "foldrMapFusion"+ (\(Forall 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 . g) a xs+ =: foldr (f . g) a (x .: xs)+ =: qed++-- |+--+-- @+-- f . foldr g a == foldr h b+-- provided, f a = b and for all x and y, f (g x y) == h x (f y).+-- @+--+-- >>> runTP $ foldrFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "f") (uninterpret "g") (uninterpret "h")+-- Inductive lemma: foldrFusion+-- Step: Base Q.E.D.+-- 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] foldrFusion :: Ɐxs ∷ [[Char]] → Bool+foldrFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> SBV b -> (SBV c -> SBV b) -> (SBV a -> SBV c -> SBV c) -> (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))+foldrFusion a b f g h = do+ let -- Assumptions under which the equality holds+ h1 = f a .== b+ h2 = quantifiedBool $ \(Forall x) (Forall y) -> f (g x y) .== h x (f y)++ induct "foldrFusion"+ (\(Forall 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))+ =: h x (f (foldr g a xs))+ ?? ih+ =: h x (foldr h b xs)+ =: foldr h b (x .: xs)+ =: qed++-- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@+--+-- >>> runTP $ foldrOverAppend @Integer (uninterpret "a") (uninterpret "f")+-- Inductive lemma: foldrOverAppend+-- Step: Base Q.E.D.+-- 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] foldrOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+foldrOverAppend :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+foldrOverAppend a f =+ induct "foldrOverAppend"+ (\(Forall xs) (Forall 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 (foldr f a ys) xs+ =: foldr f (foldr f a ys) (x .: xs)+ =: qed++-- | @foldl f e (xs ++ ys) == foldl f (foldl f e xs) ys@+--+-- >>> runTP $ foldlOverAppend @Integer @Bool (uninterpret "f")+-- Inductive lemma: foldlOverAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] foldlOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Bool → Bool+foldlOverAppend :: forall a b. (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" b -> SBool))+foldlOverAppend f =+ induct "foldlOverAppend"+ (\(Forall xs) (Forall ys) (Forall 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)+ -- 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 @"e" (a `f` x))+ =: foldl f (foldl f (a `f` x) xs) ys+ =: qed++-- | @foldr f e xs == foldl (flip f) e (reverse xs)@+--+-- >>> runTP $ foldrFoldlDuality @Integer @String (uninterpret "f")+-- Inductive lemma: foldlOverAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: foldrFoldlDuality+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Ɐe ∷ [Char] → Bool+foldrFoldlDuality :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "e" b -> SBool))+foldrFoldlDuality f = do+ foa <- foldlOverAppend (flip f)++ induct "foldrFoldlDuality"+ (\(Forall xs) (Forall e) -> foldr f e xs .== foldl (flip f) e (reverse xs)) $+ \ih (x, xs) e -> [] |- let ff = flip f+ rxs = reverse xs+ 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) [x]+ ?? foa+ =: foldl ff e (rxs ++ [x])+ =: foldl ff e (reverse (x .: xs))+ =: qed++-- | Given:+--+-- @+-- x \@ (y \@ z) = (x \@ y) \@ z (associativity of @)+-- and e \@ x = x (left unit)+-- and x \@ e = x (right unit)+-- @+--+-- Proves:+--+-- @+-- foldr (\@) e xs == foldl (\@) e xs+-- @+--+-- >>> runTP $ foldrFoldlDualityGeneralized @Integer (uninterpret "e") (uninterpret "|@|")+-- Inductive lemma: helper+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: foldrFoldlDuality+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Bool+foldrFoldlDualityGeneralized :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> SBool))+foldrFoldlDualityGeneralized e (@) = do+ -- Assumptions under which the equality holds+ let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x @ (y @ z) .== (x @ y) @ z+ lunit = quantifiedBool $ \(Forall x) -> e @ x .== x+ runit = quantifiedBool $ \(Forall x) -> x @ e .== x++ -- Helper: foldl (@) (y @ z) xs = y @ foldl (@) z xs+ -- Note the instantiation of the IH at a different value for z. It turns out+ -- we don't have to actually specify this since z3 can figure it out by itself, but we're being explicit.+ 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+ ?? ih `at` (Inst @"y" y, Inst @"z" (z @ x))+ =: y @ foldl (@) (z @ x) xs+ =: y @ foldl (@) z (x .: xs)+ =: qed++ induct "foldrFoldlDuality"+ (\(Forall xs) -> assoc .&& lunit .&& runit .=> foldr (@) e xs .== foldl (@) e xs) $+ \ih (x, xs) -> [assoc, lunit, runit] |- foldr (@) e (x .: xs)+ =: x @ foldr (@) e xs+ ?? ih+ =: x @ foldl (@) e xs+ ?? helper+ =: foldl (@) (x @ e) xs+ ?? runit+ =: foldl (@) x xs+ ?? lunit+ =: foldl (@) (e @ x) xs+ =: foldl (@) e (x .: xs)+ =: qed++-- | Given:+--+-- @+-- (x \<+> y) \<*> z = x \<+> (y \<*> z)+-- and x \<+> e = e \<*> x+-- @+--+-- Proves:+--+-- @+-- foldr (\<+>) e xs = foldl (\<*>) e xs+-- @+--+-- In Bird's Introduction to Functional Programming book (2nd edition) this is called the second duality theorem:+--+-- >>> runTP $ foldrFoldl @Integer @String (uninterpret "<+>") (uninterpret "<*>") (uninterpret "e")+-- Inductive lemma: foldl over <*>/<+>+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: foldrFoldl+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] foldrFoldl :: Ɐxs ∷ [Integer] → Bool+foldrFoldl :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool))+foldrFoldl (<+>) (<*>) e = do+ -- Assumptions about the operators+ let -- (x <+> y) <*> z == x <+> (y <*> z)+ assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> (x <+> y) <*> z .== x <+> (y <*> z)++ -- x <+> e == e <*> x+ unit = quantifiedBool $ \(Forall x) -> x <+> e .== e <*> x++ -- Helper: x <+> foldl (<*>) y xs == foldl (<*>) (x <+> y) xs+ helper <-+ induct "foldl over <*>/<+>"+ (\(Forall @"xs" xs) (Forall @"x" x) (Forall @"y" y) -> assoc .=> x <+> foldl (<*>) y xs .== foldl (<*>) (x <+> y) xs) $++ -- 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+ ?? 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++ -- Final proof:+ induct "foldrFoldl"+ (\(Forall xs) -> assoc .&& unit .=> foldr (<+>) e xs .== foldl (<*>) e xs) $+ \ih (x, xs) -> [assoc, unit] |- foldr (<+>) e (x .: xs)+ =: x <+> foldr (<+>) e xs+ ?? ih+ =: x <+> foldl (<*>) e xs+ ?? helper+ =: foldl (<*>) (x <+> e) xs+ =: foldl (<*>) (e <*> x) xs+ =: foldl (<*>) e (x .: xs)+ =: qed++-- | Provided @f@ is associative and @a@ is its both left and right-unit:+--+-- @foldr f a . concat == foldr f a . map (foldr f a)@+--+-- >>> runTP $ bookKeeping @Integer (uninterpret "a") (uninterpret "f")+-- Inductive lemma: foldBase+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: foldrOverAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: bookKeeping+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] bookKeeping :: Ɐxss ∷ [[Integer]] → Bool+--+-- NB. This theorem does not hold if @f@ does not have a left-unit! Consider the input @[[], [x]]@. Left hand side reduces to+-- @x@, while the right hand side reduces to: @f a x@. And unless @f@ is commutative or @a@ is not also a left-unit,+-- then one can find a counter-example. (Aside: if both left and right units exist for a binary operator, then they+-- are necessarily the same element, since @l = f l r = r@. So, an equivalent statement could simply say @f@ has+-- both left and right units.) A concrete counter-example is:+--+-- @+-- data T = A | B | C+--+-- f :: T -> T -> T+-- f C A = A+-- f C B = A+-- f x _ = x+-- @+--+-- You can verify @f@ is associative. Also note that @C@ is the right-unit for @f@, but it isn't the left-unit.+-- In fact, @f@ has no-left unit by the above argument. In this case, the bookkeeping law produces @B@ for+-- the left-hand-side, and @A@ for the right-hand-side for the input @[[], [B]]@.+bookKeeping :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xss" [[a]] -> SBool))+bookKeeping a f = do++ -- Assumptions about f+ let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x `f` (y `f` z) .== (x `f` y) `f` z+ rUnit = quantifiedBool $ \(Forall x) -> x `f` a .== x+ lUnit = quantifiedBool $ \(Forall x) -> a `f` x .== x++ -- Helper: @foldr f y xs = foldr f a xs `f` y@+ helper <- induct "foldBase"+ (\(Forall xs) (Forall 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+ ?? ih+ =: x `f` (foldr f a xs `f` y)+ =: (x `f` foldr f a xs) `f` y+ =: foldr f a (x .: xs) `f` y+ =: qed++ foa <- foldrOverAppend a f++ induct "bookKeeping"+ (\(Forall xss) -> assoc .&& rUnit .&& lUnit .=> foldr f a (concat xss) .== foldr f a (map (foldr f 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+ ?? ih+ =: foldr f (foldr f a (map (foldr f a) xss)) xs+ ?? helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (map (foldr f a) xss)))+ =: foldr f a xs `f` foldr f a (map (foldr f a) xss)+ =: foldr f a (foldr f a xs .: map (foldr f a) xss)+ =: foldr f a (map (foldr f a) (xs .: xss))+ =: qed++-- | @filter p (xs ++ ys) == filter p xs ++ filter p ys@+--+-- >>> runTP $ filterAppend @Integer (uninterpret "p")+-- Inductive lemma: filterAppend+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] filterAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+filterAppend :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+filterAppend p =+ induct "filterAppend"+ (\(Forall xs) (Forall 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 ++ ys)) (filter p (xs ++ ys))+ =: filter p (x .: (xs ++ ys))+ =: filter p ((x .: xs) ++ ys)+ =: qed++-- | @filter p (concat xss) == concatMap (filter p xss)@+--+-- >>> runTP $ filterConcat @Integer (uninterpret "f")+-- Inductive lemma: filterAppend+-- Step: 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.+-- Result: Q.E.D.+-- Inductive lemma: filterConcat+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] filterConcat :: Ɐxss ∷ [[Integer]] → Bool+filterConcat :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xss" [[a]] -> SBool))+filterConcat p = do+ fa <- filterAppend p++ inductWith cvc5 "filterConcat"+ (\(Forall xss) -> filter p (concat xss) .== concatMap (filter p) xss) $+ \ih (xs, xss) -> [] |- filter p (concat (xs .: xss))+ =: filter p (xs ++ concat xss)+ ?? fa+ =: filter p xs ++ filter p (concat xss)+ ?? ih+ =: concatMap (filter p) (xs .: xss)+ =: qed++-- | @takeWhile f xs ++ dropWhile f xs == xs@+--+-- >>> runTP $ takeDropWhile @Integer (uninterpret "f")+-- Inductive lemma: takeDropWhile+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] takeDropWhile :: Ɐxs ∷ [Integer] → Bool+takeDropWhile :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))+takeDropWhile f =+ induct "takeDropWhile"+ (\(Forall xs) -> takeWhile f xs ++ dropWhile f xs .== xs) $+ \ih (x, xs) -> [] |- takeWhile f (x .: xs) ++ dropWhile f (x .: xs)+ =: cases [ f x ==> x .: takeWhile f xs ++ dropWhile f xs+ ?? ih+ =: x .: xs+ =: qed+ , sNot (f x) ==> [] ++ x .: xs+ =: x .: xs+ =: qed+ ]+-- | Remove adjacent duplicates.+destutter :: SymVal a => SList a -> SList a+destutter = smtFunction "destutter" $ \xs -> ite (null xs .|| null (tail xs))+ xs+ (let (a, as) = uncons xs+ r = destutter as+ in ite (a .== head as) r (a .: r))++-- | @destutter (destutter xs) == destutter xs@+--+-- >>> runTP $ destutterIdempotent @Integer+-- Inductive lemma: helper1+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: helper2+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): helper3+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 (2 way full case split)+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2.1 Q.E.D.+-- Step: 1.2.2.2 (2 way case split)+-- Step: 1.2.2.2.1.1 Q.E.D.+-- Step: 1.2.2.2.1.2 Q.E.D.+-- Step: 1.2.2.2.2.1 Q.E.D.+-- Step: 1.2.2.2.2.2 Q.E.D.+-- Step: 1.2.2.2.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: destutterIdempotent Q.E.D.+-- [Proven] destutterIdempotent :: Ɐxs ∷ [Integer] → Bool+destutterIdempotent :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))+destutterIdempotent = do++ -- No adjacent duplicates+ let noAdd = smtFunction "noAdd" $ \xs -> null xs .|| null (tail xs) .|| (head xs ./= head (tail xs) .&& noAdd (tail xs))++ -- Helper: The head of a destuttered non-empty list does not change+ helper1 <- induct "helper1"+ (\(Forall @"xs" (xs :: SList a)) (Forall @"h" h) -> head (destutter (h .: xs)) .== h) $+ \ih (x, xs) h -> []+ |- head (destutter (h .: x .: xs))+ =: cases [ h ./= x ==> trivial+ , h .== x ==> head (destutter (x .: xs))+ ?? ih+ =: x+ =: qed+ ]++ -- Helper: show that if a list has no adjacent duplicates, then destutter leaves it unchanged:+ helper2 <- induct "helper2"+ (\(Forall @"xs" (xs :: SList a)) -> noAdd xs .=> destutter xs .== xs) $+ \ih (x, xs) -> [noAdd (x .: xs)]+ |- destutter (x .: xs)+ ?? ih+ =: x .: xs+ =: qed++ -- Helper: prove that noAdd is true for the result of destutter+ helper3 <- sInductWith cvc5 "helper3"+ (\(Forall @"xs" (xs :: SList a)) -> noAdd (destutter xs))+ (length, []) $+ \ih xs -> []+ |- noAdd (destutter xs)+ =: split xs+ trivial+ (\a as -> split as+ trivial+ (\b bs -> noAdd (destutter (a .: b .: bs))+ =: cases [a .== b ==> noAdd (destutter (b .: bs))+ ?? ih+ =: sTrue+ =: qed+ , a ./= b ==> noAdd (a .: destutter (b .: bs))+ ?? helper1 `at` (Inst @"xs" bs, Inst @"h" b)+ ?? ih+ =: sTrue+ =: qed+ ]))++ -- Now we can prove idempotency easily:+ lemma "destutterIdempotent"+ (\(Forall xs) -> destutter (destutter xs) .== destutter xs)+ [proofOf helper2, proofOf helper3]++-- | @(as ++ bs) \\ cs == (as \\ cs) ++ (bs \\ cs)@+--+-- >>> runTP $ appendDiff @Integer+-- Inductive lemma: appendDiff+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] appendDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool+appendDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))+appendDiff = induct "appendDiff"+ (\(Forall as) (Forall bs) (Forall cs) -> (as ++ bs) \\ cs .== (as \\ cs) ++ (bs \\ cs)) $+ \ih (a, as) bs cs -> [] |- (a .: as ++ bs) \\ cs+ =: (a .: (as ++ bs)) \\ cs+ =: ite (a `elem` cs) ((as ++ bs) \\ cs) (a .: ((as ++ bs) \\ cs))+ ?? ih+ =: ((a .: as) \\ cs) ++ (bs \\ cs)+ =: qed++-- | @as \\ (bs ++ cs) == (as \\ bs) \\ cs@+--+-- >>> runTP $ diffAppend @Integer+-- Inductive lemma: diffAppend+-- Step: Base Q.E.D.+-- 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] diffAppend :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool+diffAppend :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))+diffAppend = induct "diffAppend"+ (\(Forall as) (Forall bs) (Forall cs) -> as \\ (bs ++ cs) .== (as \\ bs) \\ cs) $+ \ih (a, as) bs cs -> [] |- (a .: as) \\ (bs ++ cs)+ =: ite (a `elem` (bs ++ cs)) (as \\ (bs ++ cs)) (a .: (as \\ (bs ++ cs)))+ ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)+ =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: (as \\ (bs ++ cs)))+ ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)+ =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: ((as \\ bs) \\ cs))+ =: ((a .: as) \\ bs) \\ cs+ =: qed++-- | @(as \\ bs) \\ cs == (as \\ cs) \\ bs@+--+-- >>> runTP $ diffDiff @Integer+-- Inductive lemma: diffDiff+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.1.3 (2 way case split)+-- Step: 1.1.3.1 Q.E.D.+-- Step: 1.1.3.2.1 Q.E.D.+-- Step: 1.1.3.2.2 (a ∉ cs) Q.E.D.+-- Step: 1.1.3.Completeness Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 (2 way case split)+-- Step: 1.2.2.1.1 Q.E.D.+-- Step: 1.2.2.1.2 Q.E.D.+-- Step: 1.2.2.1.3 (a ∈ cs) Q.E.D.+-- Step: 1.2.2.2.1 Q.E.D.+-- Step: 1.2.2.2.2 Q.E.D.+-- Step: 1.2.2.2.3 (a ∉ bs) Q.E.D.+-- Step: 1.2.2.2.4 (a ∉ cs) Q.E.D.+-- Step: 1.2.2.Completeness Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] diffDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool+diffDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))+diffDiff = induct "diffDiff"+ (\(Forall as) (Forall bs) (Forall cs) -> (as \\ bs) \\ cs .== (as \\ cs) \\ bs) $+ \ih (a, as) bs cs ->+ [] |- ((a .: as) \\ bs) \\ cs+ =: cases [ a `elem` bs ==> (as \\ bs) \\ cs+ ?? ih+ =: (as \\ cs) \\ bs+ =: cases [ a `elem` cs ==> ((a .: as) \\ cs) \\ bs+ =: qed+ , a `notElem` cs ==> (a .: (as \\ cs)) \\ bs+ ?? "a ∉ cs"+ =: ((a .: as) \\ cs) \\ bs+ =: qed+ ]+ , a `notElem` bs ==> (a .: (as \\ bs)) \\ cs+ =: cases [ a `elem` cs ==> (as \\ bs) \\ cs+ ?? ih+ =: (as \\ cs) \\ bs+ ?? "a ∈ cs"+ =: ((a .: as) \\ cs) \\ bs+ =: qed+ , a `notElem` cs ==> a .: ((as \\ bs) \\ cs)+ ?? ih+ =: a .: ((as \\ cs) \\ bs)+ ?? "a ∉ bs"+ =: (a .: (as \\ cs)) \\ bs+ ?? "a ∉ cs"+ =: ((a .: as) \\ cs) \\ bs+ =: qed+ ]+ ]++-- | Are the two lists disjoint?+disjoint :: (Eq a, SymVal a) => SList a -> SList a -> SBool+disjoint = smtFunction "disjoint" $ \xs ys -> null xs .|| head xs `notElem` ys .&& disjoint (tail xs) ys++-- | @disjoint as bs .=> as \\ bs == as@+--+-- >>> runTP $ disjointDiff @Integer+-- Inductive lemma: disjointDiff+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- [Proven] disjointDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Bool+disjointDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> SBool))+disjointDiff = induct "disjointDiff"+ (\(Forall as) (Forall bs) -> disjoint as bs .=> as \\ bs .== as) $+ \ih (a, as) bs -> [disjoint (a .: as) bs]+ |- (a .: as) \\ bs+ =: a .: (as \\ bs)+ ?? ih+ =: a .: as+ =: qed++-- | @fst (partition f xs) == filter f xs@+--+-- >>> runTP $ partition1 @Integer (uninterpret "f")+-- Inductive lemma: partition1+-- Step: Base Q.E.D.+-- 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] partition1 :: Ɐxs ∷ [Integer] → Bool+partition1 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))+partition1 f =+ induct "partition1"+ (\(Forall 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@+--+-- >>> runTP $ partition2 @Integer (uninterpret "f")+-- Inductive lemma: partition2+-- Step: Base Q.E.D.+-- 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] partition2 :: Ɐxs ∷ [Integer] → Bool+partition2 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))+partition2 f =+ induct "partition2"+ (\(Forall 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 n (take m xs) == take (n `smin` m) xs@+--+-- >>> runTP $ take_take @Integer+-- Lemma: take_take Q.E.D.+-- [Proven] take_take :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+take_take :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))+take_take = lemma "take_take"+ (\(Forall m) (Forall n) (Forall xs) -> take n (take m xs) .== take (n `smin` m) xs)+ []++-- | @n >= 0 && m >= 0 ==> drop n (drop m xs) == drop (n + m) xs@+--+-- >>> runTP $ drop_drop @Integer+-- Lemma: drop_drop Q.E.D.+-- [Proven] drop_drop :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+drop_drop :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))+drop_drop = lemma "drop_drop"+ (\(Forall m) (Forall n) (Forall xs) -> n .>= 0 .&& m .>= 0 .=> drop n (drop m xs) .== drop (n + m) xs)+ []++-- | @take n xs ++ drop n xs == xs@+--+-- >>> runTP $ take_drop @Integer+-- Lemma: take_drop Q.E.D.+-- [Proven] take_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+take_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+take_drop = lemma "take_drop"+ (\(Forall n) (Forall xs) -> take n xs ++ drop n xs .== xs)+ []++-- | @n .> 0 ==> take n (x .: xs) == x .: take (n - 1) xs@+--+-- >>> runTP $ take_cons @Integer+-- Lemma: take_cons Q.E.D.+-- [Proven] take_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool+take_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))+take_cons = lemma "take_cons"+ (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> take n (x .: xs) .== x .: take (n - 1) xs)+ []++-- | @take n (map f xs) == map f (take n xs)@+--+-- >>> runTP $ take_map @Integer @Integer (uninterpret "f")+-- 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+-- Step: 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.+-- Result: Q.E.D.+-- Lemma: take_map+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] take_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+take_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+take_map f = do+ tc <- take_cons @a++ map1 <- lemma "map1"+ (\(Forall x) (Forall 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)+ =: 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)+ ?? tc+ =: map f (take n (x .: xs))+ =: qed++ calc "take_map"+ (\(Forall n) (Forall xs) -> take n (map f xs) .== map f (take n xs)) $+ \n xs -> [] |- take n (map f xs)+ ?? h1+ ?? h2+ =: map f (take n xs)+ =: qed++-- | @n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs@+--+-- >>> runTP $ drop_cons @Integer+-- Lemma: drop_cons Q.E.D.+-- [Proven] drop_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool+drop_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))+drop_cons = lemma "drop_cons"+ (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs)+ []++-- | @drop n (map f xs) == map f (drop n xs)@+--+-- >>> runTP $ drop_map @Integer @String (uninterpret "f")+-- 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+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Result: 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 :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+drop_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+drop_map f = do+ dcA <- drop_cons @a+ dcB <- drop_cons @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)+ ?? dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs))+ =: drop (n - 1) (map f xs)+ ?? ih `at` Inst @"n" (n-1)+ =: map f (drop (n - 1) xs)+ ?? 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 n) (Forall xs) -> drop n (map f xs) .== map f (drop n xs)) $+ \n xs -> [] |- 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@+--+-- >>> runTP $ length_take @Integer+-- Lemma: length_take Q.E.D.+-- [Proven] length_take :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+length_take :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+length_take = lemma "length_take"+ (\(Forall n) (Forall xs) -> n .>= 0 .=> length (take n xs) .== length xs `smin` n)+ []++-- | @n >= 0 ==> length (drop n xs) == (length xs - n) \`max\` 0@+--+-- >>> runTP $ length_drop @Integer+-- Lemma: length_drop Q.E.D.+-- [Proven] length_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+length_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+length_drop = lemma "length_drop"+ (\(Forall n) (Forall xs) -> n .>= 0 .=> length (drop n xs) .== (length xs - n) `smax` 0)+ []++-- | @length xs \<= n ==\> take n xs == xs@+--+-- >>> runTP $ take_all @Integer+-- Lemma: take_all Q.E.D.+-- [Proven] take_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+take_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+take_all = lemma "take_all"+ (\(Forall n) (Forall xs) -> length xs .<= n .=> take n xs .== xs)+ []++-- | @length xs \<= n ==\> drop n xs == nil@+--+-- >>> runTP $ drop_all @Integer+-- Lemma: drop_all Q.E.D.+-- [Proven] drop_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool+drop_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))+drop_all = lemma "drop_all"+ (\(Forall n) (Forall xs) -> length xs .<= n .=> drop n xs .== nil)+ []++-- | @take n (xs ++ ys) == (take n xs ++ take (n - length xs) ys)@+--+-- >>> runTP $ take_append @Integer+-- Lemma: take_append Q.E.D.+-- [Proven] take_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+take_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))+take_append = lemmaWith cvc5 "take_append"+ (\(Forall n) (Forall xs) (Forall ys) -> take n (xs ++ ys) .== take n xs ++ take (n - length xs) ys)+ []++-- | @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.+--+-- >>> runTP $ drop_append @Integer+-- Lemma: drop_append Q.E.D.+-- [Proven] drop_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+drop_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))+drop_append = lemmaWith cvc5 "drop_append"+ (\(Forall n) (Forall xs) (Forall ys) -> drop n (xs ++ ys) .== drop n xs ++ drop (n - length xs) ys)+ []++-- | @length xs == length ys ==> map fst (zip xs ys) = xs@+--+-- >>> runTP $ map_fst_zip @Integer @Integer+-- Inductive lemma: map_fst_zip+-- Step: Base Q.E.D.+-- 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] map_fst_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool+map_fst_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))+map_fst_zip = induct "map_fst_zip"+ (\(Forall xs, Forall ys) -> length xs .== length ys .=> map fst (zip xs ys) .== xs) $+ \ih (x, xs, y, 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)+ ?? ih+ =: x .: xs+ =: qed++-- | @length xs == length ys ==> map snd (zip xs ys) = xs@+--+-- >>> runTP $ map_snd_zip @Integer @Integer+-- Inductive lemma: map_snd_zip+-- Step: Base Q.E.D.+-- 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] map_snd_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool+map_snd_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))+map_snd_zip = induct "map_snd_zip"+ (\(Forall xs, Forall ys) -> length xs .== length ys .=> map snd (zip xs ys) .== ys) $+ \ih (x, xs, y, 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)+ ?? ih+ =: y .: ys+ =: qed++-- | @map fst (zip xs ys) == take (min (length xs) (length ys)) xs@+--+-- >>> runTP $ map_fst_zip_take @Integer @Integer+-- Lemma: take_cons Q.E.D.+-- Inductive lemma: map_fst_zip_take+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] map_fst_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool+map_fst_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))+map_fst_zip_take = do+ tc <- take_cons @a++ induct "map_fst_zip_take"+ (\(Forall xs, Forall ys) -> map fst (zip xs ys) .== take (length xs `smin` length ys) xs) $+ \ih (x, xs, y, 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@+--+-- >>> runTP $ map_snd_zip_take @Integer @Integer+-- Lemma: take_cons Q.E.D.+-- Inductive lemma: map_snd_zip_take+-- Step: 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.+-- Result: Q.E.D.+-- [Proven] map_snd_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool+map_snd_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))+map_snd_zip_take = do+ tc <- take_cons @a++ induct "map_snd_zip_take"+ (\(Forall xs, Forall ys) -> map snd (zip xs ys) .== take (length xs `smin` length ys) ys) $+ \ih (x, xs, y, 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++-- | Count the number of occurrences of an element in a list+count :: SymVal a => SBV a -> SList a -> SInteger+count = smtFunction "count" $ \e l -> ite (null l)+ 0+ (let (x, xs) = uncons l+ cxs = count e xs+ in ite (e .== x) (1 + cxs) cxs)++-- | Interleave the elements of two lists. If one ends, we take the rest from the other.+interleave :: SymVal a => SList a -> SList a -> SList a+interleave = smtFunction "interleave" (\xs ys -> ite (null xs) ys (head xs .: interleave ys (tail xs)))++-- | Prove that interleave preserves total length.+--+-- The induction here is on the total length of the lists, and hence+-- we use the generalized induction principle. We have:+--+-- >>> runTP $ interleaveLen @Integer+-- Inductive lemma (strong): interleaveLen+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] interleaveLen :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+interleaveLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+interleaveLen = sInduct "interleaveLen"+ (\(Forall xs) (Forall ys) -> length xs + length ys .== length (interleave xs ys))+ (\xs ys -> length xs + length ys, []) $+ \ih xs ys -> [] |- length xs + length ys .== length (interleave xs ys)+ =: split xs+ trivial+ (\a as -> length (a .: as) + length ys .== length (interleave (a .: as) ys)+ =: 1 + length as + length ys .== 1 + length (interleave ys as)+ ?? ih `at` (Inst @"xs" ys, Inst @"ys" as)+ =: sTrue+ =: qed)++-- | Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.+uninterleave :: SymVal a => SList a -> STuple [a] [a]+uninterleave lst = uninterleaveGen lst (tuple (nil, nil))++-- | Generalized form of uninterleave with the auxilary lists made explicit.+uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]+uninterleaveGen = smtFunction "uninterleave" (\xs alts -> let (es, os) = untuple alts+ in ite (null xs)+ (tuple (reverse es, reverse os))+ (uninterleaveGen (tail xs) (tuple (os, head xs .: es))))++-- | The functions 'uninterleave' and 'interleave' are inverses so long as the inputs are of the same length. (The equality+-- would even hold if the first argument has one extra element, but we keep things simple here.)+--+-- We have:+--+-- >>> runTP $ interleaveRoundTrip @Integer+-- Lemma: revCons Q.E.D.+-- Inductive lemma (strong): roundTripGen+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (4 way full case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3 Q.E.D.+-- Step: 1.4.1 Q.E.D.+-- Step: 1.4.2 Q.E.D.+-- Step: 1.4.3 Q.E.D.+-- Step: 1.4.4 Q.E.D.+-- Step: 1.4.5 Q.E.D.+-- Step: 1.4.6 Q.E.D.+-- Step: 1.4.7 Q.E.D.+-- Step: 1.4.8 Q.E.D.+-- Result: Q.E.D.+-- Lemma: interleaveRoundTrip+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- [Proven] interleaveRoundTrip :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool+interleaveRoundTrip :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))+interleaveRoundTrip = do++ revHelper <- lemma "revCons" (\(Forall a) (Forall as) (Forall bs) -> reverse @a (a .: as) ++ bs .== reverse as ++ (a .: bs)) []++ -- Generalize the theorem first to take the helper lists explicitly+ roundTripGen <- sInductWith cvc5+ "roundTripGen"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"alts" alts) ->+ length xs .== length ys .=> let (es, os) = untuple alts+ in uninterleaveGen (interleave xs ys) alts .== tuple (reverse es ++ xs, reverse os ++ ys))+ (\xs ys _alts -> length xs + length ys, []) $+ \ih xs ys alts -> [length xs .== length ys]+ |- let (es, os) = untuple alts+ in uninterleaveGen (interleave xs ys) alts+ =: split2 (xs, ys)+ trivial+ trivial+ trivial+ (\(a, as) (b, bs) -> uninterleaveGen (interleave (a .: as) (b .: bs)) alts+ =: uninterleaveGen (a .: interleave (b .: bs) as) alts+ =: uninterleaveGen (a .: b .: interleave as bs) alts+ =: uninterleaveGen (interleave as bs) (tuple (a .: es, b .: os))+ ?? ih `at` (Inst @"xs" as, Inst @"ys" bs, Inst @"alts" (tuple (a .: es, b .: os)))+ =: tuple (reverse (a .: es) ++ as, reverse (b .: os) ++ bs)+ ?? revHelper `at` (Inst @"a" a, Inst @"as" es, Inst @"bs" as)+ =: tuple (reverse es ++ (a .: as), reverse (b .: os) ++ bs)+ ?? revHelper `at` (Inst @"a" b, Inst @"as" os, Inst @"bs" bs)+ =: tuple (reverse es ++ (a .: as), reverse os ++ (b .: bs))+ =: tuple (reverse es ++ xs, reverse os ++ ys)+ =: qed)++ -- Round-trip theorem:+ calc "interleaveRoundTrip"+ (\(Forall xs) (Forall ys) -> length xs .== length ys .=> uninterleave (interleave xs ys) .== tuple (xs, ys)) $+ \xs ys -> [length xs .== length ys]+ |- uninterleave (interleave xs ys)+ =: uninterleaveGen (interleave xs ys) (tuple (nil, nil))+ ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple (nil, nil)))+ =: tuple (reverse nil ++ xs, reverse nil ++ ys)+ =: qed++-- | @count e (xs ++ ys) == count e xs + count e ys@+--+-- >>> runTP $ countAppend @Integer+-- Inductive lemma: countAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (unfold count) Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 (simplify) Q.E.D.+-- Result: Q.E.D.+-- [Proven] countAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Integer → Bool+countAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))+countAppend =+ induct "countAppend"+ (\(Forall xs) (Forall ys) (Forall e) -> count e (xs ++ ys) .== count e xs + count e ys) $+ \ih (x, xs) ys e -> [] |- count e ((x .: xs) ++ ys)+ =: count e (x .: (xs ++ ys))+ ?? "unfold count"+ =: (let r = count e (xs ++ ys) in ite (e .== x) (1+r) r)+ ?? ih `at` (Inst @"ys" ys, Inst @"e" e)+ =: (let r = count e xs + count e ys in ite (e .== x) (1+r) r)+ ?? "simplify"+ =: count e (x .: xs) + count e ys+ =: qed++-- | @count e (take n xs) + count e (drop n xs) == count e xs@+--+-- >>> runTP $ takeDropCount @Integer+-- Inductive lemma: countAppend+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (unfold count) Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 (simplify) Q.E.D.+-- Result: Q.E.D.+-- Lemma: take_drop Q.E.D.+-- Lemma: takeDropCount+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- [Proven] takeDropCount :: Ɐxs ∷ [Integer] → Ɐn ∷ Integer → Ɐe ∷ Integer → Bool+takeDropCount :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool))+takeDropCount = do+ capp <- countAppend @a+ takeDrop <- take_drop @a++ calc "takeDropCount"+ (\(Forall xs) (Forall n) (Forall e) -> count e (take n xs) + count e (drop n xs) .== count e xs) $+ \xs n e -> [] |- count e (take n xs) + count e (drop n xs)+ ?? capp `at` (Inst @"xs" (take n xs), Inst @"ys" (drop n xs), Inst @"e" e)+ =: count e (take n xs ++ drop n xs)+ ?? takeDrop+ =: count e xs+ =: qed++-- | @count e xs >= 0@+--+-- >>> runTP $ countNonNeg @Integer+-- Inductive lemma: countNonNeg+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] countNonNeg :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool+countNonNeg :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))+countNonNeg =+ induct "countNonNeg"+ (\(Forall xs) (Forall e) -> count e xs .>= 0) $+ \ih (x, xs) e -> [] |- count e (x .: xs) .>= 0+ =: cases [ e .== x ==> 1 + count e xs .>= 0+ ?? ih+ =: sTrue+ =: qed+ , e ./= x ==> count e xs .>= 0+ ?? ih+ =: sTrue+ =: qed+ ]++-- | @e \`elem\` xs ==> count e xs .> 0@+--+-- >>> runTP $ countElem @Integer+-- Inductive lemma: countNonNeg+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma: countElem+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1.1 Q.E.D.+-- Step: 1.1.2 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] countElem :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool+countElem :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))+countElem = do++ cnn <- countNonNeg @a++ induct "countElem"+ (\(Forall xs) (Forall e) -> e `elem` xs .=> count e xs .> 0) $+ \ih (x, xs) e -> [e `elem` (x .: xs)]+ |- count e (x .: xs) .> 0+ =: cases [ e .== x ==> 1 + count e xs .> 0+ ?? cnn+ =: sTrue+ =: qed+ , e ./= x ==> count e xs .> 0+ ?? ih+ =: sTrue+ =: qed+ ]++-- | @count e xs .> 0 .=> e \`elem\` xs@+--+-- >>> runTP $ elemCount @Integer+-- Inductive lemma: elemCount+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] elemCount :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool+elemCount :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))+elemCount =+ induct "elemCount"+ (\(Forall xs) (Forall e) -> count e xs .> 0 .=> e `elem` xs) $+ \ih (x, xs) e -> [count e xs .> 0]+ |- e `elem` (x .: xs)+ =: cases [ e .== x ==> trivial+ , e ./= x ==> e `elem` xs+ ?? ih+ =: sTrue+ =: qed+ ]++{- HLint ignore revRev "Redundant reverse" -}+{- HLint ignore allAny "Use and" -}+{- HLint ignore bookKeeping "Fuse foldr/map" -}+{- 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" -}+{- HLint ignore mapCompose "Use map once" -}+{- HLint ignore tailsAppend "Avoid lambda" -}+{- HLint ignore tailsAppend "Use :" -}+{- HLint ignore mapReverse "Evaluate" -}+{- HLint ignore takeDropWhile "Evaluate" -}
Documentation/SBV/Examples/TP/Majority.hs view
@@ -25,7 +25,7 @@ import Data.SBV.List import Data.SBV.TP-import qualified Data.SBV.TP.List as TP+import qualified Documentation.SBV.Examples.TP.Lists as TP -- * Calculating majority
Documentation/SBV/Examples/TP/MergeSort.hs view
@@ -26,8 +26,8 @@ import Data.SBV.List import Data.SBV.Tuple import Data.SBV.TP-import qualified Data.SBV.TP.List as TP +import qualified Documentation.SBV.Examples.TP.Lists as TP import qualified Documentation.SBV.Examples.TP.SortHelpers as SH #ifdef DOCTEST
Documentation/SBV/Examples/TP/Primes.hs view
@@ -72,7 +72,7 @@ -- Step: 1.1 Q.E.D. -- Step: 1.2.1 Q.E.D. -- Step: 1.2.2 Q.E.D.--- Step: 1.2.3 (hard) Q.E.D.+-- Step: 1.2.3 Q.E.D. -- Step: 1.2.4 Q.E.D. -- Step: 1.Completeness Q.E.D. -- Result: Q.E.D.@@ -90,8 +90,8 @@ ?? z .== z `sEDiv` y * y =: x `dvd` (z `sEDiv` y * y) ?? y .== y `sEDiv` x * x+ ?? x `dvd` y =: x `dvd` ((z `sEDiv` y) * (y `sEDiv` x * x))- ?? "hard" =: x `dvd` (x * ((z `sEDiv` y) * (y `sEDiv` x))) ?? dp `at` (Inst @"x" x, Inst @"y" x, Inst @"z" ((z `sEDiv` y) * (y `sEDiv` x))) =: sTrue@@ -131,7 +131,7 @@ =: qed , n `sEMod` k ./= 0 ==> d `dvd` n .&& k .<= d .&& d .<= n ?? d .== ld (k+1) n- ?? ih+ ?? ih `at` (Inst @"k" (k+1), Inst @"n" n) =: sTrue =: qed ]@@ -172,7 +172,9 @@ -- Lemma: leastDivisorIsLeast Q.E.D. -- Lemma: helper1 Q.E.D. -- Lemma: helper2 Q.E.D.--- Lemma: helper3 Q.E.D.+-- Lemma: helper3+-- Step: 1 Q.E.D.+-- Result: Q.E.D. -- Lemma: helper4 Q.E.D. -- Lemma: helper5 -- Step: 1 Q.E.D.@@ -185,7 +187,8 @@ ldd <- recall "leastDivisorDivides" leastDivisorDivides ldl <- recall "leastDivisorIsLeast" leastDivisorIsLeast - h1 <- lemma "helper1"+ h1 <- lemmaWith cvc5+ "helper1" (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) `dvd` ld k n .&& ld k (ld k n) .<= ld k n) [proofOf ldd] @@ -193,9 +196,15 @@ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k n `dvd` n) [proofOf ldd] - h3 <- lemma "helper3"- (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) `dvd` n)- [proofOf h1, proofOf h2, proofOf dt]+ h3 <- calc "helper3"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) `dvd` n) $+ \k n -> [n .>= k, k .>= 2]+ |- ld k (ld k n) `dvd` n+ ?? h1+ ?? h2+ ?? dt `at` (Inst @"x" (ld k (ld k n)), Inst @"y" (ld k n), Inst @"z" n)+ =: sTrue+ =: qed h4 <- lemma "helper4" (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> k .<= ld k (ld k n))@@ -242,7 +251,7 @@ -- [Proven] leastDivisorIsPrime :: Ɐn ∷ Integer → Bool leastDivisorIsPrime :: TP (Proof (Forall "n" Integer -> SBool)) leastDivisorIsPrime = do- ldt <- recall "leastDivisorTwice" leastDivisorTwice+ ldt <- recall "leastDivisorTwice" leastDivisorTwice ldd <- recall "leastDivisorDivides" leastDivisorDivides calc "leastDivisorIsPrime"
Documentation/SBV/Examples/TP/QuickSort.hs view
@@ -31,7 +31,7 @@ import Data.SBV.List hiding (partition) import Data.SBV.Tuple import Data.SBV.TP-import qualified Data.SBV.TP.List as TP+import qualified Documentation.SBV.Examples.TP.Lists as TP import qualified Documentation.SBV.Examples.TP.SortHelpers as SH
Documentation/SBV/Examples/TP/Reverse.hs view
@@ -30,7 +30,7 @@ import Data.SBV.List hiding (partition) import Data.SBV.TP -import qualified Data.SBV.TP.List as TP+import qualified Documentation.SBV.Examples.TP.Lists as TP #ifdef DOCTEST -- $setup
Documentation/SBV/Examples/TP/SortHelpers.hs view
@@ -25,7 +25,7 @@ import Data.SBV import Data.SBV.List import Data.SBV.TP-import Data.SBV.TP.List+import Documentation.SBV.Examples.TP.Lists #ifdef DOCTEST -- $setup
LICENSE view
@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2025, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2026, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
README.md view
@@ -1,6 +1,6 @@ # SBV: SMT Based Verification in Haskell -[](https://github.com/LeventErkok/sbv/actions/workflows/haskell-ci.yml)+[](https://github.com/LeventErkok/sbv/actions/workflows/ci.yml) On Hackage: http://hackage.haskell.org/package/sbv
SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs view
@@ -26,3 +26,5 @@ , runIO "CodeGen" genCCode ] where testLeft = \x y -> tstShiftLeft x y 0 .== x + y++{- HLint ignore module "Redundant lambda" -}
SBVBenchSuite/BenchSuite/Crypto/AES.hs view
@@ -33,3 +33,5 @@ , runIO "CodeGen.AES128Lib" cgAES128Library ] where inverseGFPrf = \x -> x ./= 0 .=> x `gf28Mult` gf28Inverse x .== 1++{- HLint ignore module "Redundant lambda" -}
SBVBenchSuite/BenchSuite/Misc/Enumerate.hs view
@@ -35,3 +35,5 @@ constrain $ \(Forall e) -> mx .>= (e::SE) _minE = do mx <- free "minE" constrain $ \(Forall e) -> mx .<= (e::SE)++{- HLint ignore module "Redundant lambda" -}
SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs view
@@ -129,3 +129,5 @@ relCompFull = \(a :: SI) -> a \\ full .== empty distSubset1 = \(a :: SI) b c -> a `isSubsetOf` (b `union` c) .=> a `isSubsetOf` b .&& a `isSubsetOf` c distSubset2 = \(a :: SI) b c -> (b `intersection` c) `isSubsetOf` a .=> b `isSubsetOf` a .&& c `isSubsetOf` a++{- HLint ignore module "Redundant lambda" -}
SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs view
@@ -19,9 +19,6 @@ import Utils.SBVBenchFramework import BenchSuite.Bench.Bench as S -import Data.Maybe (fromMaybe)-- -- benchmark suite benchmarks :: Runner benchmarks = rGroup@@ -32,4 +29,4 @@ checkPuzzle :: Puzzle -> IO Bool checkPuzzle p = do final <- fillBoard p let vld = valid (map (map literal) final)- pure $ fromMaybe False (unliteral vld)+ pure $ Just True == unliteral vld
SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs view
@@ -33,3 +33,6 @@ r <- free "r" return $ not (p `or` (q `and` r)) .== (not p `and` not q) `or` (not p `and` not r)++{- HLint ignore module "Redundant lambda" -}+{- HLint ignore module "Redundant not" -}
SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs view
@@ -36,3 +36,5 @@ sFalse correct = \a1 a0 b1 b0 -> mul22_hi a1 a0 b1 b0 .== (a1 .&& b0) .<+> (a0 .&& b1)++{- HLint ignore module "Redundant lambda" -}
SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs view
@@ -41,3 +41,5 @@ f' = derivative f f'' = universal f f''' = existential f++{- HLint ignore module "Redundant lambda" -}
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 1086; Tried: 1086; Skipped: 0; Success: 1086; Errors: 0; Failures 0-Examples: 969; Tried: 969; Skipped: 0; Success: 969; Errors: 0; Failures 0-Setup: 117; Tried: 117; Skipped: 0; Success: 117; Errors: 0; Failures 0+Total: 1089; Tried: 1089; Skipped: 0; Success: 1089; Errors: 0; Failures 0+Examples: 971; Tried: 971; Skipped: 0; Success: 971; Errors: 0; Failures 0+Setup: 118; Tried: 118; Skipped: 0; Success: 118; Errors: 0; Failures 0
SBVTestSuite/GoldFiles/lambda70.gold view
@@ -46,16 +46,18 @@ [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) [SEND] (get-value (x_eu1))-[RECV] ((x_eu1 ((as const (Array Int Int)) 0)))+[RECV] ((x_eu1 (store ((as const (Array Int Int)) 1) 1 0))) [SEND] (get-value (x_eu2))-[RECV] ((x_eu2 ((as const (Array Int Int)) 1)))+[RECV] ((x_eu2 (store ((as const (Array Int Int)) 0) 1 1))) *** Solver : Z3 *** Exit code: ExitSuccess RESULT: Satisfiable. Model: x_eu1 :: Integer -> Integer- x_eu1 _ = 0+ x_eu1 1 = 0+ x_eu1 _ = 1 x_eu2 :: Integer -> Integer- x_eu2 _ = 1+ x_eu2 1 = 1+ x_eu2 _ = 0
+ SBVTestSuite/GoldFiles/qOpt_1.gold view
@@ -0,0 +1,109 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () Int 1)+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () Int) ; tracks user variable "x1"+[GOOD] (declare-fun s4 () Int) ; tracks user variable "x2"+[GOOD] (declare-fun s7 () Int) ; tracks user variable "x3"+[GOOD] (declare-fun s10 () Int) ; tracks user variable "x4"+[GOOD] (declare-fun s13 () Int) ; tracks user variable "x5"+[GOOD] ; --- optimization tracker variables ---+[GOOD] (declare-fun s3 () Int) ; tracks goal1+[GOOD] (declare-fun s6 () Int) ; tracks goal2+[GOOD] (declare-fun s9 () Int) ; tracks goal3+[GOOD] (declare-fun s12 () Int) ; tracks goal4+[GOOD] (declare-fun s15 () Int) ; tracks goal5+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s2 () Bool (<= s1 s0))+[GOOD] (define-fun s5 () Bool (<= s1 s4))+[GOOD] (define-fun s8 () Bool (<= s1 s7))+[GOOD] (define-fun s11 () Bool (<= s1 s10))+[GOOD] (define-fun s14 () Bool (<= s1 s13))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert s2)+[GOOD] (assert s5)+[GOOD] (assert s8)+[GOOD] (assert s11)+[GOOD] (assert s14)+[GOOD] (assert (= s0 s3))+[GOOD] (maximize s3)+[GOOD] (assert (= s4 s6))+[GOOD] (maximize s6)+[GOOD] (assert (= s7 s9))+[GOOD] (maximize s9)+[GOOD] (assert (= s10 s12))+[GOOD] (maximize s12)+[GOOD] (assert (= s13 s15))+[GOOD] (maximize s15)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-objectives)+[RECV] (objectives+ (s3 oo)+ (s6 (interval (* (- 1) oo) oo))+ (s9 (interval (* (- 1) oo) oo))+ (s12 (interval (* (- 1) oo) oo))+ (s15 (interval (* (- 1) oo) oo))+ )+[SEND] (get-value (s0))+[RECV] ((s0 1))+[SEND] (get-value (s4))+[RECV] ((s4 1))+[SEND] (get-value (s7))+[RECV] ((s7 1))+[SEND] (get-value (s10))+[RECV] ((s10 1))+[SEND] (get-value (s13))+[RECV] ((s13 1))+[SEND] (get-value (s3))+[RECV] ((s3 1))+[SEND] (get-value (s6))+[RECV] ((s6 1))+[SEND] (get-value (s9))+[RECV] ((s9 1))+[SEND] (get-value (s12))+[RECV] ((s12 1))+[SEND] (get-value (s15))+[RECV] ((s15 1))+[SEND] (get-objectives)+[RECV] (objectives+ (s3 oo)+ (s6 (interval (* (- 1) oo) oo))+ (s9 (interval (* (- 1) oo) oo))+ (s12 (interval (* (- 1) oo) oo))+ (s15 (interval (* (- 1) oo) oo))+ )+*** Solver : Z3+*** Exit code: ExitFailure (-15)++EXCEPTION CAUGHT:++*** Data.SBV.getValue: The current solver state is satisfiable in an extension field.+*** That is, the optimized values assume epsilon/infinity values.+***+*** Calls to getValue is not supported in this context. Instead, use the 'optimize' method+*** directly and inspect the objective values explicitly.+***+*** The current model is:+***+*** Optimal in an extension field:+*** goal1 = oo :: Integer+*** goal2 = [-oo .. oo] :: [Integer]+*** goal3 = [-oo .. oo] :: [Integer]+*** goal4 = [-oo .. oo] :: [Integer]+*** goal5 = [-oo .. oo] :: [Integer]+
+ SBVTestSuite/GoldFiles/qOpt_2.gold view
@@ -0,0 +1,119 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () Int 1)+[GOOD] (define-fun s3 () Int 10)+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () Int) ; tracks user variable "x1"+[GOOD] (declare-fun s6 () Int) ; tracks user variable "x2"+[GOOD] (declare-fun s10 () Int) ; tracks user variable "x3"+[GOOD] (declare-fun s14 () Int) ; tracks user variable "x4"+[GOOD] (declare-fun s18 () Int) ; tracks user variable "x5"+[GOOD] ; --- optimization tracker variables ---+[GOOD] (declare-fun s5 () Int) ; tracks goal1+[GOOD] (declare-fun s9 () Int) ; tracks goal2+[GOOD] (declare-fun s13 () Int) ; tracks goal3+[GOOD] (declare-fun s17 () Int) ; tracks goal4+[GOOD] (declare-fun s21 () Int) ; tracks goal5+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s2 () Bool (<= s1 s0))+[GOOD] (define-fun s4 () Bool (< s0 s3))+[GOOD] (define-fun s7 () Bool (<= s1 s6))+[GOOD] (define-fun s8 () Bool (< s6 s3))+[GOOD] (define-fun s11 () Bool (<= s1 s10))+[GOOD] (define-fun s12 () Bool (< s10 s3))+[GOOD] (define-fun s15 () Bool (<= s1 s14))+[GOOD] (define-fun s16 () Bool (< s14 s3))+[GOOD] (define-fun s19 () Bool (<= s1 s18))+[GOOD] (define-fun s20 () Bool (< s18 s3))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert s2)+[GOOD] (assert s4)+[GOOD] (assert s7)+[GOOD] (assert s8)+[GOOD] (assert s11)+[GOOD] (assert s12)+[GOOD] (assert s15)+[GOOD] (assert s16)+[GOOD] (assert s19)+[GOOD] (assert s20)+[GOOD] (assert (= s0 s5))+[GOOD] (maximize s5)+[GOOD] (assert (= s6 s9))+[GOOD] (maximize s9)+[GOOD] (assert (= s10 s13))+[GOOD] (maximize s13)+[GOOD] (assert (= s14 s17))+[GOOD] (maximize s17)+[GOOD] (assert (= s18 s21))+[GOOD] (maximize s21)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-objectives)+[RECV] (objectives+ (s5 9)+ (s9 9)+ (s13 9)+ (s17 9)+ (s21 9)+ )+[SEND] (get-value (s0))+[RECV] ((s0 9))+[SEND] (get-objectives)+[RECV] (objectives+ (s5 9)+ (s9 9)+ (s13 9)+ (s17 9)+ (s21 9)+ )+[SEND] (get-value (s6))+[RECV] ((s6 9))+[SEND] (get-objectives)+[RECV] (objectives+ (s5 9)+ (s9 9)+ (s13 9)+ (s17 9)+ (s21 9)+ )+[SEND] (get-value (s10))+[RECV] ((s10 9))+[SEND] (get-objectives)+[RECV] (objectives+ (s5 9)+ (s9 9)+ (s13 9)+ (s17 9)+ (s21 9)+ )+[SEND] (get-value (s14))+[RECV] ((s14 9))+[SEND] (get-objectives)+[RECV] (objectives+ (s5 9)+ (s9 9)+ (s13 9)+ (s17 9)+ (s21 9)+ )+[SEND] (get-value (s18))+[RECV] ((s18 9))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:[9,9,9,9,9]+DONE!
SBVTestSuite/GoldFiles/set_uninterp1.gold view
@@ -60,45 +60,45 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) true) C false)))+[RECV] ((s0 (store ((as const (Array E Bool)) false) A true))) [GOOD] (push 1)-[GOOD] (define-fun s7 () (Array E Bool) (store ((as const (Array E Bool)) true) (as C E) false))+[GOOD] (define-fun s7 () (Array E Bool) (store ((as const (Array E Bool)) false) (as A E) true)) [GOOD] (define-fun s8 () Bool (distinct s0 s7)) [GOOD] (assert s8) Fast allSat, Looking for solution 5 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) B false)))+[RECV] ((s0 (store ((as const (Array E Bool)) false) B true))) [GOOD] (push 1)-[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as C E) false) (as B E) false))+[GOOD] (define-fun s9 () (Array E Bool) (store ((as const (Array E Bool)) false) (as B E) true)) [GOOD] (define-fun s10 () Bool (distinct s0 s9)) [GOOD] (assert s10) Fast allSat, Looking for solution 6 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) false) C true)))+[RECV] ((s0 (store (store ((as const (Array E Bool)) true) B false) A false))) [GOOD] (push 1)-[GOOD] (define-fun s11 () (Array E Bool) (store ((as const (Array E Bool)) false) (as C E) true))+[GOOD] (define-fun s11 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as B E) false) (as A E) false)) [GOOD] (define-fun s12 () Bool (distinct s0 s11)) [GOOD] (assert s12) Fast allSat, Looking for solution 7 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))+[RECV] ((s0 (store ((as const (Array E Bool)) true) B false))) [GOOD] (push 1)-[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as A E) true))+[GOOD] (define-fun s13 () (Array E Bool) (store ((as const (Array E Bool)) true) (as B E) false)) [GOOD] (define-fun s14 () Bool (distinct s0 s13)) [GOOD] (assert s14) Fast allSat, Looking for solution 8 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) false) B true)))+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true))) [GOOD] (push 1)-[GOOD] (define-fun s15 () (Array E Bool) (store ((as const (Array E Bool)) false) (as B E) true))+[GOOD] (define-fun s15 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as B E) true) (as A E) true)) [GOOD] (define-fun s16 () Bool (distinct s0 s15)) [GOOD] (assert s16) Fast allSat, Looking for solution 9@@ -117,15 +117,15 @@ FINAL: Solution #1:- s0 = {B} :: {E}+ s0 = {A,B} :: {E} Solution #2:- s0 = {A,C} :: {E}+ s0 = U - {B} :: {E} Solution #3:- s0 = {C} :: {E}+ s0 = U - {A,B} :: {E} Solution #4:- s0 = U - {B,C} :: {E}+ s0 = {B} :: {E} Solution #5:- s0 = U - {C} :: {E}+ s0 = {A} :: {E} Solution #6: s0 = U - {A} :: {E} Solution #7:
SBVTestSuite/TestSuite/ADT/MutRec.hs view
@@ -15,7 +15,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} -{-# OPTIONS_GHC -Wall -Werror #-}+{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-record-selectors #-} module TestSuite.ADT.MutRec(tests) where
SBVTestSuite/TestSuite/Arrays/Query.hs view
@@ -217,3 +217,5 @@ query $ do constrain $ readArray x (literal ('z', 5 % 3)) .== literal (5 % 3, 'z') checkSat++{- HLint ignore module "Reduce duplication" -}
SBVTestSuite/TestSuite/Basics/Lambda.hs view
@@ -207,6 +207,17 @@ , goldenCapturedIO "lambda69" $ runS $ \(Forall x) (Forall y) -> uninterpret "F" x y .== 2*x+(3-y::SInteger) -- Most skolems are tested inline, here's a fancy one!+ -- This is satisfiable. A model for this will present two functions, x_eu1 and x_eu2+ -- If these functions differ on all mappings i.e. forall x. x_eu1 x /= x_eu2 x, then+ -- it would be a valid model for this problem. Note that these functions can+ -- be constant functions mapping to different values; or functions that distinguish+ -- some subset of inputs, so long as they map it to different values. Examples:+ -- x_eu1 _ = 0 x_eu2 _ = 0+ -- OR+ -- x_eu1 1 = 0 x_eu2 1 = 1+ -- x_eu1 _ = 1 x_eu2 _ = 0+ --+ -- are all good. , goldenCapturedIO "lambda70" $ let phi :: ExistsUnique "x" Integer -> SBool phi (ExistsUnique x) = x .== 0 .|| x .== 1
SBVTestSuite/TestSuite/Basics/Quantifiers.hs view
@@ -9,14 +9,10 @@ -- Various combinations of quantifiers ----------------------------------------------------------------------------- -{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-}--#if MIN_VERSION_base(4,19,0) {-# LANGUAGE TypeAbstractions #-}-#endif {-# OPTIONS_GHC -Wall -Werror #-}
SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr view
@@ -2,7 +2,7 @@ mkSymbolic: Unsupported constructor kind Datatype : A Constructor: F- Kind : GHC.Num.Integer.Integer -> GHC.Types.Bool+ Kind : GHC.Internal.Bignum.Integer.Integer -> GHC.Internal.Types.Bool Higher order fields (i.e., function values) are not supported.
SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr view
@@ -2,7 +2,7 @@ mkSymbolic: Unsupported constructor kind Datatype : A Constructor: F- Kind : T.A -> GHC.Types.Bool+ Kind : T.A -> GHC.Internal.Types.Bool Higher order fields (i.e., function values) are not supported.
SBVTestSuite/TestSuite/Optimization/Basics.hs view
@@ -9,18 +9,26 @@ -- Test suite for optimization routines ----------------------------------------------------------------------------- +{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall -Werror #-} module TestSuite.Optimization.Basics(tests) where import Utils.SBVTestFramework+import Data.SBV.Control +import Control.Monad++import qualified Control.Exception as C+ -- Test suite tests :: TestTree tests = testGroup "Optimization.Basics" $ [ goldenVsStringShow "optBasics1" (optimize Lexicographic optBasics1) , goldenVsStringShow "optBasics2" (optimize Lexicographic optBasics2)+ , goldenCapturedIO "qOpt_1" (qOpt False)+ , goldenCapturedIO "qOpt_2" (qOpt True) ] ++ [ goldenVsStringShow ("optBasicsRange_" ++ n) (optimize Lexicographic f) | (n, f) <- [ ("08_unsigned_max", sWord8 "x" >>= maximize "m")@@ -60,3 +68,18 @@ constrain $ y .> 1 minimize "x_plus_y" $ x+y++qOpt :: Bool -> FilePath -> IO ()+qOpt mb rf = testQuery $ do+ vs <- forM [1 .. 5] $ \i -> do x <- sInteger ("x" <> show (i::Int))+ constrain $ 1 .<= x+ when mb $ constrain $ x .< 10+ maximize ("goal" <> show i) x+ pure x+ query $ do cs <- checkSat+ case cs of+ Sat -> forM vs getValue+ _ -> pure []+ where testQuery fv = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} fv+ appendFile rf ("\n FINAL:" ++ show r ++ "\nDONE!\n")+ `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\nEXCEPTION CAUGHT:\n" ++ show e ++ "\n"))
SBVTestSuite/TestSuite/Puzzles/Sudoku.hs view
@@ -15,7 +15,6 @@ import Documentation.SBV.Examples.Puzzles.Sudoku -import Data.Maybe (fromMaybe) import Utils.SBVTestFramework tests :: TestTree@@ -27,4 +26,4 @@ checkPuzzle :: Puzzle -> IO Bool checkPuzzle p = do final <- fillBoard p let vld = valid (map (map literal) final)- pure $ fromMaybe False (unliteral vld)+ pure $ Just True == unliteral vld
SBVTestSuite/TestSuite/Queries/UISatEx.hs view
@@ -14,11 +14,8 @@ {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}--#if MIN_VERSION_base(4,19,0) {-# LANGUAGE TypeAbstractions #-}-#endif+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-}
sbv.cabal view
@@ -1,13 +1,13 @@ Cabal-Version: 2.2 Name : sbv-Version : 13.3+Version : 13.4 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 (Satisfiability Modulo Theories) solvers. -Copyright : Levent Erkok, 2010-2025+Copyright : Levent Erkok, 2010-2026 License : BSD-3-Clause License-file : LICENSE Stability : Experimental@@ -21,8 +21,6 @@ SBVTestSuite/TestSuite/CompileTests/SCase/*.stderr Extra-Doc-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.10.1- flag doctest_is_running description: Define this flag during doctest run default : False@@ -135,7 +133,6 @@ , Data.SBV.Tuple , Data.SBV.RegExp , Data.SBV.TP- , Data.SBV.TP.List , Data.SBV.Tools.BMC , Data.SBV.Tools.BVOptimize , Data.SBV.Tools.Induction@@ -226,6 +223,7 @@ , Documentation.SBV.Examples.Puzzles.Orangutans , Documentation.SBV.Examples.Puzzles.Rabbits , Documentation.SBV.Examples.Puzzles.SendMoreMoney+ , Documentation.SBV.Examples.Puzzles.SquareBirthday , Documentation.SBV.Examples.Puzzles.Sudoku , Documentation.SBV.Examples.Puzzles.Tower , Documentation.SBV.Examples.Puzzles.U2Bridge@@ -247,6 +245,7 @@ , Documentation.SBV.Examples.TP.GCD , Documentation.SBV.Examples.TP.InsertionSort , Documentation.SBV.Examples.TP.Kleene+ , Documentation.SBV.Examples.TP.Lists , Documentation.SBV.Examples.TP.McCarthy91 , Documentation.SBV.Examples.TP.Majority , Documentation.SBV.Examples.TP.MergeSort