From d9cacb7f0e1447370b50db85dfa6dac192a829b2 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Thu, 29 Aug 2024 13:00:45 -0700 Subject: [PATCH] KnuckleDragger: Introduce a Proven type --- Data/SBV/Tools/KnuckleDragger.hs | 37 +++++++++---------- .../SBV/Examples/KnuckleDragger/Kleene.hs | 10 ++--- 2 files changed, 23 insertions(+), 24 deletions(-) diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs index 02b703151..06fdd3b1b 100644 --- a/Data/SBV/Tools/KnuckleDragger.hs +++ b/Data/SBV/Tools/KnuckleDragger.hs @@ -17,7 +17,7 @@ {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Tools.KnuckleDragger ( - axiom, lemma, theorem, qb, ChainLemma(..) + axiom, lemma, theorem, chainLemma, Proven ) where import Data.SBV @@ -37,42 +37,41 @@ start knd nm = do let tab = 2 * length (filter (== '.') nm) putStr $ replicate tab ' ' ++ knd ++ nm pure tab +-- | A proven property. Note that axioms are considered proven. +data Proven = ProvenBool { boolOf :: SBool } + -- | Accept the given definition as a fact. Usually used to introduce definitial axioms, -- giving meaning to uninterpreted symbols. -axiom :: QuantifiedBool a => String -> a -> IO SBool +axiom :: QuantifiedBool a => String -> a -> IO Proven axiom nm p = do putStrLn $ "Axiom: " ++ tag 0 nm "Admitted." - pure (qb p) + pure $ ProvenBool (quantifiedBool p) -- | Helper to generate lemma/theorem statements. -lemmaGen :: QuantifiedBool a => String -> String -> a -> [SBool] -> IO SBool +lemmaGen :: QuantifiedBool a => String -> String -> a -> [Proven] -> IO Proven lemmaGen what nm p by = do tab <- start what nm - t <- isTheorem (quantifiedBool (sAnd by .=> qb p)) + t <- isTheorem (quantifiedBool (sAnd (map boolOf by) .=> quantifiedBool p)) if t then putStrLn $ drop (length nm) $ tag tab nm "Q.E.D." else do putStrLn $ "\n*** Failed to prove " ++ nm ++ ":" print =<< proveWith z3{verbose=True} (quantifiedBool p) error "Failed" - pure (qb p) + pure $ ProvenBool (quantifiedBool p) -- | Prove a given statement, using auxiliaries as helpers. -lemma :: QuantifiedBool a => String -> a -> [SBool] -> IO SBool +lemma :: QuantifiedBool a => String -> a -> [Proven] -> IO Proven lemma = lemmaGen "Lemma: " -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as lemma, except for the name. -theorem :: QuantifiedBool a => String -> a -> [SBool] -> IO SBool +theorem :: QuantifiedBool a => String -> a -> [Proven] -> IO Proven theorem = lemmaGen "Theorem: " --- | Synonym for 'quantifiedBool', shorter to type. -qb :: QuantifiedBool a => a -> SBool -qb = quantifiedBool - -- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem -- as a sequence of equalities, each step following from the previous. class ChainLemma steps step | steps -> step where - chainLemma :: QuantifiedBool a => String -> a -> steps -> [SBool] -> IO SBool + chainLemma :: QuantifiedBool a => String -> a -> steps -> [Proven] -> IO Proven makeSteps :: steps -> [step] - makeInter :: steps -> step -> step -> SBool + makeInter :: steps -> step -> step -> SBool chainLemma nm result steps base = do void (start "Chain: " (nm ++ "\n")) @@ -81,24 +80,24 @@ class ChainLemma steps step | steps -> step where go _ sofar [_] = lemma nm result sofar go i sofar (a:b:rest) = do let intermediate = makeInter steps a b _step <- lemma (nm ++ "." ++ show i) intermediate sofar - go (i+1) (qb intermediate : sofar) (b:rest) + go (i+1) (ProvenBool (quantifiedBool intermediate) : sofar) (b:rest) -- | Chaining lemmas that depend on a single quantified varible. instance (SymVal a, EqSymbolic z) => ChainLemma (SBV a -> [z]) (SBV a -> z) where makeSteps steps = [\x -> steps x !! i | i <- [0 .. length (steps undefined) - 1]] - makeInter _ a b = qb $ \(Forall x) -> a x .== b x + makeInter _ a b = quantifiedBool $ \(Forall x) -> a x .== b x -- | Chaining lemmas that depend on two quantified varibles. instance (SymVal a, SymVal b, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> [z]) (SBV a -> SBV b -> z) where makeSteps steps = [\x y -> steps x y !! i | i <- [0 .. length (steps undefined undefined) - 1]] - makeInter _ a b = qb $ \(Forall x) (Forall y) -> a x y .== b x y + makeInter _ a b = quantifiedBool $ \(Forall x) (Forall y) -> a x y .== b x y -- | Chaining lemmas that depend on three quantified varibles. instance (SymVal a, SymVal b, SymVal c, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> [z]) (SBV a -> SBV b -> SBV c -> z) where makeSteps steps = [\x y z -> steps x y z !! i | i <- [0 .. length (steps undefined undefined undefined) - 1]] - makeInter _ a b = qb $ \(Forall x) (Forall y) (Forall z) -> a x y z .== b x y z + makeInter _ a b = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> a x y z .== b x y z -- | Chaining lemmas that depend on four quantified varibles. instance (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> [z]) (SBV a -> SBV b -> SBV c -> SBV d -> z) where makeSteps steps = [\x y z w -> steps x y z w !! i | i <- [0 .. length (steps undefined undefined undefined undefined) - 1]] - makeInter _ a b = qb $ \(Forall x) (Forall y) (Forall z) (Forall w) -> a x y z w .== b x y z w + makeInter _ a b = quantifiedBool $ \(Forall x) (Forall y) (Forall z) (Forall w) -> a x y z w .== b x y z w diff --git a/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs b/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs index f88ad7886..031779521 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs @@ -106,11 +106,11 @@ example = do least_fix <- axiom "least_fix" $ \(Forall x) (Forall e) (Forall f) -> ((f + e * x) <= x) .=> ((star e * f) <= x) -- Collect the basic axioms in a list for easy reference - let kleene = [ qb par_assoc, qb par_comm, qb par_idem, qb par_zero - , qb seq_assoc, qb seq_zero, qb seq_one - , qb ldistrib, qb rdistrib - , qb unfold - , qb least_fix + let kleene = [ par_assoc, par_comm, par_idem, par_zero + , seq_assoc, seq_zero, seq_one + , ldistrib, rdistrib + , unfold + , least_fix ] -- Various proofs: