diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,35 @@ * Hackage: * GitHub: +### 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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 diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -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_" -} diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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_" -} diff --git a/Data/SBV/Core/Concrete.hs b/Data/SBV/Core/Concrete.hs --- a/Data/SBV/Core/Concrete.hs +++ b/Data/SBV/Core/Concrete.hs @@ -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)) diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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@ diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -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. -- diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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. diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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 diff --git a/Data/SBV/TP.hs b/Data/SBV/TP.hs --- a/Data/SBV/TP.hs +++ b/Data/SBV/TP.hs @@ -72,7 +72,7 @@ , disp -- * Recall an old proof, quietly proving it - , recall + , recall, recallWith ) where import Data.SBV.TP.TP diff --git a/Data/SBV/TP/Kernel.hs b/Data/SBV/TP/Kernel.hs --- a/Data/SBV/TP/Kernel.hs +++ b/Data/SBV/TP/Kernel.hs @@ -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) diff --git a/Data/SBV/TP/List.hs b/Data/SBV/TP/List.hs deleted file mode 100644 --- a/Data/SBV/TP/List.hs +++ /dev/null @@ -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" -} diff --git a/Data/SBV/TP/TP.hs b/Data/SBV/TP/TP.hs --- a/Data/SBV/TP/TP.hs +++ b/Data/SBV/TP/TP.hs @@ -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" -} diff --git a/Documentation/SBV/Examples/ADT/Expr.hs b/Documentation/SBV/Examples/ADT/Expr.hs --- a/Documentation/SBV/Examples/ADT/Expr.hs +++ b/Documentation/SBV/Examples/ADT/Expr.hs @@ -162,3 +162,5 @@ io $ putStrLn $ "e1: " ++ show e1v io $ putStrLn $ "e2: " ++ show e2v _ -> error $ "Unexpected result: " ++ show cs + +{- HLint ignore module "Reduce duplication" -} diff --git a/Documentation/SBV/Examples/ADT/Param.hs b/Documentation/SBV/Examples/ADT/Param.hs --- a/Documentation/SBV/Examples/ADT/Param.hs +++ b/Documentation/SBV/Examples/ADT/Param.hs @@ -181,3 +181,5 @@ io $ putStrLn $ "e2: " ++ show e2v io $ putStrLn $ "e3: " ++ show e3v _ -> error $ "Unexpected result: " ++ show cs + +{- HLint ignore module "Reduce duplication" -} diff --git a/Documentation/SBV/Examples/Crypto/AES.hs b/Documentation/SBV/Examples/Crypto/AES.hs --- a/Documentation/SBV/Examples/Crypto/AES.hs +++ b/Documentation/SBV/Examples/Crypto/AES.hs @@ -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" -} diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs --- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs @@ -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 #-} diff --git a/Documentation/SBV/Examples/Misc/LambdaArray.hs b/Documentation/SBV/Examples/Misc/LambdaArray.hs --- a/Documentation/SBV/Examples/Misc/LambdaArray.hs +++ b/Documentation/SBV/Examples/Misc/LambdaArray.hs @@ -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" -} diff --git a/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs @@ -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 , 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 diff --git a/Documentation/SBV/Examples/TP/Basics.hs b/Documentation/SBV/Examples/TP/Basics.hs --- a/Documentation/SBV/Examples/TP/Basics.hs +++ b/Documentation/SBV/Examples/TP/Basics.hs @@ -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 -- -- 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 -- -- 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 diff --git a/Documentation/SBV/Examples/TP/BinarySearch.hs b/Documentation/SBV/Examples/TP/BinarySearch.hs --- a/Documentation/SBV/Examples/TP/BinarySearch.hs +++ b/Documentation/SBV/Examples/TP/BinarySearch.hs @@ -263,3 +263,5 @@ =: sTrue =: qed ] + +{- HLint ignore module "Reduce duplication" -} diff --git a/Documentation/SBV/Examples/TP/GCD.hs b/Documentation/SBV/Examples/TP/GCD.hs --- a/Documentation/SBV/Examples/TP/GCD.hs +++ b/Documentation/SBV/Examples/TP/GCD.hs @@ -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" diff --git a/Documentation/SBV/Examples/TP/Lists.hs b/Documentation/SBV/Examples/TP/Lists.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/Lists.hs @@ -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" -} diff --git a/Documentation/SBV/Examples/TP/Majority.hs b/Documentation/SBV/Examples/TP/Majority.hs --- a/Documentation/SBV/Examples/TP/Majority.hs +++ b/Documentation/SBV/Examples/TP/Majority.hs @@ -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 diff --git a/Documentation/SBV/Examples/TP/MergeSort.hs b/Documentation/SBV/Examples/TP/MergeSort.hs --- a/Documentation/SBV/Examples/TP/MergeSort.hs +++ b/Documentation/SBV/Examples/TP/MergeSort.hs @@ -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 diff --git a/Documentation/SBV/Examples/TP/Primes.hs b/Documentation/SBV/Examples/TP/Primes.hs --- a/Documentation/SBV/Examples/TP/Primes.hs +++ b/Documentation/SBV/Examples/TP/Primes.hs @@ -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" diff --git a/Documentation/SBV/Examples/TP/QuickSort.hs b/Documentation/SBV/Examples/TP/QuickSort.hs --- a/Documentation/SBV/Examples/TP/QuickSort.hs +++ b/Documentation/SBV/Examples/TP/QuickSort.hs @@ -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 diff --git a/Documentation/SBV/Examples/TP/Reverse.hs b/Documentation/SBV/Examples/TP/Reverse.hs --- a/Documentation/SBV/Examples/TP/Reverse.hs +++ b/Documentation/SBV/Examples/TP/Reverse.hs @@ -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 diff --git a/Documentation/SBV/Examples/TP/SortHelpers.hs b/Documentation/SBV/Examples/TP/SortHelpers.hs --- a/Documentation/SBV/Examples/TP/SortHelpers.hs +++ b/Documentation/SBV/Examples/TP/SortHelpers.hs @@ -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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # SBV: SMT Based Verification in Haskell -[![Build Status](https://github.com/LeventErkok/sbv/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/LeventErkok/sbv/actions/workflows/haskell-ci.yml) +[![Build Status](https://github.com/LeventErkok/sbv/actions/workflows/ci.yml/badge.svg)](https://github.com/LeventErkok/sbv/actions/workflows/ci.yml) On Hackage: http://hackage.haskell.org/package/sbv diff --git a/SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs b/SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs --- a/SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs +++ b/SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs @@ -26,3 +26,5 @@ , runIO "CodeGen" genCCode ] where testLeft = \x y -> tstShiftLeft x y 0 .== x + y + +{- HLint ignore module "Redundant lambda" -} diff --git a/SBVBenchSuite/BenchSuite/Crypto/AES.hs b/SBVBenchSuite/BenchSuite/Crypto/AES.hs --- a/SBVBenchSuite/BenchSuite/Crypto/AES.hs +++ b/SBVBenchSuite/BenchSuite/Crypto/AES.hs @@ -33,3 +33,5 @@ , runIO "CodeGen.AES128Lib" cgAES128Library ] where inverseGFPrf = \x -> x ./= 0 .=> x `gf28Mult` gf28Inverse x .== 1 + +{- HLint ignore module "Redundant lambda" -} diff --git a/SBVBenchSuite/BenchSuite/Misc/Enumerate.hs b/SBVBenchSuite/BenchSuite/Misc/Enumerate.hs --- a/SBVBenchSuite/BenchSuite/Misc/Enumerate.hs +++ b/SBVBenchSuite/BenchSuite/Misc/Enumerate.hs @@ -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" -} diff --git a/SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs b/SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs --- a/SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs +++ b/SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs @@ -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" -} diff --git a/SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs b/SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs --- a/SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs +++ b/SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs @@ -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 diff --git a/SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs b/SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs --- a/SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs +++ b/SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs @@ -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" -} diff --git a/SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs b/SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs --- a/SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs +++ b/SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs @@ -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" -} diff --git a/SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs b/SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs --- a/SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs +++ b/SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs @@ -41,3 +41,5 @@ f' = derivative f f'' = universal f f''' = existential f + +{- HLint ignore module "Redundant lambda" -} diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/lambda70.gold b/SBVTestSuite/GoldFiles/lambda70.gold --- a/SBVTestSuite/GoldFiles/lambda70.gold +++ b/SBVTestSuite/GoldFiles/lambda70.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/qOpt_1.gold b/SBVTestSuite/GoldFiles/qOpt_1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/qOpt_1.gold @@ -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] + diff --git a/SBVTestSuite/GoldFiles/qOpt_2.gold b/SBVTestSuite/GoldFiles/qOpt_2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/qOpt_2.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold --- a/SBVTestSuite/GoldFiles/set_uninterp1.gold +++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold @@ -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: diff --git a/SBVTestSuite/TestSuite/ADT/MutRec.hs b/SBVTestSuite/TestSuite/ADT/MutRec.hs --- a/SBVTestSuite/TestSuite/ADT/MutRec.hs +++ b/SBVTestSuite/TestSuite/ADT/MutRec.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Arrays/Query.hs b/SBVTestSuite/TestSuite/Arrays/Query.hs --- a/SBVTestSuite/TestSuite/Arrays/Query.hs +++ b/SBVTestSuite/TestSuite/Arrays/Query.hs @@ -217,3 +217,5 @@ query $ do constrain $ readArray x (literal ('z', 5 % 3)) .== literal (5 % 3, 'z') checkSat + +{- HLint ignore module "Reduce duplication" -} diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Basics/Quantifiers.hs b/SBVTestSuite/TestSuite/Basics/Quantifiers.hs --- a/SBVTestSuite/TestSuite/Basics/Quantifiers.hs +++ b/SBVTestSuite/TestSuite/Basics/Quantifiers.hs @@ -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 #-} diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr @@ -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. diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr @@ -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. diff --git a/SBVTestSuite/TestSuite/Optimization/Basics.hs b/SBVTestSuite/TestSuite/Optimization/Basics.hs --- a/SBVTestSuite/TestSuite/Optimization/Basics.hs +++ b/SBVTestSuite/TestSuite/Optimization/Basics.hs @@ -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")) diff --git a/SBVTestSuite/TestSuite/Puzzles/Sudoku.hs b/SBVTestSuite/TestSuite/Puzzles/Sudoku.hs --- a/SBVTestSuite/TestSuite/Puzzles/Sudoku.hs +++ b/SBVTestSuite/TestSuite/Puzzles/Sudoku.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Queries/UISatEx.hs b/SBVTestSuite/TestSuite/Queries/UISatEx.hs --- a/SBVTestSuite/TestSuite/Queries/UISatEx.hs +++ b/SBVTestSuite/TestSuite/Queries/UISatEx.hs @@ -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 #-} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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