Skip to content

Commit

Permalink
KD: Get rid of the smt trivial proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Feb 4, 2025
1 parent 7af072e commit 40f690f
Show file tree
Hide file tree
Showing 6 changed files with 167 additions and 173 deletions.
13 changes: 1 addition & 12 deletions Data/SBV/Tools/KD/Kernel.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ module Data.SBV.Tools.KD.Kernel (
, lemma, lemmaWith, lemmaGen
, theorem, theoremWith
, InductionTactic(..)
, sorry, smt
, sorry
, checkSatThen
) where

Expand Down Expand Up @@ -98,17 +98,6 @@ sorry = Proof { rootOfTrust = Self
-- solver to determine as false, we avoid the constant folding.
p (Forall @"__sbvKD_sorry" (x :: SBool)) = label "SORRY: KnuckleDragger, proof uses \"sorry\"" x

-- | A manifestly true theorem. Not useful by itself, but it acts as a place holder in chain-proofs where
-- we're essentially telling SBV to prove the step without anything extra. The name is picked as smt to indicate the solver handles it.
smt :: Proof
smt = Proof { rootOfTrust = None
, isUserAxiom = False
, getProof = label "trivial" p
, getProp = toDyn p
, proofName = "smt"
}
where p = sTrue

-- | Helper to generate lemma/theorem statements.
lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen cfg@SMTConfig{kdOptions = KDOptions{measureTime}} tag nms inputProp by = do
Expand Down
24 changes: 16 additions & 8 deletions Data/SBV/Tools/KD/KnuckleDragger.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ module Data.SBV.Tools.KD.KnuckleDragger (
, induct, inductAlt1, inductAlt2
, inductiveLemma, inductiveLemmaWith
, inductiveTheorem, inductiveTheoremWith
, sorry, smt
, sorry
, KD, runKD, runKDWith, use
, (|-), (<:), (=:), (?), qed
) where
Expand Down Expand Up @@ -680,24 +680,32 @@ class ProofHint a b where
(?) :: a -> b -> ProofStep a
infixl 2 ?

-- | Giving just one proof as a helper
-- | Giving just one proof as a helper.
instance ProofHint a Proof where
a ? p = ProofStep a [p]

-- | Giving a bunch of proofs as a helper
-- | Giving a bunch of proofs as a helper.
instance ProofHint a [Proof] where
a ? ps = ProofStep a ps

-- | Chain steps in a calculational proof.
class ChainStep arg a where
(=:) :: arg -> [ProofStep a] -> [ProofStep a]
infixr 1 =:

-- | Chaining a step to another
instance ChainStep (ProofStep a) a where
a =: b = a : b

-- | Chaining a step to another
instance ChainStep a a where
a =: b = ProofStep a [] : b

-- | Start reasoning for the calculational proof.
(<:) :: a -> [ProofStep a] -> [ProofStep a]
a <: b = ProofStep a [] =: b
infixr 1 <:

-- | Chain steps in a calculational proof.
(=:) :: ProofStep a -> [ProofStep a] -> [ProofStep a]
a =: b = a : b
infixr 1 =:

-- | Mark the end of a calculational proof.
qed :: [ProofStep a]
qed = []
Expand Down
3 changes: 0 additions & 3 deletions Data/SBV/Tools/KnuckleDragger.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,6 @@ module Data.SBV.Tools.KnuckleDragger (
, inductiveLemma, inductiveLemmaWith
, inductiveTheorem, inductiveTheoremWith

-- * Proof by smt
, smt

-- * Creating instances of proofs
, at, Inst(..)

Expand Down
34 changes: 17 additions & 17 deletions Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,35 +68,35 @@ notDiv3 = runKDWith z3NoAutoConfig $ do
case0 <- chainLemma "case_n_mod_3_eq_0"
(\(Forall @"n" n) -> n `sEMod` 3 .== 0 .=> p n)
(\n -> n `sEMod` 3 .== 0 |- let w = some "witness" $ \k -> n .== 3*k
in s n <: s (3*w) ? smt
=: s (3*w) ? smt
=: 2*(3*w)*(3*w) + 3*w + 1 ? smt
=: 18*w*w + 3*w + 1 ? smt
=: 3*(6*w*w + w) + 1 ? smt
in s n <: s (3*w)
=: s (3*w)
=: 2*(3*w)*(3*w) + 3*w + 1
=: 18*w*w + 3*w + 1
=: 3*(6*w*w + w) + 1
=: qed)

-- Case 1: n = 1 (mod 3)
case1 <- chainLemma "case_n_mod_3_eq_1"
(\(Forall @"n" n) -> n `sEMod` 3 .== 1 .=> p n)
(\n -> n `sEMod` 3 .== 1 |- let w = some "witness" $ \k -> n .== 3*k + 1
in s n <: s (3*w+1) ? smt
=: 2*(3*w+1)*(3*w+1) + (3*w+1) + 1 ? smt
=: 2*(9*w*w + 3*w + 3*w + 1) + (3*w + 1) + 1 ? smt
=: 18*w*w + 12*w + 2 + 3*w + 2 ? smt
=: 18*w*w + 15*w + 4 ? smt
=: 3*(6*w*w + 5*w + 1) + 1 ? smt
in s n <: s (3*w+1)
=: 2*(3*w+1)*(3*w+1) + (3*w+1) + 1
=: 2*(9*w*w + 3*w + 3*w + 1) + (3*w + 1) + 1
=: 18*w*w + 12*w + 2 + 3*w + 2
=: 18*w*w + 15*w + 4
=: 3*(6*w*w + 5*w + 1) + 1
=: qed)

-- Case 2: n = 2 (mod 3)
case2 <- chainLemma "case_n_mod_3_eq_2"
(\(Forall @"n" n) -> n `sEMod` 3 .== 2 .=> p n)
(\n -> n `sEMod` 3 .== 2 |- let w = some "witness" $ \k -> n .== 3*k + 2
in s n <: s (3*w+2) ? smt
=: 2*(3*w+2)*(3*w+2) + (3*w+2) + 1 ? smt
=: 2*(9*w*w + 6*w + 6*w + 4) + (3*w + 2) + 1 ? smt
=: 18*w*w + 24*w + 8 + 3*w + 3 ? smt
=: 18*w*w + 27*w + 11 ? smt
=: 3*(6*w*w + 9*w + 3) + 2 ? smt
in s n <: s (3*w+2)
=: 2*(3*w+2)*(3*w+2) + (3*w+2) + 1
=: 2*(9*w*w + 6*w + 6*w + 4) + (3*w + 2) + 1
=: 18*w*w + 24*w + 8 + 3*w + 3
=: 18*w*w + 27*w + 11
=: 3*(6*w*w + 9*w + 3) + 2
=: qed)

-- Note that z3 is smart enough to figure out the above cases are complete, so
Expand Down
Loading

0 comments on commit 40f690f

Please sign in to comment.