diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,15 @@ * Hackage: * GitHub: +### Version 11.4, 2025-03-12 + + * Generalize the strong-induction principle to use lexicographic order for simultanous + induction over two lists. + + * Added a proof of correctness for the merge-sort algorithm using KnuckleDragger + + * More exports from Data.SBV.Internals to enable compilation of SBVPlugin. + ### Version 11.3, 2025-03-10 * Fix various haddock documentation links diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -33,6 +33,8 @@ -- Functions for checking satisfiability ('sat' and 'allSat') are also -- provided. -- +-- __Symbolic Types__ +-- -- The sbv library introduces the following symbolic types: -- -- * 'SBool': Symbolic Booleans (bits). @@ -112,6 +114,9 @@ -- return a satisfying assignment, if there is one. The 'allSat' function returns -- all satisfying assignments. -- +-- +-- __Solvers__ +-- -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: -- -- @@ -143,6 +148,27 @@ -- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included. +-- +-- +-- __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. +-- 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 +-- be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT +-- solvers alone. See "Data.SBV.Tools.KnuckleDragger" for the API, and +-- +-- - "Documentation.SBV.Examples.KnuckleDragger.InsertionSort" +-- - "Documentation.SBV.Examples.KnuckleDragger.MergeSort" +-- - "Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational" +-- - "Documentation.SBV.Examples.KnuckleDragger.ShefferStroke" +-- - "Documentation.SBV.Examples.KnuckleDragger.Lists" +-- +-- for various proofs performed in this style. ----------------------------------------------------------------------------- {-# LANGUAGE DataKinds #-} diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -33,6 +33,9 @@ -- * Internal structures useful for low-level programming , module Data.SBV.Core.Data + -- * Is this name reserved? + , isReserved, UIName(..) + -- * Operations useful for instantiating SBV type classes , genLiteral, genFromCV, CV(..), genMkSymVar, genParse, showModel, SMTModel(..), liftQRem, liftDMod, registerKind, svToSV , ProvableM(), SatisfiableM(), UICodeKind(..) @@ -74,7 +77,7 @@ import Data.SBV.Core.Kind (BVIsNonZero, ValidFloat) import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod) -import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..)) +import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..), UIName(..)) import Data.SBV.Core.Floating (sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord, svFloatingPointAsSWord) @@ -83,6 +86,7 @@ import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen +import Data.SBV.SMT.SMTLibNames import Data.SBV.SMT.SMT (genParse, showModel, SatModel(..)) import Data.SBV.Provers.Prover (ProvableM, SatisfiableM) diff --git a/Data/SBV/Tools/KD/KnuckleDragger.hs b/Data/SBV/Tools/KD/KnuckleDragger.hs --- a/Data/SBV/Tools/KD/KnuckleDragger.hs +++ b/Data/SBV/Tools/KD/KnuckleDragger.hs @@ -128,6 +128,11 @@ cover = sAnd regulars .&& sNot (sOr [b | (_, b) <- caseSplits]) +-- | Propagate the settings for ribbon/timing from top to current. Because in any subsequent configuration +-- in a lemmaWith, inductWith etc., we just want to change the solver, not the actual settings for KD. +kdMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig +kdMergeCfg cur top = cur{kdOptions = kdOptions top} + -- | A class for doing equational reasoning style calculational proofs. Use 'calc' to prove a given theorem -- as a sequence of equalities, each step following from the previous. class CalcLemma a steps where @@ -167,10 +172,10 @@ {-# MINIMAL calcSteps #-} calcSteps :: a -> steps -> Symbolic (SBool, CalcStrategy) - calc nm p steps = getKDConfig >>= \cfg -> calcWith cfg nm p steps - calcThm nm p steps = getKDConfig >>= \cfg -> calcThmWith cfg nm p steps - calcWith = calcGeneric False - calcThmWith = calcGeneric True + calc nm p steps = getKDConfig >>= \cfg -> calcWith cfg nm p steps + calcThm nm p steps = getKDConfig >>= \cfg -> calcThmWith cfg nm p steps + calcWith cfg nm p steps = getKDConfig >>= \cfg' -> calcGeneric False (kdMergeCfg cfg cfg') nm p steps + calcThmWith cfg nm p steps = getKDConfig >>= \cfg' -> calcGeneric True (kdMergeCfg cfg cfg') nm p steps calcGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> KD Proof calcGeneric tagTheorem cfg@SMTConfig{kdOptions = KDOptions{measureTime}} nm result steps = do @@ -376,15 +381,15 @@ -- partial correctness is guaranteed if non-terminating functions are involved. sInductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof - induct nm p steps = getKDConfig >>= \cfg -> inductWith cfg nm p steps - inductThm nm p steps = getKDConfig >>= \cfg -> inductThmWith cfg nm p steps - inductWith = inductGeneric RegularInduction False - inductThmWith = inductGeneric RegularInduction True + induct nm p steps = getKDConfig >>= \cfg -> inductWith cfg nm p steps + inductThm nm p steps = getKDConfig >>= \cfg -> inductThmWith cfg nm p steps + inductWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric RegularInduction False (kdMergeCfg cfg cfg') nm p steps + inductThmWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric RegularInduction True (kdMergeCfg cfg cfg') nm p steps - sInduct nm p steps = getKDConfig >>= \cfg -> sInductWith cfg nm p steps - sInductThm nm p steps = getKDConfig >>= \cfg -> sInductThmWith cfg nm p steps - sInductWith = inductGeneric StrongInduction False - sInductThmWith = inductGeneric StrongInduction True + 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' -> inductGeneric StrongInduction False (kdMergeCfg cfg cfg') nm p steps + sInductThmWith cfg nm p steps = getKDConfig >>= \cfg' -> inductGeneric StrongInduction True (kdMergeCfg cfg cfg') nm p steps -- | Internal, shouldn't be needed outside the library {-# MINIMAL inductionStrategy #-} @@ -620,11 +625,25 @@ 's':_:_ -> init n _ -> n ++ "Elt" --- | Metric for induction. Currently we simply require the list we're assuming correctness for is shorter in length, which --- is a measure that is guarenteed >= 0. -- Later on, we might want to generalize this to a user given measure. -smaller :: SymVal a => SList a -> SList a -> SBool -smaller xs ys = SL.length xs .<= SL.length ys +-- | 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. Note that we use .<= here, since when called, the second argument is always the tail +-- of the induction argument. 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 +-- | Metric for induction over two lists. We use lexicographic ordering. Again, we don't expose this directly. The +-- second argument is always the tail of the induction argument, so we use .<=. Later on, we might want to generalize +-- this to a user given measure. +lexLeq2 :: (SymVal a, SymVal b) => (SList a, SList b) -> (SList a, SList b) -> SBool +lexLeq2 (xs', ys') (xs, ys) = lxs' .<= lxs -- tail of the first is the same, i.e., the first went down. So, we're good. + .|| ( lxs' .== 1 + SL.length xs -- OR, the tail did not grow (note the +1 due to us receiving the tail) + .&& lys' .<= lys -- and the tail of the second went down. + ) + where lxs = SL.length xs + lys = SL.length ys + lxs' = SL.length xs' + lys' = SL.length ys' + -- | Induction over 'SList'. instance (KnownSymbol nx, SymVal x, EqSymbolic z) => Inductive (Forall nx [x] -> SBool) @@ -639,8 +658,8 @@ xs <- free nxs let ih = case style of - RegularInduction -> internalAxiom "IH" $ result (Forall xs) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) -> xs' `smaller` xs .=> result (Forall xs') + RegularInduction -> internalAxiom "IH" $ result (Forall xs) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) -> xs' `lexLeq` xs .=> result (Forall xs') CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs pure InductionStrategy { @@ -667,8 +686,8 @@ a <- free na let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (a' :: Forall na a) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) + RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (a' :: Forall na a) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a pure InductionStrategy { @@ -697,8 +716,8 @@ b <- free nb let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) + RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b pure InductionStrategy { @@ -729,8 +748,8 @@ c <- free nc let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c pure InductionStrategy { @@ -763,8 +782,8 @@ d <- free nd let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d pure InductionStrategy { @@ -799,8 +818,8 @@ e <- free ne let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' e' -> xs' `smaller` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) a' b' c' d' e' -> xs' `lexLeq` xs .=> result (Forall xs') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d e pure InductionStrategy { @@ -830,8 +849,8 @@ ys <- free nys let ih = case style of - RegularInduction -> internalAxiom "IH" $ result (Forall xs) (Forall ys) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') + RegularInduction -> internalAxiom "IH" $ result (Forall xs) (Forall ys) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys pure InductionStrategy { @@ -864,8 +883,8 @@ a <- free na let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (Forall ys) (a' :: Forall na a) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) + RegularInduction -> internalAxiom "IH" $ \ a' -> result (Forall xs) (Forall ys) (a' :: Forall na a) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a pure InductionStrategy { @@ -900,8 +919,8 @@ b <- free nb let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) + RegularInduction -> internalAxiom "IH" $ \ a' b' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b pure InductionStrategy { @@ -938,8 +957,8 @@ c <- free nc let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c pure InductionStrategy { @@ -978,8 +997,8 @@ d <- free nd let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d pure InductionStrategy { @@ -1020,8 +1039,8 @@ e <- free ne let ih = case style of - RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) - StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' e' -> xs' `smaller` xs .&& ys' `smaller` ys .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) + RegularInduction -> internalAxiom "IH" $ \ a' b' c' d' e' -> result (Forall xs) (Forall ys) (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) + StrongInduction -> internalAxiom "IH" $ \(Forall xs' :: Forall nx [x]) (Forall ys' :: Forall ny [y]) a' b' c' d' e' -> (xs', ys') `lexLeq2` (xs, ys) .=> result (Forall xs') (Forall ys') (a' :: Forall na a) (b' :: Forall nb b) (c' :: Forall nc c) (d' :: Forall nd d) (e' :: Forall ne e) CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d e pure InductionStrategy { diff --git a/Documentation/SBV/Examples/BitPrecise/MergeSort.hs b/Documentation/SBV/Examples/BitPrecise/MergeSort.hs --- a/Documentation/SBV/Examples/BitPrecise/MergeSort.hs +++ b/Documentation/SBV/Examples/BitPrecise/MergeSort.hs @@ -6,7 +6,12 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Symbolic implementation of merge-sort and its correctness. +-- Symbolic implementation of merge-sort and its correctness. Note that this +-- version, while fully push-button, proves merge-sort correct for fixed number +-- of elements, i.e., not in its generality. A general proof would require +-- non-trivial applications of induction and more manual guiding. We do +-- such a proof in "Documentation.SBV.Examples.KnuckleDragger.MergeSort", which +-- shows the full-power of the theorem-proving like aspects of SBV. ----------------------------------------------------------------------------- {-# LANGUAGE TupleSections #-} diff --git a/Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs b/Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/KnuckleDragger/MergeSort.hs @@ -0,0 +1,309 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.KnuckleDragger.MergeSort +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Proving merge-sort correct. +----------------------------------------------------------------------------- + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.KnuckleDragger.MergeSort where + +import Data.SBV +import Data.SBV.Tools.KnuckleDragger + +import Prelude hiding (null, length, head, tail, elem, splitAt, (++), take, drop) +import Data.SBV.List + +-- * Merge sort + +-- | Merge two already sorted lists into another +merge :: SList Integer -> SList Integer -> SList Integer +merge = smtFunction "merge" $ \l r -> ite (null l) r + $ ite (null r) l + $ let (a, as) = uncons l + (b, bs) = uncons r + in ite (a .<= b) (a .: merge as r) (b .: merge l bs) + +-- | Merge sort, using 'merge' above to successively sort halved input +mergeSort :: SList Integer -> SList Integer +mergeSort = smtFunction "mergeSort" $ \l -> ite (length l .<= 1) l + $ let (h1, h2) = splitAt (length l `sEDiv` 2) l + in merge (mergeSort h1) (mergeSort h2) +-- * Helper functions + +-- | A predicate testing whether a given list is non-decreasing. +nonDecreasing :: SList Integer -> SBool +nonDecreasing = smtFunction "nonDecreasing" $ \l -> null l .|| null (tail l) + .|| let (x, l') = uncons l + (y, _) = uncons l' + in x .<= y .&& nonDecreasing l' + +-- | Count the number of occurrences of an element in a list +count :: SInteger -> SList Integer -> SInteger +count = smtFunction "count" $ \e l -> ite (null l) + 0 + (let (x, xs) = uncons l + cxs = count e xs + in ite (e .== x) (1 + cxs) cxs) + +-- | Are two lists permutations of each other? +isPermutation :: SList Integer -> SList Integer -> SBool +isPermutation xs ys = quantifiedBool (\(Forall @"x" x) -> count x xs .== count x ys) + +-- * Correctness proof + +-- | Correctness of merge-sort. +-- +-- We have: +-- +-- >>> correctness +-- Lemma: nonDecrInsert Q.E.D. +-- Lemma: nonDecTail Q.E.D. +-- Inductive lemma (strong): mergeKeepsSort +-- Base: mergeKeepsSort.Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Asms: 3 Q.E.D. +-- Step: 3 Q.E.D. +-- Asms: 4 Q.E.D. +-- Step: 4 Q.E.D. +-- Asms: 5 Q.E.D. +-- Step: 5 Q.E.D. +-- Asms: 6 Q.E.D. +-- Step: 6 Q.E.D. +-- Step: 7 Q.E.D. +-- Step: mergeKeepsSort.Step Q.E.D. +-- Inductive lemma (strong): sortNonDecreasing +-- Base: sortNonDecreasing.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: sortNonDecreasing.Step Q.E.D. +-- Inductive lemma (strong): mergeCount +-- Base: mergeCount.Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Step: 6 Q.E.D. +-- Step: 7 Q.E.D. +-- Step: mergeCount.Step Q.E.D. +-- Inductive lemma: countAppend +-- Base: countAppend.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: countAppend.Step 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. +-- Inductive lemma (strong): sortIsPermutation +-- Base: sortIsPermutation.Base Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Step: 6 Q.E.D. +-- Step: sortIsPermutation.Step Q.E.D. +-- Lemma: mergeSortIsCorrect Q.E.D. +-- [Proven] mergeSortIsCorrect +correctness :: IO Proof +correctness = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = 50}} $ 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)) + [] + + nonDecrTail <- lemma "nonDecTail" + (\(Forall @"x" x) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs) + [] + + mergeKeepsSort <- + sInductWith cvc5 "mergeKeepsSort" + (\(Forall @"xs" xs) (Forall @"ys" ys) -> nonDecreasing xs .&& nonDecreasing ys .=> nonDecreasing (merge xs ys)) $ + \ih x xs y ys -> [nonDecreasing (x .: xs), nonDecreasing (y .: ys)] + |- nonDecreasing (merge (x .: xs) (y .: ys)) + ?? "unfold merge" + =: nonDecreasing (ite (x .<= y) + (x .: merge xs (y .: ys)) + (y .: merge (x .: xs) ys)) + ?? "push nonDecreasing down" + =: ite (x .<= y) + (nonDecreasing (x .: merge xs (y .: ys))) + (nonDecreasing (y .: merge (x .: xs) ys)) + ?? [ hprf $ nonDecrIns `at` (Inst @"x" x, Inst @"ys" (merge xs (y .: ys))) + , hyp $ nonDecreasing (x .: xs) + , hyp $ nonDecreasing (y .: ys) + ] + =: ite (x .<= y) + (nonDecreasing (merge xs (y .: ys))) + (nonDecreasing (y .: merge (x .: xs) ys)) + ?? [ hprf $ nonDecrIns `at` (Inst @"x" y, Inst @"ys" (merge (x .: xs) ys)) + , hyp $ nonDecreasing (x .: xs) + , hyp $ nonDecreasing (y .: ys) + ] + =: ite (x .<= y) + (nonDecreasing (merge xs (y .: ys))) + (nonDecreasing (merge (x .: xs) ys)) + ?? [ hprf $ ih `at` (Inst @"xs" xs, Inst @"ys" (y .: ys)) + , hprf $ nonDecrTail `at` (Inst @"x" x, Inst @"xs" xs) + , hyp $ nonDecreasing (y .: ys) + , hyp $ nonDecreasing (x .: xs) + ] + =: ite (x .<= y) + sTrue + (nonDecreasing (merge (x .: xs) ys)) + ?? [ hprf $ ih `at` (Inst @"xs" (x .: xs), Inst @"ys" ys) + , hprf $ nonDecrTail `at` (Inst @"x" y, Inst @"xs" ys) + , hyp $ nonDecreasing (y .: ys) + , hyp $ nonDecreasing (x .: xs) + ] + =: ite (x .<= y) sTrue sTrue + ?? "simplify" + =: sTrue + =: qed + + sortNonDecreasing <- + sInduct "sortNonDecreasing" + (\(Forall @"xs" xs) -> nonDecreasing (mergeSort xs)) $ + \ih x xs -> [] |- nonDecreasing (mergeSort (x .: xs)) + ?? "unfold" + =: let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs) + in nonDecreasing (ite (length (x .: xs) .<= 1) + (x .: xs) + (merge (mergeSort h1) (mergeSort h2))) + ?? "push nonDecreasing down" + =: ite (length (x .: xs) .<= 1) + (nonDecreasing (x .: xs)) + (nonDecreasing (merge (mergeSort h1) (mergeSort h2))) + ?? ih `at` Inst @"xs" xs + =: ite (length (x .: xs) .<= 1) + sTrue + (nonDecreasing (merge (mergeSort h1) (mergeSort h2))) + ?? [ ih `at` Inst @"xs" h1 + , ih `at` Inst @"xs" h2 + , mergeKeepsSort `at` (Inst @"xs" (mergeSort h1), Inst @"ys" (mergeSort h2)) + ] + =: sTrue + =: qed + + -------------------------------------------------------------------------------------------- + -- Part II. Prove that the output of merge sort is a permuation of its input + -------------------------------------------------------------------------------------------- + + mergeCount <- + sInduct "mergeCount" + (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"e" e) -> count e (merge xs ys) .== count e xs + count e ys) $ + \ih x xs y ys e -> [] |- count e (merge (x .: xs) (y .: ys)) + ?? "unfold merge" + =: count e (ite (x .<= y) + (x .: merge xs (y .: ys)) + (y .: merge (x .: xs) ys)) + ?? "push count inside" + =: ite (x .<= y) + (count e (x .: merge xs (y .: ys))) + (count e (y .: merge (x .: xs) ys)) + ?? "unfold count, twice" + =: 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 `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 `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) + ?? "unfold count in reverse, twice" + =: ite (x .<= y) + (count e (x .: xs) + count e (y .: ys)) + (count e (x .: xs) + count e (y .: ys)) + ?? "simplify" + =: count e (x .: xs) + count e (y .: ys) + =: qed + + countAppend <- + induct "countAppend" + (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"e" e) -> count e (xs ++ ys) .== count e xs + count e ys) $ + \ih x xs ys e -> [] |- count e ((x .: xs) ++ ys) + =: count e (x .: (xs ++ ys)) + ?? "unfold count" + =: (let r = count e (xs ++ ys) in ite (e .== x) (1+r) r) + ?? ih `at` (Inst @"ys" ys, Inst @"e" e) + =: (let r = count e xs + count e ys in ite (e .== x) (1+r) r) + ?? "simplify" + =: count e (x .: xs) + count e ys + =: qed + + takeDropCount <- do + + takeDrop <- lemma "take_drop" + (\(Forall @"n" n) (Forall @"xs" (xs :: SList Integer)) -> take n xs ++ drop n xs .== xs) + [] + + calc "takeDropCount" + (\(Forall @"xs" xs) (Forall @"n" n) (Forall @"e" e) -> count e (take n xs) + count e (drop n xs) .== count e xs) $ + \xs n e -> [] |- count e (take n xs) + count e (drop n xs) + ?? countAppend `at` (Inst @"xs" (take n xs), Inst @"ys" (drop n xs), Inst @"e" e) + =: count e (take n xs ++ drop n xs) + ?? takeDrop + =: count e xs + =: qed + + sortIsPermutation <- + sInduct "sortIsPermutation" + (\(Forall @"xs" xs) (Forall @"e" e) -> count e xs .== count e (mergeSort xs)) $ + \ih x xs e -> [] |- count e (mergeSort (x .: xs)) + ?? "unfold mergeSort" + =: count e (ite (length (x .: xs) .<= 1) + (x .: xs) + (let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs) + in merge (mergeSort h1) (mergeSort h2))) + ?? "push count down, simplify, rearrange" + =: let (h1, h2) = splitAt (length (x .: xs) `sEDiv` 2) (x .: xs) + in ite (null xs) + (count e (singleton x)) + (count e (merge (mergeSort h1) (mergeSort h2))) + ?? 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)) + ?? ih `at` (Inst @"xs" h2, Inst @"e" e) + =: ite (null xs) + (count e (singleton x)) + (count e h1 + count e h2) + ?? takeDropCount `at` (Inst @"xs" (x .: xs), Inst @"n" (length (x .: xs) `sEDiv` 2), Inst @"e" e) + =: ite (null xs) + (count e (singleton x)) + (count e (x .: xs)) + =: qed + + -------------------------------------------------------------------------------------------- + -- Put the two parts together for the final proof + -------------------------------------------------------------------------------------------- + lemma "mergeSortIsCorrect" + (\(Forall @"xs" xs) -> let out = mergeSort xs in nonDecreasing out .&& isPermutation xs out) + [sortNonDecreasing, sortIsPermutation] diff --git a/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs b/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs --- a/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Numeric.hs @@ -61,8 +61,6 @@ -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@. -- --- Note that z3 (as of mid Feb 2025) can't converge on this quickly, but CVC5 does just fine. We have: --- -- >>> sumProof -- Inductive lemma: sum_correct -- Base: sum_correct.Base Q.E.D. @@ -76,7 +74,7 @@ sumProof :: IO Proof sumProof = runKD $ do let sum :: SInteger -> SInteger - sum = smtFunction "sum" $ \n -> ite (n .== 0) 0 (n + sum (n - 1)) + sum = smtFunction "sum" $ \n -> ite (n .<= 0) 0 (n + sum (n - 1)) spec :: SInteger -> SInteger spec n = (n * (n+1)) `sDiv` 2 @@ -84,7 +82,7 @@ p :: SInteger -> SBool p n = sum n .== spec n - inductWith cvc5 "sum_correct" + 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)] @@ -94,8 +92,6 @@ -- | Prove that sum of square of numbers from @0@ to @n@ is @n*(n+1)*(2n+1)/6@. -- --- Note that z3 (as of mid Feb 2025) can't converge on this quickly, but CVC5 does just fine. We have: --- -- >>> sumSquareProof -- Inductive lemma: sumSquare_correct -- Base: sumSquare_correct.Base Q.E.D. @@ -109,7 +105,7 @@ sumSquareProof :: IO Proof sumSquareProof = runKD $ do let sumSquare :: SInteger -> SInteger - sumSquare = smtFunction "sumSquare" $ \n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1)) + sumSquare = smtFunction "sumSquare" $ \n -> ite (n .<= 0) 0 (n * n + sumSquare (n - 1)) spec :: SInteger -> SInteger spec n = (n * (n+1) * (2*n+1)) `sDiv` 6 @@ -117,7 +113,7 @@ p :: SInteger -> SBool p n = sumSquare n .== spec n - inductWith cvc5 "sumSquare_correct" + 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)] diff --git a/Documentation/SBV/Examples/Puzzles/Coins.hs b/Documentation/SBV/Examples/Puzzles/Coins.hs --- a/Documentation/SBV/Examples/Puzzles/Coins.hs +++ b/Documentation/SBV/Examples/Puzzles/Coins.hs @@ -21,7 +21,7 @@ -- you: Really? and these six coins are all US government coins currently in production? -- friend: Yes. -- you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back? --- friend: Sorry, I would like to but I cant with the coins I have. +-- friend: Sorry, I would like to but I can't with the coins I have. -- What coins are your friend holding? -- @ -- diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -95,6 +95,18 @@ 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 + +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. +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 +be used to establish correctness of various mathematical claims and algorithms that are usually beyond the scope of SMT +solvers alone. See the documentation under the `Documentation.SBV.Examples.KnuckleDragger` directory. + ## Copyright, License The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for details. diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 937; Tried: 937; Skipped: 0; Success: 937; Errors: 0; Failures 0 -Examples: 809; Tried: 809; Skipped: 0; Success: 809; Errors: 0; Failures 0 +Total: 938; Tried: 938; Skipped: 0; Success: 938; Errors: 0; Failures 0 +Examples: 810; Tried: 810; Skipped: 0; Success: 810; Errors: 0; Failures 0 Setup: 128; Tried: 128; Skipped: 0; Success: 128; Errors: 0; Failures 0 diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -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.1") +[RECV] (:version "4.14.2") [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.1") +[RECV] (:version "4.14.2") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 11.3 +Version : 11.4 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT @@ -158,6 +158,7 @@ , Documentation.SBV.Examples.KnuckleDragger.InsertionSort , Documentation.SBV.Examples.KnuckleDragger.Kleene , Documentation.SBV.Examples.KnuckleDragger.Lists + , Documentation.SBV.Examples.KnuckleDragger.MergeSort , Documentation.SBV.Examples.KnuckleDragger.Numeric , Documentation.SBV.Examples.KnuckleDragger.ShefferStroke , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational