sbv 11.5 → 11.6
raw patch · 30 files changed
+1100/−621 lines, 30 filesdep ~base
Dependency ranges changed: base
Files
- CHANGES.md +10/−0
- Data/SBV.hs +10/−3
- Data/SBV/Core/Data.hs +0/−7
- Data/SBV/Core/Model.hs +21/−0
- Data/SBV/Core/Symbolic.hs +29/−42
- Data/SBV/SMT/SMTLib2.hs +2/−2
- Data/SBV/Tools/KD/Kernel.hs +3/−3
- Data/SBV/Tools/KD/KnuckleDragger.hs +226/−300
- Data/SBV/Tools/KD/Utils.hs +11/−4
- Data/SBV/Tools/KnuckleDragger.hs +4/−4
- Documentation/SBV/Examples/KnuckleDragger/Basics.hs +33/−0
- Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs +271/−0
- Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs +3/−3
- Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs +48/−48
- Documentation/SBV/Examples/KnuckleDragger/Kleene.hs +6/−5
- Documentation/SBV/Examples/KnuckleDragger/Lists.hs +32/−27
- Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs +99/−92
- Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +42/−12
- Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs +9/−9
- Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs +2/−4
- Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs +218/−37
- Documentation/SBV/Examples/Transformers/SymbolicEval.hs +1/−1
- README.md +4/−3
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/GoldFiles/nested1.gold +2/−2
- SBVTestSuite/GoldFiles/nested2.gold +2/−2
- SBVTestSuite/GoldFiles/nested3.gold +2/−2
- SBVTestSuite/GoldFiles/nested4.gold +2/−2
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- sbv.cabal +3/−2
CHANGES.md view
@@ -1,6 +1,16 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 11.6, 2025-05-10+ + * Make SBV compile cleanly with GHC 9.8.4. This is really as far back a GHC you should be using,+ unless you can't use anything newer.++ * KnuckleDragger:+ - Simplify and generalize inductive proofs. You can now do proofs with user-specified measure functions.+ - Tweak proof-traces to print user given hints (aids in debugging).+ - Add a proof of correctness for the binary-search algorithm.+ ### Version 11.5, 2025-04-25 * Documentation updates
Data/SBV.hs view
@@ -150,12 +150,13 @@ -- get in touch if there is a solver you'd like to see included. -- ----- __Semi-automated theorem proving__+-- __KnuckleDragger: Semi-automated theorem proving__ -- -- While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT -- solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about--- any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a--- style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs.+-- any recursive algorithm, and most such proofs require carefully constructed equational steps.+--+-- SBV allows for a style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs. -- The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion -- and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle -- etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can@@ -169,6 +170,12 @@ -- - "Documentation.SBV.Examples.KnuckleDragger.Lists" -- -- for various proofs performed in this style.+--+-- Note that knuckle-dragger proofs are upto termination, i.e., if you axiomatize+-- non-terminating behavior, then you can prove arbitrary results. SBV neither+-- checks nor ensures termination, which is beyond its scope and capabilities.+-- So, any KnuckleDragger proof should be considered true so long as all functions+-- used in the property are terminating. ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}
Data/SBV/Core/Data.hs view
@@ -396,13 +396,6 @@ instance Show (SBV a) where show (SBV sv) = show sv --- | This instance is only defined so that we can define an instance for--- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use--- 'Data.SBV.EqSymbolic' instead.-instance Eq (SBV a) where- SBV a == SBV b = a == b- SBV a /= SBV b = a /= b- instance HasKind a => HasKind (SBV a) where kindOf _ = kindOf (Proxy @a)
Data/SBV/Core/Model.hs view
@@ -1597,6 +1597,27 @@ swb <- sbvToSV st b newExpr st k (SBVApp (NonLinear w) [swa, swb]) +-- Bail out nicely.+noEquals :: String -> String -> (String, String) -> a+noEquals o n (l, r) = error $ unlines [ ""+ , "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!"+ , "***"+ , "*** Received: (" ++ l ++ ") " ++ o ++ " (" ++ r ++ ")"+ , "*** Instead use: (" ++ l ++ ") " ++ n ++ " (" ++ r ++ ")"+ , "***"+ , "*** The Eq instance for symbolic values are necessiated only because"+ , "*** of the Bits class requirement. You must use symbolic equality"+ , "*** operators instead. (And complain to Haskell folks that they"+ , "*** remove the 'Eq' superclass from 'Bits'!.)"+ ]++-- | This instance is only defined so that we can define an instance for+-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use+-- 'Data.SBV.EqSymbolic' instead.+instance SymVal a => Eq (SBV a) where+ a == b = fromMaybe (noEquals "==" ".==" (show a, show b)) (unliteral (a .== b))+ a /= b = fromMaybe (noEquals "/=" "./=" (show a, show b)) (unliteral (a ./= b))+ -- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values -- | Using 'popCount' or 'testBit' on non-concrete values will result in an
Data/SBV/Core/Symbolic.hs view
@@ -1167,7 +1167,7 @@ -- | Find a user-input from its SV. Note that only level-0 vars -- can be found this way.-lookupInput :: Eq a => (a -> SV) -> SV -> S.Seq a -> Maybe a+lookupInput :: (a -> SV) -> SV -> S.Seq a -> Maybe a lookupInput f sv ns | l == Just 0 = res | True = Nothing -- l != Just 0, a lambda var, whether top-level or in a scope, so we ignore@@ -1282,6 +1282,7 @@ -- sure sharing is preserved. data SVal = SVal !Kind !(Either CV (Cached SV)) +-- | Kind instance for SVal simply passes the kind out instance HasKind SVal where kindOf (SVal k _) = k @@ -1294,29 +1295,6 @@ show (SVal k (Left c)) = showCV False c ++ " :: " ++ show k show (SVal k (Right _)) = "<symbolic> :: " ++ show k --- | This instance is only defined so that we can define an instance for--- 'Data.Bits.Bits'. '==' and '/=' simply throw an error.--- We really don't want an 'Eq' instance for 'Data.SBV.SBV' or t'SVal'. As it really makes no sense.--- But since we do want the 'Data.Bits.Bits' instance, we're forced to define equality. See--- <http://github.com/LeventErkok/sbv/issues/301>. We simply error out.-instance Eq SVal where- a == b = noEquals "==" ".==" (show a, show b)- a /= b = noEquals "/=" "./=" (show a, show b)---- Bail out nicely.-noEquals :: String -> String -> (String, String) -> a-noEquals o n (l, r) = error $ unlines [ ""- , "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!"- , "***"- , "*** Received: " ++ l ++ " " ++ o ++ " " ++ r- , "*** Instead use: " ++ l ++ " " ++ n ++ " " ++ r- , "***"- , "*** The Eq instance for symbolic values are necessiated only because"- , "*** of the Bits class requirement. You must use symbolic equality"- , "*** operators instead. (And complain to Haskell folks that they"- , "*** remove the 'Eq' superclass from 'Bits'!.)"- ]- -- | Things we do not support in interactive mode, at least for now! noInteractive :: [String] -> a noInteractive ss = error $ unlines $ ""@@ -1954,24 +1932,33 @@ -- | Catch the catastrophic case of context mismatch contextMismatchError :: SBVContext -> SBVContext -> Maybe (Int, Int) -> Maybe (Int, Int) -> a-contextMismatchError ctx1 ctx2 level1 level2 = error $ unlines $ prefix ++ rest- where prefix | ctx1 /= ctx2 = [ "Data.SBV: Mismatched contexts detected."- , "***"- , "*** Current context: " ++ show ctx1- , "*** Mixed with : " ++ show ctx2- ]- | True = [ "Data.SBV: Mismatched levels detected in the same context."- , "***"- , "*** Refers to: " ++ show level1- , "*** And also : " ++ show level2- ]-- rest = [ "***"- , "*** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc."- , "*** while another one is in execution, or use results from one such call in another."- , "*** Please avoid such nested calls, all interactions should be from the same context."- , "*** See https://github.com/LeventErkok/sbv/issues/71 for several examples."- ]+contextMismatchError ctx1 ctx2 level1 level2 = error $ unlines msg+ where msg | ctx1 /= ctx2 = [ "Data.SBV: Mismatched contexts detected."+ , "***"+ , "*** Current context: " ++ show ctx1+ , "*** Mixed with : " ++ show ctx2+ , "***"+ , "*** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc."+ , "*** while another one is in execution, or use results from one such call in another."+ , "*** Please avoid such nested calls, all interactions should be from the same context."+ , "*** See https://github.com/LeventErkok/sbv/issues/71 for several examples."+ ]+ | True = [ "Data.SBV: Mismatched levels detected in the same context."+ , "***"+ , "*** Refers to: " ++ show level1+ , "*** And also : " ++ show level2+ , "***"+ , "*** A typical reason for this is the use of a higher order function, typically from"+ , "*** Data.SBV.List, with a lambda that refers to a free variable. (For instance calling"+ , "*** 'f e xs = filter (.> e) xs' where 'x' is free in the lambda-expression '(.> e)'.)"+ , "***"+ , "*** While SBV does allow symbolic use of a selected subset of higher-order functions"+ , "*** like filter/map/fold, the lambda-arguments must be closed. (This is due to the"+ , "*** fact that SMTLib doesn't allow higher-order functions, and SBV firstifies such"+ , "*** uses with a simple translation that doesn't allow for captured variables.) As"+ , "*** SMTLib gains more higher order features, we might relax this constraint. Please"+ , "*** report your use case as an example application."+ ] -- | Run a symbolic computation in a given state runSymbolicInState :: MonadIO m => State -> SymbolicT m a -> m (a, Result)
Data/SBV/SMT/SMTLib2.hs view
@@ -25,7 +25,7 @@ import Data.List (intercalate, partition, nub, elemIndex) import Data.Maybe (listToMaybe, catMaybes) -import qualified Data.Foldable as F (toList)+import qualified Data.Foldable as F (toList, foldl') import qualified Data.Map.Strict as M import qualified Data.IntMap.Strict as IM import Data.Set (Set)@@ -79,7 +79,7 @@ -- Below can simply be defined as: nub (sort (G.universeBi asgnsSeq)) -- Alas, it turns out this is really expensive when we have nested lambdas, so we do an explicit walk- allTopOps = Set.toList $ foldl' (\sofar (_, SBVApp o _) -> Set.insert o sofar) Set.empty asgnsSeq+ allTopOps = Set.toList $ F.foldl' (\sofar (_, SBVApp o _) -> Set.insert o sofar) Set.empty asgnsSeq hasInteger = KUnbounded `Set.member` kindInfo hasArrays = not (null [() | KArray{} <- allKinds])
Data/SBV/Tools/KD/Kernel.hs view
@@ -176,9 +176,9 @@ die = error "Failed" fullNm = case ctx of- KDProofOneShot s _ -> s- KDProofStep True s ss -> "assumptions for " ++ intercalate "." (s : ss)- KDProofStep False s ss -> intercalate "." (s : ss)+ KDProofOneShot s _ -> s+ KDProofStep True s _ ss -> "assumptions for " ++ intercalate "." (s : ss)+ KDProofStep False s _ ss -> intercalate "." (s : ss) unknown = do r <- getUnknownReason liftIO $ do putStrLn $ "\n*** Failed to prove " ++ fullNm ++ "."
Data/SBV/Tools/KD/KnuckleDragger.hs view
@@ -38,7 +38,7 @@ , sInduct, sInductWith, sInductThm, sInductThmWith , sorry , KD, runKD, runKDWith, use- , (|-), (⊢), (=:), (≡), (??), (⁇), split, split2, cases, (==>), (⟹), hyp, hprf, qed, trivial+ , (|-), (⊢), (=:), (≡), (??), (⁇), split, split2, cases, (==>), (⟹), hasm, hprf, hcmnt, qed, trivial, contradiction ) where import Data.SBV@@ -77,12 +77,13 @@ -- | Saturatable things in steps proofTreeSaturatables :: KDProof -> [SBool] proofTreeSaturatables = go- where go (ProofEnd b hs) = b : concatMap getH hs- go (ProofStep a hs r) = a : concatMap getH hs ++ go r- go (ProofBranch (_ :: Bool) () ps) = concat [b : go p | (b, p) <- ps]+ where go (ProofEnd b hs ) = b : concatMap getH hs+ go (ProofStep a hs r) = a : concatMap getH hs ++ go r+ go (ProofBranch (_ :: Bool) (_ :: [String]) ps) = concat [b : go p | (b, p) <- ps] getH (HelperProof p) = [getProof p] getH (HelperAssum b) = [b]+ getH HelperString{} = [] -- | Things that are inside calc-strategy that we have to saturate getCalcStrategySaturatables :: CalcStrategy -> [SBool]@@ -216,15 +217,15 @@ = do -- If we're not at the top-level and this is the only step, print it. -- Otherwise the noise isn't necessary. when (level > 1) $ case reverse bn of- 1 : _ -> liftIO $ do tab <- startKD cfg False "Step" level (KDProofStep False nm (map show (init bn)))+ 1 : _ -> liftIO $ do tab <- startKD cfg False "Step" level (KDProofStep False nm [] (map show (init bn))) finishKD cfg "Q.E.D." (tab, Nothing) [] _ -> pure () - pure [initialHypotheses .&& intros .=> calcResult]+ pure [intros .=> calcResult] -- Do the branches separately and collect the results. If there's coverage needed, we do it too; which -- is essentially the assumption here.- walk intros level (bnTop, ProofBranch checkCompleteness () ps) = do+ walk intros level (bnTop, ProofBranch checkCompleteness hintStrings ps) = do let bn = trimBN level bnTop @@ -237,13 +238,13 @@ stepName = map show bn - _ <- io $ startKD cfg True "Step" level (KDProofStep False nm (addSuffix stepName (" (" ++ show (length ps) ++ " way " ++ full ++ "case split)")))+ _ <- io $ startKD cfg True "Step" level (KDProofStep False nm hintStrings (addSuffix stepName (" (" ++ show (length ps) ++ " way " ++ full ++ "case split)"))) results <- concat <$> sequence [walk (intros .&& branchCond) (level + 1) (bn ++ [i, 1], p) | (i, (branchCond, p)) <- zip [1..] ps] when checkCompleteness $ smtProofStep cfg kdSt "Step" (level+1)- (KDProofStep False nm (stepName ++ ["Completeness"]))- (Just (initialHypotheses .&& intros))+ (KDProofStep False nm [] (stepName ++ ["Completeness"]))+ (Just intros) (sOr (map fst ps)) (\d -> finishKD cfg "Q.E.D." d []) pure results@@ -262,18 +263,19 @@ | True = (cfg{kdOptions = (kdOptions cfg) { quiet = True}}, const (pure ())) as = concatMap getHelperAssumes hs+ ss = getHelperText hs case as of [] -> pure () _ -> smtProofStep quietCfg kdSt "Asms" level- (KDProofStep True nm stepName)- (Just (initialHypotheses .&& intros))+ (KDProofStep True nm [] stepName)+ (Just intros) (sAnd as) finalizer -- Now prove the step let by = concatMap getHelperProofs hs smtProofStep cfg kdSt "Step" level- (KDProofStep False nm stepName)+ (KDProofStep False nm ss stepName) (Just (sAnd (intros : as ++ map getProof by))) cur (finish [] by)@@ -281,12 +283,12 @@ -- Move to next walk intros level (next bn, p) - results <- walk sTrue 1 ([1], calcProofTree)+ results <- walk initialHypotheses 1 ([1], calcProofTree) queryDebug [nm ++ ": Proof end: proving the result:"] smtProofStep cfg kdSt "Result" 1- (KDProofStep False nm [""])+ (KDProofStep False nm [] [""]) (Just (initialHypotheses .=> sAnd results)) resultBool $ \d -> do mbElapsed <- getElapsedTime mbStartTime@@ -321,7 +323,7 @@ CalcStep begin end hs' -> ProofEnd (begin .== end) (hs' ++ hs) -- Branch: Just push it down. We use the hints from previous step, and pass the current ones down.- go step (ProofBranch c hs ps) = ProofBranch c () [(branchCond, go step' p) | (branchCond, p) <- ps]+ go step (ProofBranch c hs ps) = ProofBranch c (getHelperText hs) [(branchCond, go step' p) | (branchCond, p) <- ps] where step' = case step of CalcStart hs' -> CalcStart (hs' ++ hs) CalcStep a b hs' -> CalcStep a b (hs' ++ hs)@@ -369,20 +371,22 @@ -- | Captures the schema for an inductive proof. Base case might be nothing, to cover strong induction. data InductionStrategy = InductionStrategy { inductionIntros :: SBool+ , inductionMeasure :: Maybe SBool , inductionBaseCase :: Maybe SBool , inductionProofTree :: KDProof , inductiveStep :: SBool } --- | Are we doing strong induction or regular induction?-data InductionStyle = RegularInduction | StrongInduction+-- | Are we doing regular induction or measure based general induction?+data InductionStyle = RegularInduction | GeneralInduction getInductionStrategySaturatables :: InductionStrategy -> [SBool] getInductionStrategySaturatables (InductionStrategy inductionIntros+ inductionMeasure inductionBaseCase inductionProofSteps inductiveStep)- = inductionIntros : inductiveStep : proofTreeSaturatables inductionProofSteps ++ maybeToList inductionBaseCase+ = inductionIntros : inductiveStep : proofTreeSaturatables inductionProofSteps ++ maybeToList inductionBaseCase ++ maybeToList inductionMeasure -- | A class for doing regular inductive proofs. class Inductive a steps where@@ -415,36 +419,59 @@ {-# MINIMAL inductionStrategy #-} inductionStrategy :: Proposition a => a -> (Proof -> steps) -> Symbolic InductionStrategy --- | A class for doing strong inductive proofs.-class SInductive a steps where- -- | Inductively prove a lemma, using strong induction, using the default config.+-- | A class of measures, used for inductive arguments.+class OrdSymbolic a => Measure a where+ zero :: a++-- | An integer as a measure+instance Measure SInteger where+ zero = 0++-- | A tuple of integers as a measure+instance Measure (SInteger, SInteger) where+ zero = (0, 0)++-- | A triple of integers as a measure+instance Measure (SInteger, SInteger, SInteger) where+ zero = (0, 0, 0)++-- | A quadruple of integers as a measure+instance Measure (SInteger, SInteger, SInteger, SInteger) where+ zero = (0, 0, 0, 0)++instance Measure (SInteger, SInteger, SInteger, SInteger, SInteger) where+ zero = (0, 0, 0, 0, 0)++-- | A class for doing generalized measure based strong inductive proofs.+class SInductive a measure steps where+ -- | Inductively prove a lemma, using measure based induction, using the default config. -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only -- partial correctness is guaranteed if non-terminating functions are involved.- sInduct :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof+ sInduct :: Proposition a => String -> a -> measure -> (Proof -> steps) -> KD Proof - -- | Inductively prove a theorem, using strong induction. Same as 'sInduct', but tagged as a theorem, using the default config.+ -- | Inductively prove a theorem, using measure based induction. Same as 'sInduct', but tagged as a theorem, using the default config. -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only -- partial correctness is guaranteed if non-terminating functions are involved.- sInductThm :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof+ sInductThm :: Proposition a => String -> a -> measure -> (Proof -> steps) -> KD Proof -- | Same as 'sInduct', but with the given solver configuration. -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only -- partial correctness is guaranteed if non-terminating functions are involved.- sInductWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof+ sInductWith :: Proposition a => SMTConfig -> String -> a -> measure -> (Proof -> steps) -> KD Proof -- | Same as 'sInductThm', but with the given solver configuration. -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only -- partial correctness is guaranteed if non-terminating functions are involved.- sInductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof+ sInductThmWith :: Proposition a => SMTConfig -> String -> a -> measure -> (Proof -> steps) -> KD Proof - sInduct nm p steps = getKDConfig >>= \cfg -> sInductWith cfg nm p steps- sInductThm nm p steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p steps- sInductWith cfg nm p steps = getKDConfig >>= \cfg' -> inductionEngine StrongInduction False (kdMergeCfg cfg cfg') nm p (sInductionStrategy p steps)- sInductThmWith cfg nm p steps = getKDConfig >>= \cfg' -> inductionEngine StrongInduction True (kdMergeCfg cfg cfg') nm p (sInductionStrategy p steps)+ sInduct nm p m steps = getKDConfig >>= \cfg -> sInductWith cfg nm p m steps+ sInductThm nm p m steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p m steps+ sInductWith cfg nm p m steps = getKDConfig >>= \cfg' -> inductionEngine GeneralInduction False (kdMergeCfg cfg cfg') nm p (sInductionStrategy p m steps)+ sInductThmWith cfg nm p m steps = getKDConfig >>= \cfg' -> inductionEngine GeneralInduction True (kdMergeCfg cfg cfg') nm p (sInductionStrategy p m steps) -- | Internal, shouldn't be needed outside the library {-# MINIMAL sInductionStrategy #-}- sInductionStrategy :: Proposition a => a -> (Proof -> steps) -> Symbolic InductionStrategy+ sInductionStrategy :: Proposition a => a -> measure -> (Proof -> steps) -> Symbolic InductionStrategy -- | Do an inductive proof, based on the given strategy inductionEngine :: Proposition a => InductionStyle -> Bool -> SMTConfig -> String -> a -> Symbolic InductionStrategy -> KD Proof@@ -455,13 +482,14 @@ qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out - let strong = case style of- RegularInduction -> ""- StrongInduction -> " (strong)"+ let qual = case style of+ RegularInduction -> ""+ GeneralInduction -> " (strong)" - message cfg $ "Inductive " ++ (if tagTheorem then "theorem" else "lemma") ++ strong ++ ": " ++ nm ++ "\n"+ message cfg $ "Inductive " ++ (if tagTheorem then "theorem" else "lemma") ++ qual ++ ": " ++ nm ++ "\n" strategy@InductionStrategy { inductionIntros+ , inductionMeasure , inductionBaseCase , inductionProofTree , inductiveStep@@ -471,11 +499,19 @@ query $ do + case inductionMeasure of+ Nothing -> queryDebug [nm ++ ": Induction" ++ qual ++ ", there is no custom measure to show non-negativeness."]+ Just ms -> do queryDebug [nm ++ ": Induction, proving measure is always non-negative:"]+ smtProofStep cfg kdSt "Step" 1+ (KDProofStep False nm [] ["Measure is non-negative"])+ (Just inductionIntros)+ ms+ (\d -> finishKD cfg "Q.E.D." d []) case inductionBaseCase of- Nothing -> queryDebug [nm ++ ": Induction" ++ strong ++ ", there is no proving base case:"]+ Nothing -> queryDebug [nm ++ ": Induction" ++ qual ++ ", there is no base case to prove."] Just bc -> do queryDebug [nm ++ ": Induction, proving base case:"] smtProofStep cfg kdSt "Step" 1- (KDProofStep False nm ["Base"])+ (KDProofStep False nm [] ["Base"]) (Just inductionIntros) bc (\d -> finishKD cfg "Q.E.D." d [])@@ -484,9 +520,10 @@ -- Induction strategy helper mkIndStrategy :: EqSymbolic a => Maybe SBool -> Maybe SBool -> (SBool, KDProofRaw a) -> SBool -> InductionStrategy-mkIndStrategy mbExtraConstraint mbBaseCase indSteps step =+mkIndStrategy mbMeasure mbBaseCase indSteps step = let CalcStrategy { calcIntros, calcProofTree } = mkCalcSteps indSteps- in InductionStrategy { inductionIntros = maybe id (.&&) mbExtraConstraint calcIntros+ in InductionStrategy { inductionIntros = calcIntros+ , inductionMeasure = mbMeasure , inductionBaseCase = mbBaseCase , inductionProofTree = calcProofTree , inductiveStep = step@@ -514,56 +551,32 @@ instance (KnownSymbol nn, EqSymbolic z) => Inductive (Forall nn Integer -> SBool) (SInteger -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (n, nn) <- mkVar (Proxy @nn)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0)))- (steps (internalAxiom "IH" (result (Forall n))) n)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0)))+ (steps (internalAxiom "IH" (n .>= zero .=> result (Forall n))) n) (indResult [nn ++ "+1"] (result (Forall (n+1)))) --- | Strong induction over 'SInteger'-instance (KnownSymbol nn, EqSymbolic z) => SInductive (Forall nn Integer -> SBool) (SInteger -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) -> 0 .<= n' .&& n' .< n .=> result (Forall n'))) n)- (indResult [nn] (result (Forall n)))- -- | Induction over 'SInteger', taking an extra argument instance (KnownSymbol nn, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> SBool) (SInteger -> SBV a -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (n, nn) <- mkVar (Proxy @nn) (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0) (Forall a)))- (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall n) (Forall a'))) n a)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0) (Forall a)))+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) -> n .>= zero .=> result (Forall n) (Forall a'))) n a) (indResult [nn ++ "+1", na] (result (Forall (n+1)) (Forall a))) --- | Strong induction over 'SInteger', taking an extra argument-instance (KnownSymbol nn, KnownSymbol na, SymVal a, EqSymbolic z) => SInductive (Forall nn Integer -> Forall na a -> SBool) (SInteger -> SBV a -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) (Forall a' :: Forall na a) -> 0 .<= n' .&& n' .< n .=> result (Forall n') (Forall a'))) n a)- (indResult [nn, na] (result (Forall n) (Forall a)))- -- | Induction over 'SInteger', taking two extra arguments instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) (SInteger -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (n, nn) <- mkVar (Proxy @nn) (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0) (Forall a) (Forall b)))- (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall n) (Forall a') (Forall b'))) n a b)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0) (Forall a) (Forall b)))+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b'))) n a b) (indResult [nn ++ "+1", na, nb] (result (Forall (n+1)) (Forall a) (Forall b))) --- | Strong induction over 'SInteger', taking two extra arguments-instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => SInductive (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) (SInteger -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> 0 .<= n' .&& n' .< n .=> result (Forall n') (Forall a') (Forall b'))) n a b)- (indResult [nn, na, nb] (result (Forall n) (Forall a) (Forall b)))- -- | Induction over 'SInteger', taking three extra arguments instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -571,21 +584,11 @@ (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0) (Forall a) (Forall b) (Forall c)))- (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall n) (Forall a') (Forall b') (Forall c'))) n a b c)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0) (Forall a) (Forall b) (Forall c)))+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c'))) n a b c) (indResult [nn ++ "+1", na, nb, nc] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c))) --- | Strong induction over 'SInteger', taking three extra arguments-instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => SInductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> 0 .<= n' .&& n' .< n .=> result (Forall n') (Forall a') (Forall b') (Forall c'))) n a b c)- (indResult [nn, na, nb, nc] (result (Forall n) (Forall a) (Forall b) (Forall c)))- -- | Induction over 'SInteger', taking four extra arguments instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -594,22 +597,11 @@ (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d)))- (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d'))) n a b c d)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d)))+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d'))) n a b c d) (indResult [nn ++ "+1", na, nb, nc, nd] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d))) --- | Strong induction over 'SInteger', taking four extra arguments-instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => SInductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> 0 .<= n' .&& n' .< n .=> result (Forall n') (Forall a') (Forall b') (Forall c') (Forall d'))) n a b c d)- (indResult [nn, na, nb, nc, nd] (result (Forall n) (Forall a) (Forall b) (Forall c) (Forall d)))- -- | Induction over 'SInteger', taking five extra arguments instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -619,23 +611,11 @@ (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd) (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy (Just (n .>= 0)) (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))- (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) n a b c d e)+ pure $ mkIndStrategy Nothing+ (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> n .>= zero .=> result (Forall n) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) n a b c d e) (indResult [nn ++ "+1", na, nb, nc, nd, ne] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e))) --- | Strong induction over 'SInteger', taking five extra arguments-instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => SInductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (n, nn) <- mkVar (Proxy @nn)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy (Just (n .>= 0)) Nothing- (steps (internalAxiom "IH" (\(Forall n' :: Forall nn Integer) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> 0 .<= n' .&& n' .< n .=> result (Forall n') (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) n a b c d e)- (indResult [nn, na, nb, nc, nd, ne] (result (Forall n) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))- -- Given a user name for the list, get a name for the element, in the most suggestive way possible -- xs -> x -- xss -> xs@@ -645,65 +625,36 @@ 's':_:_ -> init n _ -> n ++ "Elt" --- | Metric for induction over lists. Currently we simply require the list we're assuming correctness for is shorter in length, which--- is a measure that is guarenteed >= 0. Later on, we might want to generalize this to a user given measure.-lexLeq :: SymVal a => SList a -> SList a -> SBool-lexLeq xs ys = SL.length xs .< SL.length ys- -- | Induction over 'SList' instance (KnownSymbol nxs, SymVal x, EqSymbolic z) => Inductive (Forall nxs [x] -> SBool) (SBV x -> SList x -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (x, xs, nxxs) <- mkLVar (Proxy @nxs)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil))) (steps (internalAxiom "IH" (result (Forall xs))) x xs) (indResult [nxxs] (result (Forall (x SL..: xs)))) --- | Strong induction over 'SList'-instance (KnownSymbol nxs, SymVal x, EqSymbolic z) => SInductive (Forall nxs [x] -> SBool) (SList x -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) -> xs' `lexLeq` xs .=> result (Forall xs'))) xs)- (indResult [nxs] (result (Forall xs)))- -- | Induction over 'SList', taking an extra argument instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> SBool) (SBV x -> SList x -> SBV a -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (x, xs, nxxs) <- mkLVar (Proxy @nxs) (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil) (Forall a)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil) (Forall a))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs) (Forall a'))) x xs a) (indResult [nxxs, na] (result (Forall (x SL..: xs)) (Forall a))) --- | Strong induction over 'SList', taking an extra argument-instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, EqSymbolic z) => SInductive (Forall nxs [x] -> Forall na a -> SBool) (SList x -> SBV a -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) (Forall a' :: Forall na a) -> xs' `lexLeq` xs .=> result (Forall xs') (Forall a'))) xs a)- (indResult [nxs, na] (result (Forall xs) (Forall a)))- -- | Induction over 'SList', taking two extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (x, xs, nxxs) <- mkLVar (Proxy @nxs) (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil) (Forall a) (Forall b)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil) (Forall a) (Forall b))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs) (Forall a') (Forall b'))) x xs a b) (indResult [nxxs, na, nb] (result (Forall (x SL..: xs)) (Forall a) (Forall b))) --- | Strong induction over 'SList', taking two extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => SInductive (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) (SList x -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> xs' `lexLeq` xs .=> result (Forall xs') (Forall a') (Forall b'))) xs a b)- (indResult [nxs, na, nb] (result (Forall xs) (Forall a) (Forall b)))- -- | Induction over 'SList', taking three extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -711,21 +662,11 @@ (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs) (Forall a') (Forall b') (Forall c'))) x xs a b c) (indResult [nxxs, na, nb, nc] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c))) --- | Strong induction over 'SList', taking three extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => SInductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SList x -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> xs' `lexLeq` xs .=> result (Forall xs') (Forall a') (Forall b') (Forall c'))) xs a b c)- (indResult [nxs, na, nb, nc] (result (Forall xs) (Forall a) (Forall b) (Forall c)))- -- | Induction over 'SList', taking four extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -734,22 +675,11 @@ (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d'))) x xs a b c d) (indResult [nxxs, na, nb, nc, nd] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d))) --- | Strong induction over 'SList', taking four extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => SInductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SList x -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> xs' `lexLeq` xs .=> result (Forall xs') (Forall a') (Forall b') (Forall c') (Forall d'))) xs a b c d)- (indResult [nxs, na, nb, nc, nd] (result (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d)))- -- | Induction over 'SList', taking five extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -759,72 +689,32 @@ (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd) (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) x xs a b c d e) (indResult [nxxs, na, nb, nc, nd, ne] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e))) --- | Strong induction over 'SList', taking five extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => SInductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> xs' `lexLeq` xs .=> result (Forall xs') (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) xs a b c d e)- (indResult [nxs, na, nb, nc, nd, ne] (result (Forall xs) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))---- | Metric for induction over two lists. We use lexicographic ordering. -lexLeq2 :: (SymVal a, SymVal b) => (SList a, SList b) -> (SList a, SList b) -> SBool-lexLeq2 (xs', ys') (xs, ys) = lxs' .< lxs -- First one got smaller- .|| ( lxs' .== lxs -- OR, the first one did not grow- .&& lys' .< lys -- and the second went down- )- where lxs' = SL.length xs'- lys' = SL.length ys'- lxs = SL.length xs- lys = SL.length ys- -- | Induction over two 'SList', simultaneously instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> SBool) ((SBV x, SList x, SBV y, SList y) -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (x, xs, nxxs) <- mkLVar (Proxy @nxs) (y, ys, nyys) <- mkLVar (Proxy @nys)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) .&& result (Forall SL.nil, Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall SL.nil)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) .&& result (Forall SL.nil, Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall SL.nil))) (steps (internalAxiom "IH" (result (Forall xs, Forall ys))) (x, xs, y, ys)) (indResult [nxxs, nyys] (result (Forall (x SL..: xs), Forall (y SL..: ys)))) --- | Strong induction over two 'SList', simultaneously-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> SBool) ((SList x, SList y) -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys'))) (xs, ys))- (indResult [nxs, nys] (result (Forall xs, Forall ys)))- -- | Induction over two 'SList', simultaneously, taking an extra argument instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do (x, xs, nxxs) <- mkLVar (Proxy @nxs) (y, ys, nyys) <- mkLVar (Proxy @nys) (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) -> result (Forall xs, Forall ys) (Forall a'))) (x, xs, y, ys) a) (indResult [nxxs, nyys, na] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a))) --- | Strong induction over two 'SList', simultaneously, taking an extra argument-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) ((SList x, SList y) -> SBV a -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- (a, na) <- mkVar (Proxy @na)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) (Forall a' :: Forall na a) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys') (Forall a'))) (xs, ys) a)- (indResult [nxs, nys, na] (result (Forall xs, Forall ys) (Forall a)))- -- | Induction over two 'SList', simultaneously, taking two extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -832,21 +722,66 @@ (y, ys, nyys) <- mkLVar (Proxy @nys) (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> result (Forall xs, Forall ys) (Forall a') (Forall b'))) (x, xs, y, ys) a b) (indResult [nxxs, nyys, na, nb] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b))) --- | Strong induction over two 'SList', simultaneously, taking two extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) ((SList x, SList y) -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys') (Forall a') (Forall b'))) (xs, ys) a b)- (indResult [nxs, nys, na, nb] (result (Forall xs, Forall ys) (Forall a) (Forall b)))+-- | Generalized induction with one parameter+instance (KnownSymbol na, SymVal a, EqSymbolic z, Measure m) => SInductive (Forall na a -> SBool) (SBV a -> m) (SBV a -> (SBool, KDProofRaw z)) where+ sInductionStrategy result measure steps = do+ (a, na) <- mkVar (Proxy @na)+ pure $ mkIndStrategy (Just (measure a .>= zero))+ Nothing+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) -> measure a' .< measure a .=> result (Forall a'))) a)+ (indResult [na] (result (Forall a))) +-- | Generalized induction with two parameters+instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> SBool) (SBV a -> SBV b -> m) (SBV a -> SBV b -> (SBool, KDProofRaw z)) where+ sInductionStrategy result measure steps = do+ (a, na) <- mkVar (Proxy @na)+ (b, nb) <- mkVar (Proxy @nb)+ pure $ mkIndStrategy (Just (measure a b .>= zero))+ Nothing+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) -> measure a' b' .< measure a b .=> result (Forall a') (Forall b'))) a b)+ (indResult [na, nb] (result (Forall a) (Forall b)))++-- | Generalized induction with three parameters+instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> SBool) (SBV a -> SBV b -> SBV c -> m) (SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where+ sInductionStrategy result measure steps = do+ (a, na) <- mkVar (Proxy @na)+ (b, nb) <- mkVar (Proxy @nb)+ (c, nc) <- mkVar (Proxy @nc)+ pure $ mkIndStrategy (Just (measure a b c .>= zero))+ Nothing+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> measure a' b' c' .< measure a b c .=> result (Forall a') (Forall b') (Forall c'))) a b c)+ (indResult [na, nb, nc] (result (Forall a) (Forall b) (Forall c)))++-- | Generalized induction with four parameters+instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SBV a -> SBV b -> SBV c -> SBV d -> m) (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where+ sInductionStrategy result measure steps = do+ (a, na) <- mkVar (Proxy @na)+ (b, nb) <- mkVar (Proxy @nb)+ (c, nc) <- mkVar (Proxy @nc)+ (d, nd) <- mkVar (Proxy @nd)+ pure $ mkIndStrategy (Just (measure a b c d .>= zero))+ Nothing+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> measure a' b' c' d' .< measure a b c d .=> result (Forall a') (Forall b') (Forall c') (Forall d'))) a b c d)+ (indResult [na, nb, nc, nd] (result (Forall a) (Forall b) (Forall c) (Forall d)))++-- | Generalized induction with five parameters+instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> m) (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where+ sInductionStrategy result measure steps = do+ (a, na) <- mkVar (Proxy @na)+ (b, nb) <- mkVar (Proxy @nb)+ (c, nc) <- mkVar (Proxy @nc)+ (d, nd) <- mkVar (Proxy @nd)+ (e, ne) <- mkVar (Proxy @ne)+ pure $ mkIndStrategy (Just (measure a b c d e .>= zero))+ Nothing+ (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> measure a' b' c' d' e' .< measure a b c d e .=> result (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) a b c d e)+ (indResult [na, nb, nc, nd, ne] (result (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))+ -- | Induction over two 'SList', simultaneously, taking three extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -855,22 +790,11 @@ (a, na) <- mkVar (Proxy @na) (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c'))) (x, xs, y, ys) a b c) (indResult [nxxs, nyys, na, nb, nc] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c))) --- | Strong induction over two 'SList', simultaneously, taking three extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> SBool) ((SList x, SList y) -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys') (Forall a') (Forall b') (Forall c'))) (xs, ys) a b c)- (indResult [nxs, nys, na, nb, nc] (result (Forall xs, Forall ys) (Forall a) (Forall b) (Forall c)))- -- | Induction over two 'SList', simultaneously, taking four extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -880,23 +804,11 @@ (b, nb) <- mkVar (Proxy @nb) (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d'))) (x, xs, y, ys) a b c d) (indResult [nxxs, nyys, na, nb, nc, nd] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d))) --- | Strong induction over two 'SList', simultaneously, taking four extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) ((SList x, SList y) -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys') (Forall a') (Forall b') (Forall c') (Forall d'))) (xs, ys) a b c d)- (indResult [nxs, nys, na, nb, nc, nd] (result (Forall xs, Forall ys) (Forall a) (Forall b) (Forall c) (Forall d)))- -- | Induction over two 'SList', simultaneously, taking five extra arguments instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where inductionStrategy result steps = do@@ -907,24 +819,11 @@ (c, nc) <- mkVar (Proxy @nc) (d, nd) <- mkVar (Proxy @nd) (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy Nothing (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))+ pure $ mkIndStrategy Nothing+ (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e))) (steps (internalAxiom "IH" (\(Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> result (Forall xs, Forall ys) (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) (x, xs, y, ys) a b c d e) (indResult [nxxs, nyys, na, nb, nc, nd, ne] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e))) --- | Strong induction over two 'SList', simultaneously, taking five extra arguments-instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => SInductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) ((SList x, SList y) -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where- sInductionStrategy result steps = do- (xs, nxs) <- mkVar (Proxy @nxs)- (ys, nys) <- mkVar (Proxy @nys)- (a, na) <- mkVar (Proxy @na)- (b, nb) <- mkVar (Proxy @nb)- (c, nc) <- mkVar (Proxy @nc)- (d, nd) <- mkVar (Proxy @nd)- (e, ne) <- mkVar (Proxy @ne)- pure $ mkIndStrategy Nothing Nothing- (steps (internalAxiom "IH" (\(Forall xs' :: Forall nxs [x], Forall ys' :: Forall nys [y]) (Forall a' :: Forall na a) (Forall b' :: Forall nb b) (Forall c' :: Forall nc c) (Forall d' :: Forall nd d) (Forall e' :: Forall ne e) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs', Forall ys') (Forall a') (Forall b') (Forall c') (Forall d') (Forall e'))) (xs, ys) a b c d e)- (indResult [nxs, nys, na, nb, nc, nd, ne] (result (Forall xs, Forall ys) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))- -- | Instantiation for a universally quantified variable newtype Inst (nm :: Symbol) a = Inst (SBV a) @@ -937,20 +836,15 @@ -- | Apply a universal proof to some arguments, creating an instance of the proof itself. at :: Proof -> a -> Proof - -- | Apply a universal proof to some arguments, for a pair of arguments, creating an instance of the proof itself- at2 :: Proof -> a -> Proof- -- | Single parameter instance (KnownSymbol na, HasKind a, Typeable a) => Instantiatable (Inst na a) where at = instantiate $ \f (Inst a) -> f (Forall a :: Forall na a)- at2 = at -- Single parameter, so no chance of having a pair. Just use at. -- | Two parameters instance ( KnownSymbol na, HasKind a, Typeable a , KnownSymbol nb, HasKind b, Typeable b ) => Instantiatable (Inst na a, Inst nb b) where at = instantiate $ \f (Inst a, Inst b) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b)- at2 = instantiate $ \f (Inst a, Inst b) -> f (Forall a :: Forall na a, Forall b :: Forall nb b) -- | Three parameters instance ( KnownSymbol na, HasKind a, Typeable a@@ -958,7 +852,6 @@ , KnownSymbol nc, HasKind c, Typeable c ) => Instantiatable (Inst na a, Inst nb b, Inst nc c) where at = instantiate $ \f (Inst a, Inst b, Inst c) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c)- at2 = instantiate $ \f (Inst a, Inst b, Inst c) -> f (Forall a :: Forall na a, Forall b :: Forall nb b) (Forall c :: Forall nc c) -- | Four parameters instance ( KnownSymbol na, HasKind a, Typeable a@@ -967,7 +860,6 @@ , KnownSymbol nd, HasKind d, Typeable d ) => Instantiatable (Inst na a, Inst nb b, Inst nc c, Inst nd d) where at = instantiate $ \f (Inst a, Inst b, Inst c, Inst d) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d)- at2 = instantiate $ \f (Inst a, Inst b, Inst c, Inst d) -> f (Forall a :: Forall na a, Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d) -- | Five parameters instance ( KnownSymbol na, HasKind a, Typeable a@@ -977,7 +869,6 @@ , KnownSymbol ne, HasKind e, Typeable e ) => Instantiatable (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e) where at = instantiate $ \f (Inst a, Inst b, Inst c, Inst d, Inst e) -> f (Forall a :: Forall na a) (Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d) (Forall e :: Forall ne e)- at2 = instantiate $ \f (Inst a, Inst b, Inst c, Inst d, Inst e) -> f (Forall a :: Forall na a, Forall b :: Forall nb b) (Forall c :: Forall nc c) (Forall d :: Forall nd d) (Forall e :: Forall ne e) -- | Instantiate a proof over an arg. This uses dynamic typing, kind of hacky, but works sufficiently well. instantiate :: (Typeable f, Show arg) => (f -> arg -> SBool) -> Proof -> arg -> Proof@@ -1008,35 +899,52 @@ | True = '(' : s ++ ")" -- | Helpers for a step-data Helper = HelperProof Proof -- A previously proven theorem- | HelperAssum SBool -- A hypothesis+data Helper = HelperProof Proof -- A previously proven theorem+ | HelperAssum SBool -- A hypothesis+ | HelperString String -- Just a text, only used for diagnostics -- | Get all helpers used in a proof getAllHelpers :: KDProof -> [Helper]-getAllHelpers (ProofStep _ hs p) = hs ++ getAllHelpers p-getAllHelpers (ProofBranch (_ :: Bool) () ps) = concatMap (getAllHelpers . snd) ps-getAllHelpers (ProofEnd _ hs) = hs+getAllHelpers (ProofStep _ hs p) = hs ++ getAllHelpers p+getAllHelpers (ProofBranch (_ :: Bool) (_ :: [String]) ps) = concatMap (getAllHelpers . snd) ps+getAllHelpers (ProofEnd _ hs ) = hs -- | Get proofs from helpers getHelperProofs :: Helper -> [Proof] getHelperProofs (HelperProof p) = [p] getHelperProofs HelperAssum {} = []+getHelperProofs HelperString{} = [] -- | Get proofs from helpers getHelperAssumes :: Helper -> [SBool] getHelperAssumes HelperProof {} = [] getHelperAssumes (HelperAssum b) = [b]+getHelperAssumes HelperString {} = [] +-- | Get hint strings from helpers. If there's an explicit comment given, just pass that. If not, collect all the names+getHelperText :: [Helper] -> [String]+getHelperText hs = case [s | HelperString s <- hs] of+ [] -> concatMap collect hs+ ss -> ss+ where collect :: Helper -> [String]+ collect (HelperProof p) = [proofName p | isUserAxiom p] -- Don't put out internals (inductive hypotheses)+ collect HelperAssum {} = []+ collect (HelperString s) = [s]+ -- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're -- mixing proofs and booleans in one group of hints.-hyp :: SBool -> Helper-hyp = HelperAssum+hasm :: SBool -> Helper+hasm = HelperAssum -- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're -- mixing proofs and booleans in one group of hints. hprf :: Proof -> Helper hprf = HelperProof +-- | Smart constructor for adding a comment.+hcmnt :: String -> Helper+hcmnt = HelperString+ -- | A proof is a sequence of steps, supporting branching data KDProofGen a bh b = ProofStep a [Helper] (KDProofGen a bh b) -- ^ A single step | ProofBranch Bool bh [(SBool, KDProofGen a bh b)] -- ^ A branching step. Bool indicates if completeness check is needed@@ -1045,8 +953,8 @@ -- | A proof, as written by the user. No produced result, but helpers on branches type KDProofRaw a = KDProofGen a [Helper] () --- | A proof, as processed by KD. Producing a boolean result and each step is a boolean. Helpers on branches dispersed down, and thus empty-type KDProof = KDProofGen SBool () SBool+-- | A proof, as processed by KD. Producing a boolean result and each step is a boolean. Helpers on branches dispersed down, only strings are left for printing+type KDProof = KDProofGen SBool [String] SBool -- | Class capturing giving a proof-step helper type family Hinted a where@@ -1088,7 +996,7 @@ -- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability instance Hinted a ~ KDProofRaw a => HintsTo a String where- a `addHint` _ = ProofStep a [] qed+ a `addHint` s = ProofStep a [HelperString s] qed -- | Giving just one proof as a helper, starting from a proof instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) Proof where@@ -1128,8 +1036,12 @@ -- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) String where- a `addHint` _ = a+ a `addHint` s = a `addHint` HelperString s +-- | Giving a bunch of strings as hints. This doesn't actually do anything for the solver, it just helps with readability+instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) [String] where+ a `addHint` ss = a `addHint` map HelperString ss+ -- | Capture what a given step can chain-to. This is a closed-type family, i.e., -- we don't allow users to change this and write other chainable things. Probably it is not really necessary, -- but we'll cross that bridge if someone actually asks for it.@@ -1168,18 +1080,32 @@ qed :: KDProofRaw a qed = ProofEnd () [] --- | Mark a trivial proof. This is the same as 'qed', but reads better in proof scripts.+-- | Mark a trivial proof. This is essentially the same as 'qed', but reads better in proof scripts. class Trivial a where- -- | Mark a proof as trivial, i.e., the solver should be able to deduce it without any help.- trivial :: a+ -- | Mark a proof as trivial, i.e., the solver should be able to deduce it without any help.+ trivial :: a --- | Proofs with no arguments+-- | Trivial proofs with no arguments instance Trivial (KDProofRaw a) where- trivial = qed+ trivial = qed --- | Proofs with many arguments arguments+-- | Trivial proofs with many arguments arguments instance Trivial a => Trivial (b -> a) where- trivial = const trivial+ trivial = const trivial++-- | Mark a contradictory proof path. This is essentially the same as @sFalse := qed@, but reads better in proof scripts.+class Contradiction a where+ -- | Mark a proof as contradiction, i.e., the solver should be able to conclude it by reasoning that the current path is infeasible+ contradiction :: a++-- | Contradiction proofs with no arguments+instance Contradiction (KDProofRaw SBool) where+ contradiction = sFalse =: qed++-- | Contradiction proofs with many arguments+instance Contradiction a => Contradiction (b -> a) where+ contradiction = const contradiction+ -- | Start a calculational proof, with the given hypothesis. Use @[]@ as the -- first argument if the calculation holds unconditionally. The first argument is
Data/SBV/Tools/KD/Utils.hs view
@@ -58,8 +58,12 @@ deriving newtype (Applicative, Functor, Monad, MonadIO, MonadReader KDState, MonadFail) -- | The context in which we make a check-sat call-data KDProofContext = KDProofOneShot String [Proof] -- ^ A one shot proof, with helpers used (latter only used for cex generation)- | KDProofStep Bool String [String] -- ^ A step in a full proof, running in a query. Bool indicates if these are the assumptions for that step+data KDProofContext = KDProofOneShot String -- ^ A one shot proof, with string containing its name+ [Proof] -- ^ Helpers used (latter only used for cex generation)+ | KDProofStep Bool -- ^ A proof step. If Bool is true, then these are the assumptions for that step+ String -- ^ Name of original goal+ [String] -- ^ The helper "strings" given by the user+ [String] -- ^ The step name, i.e., the name of the branch in the proof tree -- | Run a KD proof, using the default configuration. runKD :: KD a -> IO a@@ -107,12 +111,15 @@ hFlush stdout return (length line) where nm = case ctx of- KDProofOneShot n _ -> n- KDProofStep _ _ ss -> intercalate "." ss+ KDProofOneShot n _ -> n+ KDProofStep _ _ hs ss -> intercalate "." ss ++ userHints hs tab = 2 * level line = replicate tab ' ' ++ what ++ ": " ++ nm++ userHints [] = ""+ userHints ss = " (" ++ intercalate ", " ss ++ ")" -- | Finish a proof. First argument is what we got from the call of 'startKD' above. finishKD :: SMTConfig -> String -> (Int, Maybe NominalDiffTime) -> [NominalDiffTime] -> IO ()
Data/SBV/Tools/KnuckleDragger.hs view
@@ -31,11 +31,11 @@ -- * Reasoning via regular induction , induct, inductWith, inductThm, inductThmWith - -- * Reasoning via strong induction+ -- * Reasoning via measure-based strong induction , sInduct, sInductWith, sInductThm, sInductThmWith -- * Creating instances of proofs- , at, at2, Inst(..)+ , at, Inst(..) -- * Faking proofs , sorry@@ -50,13 +50,13 @@ , (=:), (≡) -- * Supplying hints for a calculation step- , (??), (⁇), hprf, hyp+ , (??), (⁇), hprf, hasm, hcmnt -- * Case splits , split, split2, cases, (⟹), (==>) -- * Finishing up a calculational proof- , qed, trivial+ , qed, trivial, contradiction ) where import Data.SBV.Tools.KD.KnuckleDragger
Documentation/SBV/Examples/KnuckleDragger/Basics.hs view
@@ -15,6 +15,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE StandaloneDeriving #-} {-# OPTIONS_GHC -Wall -Werror #-}@@ -177,3 +178,35 @@ [] pure ()++-- * No termination checks++-- | It's important to realize that KnuckleDragger proofs in SBV neither check nor guarantee that the+-- functions we use are terminating. This is beyond the scope (and current capabilities) of what SBV can handle.+-- That is, the proof is up-to-termination, i.e., any proof implicitly assumes all functions defined (or axiomatized)+-- terminate for all possible inputs. If non-termination is possible, then the logic becomes inconsistent, i.e.,+-- we can prove arbitrary results.+--+-- Here is a simple example where we tell SBV that there is a function @f@ with non terminating behavior. Using this,+-- we can deduce @False@:+--+-- >>> noTerminationChecks+-- Axiom: bad+-- Lemma: noTerminationImpliesFalse+-- Step: 1 (bad @ (n |-> 0 :: SInteger)) Q.E.D.+-- Result: Q.E.D.+-- [Proven] noTerminationImpliesFalse+noTerminationChecks :: IO Proof+noTerminationChecks = runKD $ do++ let f :: SInteger -> SInteger+ f = uninterpret "f"++ badAxiom <- axiom "bad" (\(Forall @"n" n) -> f n .== 1 + f n)++ calc "noTerminationImpliesFalse"+ sFalse+ ([] |- f 0+ ?? badAxiom `at` Inst @"n" (0 :: SInteger)+ =: 1 + f 0+ =: qed)
+ Documentation/SBV/Examples/KnuckleDragger/BinarySearch.hs view
@@ -0,0 +1,271 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.KnuckleDragger.BinarySearch+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Proving binary search correct+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.KnuckleDragger.BinarySearch where++import Prelude hiding (null, length, (!!), drop, take, tail, elem, notElem)++import Data.SBV+import Data.SBV.Maybe+import Data.SBV.Tools.KnuckleDragger++-- * Binary search++-- | We will work with arrays containing integers, indexed by integers. Note that since SMTLib arrays+-- are indexed by their entire domain, we explicitly take a lower/upper bounds as parameters, which fits well+-- with the binary search algorithm.+type Arr = SArray Integer Integer++-- | Bounds: This is the focus into the array; both indexes are inclusive.+type Idx = (SInteger, SInteger)++-- | Encode binary search in a functional style.+bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer+bsearch array (low, high) = f array low high+ where f = smtFunction "bsearch" $ \arr lo hi x ->+ let mid = (lo + hi) `sEDiv` 2+ xmid = arr `readArray` mid+ in ite (lo .> hi)+ sNothing+ (ite (xmid .== x)+ (sJust mid)+ (ite (xmid .< x)+ (bsearch arr (mid+1, hi) x)+ (bsearch arr (lo, mid-1) x)))++-- * Correctness proof++-- | A predicate testing whether a given array is non-decreasing in the given range+nonDecreasing :: Arr -> Idx -> SBool+nonDecreasing arr (low, high) = quantifiedBool $+ \(Forall @"i" i) (Forall @"j" j) -> low .<= i .&& i .<= j .&& j .<= high .=> arr `readArray` i .<= arr `readArray` j++-- | A predicate testing whether an element is in the array within the given bounds+inArray :: Arr -> Idx -> SInteger -> SBool+inArray arr (low, high) elt = quantifiedBool $ \(Exists @"i" i) -> low .<= i .&& i .<= high .&& arr `readArray` i .== elt++-- | Correctness of binary search.+--+-- We have:+--+-- >>> correctness+-- Lemma: notInRange Q.E.D.+-- Lemma: inRangeHigh Q.E.D.+-- Lemma: inRangeLow Q.E.D.+-- Lemma: nonDecreasing Q.E.D.+-- Inductive lemma (strong): bsearchAbsent+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (unfold bsearch) Q.E.D.+-- Step: 2 (push isNothing down, simplify) Q.E.D.+-- Step: 3 (2 way case split)+-- Step: 3.1 Q.E.D.+-- Step: 3.2.1 Q.E.D.+-- Step: 3.2.2 Q.E.D.+-- Step: 3.2.3 Q.E.D.+-- Step: 3.2.4 Q.E.D.+-- Step: 3.2.5 (simplify) Q.E.D.+-- Step: 3.Completeness Q.E.D.+-- Result: Q.E.D.+-- Inductive lemma (strong): bsearchPresent+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (unfold bsearch) Q.E.D.+-- Step: 2 (simplify) Q.E.D.+-- Step: 3 (3 way case split)+-- Step: 3.1 Q.E.D.+-- Step: 3.2 Q.E.D.+-- Step: 3.3.1 Q.E.D.+-- Step: 3.3.2 (3 way case split)+-- Step: 3.3.2.1 Q.E.D.+-- Step: 3.3.2.2.1 Q.E.D.+-- Step: 3.3.2.2.2 Q.E.D.+-- Step: 3.3.2.3.1 Q.E.D.+-- Step: 3.3.2.3.2 Q.E.D.+-- Step: 3.3.2.Completeness Q.E.D.+-- Step: 3.Completeness Q.E.D.+-- Result: Q.E.D.+-- Lemma: bsearchCorrect+-- 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] bsearchCorrect+correctness :: IO Proof+correctness = runKDWith z3{kdOptions = (kdOptions z3) { ribbonLength = 50 }} $ do++ -- Helper: if a value is not in a range, then it isn't in any subrange of it:+ notInRange <- lemma "notInRange"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"m" md) (Forall @"x" x)+ -> sNot (inArray arr (lo, hi) x) .&& lo .<= md .&& md .<= hi+ .=> sNot (inArray arr (lo, md) x) .&& sNot (inArray arr (md, hi) x))+ []++ -- Helper: if a value is in a range of a nonDecreasing array, and if its value is larger than a given mid point, then it's in the higher part+ inRangeHigh <- lemma "inRangeHigh"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"m" md) (Forall @"x" x)+ -> nonDecreasing arr (lo, hi) .&& inArray arr (lo, hi) x .&& lo .<= md .&& md .<= hi .&& x .> arr `readArray` md+ .=> inArray arr (md+1, hi) x)+ []++ -- Helper: if a value is in a range of a nonDecreasing array, and if its value is lower than a given mid point, then it's in the lowr part+ inRangeLow <- lemma "inRangeLow"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"m" md) (Forall @"x" x)+ -> nonDecreasing arr (lo, hi) .&& inArray arr (lo, hi) x .&& lo .<= md .&& md .<= hi .&& x .< arr `readArray` md+ .=> inArray arr (lo, md-1) x)+ []++ -- Helper: if an array is nonDecreasing, then its parts are also non-decreasing when cut in any middle point+ nonDecreasingInRange <- lemma "nonDecreasing"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"m" md)+ -> nonDecreasing arr (lo, hi) .&& lo .<= md .&& md .<= hi+ .=> nonDecreasing arr (lo, md) .&& nonDecreasing arr (md, hi))+ []++ -- Prove the case when the target is not in the array+ bsearchAbsent <- sInduct "bsearchAbsent"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"x" x) ->+ nonDecreasing arr (lo, hi) .&& sNot (inArray arr (lo, hi) x) .=> isNothing (bsearch arr (lo, hi) x))+ (\(_arr :: Arr) (lo :: SInteger) (hi :: SInteger) (_x :: SInteger) -> abs (hi - lo + 1)) $+ \ih arr lo hi x ->+ [nonDecreasing arr (lo, hi), sNot (inArray arr (lo, hi) x)]+ |- isNothing (bsearch arr (lo, hi) x)+ ?? "unfold bsearch"+ =: let mid = (lo + hi) `sEDiv` 2+ xmid = arr `readArray` mid+ in isNothing (ite (lo .> hi)+ sNothing+ (ite (xmid .== x)+ (sJust mid)+ (ite (xmid .< x)+ (bsearch arr (mid+1, hi) x)+ (bsearch arr (lo, mid-1) x))))+ ?? "push isNothing down, simplify"+ =: ite (lo .> hi)+ sTrue+ (ite (xmid .== x)+ sFalse+ (ite (xmid .< x)+ (isNothing (bsearch arr (mid+1, hi) x))+ (isNothing (bsearch arr (lo, mid-1) x))))+ =: cases [ lo .> hi ==> trivial+ , lo .<= hi ==> ite (xmid .== x)+ sFalse+ (ite (xmid .< x)+ (isNothing (bsearch arr (mid+1, hi) x))+ (isNothing (bsearch arr (lo, mid-1) x)))+ =: let inst1 l h m = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"m" m, Inst @"x" x)+ inst2 l h m = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"m" m )+ inst3 l h = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"x" x)+ in ite (xmid .< x)+ (isNothing (bsearch arr (mid+1, hi) x))+ (isNothing (bsearch arr (lo, mid-1) x))+ ?? [ notInRange `at` inst1 lo hi (mid+1)+ , nonDecreasingInRange `at` inst2 lo hi (mid+1)+ , ih `at` inst3 (mid+1) hi+ ]+ =: ite (xmid .< x)+ sTrue+ (isNothing (bsearch arr (lo, mid-1) x))+ ?? [ notInRange `at` inst1 lo hi (mid-1)+ , nonDecreasingInRange `at` inst2 lo hi (mid-1)+ , ih `at` inst3 lo (mid-1)+ ]+ =: ite (xmid .< x) sTrue sTrue+ ?? "simplify"+ =: sTrue+ =: qed+ ]++ -- Prove the case when the target is in the array+ bsearchPresent <- sInductWith cvc5 "bsearchPresent"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"x" x) ->+ nonDecreasing arr (lo, hi) .&& inArray arr (lo, hi) x .=> arr `readArray` fromJust (bsearch arr (lo, hi) x) .== x)+ (\(_arr :: Arr) (lo :: SInteger) (hi :: SInteger) (_x :: SInteger) -> abs (hi - lo + 1)) $+ \ih arr lo hi x ->+ [nonDecreasing arr (lo, hi), inArray arr (lo, hi) x]+ |- x .== arr `readArray` fromJust (bsearch arr (lo, hi) x)+ ?? "unfold bsearch"+ =: let mid = (lo + hi) `sEDiv` 2+ xmid = arr `readArray` mid+ in x .== arr `readArray` fromJust (ite (lo .> hi)+ sNothing+ (ite (xmid .== x)+ (sJust mid)+ (ite (xmid .< x)+ (bsearch arr (mid+1, hi) x)+ (bsearch arr (lo, mid-1) x))))+ ?? "simplify"+ =: ite (lo .> hi)+ (x .== arr `readArray` fromJust sNothing)+ (ite (xmid .== x)+ (x .== arr `readArray` mid)+ (ite (xmid .< x)+ (x .== arr `readArray` fromJust (bsearch arr (mid+1, hi) x))+ (x .== arr `readArray` fromJust (bsearch arr (lo, mid-1) x))))+ =: cases [ lo .> hi ==> trivial+ , lo .== hi ==> trivial+ , lo .< hi ==> ite (xmid .== x)+ (x .== arr `readArray` mid)+ (ite (xmid .< x)+ (x .== arr `readArray` fromJust (bsearch arr (mid+1, hi) x))+ (x .== arr `readArray` fromJust (bsearch arr (lo, mid-1) x)))+ =: let inst1 l h m = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"m" m, Inst @"x" x)+ inst2 l h m = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"m" m )+ inst3 l h = (Inst @"arr" arr, Inst @"lo" l, Inst @"hi" h, Inst @"x" x)+ in cases [ xmid .== x ==> trivial+ , xmid .< x ==> x .== arr `readArray` fromJust (bsearch arr (mid+1, hi) x)+ ?? [ inRangeHigh `at` inst1 lo hi mid+ , nonDecreasingInRange `at` inst2 lo hi (mid+1)+ , ih `at` inst3 (mid+1) hi+ ]+ =: sTrue+ =: qed+ , xmid .> x ==> x .== arr `readArray` fromJust (bsearch arr (lo, mid-1) x)+ ?? [ inRangeLow `at` inst1 lo hi mid+ , nonDecreasingInRange `at` inst2 lo hi (mid-1)+ , ih `at` inst3 lo (mid-1)+ ]+ =: sTrue+ =: qed+ ]+ ]++ calc "bsearchCorrect"+ (\(Forall @"arr" arr) (Forall @"lo" lo) (Forall @"hi" hi) (Forall @"x" x) ->+ nonDecreasing arr (lo, hi) .=> let res = bsearch arr (lo, hi) x+ in ite (inArray arr (lo, hi) x)+ (arr `readArray` fromJust res .== x)+ (isNothing res)) $+ \arr lo hi x -> [nonDecreasing arr (lo, hi)]+ |- let res = bsearch arr (lo, hi) x+ in ite (inArray arr (lo, hi) x)+ (arr `readArray` fromJust res .== x)+ (isNothing res)+ =: cases [ inArray arr (lo, hi) x+ ==> arr `readArray` fromJust (bsearch arr (lo, hi) x) .== x+ ?? bsearchPresent `at` (Inst @"arr" arr, Inst @"lo" lo, Inst @"hi" hi, Inst @"x" x)+ =: sTrue+ =: qed+ , sNot (inArray arr (lo, hi) x)+ ==> isNothing (bsearch arr (lo, hi) x)+ ?? bsearchAbsent `at` (Inst @"arr" arr, Inst @"lo" lo, Inst @"hi" hi, Inst @"x" x)+ =: sTrue+ =: qed+ ]
Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs view
@@ -74,7 +74,7 @@ -- Case 0: n = 0 (mod 3) c0 <- calc "case_n_mod_3_eq_0" (\(Forall @"n" n) -> case0 n .=> p n) $- \n -> [case0 n] |- s n ?? case0 n+ \n -> [case0 n] |- s n =: let w = some "witness" $ \k -> n .== 3*k -- Grab the witness for the case in s (3*w) =: s (3*w)@@ -86,7 +86,7 @@ -- Case 1: n = 1 (mod 3) c1 <- calc "case_n_mod_3_eq_1" (\(Forall @"n" n) -> case1 n .=> p n) $- \n -> [case1 n] |- s n ?? case1 n+ \n -> [case1 n] |- s n =: let w = some "witness" $ \k -> n .== 3*k+1 -- Grab the witness for n being 1 modulo 3 in s (3*w+1) =: 2*(3*w+1)*(3*w+1) + (3*w+1) + 1@@ -99,7 +99,7 @@ -- Case 2: n = 2 (mod 3) c2 <- calc "case_n_mod_3_eq_2" (\(Forall @"n" n) -> case2 n .=> p n) $- \n -> [case2 n] |- s n ?? case2 n+ \n -> [case2 n] |- s n =: let w = some "witness" $ \k -> n .== 3*k+2 -- Grab the witness for n being 2 modulo 3 in s (3*w+2) =: 2*(3*w+2)*(3*w+2) + (3*w+2) + 1
Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs view
@@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -68,49 +69,49 @@ -- We have: -- -- >>> correctness--- Lemma: nonDecTail Q.E.D.+-- Lemma: nonDecTail Q.E.D. -- Inductive lemma: insertNonDecreasing--- 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.+-- Step: Base Q.E.D.+-- Step: 1 (unfold insert) Q.E.D.+-- Step: 2 (push nonDecreasing down) Q.E.D.+-- Step: 3 (unfold simplify) Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Result: Q.E.D. -- Inductive lemma: sortNonDecreasing--- Step: Base Q.E.D.--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Result: Q.E.D.--- Lemma: elemITE Q.E.D.+-- Step: Base Q.E.D.+-- Step: 1 (unfold insertionSort) Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D.+-- Lemma: elemITE Q.E.D. -- Inductive lemma: insertIsElem--- 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.+-- 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: removeAfterInsert--- 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.+-- Step: Base Q.E.D.+-- Step: 1 (expand insert) Q.E.D.+-- Step: 2 (push removeFirst down ite) Q.E.D.+-- Step: 3 (unfold removeFirst on 'then') Q.E.D.+-- Step: 4 (unfold removeFirst on 'else') Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 (simplify) Q.E.D.+-- Result: Q.E.D. -- Inductive lemma: sortIsPermutation--- 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: insertionSortIsCorrect Q.E.D.+-- 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: insertionSortIsCorrect Q.E.D. -- [Proven] insertionSortIsCorrect correctness :: IO Proof-correctness = runKDWith cvc5 $ do+correctness = runKDWith cvc5{kdOptions = (kdOptions cvc5) { ribbonLength = 45 }} $ do -------------------------------------------------------------------------------------------- -- Part I. Prove that the output of insertion sort is non-decreasing.@@ -127,18 +128,17 @@ |- nonDecreasing (insert e (x .: xs)) ?? "unfold insert" =: nonDecreasing (ite (e .<= x) (e .: x .: xs) (x .: insert e xs))- ?? "push nonDecreasing over the ite"+ ?? "push nonDecreasing down" =: ite (e .<= x) (nonDecreasing (e .: x .: xs)) (nonDecreasing (x .: insert e xs))- ?? "unfold nonDecreasing, simplify"+ ?? "unfold simplify" =: ite (e .<= x) (nonDecreasing (x .: xs)) (nonDecreasing (x .: insert e xs))- ?? nonDecreasing (x .: xs)+ ?? nonDecreasing (x .: xs) =: (e .> x .=> nonDecreasing (x .: insert e xs))- ?? [ hyp (nonDecreasing (x .: xs))- , hprf (nonDecrTail `at` (Inst @"x" x, Inst @"xs" (insert e xs)))- , hprf ih+ ?? [ nonDecrTail `at` (Inst @"x" x, Inst @"xs" (insert e xs))+ , ih ] =: sTrue =: qed@@ -149,9 +149,9 @@ \ih x xs -> [] |- nonDecreasing (insertionSort (x .: xs)) ?? "unfold insertionSort" =: nonDecreasing (insert x (insertionSort xs))- ?? [ hprf (insertNonDecreasing `at` (Inst @"xs" (insertionSort xs), Inst @"e" x))- , hprf ih- ]+ ?? [ insertNonDecreasing `at` (Inst @"xs" (insertionSort xs), Inst @"e" x)+ , ih+ ] =: sTrue =: qed @@ -183,11 +183,11 @@ \ih x xs e -> [] |- removeFirst e (insert e (x .: xs)) ?? "expand insert" =: removeFirst e (ite (e .<= x) (e .: x .: xs) (x .: insert e xs))- ?? "push removeFirst down the if-then-else"+ ?? "push removeFirst down ite" =: ite (e .<= x) (removeFirst e (e .: x .: xs)) (removeFirst e (x .: insert e xs))- ?? "unfold removeFirst, then branch"+ ?? "unfold removeFirst on 'then'" =: ite (e .<= x) (x .: xs) (removeFirst e (x .: insert e xs))- ?? "unfold removeFirst, else branch. Note that e .== x is False, due to the pre-condition"+ ?? "unfold removeFirst on 'else'" =: ite (e .<= x) (x .: xs) (x .: removeFirst e (insert e xs)) ?? ih =: ite (e .<= x) (x .: xs) (x .: xs)
Documentation/SBV/Examples/KnuckleDragger/Kleene.hs view
@@ -76,10 +76,10 @@ -- Lemma: par_monotone Q.E.D. -- Lemma: seq_monotone Q.E.D. -- Lemma: star_star_1--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.--- Step: 3 Q.E.D.--- Step: 4 Q.E.D.+-- Step: 1 (unfold) Q.E.D.+-- Step: 2 (factor out x * star x) Q.E.D.+-- Step: 3 (par_idem) Q.E.D.+-- Step: 4 (unfold) Q.E.D. -- Result: Q.E.D. -- Lemma: subset_eq Q.E.D. -- Lemma: star_star_2_2 Q.E.D.@@ -123,7 +123,8 @@ star_star_1 <- calc "star_star_1" (\(Forall @"x" (x :: SKleene)) -> star x * star x .== star x) $ \x -> [] |- star x * star x ?? unfold- =: (1 + x * star x) * (1 + x * star x) ?? kleene+ =: (1 + x * star x) * (1 + x * star x)+ ?? hcmnt "factor out x * star x" : map hprf kleene =: (1 + 1) + (x * star x + x * star x) ?? par_idem =: 1 + x * star x ?? unfold =: star x
Documentation/SBV/Examples/KnuckleDragger/Lists.hs view
@@ -265,7 +265,7 @@ (\(Forall @"xs" xs) -> (2 :: SInteger) `notElem` xs .=> (filter (.> 2) xs .== filter (.>= 2) xs)) $ \ih x xs -> let h = (2 :: SInteger) `notElem` (x .: xs) in [h] |- filter (.> 2) (x .: xs)- =: ite (x .> 2) (x .: filter (.> 2) xs) (filter (.> 2) xs) ?? [hyp h, hprf ih]+ =: ite (x .> 2) (x .: filter (.> 2) xs) (filter (.> 2) xs) ?? ih =: ite (x .> 2) (x .: filter (.>= 2) xs) (filter (.>= 2) xs) =: qed @@ -306,8 +306,8 @@ induct "mapEquiv" (\(Forall @"xs" xs) -> f'eq'g .=> map f xs .== map g xs) $ \ih x xs -> [f'eq'g] |- map f (x .: xs) .== map g (x .: xs)- =: f x .: map f xs .== g x .: map g xs ?? f'eq'g- =: f x .: map f xs .== f x .: map g xs ?? [hyp f'eq'g, hprf ih]+ =: f x .: map f xs .== 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@@ -495,8 +495,8 @@ induct "foldrFusion" (\(Forall @"xs" xs) -> h1 .&& h2 .=> f (foldr g a xs) .== foldr h b xs) $ \ih x xs -> [h1, h2] |- f (foldr g a (x .: xs))- =: f (g x (foldr g a xs)) ?? h2- =: h x (f (foldr g a xs)) ?? [hyp h1, hyp h2, hprf ih]+ =: f (g x (foldr g a xs))+ =: h x (f (foldr g a xs)) ?? ih =: h x (foldr h b xs) =: foldr h b (x .: xs) =: qed@@ -661,7 +661,7 @@ =: foldl (@) ((y @ z) @ x) xs ?? assoc =: foldl (@) (y @ (z @ x)) xs- ?? [hyp assoc, hprf (ih `at` (Inst @"y" y, Inst @"z" (z @ x)))]+ ?? ih `at` (Inst @"y" y, Inst @"z" (z @ x)) =: y @ foldl (@) (z @ x) xs =: y @ foldl (@) z (x .: xs) =: qed@@ -669,8 +669,8 @@ induct "foldrFoldlDuality" (\(Forall @"xs" xs) -> assoc .&& lunit .&& runit .=> foldr (@) e xs .== foldl (@) e xs) $ \ih x xs -> [assoc, lunit, runit] |- foldr (@) e (x .: xs)- =: x @ foldr (@) e xs ?? [hyp assoc, hyp lunit, hyp runit, hprf ih]- =: x @ foldl (@) e xs ?? [hyp assoc, hprf helper]+ =: x @ foldr (@) e xs ?? ih+ =: x @ foldl (@) e xs ?? helper =: foldl (@) (x @ e) xs ?? runit =: foldl (@) x xs ?? lunit =: foldl (@) (e @ x) xs@@ -739,7 +739,7 @@ -- Using z to avoid confusion with the variable x already present, following Bird. -- z3 can figure out the proper instantiation of ih so the at call is unnecessary, but being explicit is helpful. \ih z xs x y -> [assoc] |- x <+> foldl (<*>) y (z .: xs)- =: x <+> foldl (<*>) (y <*> z) xs ?? [hyp assoc, hprf (ih `at` (Inst @"x" x, Inst @"y" (y <*> z)))]+ =: 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)@@ -749,9 +749,9 @@ induct "foldrFoldl" (\(Forall @"xs" xs) -> assoc .&& unit .=> foldr (<+>) e xs .== foldl (<*>) e xs) $ \ih x xs -> [assoc, unit] |- foldr (<+>) e (x .: xs)- =: x <+> foldr (<+>) e xs ?? [hyp assoc, hyp unit, hprf ih]- =: x <+> foldl (<*>) e xs ?? [hyp assoc, hprf helper]- =: foldl (<*>) (x <+> e) xs ?? unit+ =: x <+> foldr (<+>) e xs ?? ih+ =: x <+> foldl (<*>) e xs ?? helper+ =: foldl (<*>) (x <+> e) xs =: foldl (<*>) (e <*> x) xs =: foldl (<*>) e (x .: xs) =: qed@@ -837,8 +837,8 @@ helper <- induct "foldBase" (\(Forall @"xs" xs) (Forall @"y" y) -> lUnit .&& assoc .=> foldr f y xs .== foldr f a xs `f` y) $ \ih x xs y -> [lUnit, assoc] |- foldr f y (x .: xs)- =: x `f` foldr f y xs ?? [hyp lUnit, hyp assoc, hprf ih]- =: x `f` (foldr f a xs `f` y) ?? assoc+ =: x `f` foldr f y xs ?? 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@@ -848,9 +848,12 @@ induct "bookKeeping" (\(Forall @"xss" xss) -> assoc .&& rUnit .&& lUnit .=> foldr f a (concat xss) .== foldr f a (mapFoldr a xss)) $ \ih xs xss -> [assoc, rUnit, lUnit] |- foldr f a (concat (xs .: xss))- =: foldr f a (xs ++ concat xss) ?? foa- =: foldr f (foldr f a (concat xss)) xs ?? [hyp assoc, hyp rUnit, hyp lUnit, hprf ih]- =: foldr f (foldr f a (mapFoldr a xss)) xs ?? [hyp lUnit, hyp assoc, hprf (helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (mapFoldr a xss))))]+ =: foldr f a (xs ++ concat xss)+ ?? foa+ =: foldr f (foldr f a (concat xss)) xs+ ?? ih+ =: foldr f (foldr f a (mapFoldr a xss)) xs+ ?? helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (mapFoldr a xss))) =: foldr f a xs `f` foldr f a (mapFoldr a xss) =: foldr f a (foldr f a xs .: mapFoldr a xss) =: foldr f a (mapFoldr a (xs .: xss))@@ -1105,10 +1108,10 @@ h2 <- induct "take_map.n > 0" (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> take n (map f xs) .== map f (take n xs)) $ \ih x xs n -> [n .> 0] |- take n (map f (x .: xs))- =: take n (f x .: map f xs) ?? n .> 0+ =: 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) ?? [hyp (n .> 0), hprf tc]+ =: map f (x .: take (n - 1) xs) ?? tc =: map f (take n (x .: xs)) =: qed @@ -1161,11 +1164,11 @@ (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> drop n (map f xs) .== map f (drop n xs)) $ \ih x xs n -> [n .> 0] |- drop n (map f (x .: xs)) =: drop n (f x .: map f xs)- ?? [hyp (n .> 0), hprf (dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs)))]+ ?? dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs)) =: drop (n - 1) (map f xs)- ?? [hyp (n .> 0), hprf (ih `at` Inst @"n" (n-1))]+ ?? ih `at` Inst @"n" (n-1) =: map f (drop (n - 1) xs)- ?? [hyp (n .> 0), hprf (dcA `at` (Inst @"n" n, Inst @"x" x, Inst @"xs" xs))]+ ?? dcA `at` (Inst @"n" n, Inst @"x" x, Inst @"xs" xs) =: map f (drop n (x .: xs)) =: qed @@ -1229,7 +1232,7 @@ -- -- >>> take_append -- Lemma: take_append--- Step: 1 Q.E.D.+-- Step: 1 (case split on xs) Q.E.D. -- Result: Q.E.D. -- [Proven] take_append take_append :: IO Proof@@ -1271,6 +1274,7 @@ -- Step: 3 Q.E.D. -- Result: Q.E.D. -- Inductive lemma (strong): sumHalves+-- 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)@@ -1280,7 +1284,7 @@ -- Step: 1.2.2.3 Q.E.D. -- Step: 1.2.2.4 Q.E.D. -- Step: 1.2.2.5 Q.E.D.--- Step: 1.2.2.6 Q.E.D.+-- Step: 1.2.2.6 (simplify) Q.E.D. -- Result: Q.E.D. -- [Proven] sumHalves sumHalves :: IO Proof@@ -1306,7 +1310,8 @@ -- Use strong induction to prove the theorem. CVC5 solves this with ease, but z3 struggles. sInductWith cvc5 "sumHalves"- (\(Forall @"xs" xs) -> halvingSum xs .== sum xs) $+ (\(Forall @"xs" xs) -> halvingSum xs .== sum xs)+ (length @Integer) $ \ih xs -> [] |- halvingSum xs =: split xs qed (\a as -> split as qed@@ -1345,7 +1350,7 @@ =: map fst (tuple (x, y) .: zip xs ys) =: fst (tuple (x, y)) .: map fst (zip xs ys) =: x .: map fst (zip xs ys)- ?? [hprf ih, hyp (length xs .== length ys)]+ ?? ih =: x .: xs =: qed @@ -1369,7 +1374,7 @@ =: map snd (tuple (x, y) .: zip xs ys) =: snd (tuple (x, y)) .: map snd (zip xs ys) =: y .: map snd (zip xs ys)- ?? [hprf ih, hyp (length xs .== length ys)]+ ?? ih =: y .: ys =: qed
Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs view
@@ -10,6 +10,7 @@ ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -66,113 +67,115 @@ -- We have: -- -- >>> correctness--- Lemma: nonDecrInsert Q.E.D.+-- Lemma: nonDecrInsert Q.E.D. -- Inductive lemma (strong): mergeKeepsSort+-- 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.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3 Q.E.D.+-- Step: 1.4.1 (unfold merge) Q.E.D. -- Step: 1.4.2 (2 way case split)--- Step: 1.4.2.1.1 Q.E.D.--- Step: 1.4.2.1.2 Q.E.D.--- Step: 1.4.2.2.1 Q.E.D.--- Step: 1.4.2.2.2 Q.E.D.--- Step: 1.4.2.Completeness Q.E.D.--- Result: Q.E.D.+-- Step: 1.4.2.1.1 (case split) Q.E.D.+-- Step: 1.4.2.1.2 Q.E.D.+-- Step: 1.4.2.2.1 (case split) Q.E.D.+-- Step: 1.4.2.2.2 Q.E.D.+-- Step: 1.4.2.Completeness Q.E.D.+-- Result: Q.E.D. -- Inductive lemma (strong): sortNonDecreasing+-- 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.--- Step: 1.2.4 Q.E.D.--- Result: Q.E.D.+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 (unfold) Q.E.D.+-- Step: 1.2.2 (push nonDecreasing down) Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Result: Q.E.D. -- Inductive lemma (strong): mergeCount+-- 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.--- Result: Q.E.D.+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3 Q.E.D.+-- Step: 1.4.1 (unfold merge) Q.E.D.+-- Step: 1.4.2 (push count inside) Q.E.D.+-- Step: 1.4.3 (unfold count, twice) Q.E.D.+-- Step: 1.4.4 Q.E.D.+-- Step: 1.4.5 Q.E.D.+-- Step: 1.4.6 (unfold count in reverse, twice) Q.E.D.+-- Step: 1.4.7 (simplify) Q.E.D.+-- Result: Q.E.D. -- Inductive lemma: countAppend--- 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: take_drop Q.E.D.+-- 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.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Result: Q.E.D. -- Inductive lemma (strong): sortIsPermutation+-- 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.--- Step: 1.2.4 Q.E.D.--- Step: 1.2.5 Q.E.D.--- Step: 1.2.6 Q.E.D.--- Result: Q.E.D.--- Lemma: mergeSortIsCorrect Q.E.D.+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 (unfold mergeSort) Q.E.D.+-- Step: 1.2.2 (push count down, simplify, rearrange) Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.2.5 Q.E.D.+-- Step: 1.2.6 Q.E.D.+-- Result: Q.E.D.+-- Lemma: mergeSortIsCorrect Q.E.D. -- [Proven] mergeSortIsCorrect correctness :: IO Proof-correctness = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 50}} $ do+correctness = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 60}} $ do -------------------------------------------------------------------------------------------- -- Part I. Prove that the output of merge sort is non-decreasing. -------------------------------------------------------------------------------------------- - nonDecrIns <- lemma "nonDecrInsert"- (\(Forall @"x" x) (Forall @"ys" ys) -> nonDecreasing ys .&& sNot (null ys) .&& x .<= head ys- .=> nonDecreasing (x .: ys))- []+ nonDecrIns <- lemma "nonDecrInsert"+ (\(Forall @"x" x) (Forall @"ys" ys) -> nonDecreasing ys .&& sNot (null ys) .&& x .<= head ys+ .=> nonDecreasing (x .: ys))+ [] mergeKeepsSort <- sInductWith cvc5 "mergeKeepsSort"- (\(Forall @"xs" xs, Forall @"ys" ys) -> nonDecreasing xs .&& nonDecreasing ys .=> nonDecreasing (merge xs ys)) $- \ih (xs, ys) -> [nonDecreasing xs, nonDecreasing ys]- |- split2 (xs, ys)- trivial -- when both xs and ys are empty. Trivial.- trivial -- when xs is empty, but ys isn't. Trivial.- trivial -- when ys is empty, but xs isn't. Trivial.- (\(a, as) (b, bs) ->- nonDecreasing (merge (a .: as) (b .: bs))- ?? "unfold merge"- =: nonDecreasing (ite (a .<= b)- (a .: merge as (b .: bs))- (b .: merge (a .: as) bs))- ?? "case split"- =: cases [ a .<= b ==> nonDecreasing (a .: merge as (b .: bs))- ?? [ hprf $ ih `at2` (Inst @"xs" as, Inst @"ys" (b .: bs))- , hprf $ nonDecrIns `at` (Inst @"x" a, Inst @"ys" (merge as (b .: bs)))- , hyp $ nonDecreasing (a .: as)- , hyp $ nonDecreasing (b .: bs)- ]- =: sTrue- =: qed- , a .> b ==> nonDecreasing (b .: merge (a .: as) bs)- ?? [ hprf $ ih `at2` (Inst @"xs" (a .: as), Inst @"ys" bs)- , hprf $ nonDecrIns `at` (Inst @"x" b, Inst @"ys" (merge (a .: as) bs))- , hyp $ nonDecreasing (a .: as)- , hyp $ nonDecreasing (b .: bs)- ]- =: sTrue- =: qed- ])+ (\(Forall @"xs" xs) (Forall @"ys" ys) -> nonDecreasing xs .&& nonDecreasing ys .=> nonDecreasing (merge xs ys))+ (\(xs :: SList Integer) (ys :: SList Integer) -> (length xs, length ys)) $+ \ih xs ys -> [nonDecreasing xs, nonDecreasing ys]+ |- split2 (xs, ys)+ trivial -- when both xs and ys are empty. Trivial.+ trivial -- when xs is empty, but ys isn't. Trivial.+ trivial -- when ys is empty, but xs isn't. Trivial.+ (\(a, as) (b, bs) ->+ nonDecreasing (merge (a .: as) (b .: bs))+ ?? "unfold merge"+ =: nonDecreasing (ite (a .<= b)+ (a .: merge as (b .: bs))+ (b .: merge (a .: as) bs))+ ?? "case split"+ =: cases [ a .<= b ==> nonDecreasing (a .: merge as (b .: bs))+ ?? [ ih `at` (Inst @"xs" as, Inst @"ys" (b .: bs))+ , nonDecrIns `at` (Inst @"x" a, Inst @"ys" (merge as (b .: bs)))+ ]+ =: sTrue+ =: qed+ , a .> b ==> nonDecreasing (b .: merge (a .: as) bs)+ ?? [ ih `at` (Inst @"xs" (a .: as), Inst @"ys" bs)+ , nonDecrIns `at` (Inst @"x" b, Inst @"ys" (merge (a .: as) bs))+ ]+ =: sTrue+ =: qed+ ]) sortNonDecreasing <- sInduct "sortNonDecreasing"- (\(Forall @"xs" xs) -> nonDecreasing (mergeSort xs)) $+ (\(Forall @"xs" xs) -> nonDecreasing (mergeSort xs))+ (length @Integer) $ \ih xs -> [] |- split xs qed (\e es -> nonDecreasing (mergeSort (e .: es))@@ -191,7 +194,7 @@ (nonDecreasing (merge (mergeSort h1) (mergeSort h2))) ?? [ ih `at` Inst @"xs" h1 , ih `at` Inst @"xs" h2- , mergeKeepsSort `at2` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2))+ , mergeKeepsSort `at` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2)) ] =: sTrue =: qed)@@ -201,8 +204,9 @@ -------------------------------------------------------------------------------------------- mergeCount <- sInduct "mergeCount"- (\(Forall @"xs" xs, Forall @"ys" ys) (Forall @"e" e) -> count e (merge xs ys) .== count e xs + count e ys) $- \ih (as, bs) e -> [] |-+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"e" e) -> count e (merge xs ys) .== count e xs + count e ys)+ (\(xs :: SList Integer) (ys :: SList Integer) (_e :: SInteger) -> (length xs, length ys)) $+ \ih as bs e -> [] |- split2 (as, bs) trivial trivial@@ -220,11 +224,11 @@ =: ite (x .<= y) (let r = count e (merge xs (y .: ys)) in ite (e .== x) (1+r) r) (let r = count e (merge (x .: xs) ys) in ite (e .== y) (1+r) r)- ?? ih `at2` (Inst @"xs" xs, Inst @"ys" (y .: ys), Inst @"e" e)+ ?? ih `at` (Inst @"xs" xs, Inst @"ys" (y .: ys), Inst @"e" e) =: ite (x .<= y) (let r = count e xs + count e (y .: ys) in ite (e .== x) (1+r) r) (let r = count e (merge (x .: xs) ys) in ite (e .== y) (1+r) r)- ?? ih `at2` (Inst @"xs" (x .: xs), Inst @"ys" ys, Inst @"e" e)+ ?? ih `at` (Inst @"xs" (x .: xs), Inst @"ys" ys, Inst @"e" e) =: ite (x .<= y) (let r = count e xs + count e (y .: ys) in ite (e .== x) (1+r) r) (let r = count e (x .: xs) + count e ys in ite (e .== y) (1+r) r)@@ -265,8 +269,9 @@ =: qed sortIsPermutation <-- sInduct "sortIsPermutation"- (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .== count e (mergeSort xs)) $+ sInductWith cvc5 "sortIsPermutation"+ (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .== count e (mergeSort xs))+ (\(xs :: SList Integer) (_e :: SInteger) -> length xs) $ \ih as e -> [] |- split as qed (\x xs -> count e (mergeSort (x .: xs))@@ -280,12 +285,14 @@ in ite (null xs) (count e (singleton x)) (count e (merge (mergeSort h1) (mergeSort h2)))- ?? mergeCount `at2` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2), Inst @"e" e)+ ?? mergeCount `at` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2), Inst @"e" e) =: ite (null xs) (count e (singleton x)) (count e (mergeSort h1) + count e (mergeSort h2)) ?? ih `at` (Inst @"xs" h1, Inst @"e" e)- =: ite (null xs) (count e (singleton x)) (count e h1 + count e (mergeSort h2))+ =: ite (null xs)+ (count e (singleton x))+ (count e h1 + count e (mergeSort h2)) ?? ih `at` (Inst @"xs" h2, Inst @"e" e) =: ite (null xs) (count e (singleton x))
Documentation/SBV/Examples/KnuckleDragger/Numeric.hs view
@@ -9,9 +9,11 @@ -- Example use of inductive KnuckleDragger proofs, over integers. ----------------------------------------------------------------------------- -{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeAbstractions #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -22,6 +24,13 @@ import Data.SBV import Data.SBV.Tools.KnuckleDragger +#ifndef HADDOCK+-- $setup+-- >>> -- For doctest purposes only:+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Exception+#endif+ -- | Prove that sum of constants @c@ from @0@ to @n@ is @n*c@. -- -- We have:@@ -49,8 +58,8 @@ induct "sumConst_correct" (\(Forall @"n" n) -> n .>= 0 .=> sum n .== spec n) $- \ih n -> [n .>= 0] |- sum (n+1) ?? n .>= 0- =: c + sum n ?? [hprf ih, hyp (n .>= 0)]+ \ih n -> [n .>= 0] |- sum (n+1)+ =: c + sum n ?? ih =: c + spec n =: c + c*n =: c*(n+1)@@ -80,8 +89,8 @@ induct "sum_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $- \ih n -> [n .>= 0] |- sum (n+1) ?? n .>= 0- =: n+1 + sum n ?? [hprf ih, hyp (n .>= 0)]+ \ih n -> [n .>= 0] |- sum (n+1)+ =: n+1 + sum n ?? ih =: n+1 + spec n =: spec (n+1) =: qed@@ -109,8 +118,8 @@ induct "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) $- \ih n -> [n .>= 0] |- sumSquare (n+1) ?? n .>= 0- =: (n+1)*(n+1) + sumSquare n ?? [hprf ih, hyp (n .>= 0)]+ \ih n -> [n .>= 0] |- sumSquare (n+1)+ =: (n+1)*(n+1) + sumSquare n ?? ih =: (n+1)*(n+1) + spec n =: spec (n+1) =: qed@@ -151,15 +160,36 @@ \ih n -> [n .>= 0] |- emf (n+1) =: 7 `sDivides` (11 `pow` (n+1) - 4 `pow` (n+1))- ?? [hyp (n .>= 0), hprf (powN `at` (Inst @"x" (11 :: SInteger), Inst @"n" n))]+ ?? powN `at` (Inst @"x" (11 :: SInteger), Inst @"n" n) =: 7 `sDivides` (11 * 11 `pow` n - 4 `pow` (n+1))- ?? [hyp (n .>= 0), hprf (powN `at` (Inst @"x" ( 4 :: SInteger), Inst @"n" n))]+ ?? powN `at` (Inst @"x" ( 4 :: SInteger), Inst @"n" n) =: 7 `sDivides` (11 * 11 `pow` n - 4 * 4 `pow` n) =: 7 `sDivides` (7 * 11 `pow` n + 4 * 11 `pow` n - 4 * 4 `pow` n) =: 7 `sDivides` (7 * 11 `pow` n + 4 * (11 `pow` n - 4 `pow` n))- ?? [hyp (n .>= 0), hprf ih]+ ?? ih =: let x = some "x" (\v -> 7*v .== 11 `pow` n - 4 `pow` n) -- Apply the IH and grab the witness for it in 7 `sDivides` (7 * 11 `pow` n + 4 * 7 * x) =: 7 `sDivides` (7 * (11 `pow` n + 4 * x)) =: sTrue =: qed++-- | A negative example: The regular inductive proof on integers (i.e., proving at @0@, assuming at @n@ and proving at+-- @n+1@ will not allow you to conclude things when @n < 0@. The following example demonstrates this with the most+-- obvious example:+--+-- >>> badNonNegative `catch` (\(_ :: SomeException) -> pure ())+-- Inductive lemma: badNonNegative+-- Step: Base Q.E.D.+-- Step: 1+-- *** Failed to prove badNonNegative.1.+-- Falsifiable. Counter-example:+-- n = -2 :: Integer+badNonNegative :: IO ()+badNonNegative = runKD $ do+ _ <- induct "badNonNegative"+ (\(Forall @"n" (n :: SInteger)) -> n .>= 0) $+ \ih n -> [] |- n + 1 .>= (0 :: SInteger)+ ?? ih+ =: sTrue+ =: qed+ pure ()
Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs view
@@ -155,20 +155,20 @@ -- Axiom: a ⏐ (b ⏐ ﬧb) == ﬧa -- Axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a) -- Lemma: a | b = b | a--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.+-- Step: 1 (ﬧﬧa == a) Q.E.D.+-- Step: 2 (ﬧﬧa == a) Q.E.D. -- Step: 3 Q.E.D.--- Step: 4 Q.E.D.+-- Step: 4 (ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)) Q.E.D. -- Step: 5 Q.E.D.--- Step: 6 Q.E.D.--- Step: 7 Q.E.D.+-- Step: 6 (ﬧﬧa == a) Q.E.D.+-- Step: 7 (ﬧﬧa == a) Q.E.D. -- Result: Q.E.D. -- Lemma: a | a′ = b | b′--- Step: 1 Q.E.D.--- Step: 2 Q.E.D.+-- Step: 1 (ﬧﬧa == a) Q.E.D.+-- Step: 2 (a ⏐ (b ⏐ ﬧb) == ﬧa) Q.E.D. -- Step: 3 Q.E.D.--- Step: 4 Q.E.D.--- Step: 5 Q.E.D.+-- Step: 4 (a ⏐ (b ⏐ ﬧb) == ﬧa) Q.E.D.+-- Step: 5 (ﬧﬧa == a) Q.E.D. -- Result: Q.E.D. -- Lemma: a ⊔ b = b ⊔ a Q.E.D. -- Lemma: a ⊓ b = b ⊓ a Q.E.D.
Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs view
@@ -50,12 +50,12 @@ -- >>> sqrt2IsIrrational -- Lemma: oddSquaredIsOdd -- Step: 1 Q.E.D.--- Step: 2 Q.E.D.+-- Step: 2 (expand square) Q.E.D. -- Result: Q.E.D. -- Lemma: squareEvenImpliesEven Q.E.D. -- Lemma: evenSquaredIsMult4 -- Step: 1 Q.E.D.--- Step: 2 Q.E.D.+-- Step: 2 (expand square) Q.E.D. -- Result: Q.E.D. -- Lemma: sqrt2IsIrrational Q.E.D. -- [Proven] sqrt2IsIrrational@@ -78,7 +78,6 @@ oddSquaredIsOdd <- calc "oddSquaredIsOdd" (\(Forall @"a" a) -> odd a .=> odd (sq a)) $ \a -> [odd a] |- sq a- ?? odd a =: let k = some "k" $ \_k -> a .== 2*_k + 1 -- Grab the witness that a is odd in sq (2 * k + 1) ?? "expand square"@@ -95,7 +94,6 @@ evenSquaredIsMult4 <- calc "evenSquaredIsMult4" (\(Forall @"a" a) -> even a .=> 4 `sDivides` sq a) $ \a -> [even a] |- sq a- ?? even a =: let k = some "k" $ \_k -> a .== 2*_k -- Grab the witness that a is even in sq (2 * k) ?? "expand square"
Documentation/SBV/Examples/KnuckleDragger/StrongInduction.hs view
@@ -6,22 +6,24 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental ----- Examples of strong induction on integers.+-- Examples of strong induction. ----------------------------------------------------------------------------- -{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeAbstractions #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.KnuckleDragger.StrongInduction where -import Prelude hiding (length, null, tail)+import Prelude hiding (length, null, head, tail, reverse, (++)) import Data.SBV import Data.SBV.List+import Data.SBV.Tuple import Data.SBV.Tools.KnuckleDragger #ifndef HADDOCK@@ -31,12 +33,15 @@ -- >>> import Control.Exception #endif +-- * Numeric examples+ -- | Prove that the sequence @1@, @3@, @S_{k-2} + 2 S_{k-1}@ is always odd. -- -- We have: -- -- >>> oddSequence1 -- Inductive lemma (strong): oddSequence+-- Step: Measure is non-negative Q.E.D. -- Step: 1 (3 way case split) -- Step: 1.1 Q.E.D. -- Step: 1.2 Q.E.D.@@ -57,9 +62,8 @@ -- Note also that we do a "proof-by-contradiction," by deriving that -- the negation of the goal leads to falsehood. sInductWith cvc5 "oddSequence"- (\(Forall @"n" n) -> n .>= 0 .=> sNot (2 `sDivides` s n)) $+ (\(Forall @"n" n) -> n .>= 0 .=> sNot (2 `sDivides` s n)) (abs @SInteger) $ \ih n -> [n .>= 0] |- 2 `sDivides` s n- ?? n .>= 0 =: cases [ n .== 0 ==> sFalse =: qed , n .== 1 ==> sFalse =: qed , n .>= 2 ==> 2 `sDivides` (s (n-2) + 2 * s (n-1))@@ -74,27 +78,28 @@ -- We have: -- -- >>> oddSequence2--- Lemma: oddSequence_0 Q.E.D.--- Lemma: oddSequence_1 Q.E.D.+-- Lemma: oddSequence_0 Q.E.D.+-- Lemma: oddSequence_1 Q.E.D. -- Inductive lemma (strong): oddSequence_sNp2--- 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.+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 (simplify) Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 (simplify) Q.E.D.+-- Step: 6 Q.E.D.+-- Result: Q.E.D. -- Lemma: oddSequence2 -- Step: 1 (3 way case split)--- Step: 1.1 Q.E.D.--- Step: 1.2 Q.E.D.--- Step: 1.3.1 Q.E.D.--- Step: 1.3.2 Q.E.D.--- Step: 1.Completeness Q.E.D.--- Result: Q.E.D.+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.3.1 Q.E.D.+-- Step: 1.3.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D. -- [Proven] oddSequence2 oddSequence2 :: IO Proof-oddSequence2 = runKD $ do+oddSequence2 = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 50}} $ do let s :: SInteger -> SInteger s = smtFunction "seq" $ \n -> ite (n .<= 0) 1 $ ite (n .== 1) 3@@ -104,17 +109,14 @@ s1 <- lemma "oddSequence_1" (s 1 .== 3) [] sNp2 <- sInduct "oddSequence_sNp2"- (\(Forall @"n" n) -> n .>= 2 .=> s n .== 2 * n + 1) $+ (\(Forall @"n" n) -> n .>= 2 .=> s n .== 2 * n + 1) (abs @SInteger) $ \ih n -> [n .>= 2] |- s n- ?? n .>= 2 =: 2 * s (n-1) - s (n-2)- ?? [ hyp (n .>= 2)- , hprf (ih `at` Inst @"n" (n-1))- ]+ ?? ih `at` Inst @"n" (n-1) =: 2 * (2 * (n-1) + 1) - s (n-2) ?? "simplify" =: 4*n - 4 + 2 - s (n-2)- ?? [hyp (n .>= 2), hprf (ih `at` Inst @"n" (n-2))]+ ?? ih `at` Inst @"n" (n-2) =: 4*n - 2 - (2 * (n-2) + 1) ?? "simplify" =: 4*n - 2 - 2*n + 4 - 1@@ -123,24 +125,144 @@ calc "oddSequence2" (\(Forall @"n" n) -> n .>= 0 .=> s n .== 2 * n + 1) $ \n -> [n .>= 0] |- s n- ?? n .>= 0 =: cases [ n .== 0 ==> (1 :: SInteger) =: qed , n .== 1 ==> (3 :: SInteger) =: qed , n .>= 2 ==> s n- ?? [ hyp (n .>= 0)- , hprf s0- , hprf s1- , hprf $ sNp2 `at` Inst @"n" n+ ?? [ s0+ , s1+ , sNp2 `at` Inst @"n" n ] =: 2 * n + 1 =: qed ] +-- * List examples++-- | 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:+--+-- >>> interleaveLen+-- 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+interleaveLen :: IO Proof+interleaveLen = runKD $ do++ sInduct "interleaveLen"+ (\(Forall @"xs" xs) (Forall @"ys" ys) -> length xs + length ys .== length (interleave @Integer xs ys))+ (\xs ys -> length @Integer xs + length @Integer ys) $+ \ih xs ys ->+ [] |- length xs + length ys .== length (interleave @Integer 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.C+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:+--+-- >>> interleaveRoundTrip+-- 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+interleaveRoundTrip :: IO Proof+interleaveRoundTrip = runKDWith cvc5 $ do++ revHelper <- lemma "revCons" (\(Forall @"a" a) (Forall @"as" as) (Forall @"bs" bs)+ -> reverse @Integer (a .: as) ++ bs .== reverse as ++ (a .: bs)) []++ -- Generalize the theorem first to take the helper lists explicitly+ roundTripGen <- sInduct+ "roundTripGen"+ (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"alts" alts) ->+ length @Integer xs .== length ys+ .=> let (es, os) = untuple alts+ in uninterleaveGen (interleave xs ys) alts .== tuple (reverse es ++ xs, reverse os ++ ys))+ (\xs ys (_alts :: STuple [Integer] [Integer]) -> length @Integer xs + length @Integer ys) $+ \ih xs ys alts -> [length @Integer 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" xs) (Forall @"ys" ys) -> length xs .== length ys .=> uninterleave (interleave @Integer xs ys) .== tuple (xs, ys)) $+ \xs ys -> [length xs .== length ys]+ |- uninterleave (interleave @Integer xs ys)+ =: uninterleaveGen (interleave xs ys) (tuple (nil, nil))+ ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple (nil :: SList Integer, nil :: SList Integer)))+ =: tuple (reverse nil ++ xs, reverse nil ++ ys)+ =: qed++-- * Strong induction checks+ -- | For strong induction to work, We have to instantiate the proof at a "smaller" value. This -- example demonstrates what happens if we don't. We have: -- -- >>> won'tProve1 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): lengthGood+-- Step: Measure is non-negative Q.E.D. -- Step: 1 -- *** Failed to prove lengthGood.1. -- <BLANKLINE>@@ -152,7 +274,8 @@ -- Run it for 5 seconds, as otherwise z3 will hang as it can't prove make the inductive step _ <- sInductWith z3{extraArgs = ["-t:5000"]} "lengthGood"- (\(Forall @"xs" xs) -> len xs .== length xs) $+ (\(Forall @"xs" xs) -> len xs .== length xs)+ (length @Integer) $ \ih xs -> [] |- len xs -- incorrectly instantiate the IH at xs! ?? ih `at` Inst @"xs" xs@@ -165,6 +288,7 @@ -- -- >>> won'tProve2 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): badLength+-- Step: Measure is non-negative Q.E.D. -- Step: 1 -- *** Failed to prove badLength.1. -- Falsifiable. Counter-example:@@ -179,9 +303,66 @@ (1 + len (tail xs))) _ <- sInduct "badLength"- (\(Forall @"xs" xs) -> len xs .== length xs) $+ (\(Forall @"xs" xs) -> len xs .== length xs)+ (length @Integer) $ \ih xs -> [] |- len xs ?? ih `at` Inst @"xs" xs =: length xs =: qed+ pure ()++-- | The measure for strong induction should always produce a non-negative measure. The measure, in general, is an integer, or+-- a tuple of integers, for tuples upto size 5. The ordering is lexicographic. This allows us to do proofs over 5-different arguments+-- where their total measure goes down. If the measure can be negative, then we flag that as a failure, as demonstrated here. We have:+--+-- >>> won'tProve3 `catch` (\(_ :: SomeException) -> pure ())+-- Inductive lemma (strong): badMeasure+-- Step: Measure is non-negative+-- *** Failed to prove badMeasure.Measure is non-negative.+-- Falsifiable. Counter-example:+-- x = -1 :: Integer+won'tProve3 :: IO ()+won'tProve3 = runKD $ do+ _ <- sInduct "badMeasure"+ (\(Forall @"x" (x :: SInteger)) -> x .== x)+ (id @SInteger) $+ \_h (x :: SInteger) -> [] |- x+ =: x+ =: qed++ pure ()++-- | The measure must always go down using lexicographic ordering. If not, SBV will flag this as a failure. We have:+--+-- >>> won'tProve4 `catch` (\(_ :: SomeException) -> pure ())+-- Inductive lemma (strong): badMeasure+-- 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+-- *** Failed to prove badMeasure.1.2.2.+-- <BLANKLINE>+-- *** Solver reported: canceled+won'tProve4 :: IO ()+won'tProve4 = runKD $ do++ let -- a bizarre (but valid!) way to sum two integers+ weirdSum = smtFunction "weirdSum" (\x y -> ite (x .<= 0) y (weirdSum (x - 1) (y + 1)))++ _ <- sInductWith z3{extraArgs = ["-t:5000"]} "badMeasure"+ (\(Forall @"x" (x :: SInteger)) (Forall @"y" (y :: SInteger)) -> x .>= 0 .=> weirdSum x y .== x + y)+ -- This measure is not good, since it remains the same. Note that we do not get a+ -- failure, but the proof will never converge either; so we put a time bound+ (\x y -> abs x + abs @SInteger y) $+ \ih (x :: SInteger) (y :: SInteger) ->+ [x .>= 0] |- ite (x .<= 0) y (weirdSum (x - 1) (y + 1))+ =: cases [ x .<= 0 ==> trivial+ , x .> 0 ==> weirdSum (x - 1) (y + 1)+ ?? ih `at` (Inst @"x" (x - 1), Inst @"y" (y + 1))+ =: x - 1 + y + 1+ =: x + y+ =: qed+ ]+ pure ()
Documentation/SBV/Examples/Transformers/SymbolicEval.hs view
@@ -63,7 +63,7 @@ -- we only have a value during property -- evaluation. }- deriving (Eq, Show)+ deriving Show -- | Allocate an integer variable with the provided name. alloc :: String -> Alloc (SBV Integer)
README.md view
@@ -95,12 +95,13 @@ SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. See `proveWithAny`/`proveWithAll` and `satWithAny`/`satWithAll` functions. The function `sbvAvailableSolvers` can be used to query the available solvers at run-time. -### Semi-automated theorem proving+## KnuckleDragger: Semi-automated theorem proving While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about-any recursive algorithm, and most such proofs require carefully constructed equational steps. SBV allows for a-style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs.+any recursive algorithm, and most such proofs require carefully constructed equational steps.++SBV allows for a style of semi-automated theorem proving, called KnuckleDragger, that can be used to construct such proofs. The documentation includes example proofs for many list functions, and even inductive proofs for the familiar insertion and merge-sort algorithms, along with a proof that the square-root of 2 is irrational. While a proper theorem prover (such as Lean, Isabelle etc.) is a more appropriate choice for such proofs, with some guidance (and acceptance of a much larger trusted code base!), SBV can
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 939; Tried: 939; Skipped: 0; Success: 939; Errors: 0; Failures 0-Examples: 811; Tried: 811; Skipped: 0; Success: 811; Errors: 0; Failures 0-Setup: 128; Tried: 128; Skipped: 0; Success: 128; Errors: 0; Failures 0+Total: 949; Tried: 949; Skipped: 0; Success: 949; Errors: 0; Failures 0+Examples: 818; Tried: 818; Skipped: 0; Success: 818; Errors: 0; Failures 0+Setup: 131; Tried: 131; Skipped: 0; Success: 131; Errors: 0; Failures 0
SBVTestSuite/GoldFiles/nested1.gold view
@@ -2,8 +2,8 @@ Data.SBV: Mismatched contexts detected. ***-*** Current context: SBVContext (-531973508589804280)-*** Mixed with : SBVContext (-7749304166575005736)+*** Current context: SBVContext (-531973508589804280)+*** Mixed with : SBVContext (-7749304166575005736) *** *** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc. *** while another one is in execution, or use results from one such call in another.
SBVTestSuite/GoldFiles/nested2.gold view
@@ -2,8 +2,8 @@ Data.SBV: Mismatched contexts detected. ***-*** Current context: SBVContext (-531973508589804280)-*** Mixed with : SBVContext (-7749304166575005736)+*** Current context: SBVContext (-531973508589804280)+*** Mixed with : SBVContext (-7749304166575005736) *** *** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc. *** while another one is in execution, or use results from one such call in another.
SBVTestSuite/GoldFiles/nested3.gold view
@@ -25,8 +25,8 @@ Data.SBV: Mismatched contexts detected. ***-*** Current context: SBVContext (-7749304166575005736)-*** Mixed with : SBVContext (-531973508589804280)+*** Current context: SBVContext (-7749304166575005736)+*** Mixed with : SBVContext (-531973508589804280) *** *** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc. *** while another one is in execution, or use results from one such call in another.
SBVTestSuite/GoldFiles/nested4.gold view
@@ -2,8 +2,8 @@ Data.SBV: Mismatched contexts detected. ***-*** Current context: SBVContext (-531973508589804280)-*** Mixed with : SBVContext (-7749304166575005736)+*** Current context: SBVContext (-531973508589804280)+*** Mixed with : SBVContext (-7749304166575005736) *** *** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc. *** while another one is in execution, or use results from one such call in another.
SBVTestSuite/GoldFiles/query1.gold view
@@ -73,7 +73,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version)-[RECV] (:version "4.14.2")+[RECV] (:version "4.15.0") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -104,7 +104,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.14.2")+[RECV] (:version "4.15.0") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 11.5+Version : 11.6 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@@ -33,7 +33,7 @@ common common-settings default-language: Haskell2010 ghc-options : -Wall- build-depends : base >= 4.19 && < 5+ build-depends : base >= 4.19.2 && < 5 other-extensions: BangPatterns CPP ConstraintKinds@@ -163,6 +163,7 @@ , Documentation.SBV.Examples.Lists.BoundedMutex , Documentation.SBV.Examples.Lists.CountOutAndTransfer , Documentation.SBV.Examples.KnuckleDragger.Basics+ , Documentation.SBV.Examples.KnuckleDragger.BinarySearch , Documentation.SBV.Examples.KnuckleDragger.CaseSplit , Documentation.SBV.Examples.KnuckleDragger.InsertionSort , Documentation.SBV.Examples.KnuckleDragger.Kleene