diff --git a/Data/SBV/Tools/KD/Kernel.hs b/Data/SBV/Tools/KD/Kernel.hs index d490b7b6..d294b48d 100644 --- a/Data/SBV/Tools/KD/Kernel.hs +++ b/Data/SBV/Tools/KD/Kernel.hs @@ -25,7 +25,7 @@ module Data.SBV.Tools.KD.Kernel ( , lemma, lemmaWith, lemmaGen , theorem, theoremWith , InductionTactic(..) - , sorry, smt + , sorry , checkSatThen ) where @@ -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 diff --git a/Data/SBV/Tools/KD/KnuckleDragger.hs b/Data/SBV/Tools/KD/KnuckleDragger.hs index 95088837..c4b851ac 100644 --- a/Data/SBV/Tools/KD/KnuckleDragger.hs +++ b/Data/SBV/Tools/KD/KnuckleDragger.hs @@ -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 @@ -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 = [] diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs index b250f757..dd67c3d1 100644 --- a/Data/SBV/Tools/KnuckleDragger.hs +++ b/Data/SBV/Tools/KnuckleDragger.hs @@ -35,9 +35,6 @@ module Data.SBV.Tools.KnuckleDragger ( , inductiveLemma, inductiveLemmaWith , inductiveTheorem, inductiveTheoremWith - -- * Proof by smt - , smt - -- * Creating instances of proofs , at, Inst(..) diff --git a/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs b/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs index 1a03a636..a56257e8 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs @@ -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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs b/Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs index 8d43e66f..cf4d53d3 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/ShefferStroke.hs @@ -370,9 +370,9 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = commut <- chainLemma "a | b = b | a" (\AB -> a ⏐ b .== b ⏐ a) $ \a b -> sTrue |- a ⏐ b <: ﬧﬧ(a ⏐ b) ? sh1 =: ﬧﬧ(a ⏐ ﬧﬧ b) ? sh1 - =: ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b)) ? smt + =: ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b)) =: ﬧ ((ﬧﬧ b ⏐ a) ⏐ (ﬧﬧ b ⏐ a)) ? sh3 - =: ﬧﬧ(ﬧﬧ b ⏐ a) ? smt + =: ﬧﬧ(ﬧﬧ b ⏐ a) =: ﬧﬧ b ⏐ a ? sh1 =: b ⏐ a ? sh1 =: qed @@ -398,60 +398,60 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = compl2 <- lemma "a ⊓ aᶜ = ⲳ" (\A -> a ⨅ ﬧ a .== ⲳ) [sh1, commut, all_bot] bound1 <- chainLemma "a ⊔ т = т" (\A -> a ⨆ т .== т) $ - \a -> sTrue |- a ⨆ т <: (a ⨆ т) ⨅ т ? ident2 - =: т ⨅ (a ⨆ т) ? commut2 - =: (a ⨆ ﬧ a) ⨅ (a ⨆ т) ? compl1 - =: a ⨆ (ﬧ a ⨅ т) ? distrib1 - =: a ⨆ ﬧ a ? ident2 - =: (т :: SStroke) ? compl1 - =: qed + \(a :: SStroke) -> sTrue |- a ⨆ т <: (a ⨆ т) ⨅ т ? ident2 + =: т ⨅ (a ⨆ т) ? commut2 + =: (a ⨆ ﬧ a) ⨅ (a ⨆ т) ? compl1 + =: a ⨆ (ﬧ a ⨅ т) ? distrib1 + =: a ⨆ ﬧ a ? ident2 + =: (т :: SStroke) ? compl1 + =: qed bound2 <- chainLemma "a ⊓ ⲳ = ⲳ" (\A -> a ⨅ ⲳ .== ⲳ) $ - \a -> sTrue |- a ⨅ ⲳ <: (a ⨅ ⲳ) ⨆ ⲳ ? ident1 - =: ⲳ ⨆ (a ⨅ ⲳ) ? commut1 - =: (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ? compl2 - =: a ⨅ (ﬧ a ⨆ ⲳ) ? distrib2 - =: a ⨅ ﬧ a ? ident1 - =: (ⲳ :: SStroke) ? compl2 - =: qed + \(a :: SStroke) -> sTrue |- a ⨅ ⲳ <: (a ⨅ ⲳ) ⨆ ⲳ ? ident1 + =: ⲳ ⨆ (a ⨅ ⲳ) ? commut1 + =: (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ? compl2 + =: a ⨅ (ﬧ a ⨆ ⲳ) ? distrib2 + =: a ⨅ ﬧ a ? ident1 + =: (ⲳ :: SStroke) ? compl2 + =: qed absorb1 <- chainLemma "a ⊔ (a ⊓ b) = a" (\AB -> a ⨆ (a ⨅ b) .== a) $ - \a b -> sTrue |- a ⨆ (a ⨅ b) <: (a ⨅ т) ⨆ (a ⨅ b) ? ident2 - =: a ⨅ (т ⨆ b) ? distrib2 - =: a ⨅ (b ⨆ т) ? commut1 - =: a ⨅ т ? bound1 - =: (a :: SStroke) ? ident2 - =: qed + \(a :: SStroke) b -> sTrue |- a ⨆ (a ⨅ b) <: (a ⨅ т) ⨆ (a ⨅ b) ? ident2 + =: a ⨅ (т ⨆ b) ? distrib2 + =: a ⨅ (b ⨆ т) ? commut1 + =: a ⨅ т ? bound1 + =: a ? ident2 + =: qed absorb2 <- chainLemma "a ⊓ (a ⊔ b) = a" (\AB -> a ⨅ (a ⨆ b) .== a) $ - \a b -> sTrue |- a ⨅ (a ⨆ b) <: (a ⨆ ⲳ) ⨅ (a ⨆ b) ? ident1 - =: a ⨆ (ⲳ ⨅ b) ? distrib1 - =: a ⨆ (b ⨅ ⲳ) ? commut2 - =: a ⨆ ⲳ ? bound2 - =: (a :: SStroke) ? ident1 - =: qed + \(a :: SStroke) b -> sTrue |- a ⨅ (a ⨆ b) <: (a ⨆ ⲳ) ⨅ (a ⨆ b) ? ident1 + =: a ⨆ (ⲳ ⨅ b) ? distrib1 + =: a ⨆ (b ⨅ ⲳ) ? commut2 + =: a ⨆ ⲳ ? bound2 + =: a ? ident1 + =: qed idemp2 <- chainLemma "a ⊓ a = a" (\A -> a ⨅ a .== a) $ - \a -> sTrue |- a ⨅ a <: a ⨅ (a ⨆ (ⲳ :: SStroke)) ? ident1 - =: a ? absorb2 - =: qed + \(a :: SStroke) -> sTrue |- a ⨅ a <: a ⨅ (a ⨆ ⲳ) ? ident1 + =: a ? absorb2 + =: qed inv <- chainLemma "a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ" (\AAp -> a ⨆ a' .== т .=> a ⨅ a' .== ⲳ .=> a' .== ﬧ a) $ - \a a' -> a ⨆ a' .== т .&& a ⨅ a' .== ⲳ - |- a' <: a' ⨅ т ? ident2 - =: a' ⨅ (a ⨆ ﬧ a) ? compl1 - =: (a' ⨅ a) ⨆ (a' ⨅ ﬧ a) ? distrib2 - =: (a' ⨅ a) ⨆ (ﬧ a ⨅ a') ? commut2 - =: (a ⨅ a') ⨆ (ﬧ a ⨅ a') ? commut2 - =: ⲳ ⨆ (ﬧ a ⨅ a') ? compl2 - =: (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ? compl2 - =: (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ? commut2 - =: ﬧ a ⨅ (a ⨆ a') ? distrib2 - =: ﬧ a ⨅ т ? smt - =: (ﬧ a :: SStroke) ? ident2 - =: qed + \(a :: SStroke) a' -> a ⨆ a' .== т .&& a ⨅ a' .== ⲳ + |- a' <: a' ⨅ т ? ident2 + =: a' ⨅ (a ⨆ ﬧ a) ? compl1 + =: (a' ⨅ a) ⨆ (a' ⨅ ﬧ a) ? distrib2 + =: (a' ⨅ a) ⨆ (ﬧ a ⨅ a') ? commut2 + =: (a ⨅ a') ⨆ (ﬧ a ⨅ a') ? commut2 + =: ⲳ ⨆ (ﬧ a ⨅ a') ? compl2 + =: (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ? compl2 + =: (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ? commut2 + =: ﬧ a ⨅ (a ⨆ a') ? distrib2 + =: ﬧ a ⨅ т + =: ﬧ a ? ident2 + =: qed dne <- lemma "aᶜᶜ = a" (\A -> ﬧﬧ a .== a) [inv, compl1, compl2, commut1, commut2] inv_elim <- lemma "aᶜ = bᶜ → a = b" (\AB -> ﬧ a .== ﬧ b .=> a .== b) [dne] @@ -459,22 +459,22 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = cancel <- lemma "a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b" (\AB -> a ⨆ ﬧ b .== т .=> a ⨅ ﬧ b .== ⲳ .=> a .== b) [inv, inv_elim] a1 <- chainLemma "a ⊔ (aᶜ ⊔ b) = т" (\AB -> a ⨆ (ﬧ a ⨆ b) .== т) $ - \a b -> sTrue |- a ⨆ (ﬧ a ⨆ b) <: (a ⨆ (ﬧ a ⨆ b)) ⨅ т ? ident2 - =: т ⨅ (a ⨆ (ﬧ a ⨆ b)) ? commut2 - =: (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ? compl1 - =: a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b)) ? distrib1 - =: a ⨆ ﬧ a ? absorb2 - =: (т :: SStroke) ? compl1 - =: qed + \(a :: SStroke) b -> sTrue |- a ⨆ (ﬧ a ⨆ b) <: (a ⨆ (ﬧ a ⨆ b)) ⨅ т ? ident2 + =: т ⨅ (a ⨆ (ﬧ a ⨆ b)) ? commut2 + =: (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ? compl1 + =: a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b)) ? distrib1 + =: a ⨆ ﬧ a ? absorb2 + =: (т :: SStroke) ? compl1 + =: qed a2 <- chainLemma "a ⊓ (aᶜ ⊓ b) = ⲳ" (\AB -> a ⨅ (ﬧ a ⨅ b) .== ⲳ) $ - \a b -> sTrue |- a ⨅ (ﬧ a ⨅ b) <: (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ ? ident1 - =: ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b)) ? commut1 - =: (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ? compl2 - =: a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b)) ? distrib2 - =: a ⨅ ﬧ a ? absorb1 - =: (ⲳ :: SStroke) ? compl2 - =: qed + \(a :: SStroke) b -> sTrue |- a ⨅ (ﬧ a ⨅ b) <: (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ ? ident1 + =: ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b)) ? commut1 + =: (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ? compl2 + =: a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b)) ? distrib2 + =: a ⨅ ﬧ a ? absorb1 + =: (ⲳ :: SStroke) ? compl2 + =: qed dm1 <- lemma "(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ" (\AB -> ﬧ(a ⨆ b) .== ﬧ a ⨅ ﬧ b) [a1, a2, dne, commut1, commut2, ident1, ident2, distrib1, distrib2] @@ -493,30 +493,30 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = [distrib1, absorb1, absorb2, commut2] f1 <- chainLemma "(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ b .== т) $ - \a b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨆ ﬧ b <: ﬧ b ⨆ (a ⨆ (b ⨆ c)) ? commut1 - =: (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т ? ident2 - =: т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? commut2 - =: (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? compl1 - =: (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? commut1 - =: ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c))) ? distrib1 - =: ﬧ b ⨆ b ? e1 - =: b ⨆ ﬧ b ? commut1 - =: (т :: SStroke) ? compl1 - =: qed + \(a :: SStroke) b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨆ ﬧ b <: ﬧ b ⨆ (a ⨆ (b ⨆ c)) ? commut1 + =: (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т ? ident2 + =: т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? commut2 + =: (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? compl1 + =: (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ? commut1 + =: ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c))) ? distrib1 + =: ﬧ b ⨆ b ? e1 + =: b ⨆ ﬧ b ? commut1 + =: (т :: SStroke) ? compl1 + =: qed g1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ cᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ c .== т) [commut1, f1] h1 <- chainLemma "(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ a .== ⲳ) $ - \a b c -> sTrue |- ﬧ(a ⨆ b ⨆ c) ⨅ a <: a ⨅ ﬧ (a ⨆ b ⨆ c) ? commut2 - =: a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? dm1 - =: (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ ? ident1 - =: ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? commut1 - =: (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? compl2 - =: a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? distrib2 - =: a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b))) ? commut2 - =: a ⨅ ﬧ a ? e2 - =: (ⲳ :: SStroke) ? compl2 - =: qed + \(a :: SStroke) b c -> sTrue |- ﬧ(a ⨆ b ⨆ c) ⨅ a <: a ⨅ ﬧ (a ⨆ b ⨆ c) ? commut2 + =: a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? dm1 + =: (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ ? ident1 + =: ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? commut1 + =: (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? compl2 + =: a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ? distrib2 + =: a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b))) ? commut2 + =: a ⨅ ﬧ a ? e2 + =: (ⲳ :: SStroke) ? compl2 + =: qed i1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ b .== ⲳ) [commut1, h1] j1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ c .== ⲳ) [a2, dne, commut2] @@ -524,56 +524,56 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = assoc1 <- do c1 <- chainLemma "(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) .== т) $ - \a b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) - <: (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? dm1 - =: ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ? distrib1 - =: ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т ? g1 - =: (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b) ? ident2 - =: ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? distrib1 - =: т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? d1 - =: т ⨅ т ? f1 - =: (т :: SStroke) ? idemp2 - =: qed + \(a :: SStroke) b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) + <: (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c) ? dm1 + =: ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ? distrib1 + =: ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т ? g1 + =: (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b) ? ident2 + =: ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? distrib1 + =: т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b) ? d1 + =: т ⨅ (т :: SStroke) ? f1 + =: (т :: SStroke) ? idemp2 + =: qed c2 <- chainLemma "(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ" (\ABC -> (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) .== ⲳ) $ - \a b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) - <: ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c)) ? commut2 - =: (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ? distrib2 - =: (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut2 - =: (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut2 - =: ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? h1 - =: ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ ? commut1 - =: (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c) ? ident1 - =: ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c) ? commut2 - =: (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c) ? distrib2 - =: (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ ? j1 - =: ⲳ ⨆ ⲳ ? i1 - =: (ⲳ :: SStroke) ? ident1 - =: qed + \(a :: SStroke) b c -> sTrue |- (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) + <: ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c)) ? commut2 + =: (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ? distrib2 + =: (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut2 + =: (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? commut2 + =: ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ? h1 + =: ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ ? commut1 + =: (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c) ? ident1 + =: ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c) ? commut2 + =: (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c) ? distrib2 + =: (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ ? j1 + =: ⲳ ⨆ (ⲳ :: SStroke) ? i1 + =: (ⲳ :: SStroke) ? ident1 + =: qed lemma "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c" (\ABC -> a ⨆ (b ⨆ c) .== (a ⨆ b) ⨆ c) [c1, c2, cancel] assoc2 <- chainLemma "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c" (\ABC -> a ⨅ (b ⨅ c) .== (a ⨅ b) ⨅ c) $ - \a b c -> sTrue |- a ⨅ (b ⨅ c) <: ﬧﬧ(a ⨅ (b ⨅ c)) ? dne - =: ﬧﬧ((a ⨅ b) ⨅ c) ? assoc1 - =: ((a ⨅ b) ⨅ (c :: SStroke)) ? dne - =: qed + \(a :: SStroke) b c -> sTrue |- a ⨅ (b ⨅ c) <: ﬧﬧ(a ⨅ (b ⨅ c)) ? dne + =: ﬧﬧ((a ⨅ b) ⨅ c) ? assoc1 + =: ((a ⨅ b) ⨅ c) ? dne + =: qed le_antisymm <- chainLemma "a ≤ b → b ≤ a → a = b" (\AB -> a ≤ b .=> b ≤ a .=> a .== b) $ - \a b -> a ≤ b .&& b ≤ a |- a <: b ⨅ a ? smt - =: a ⨅ b ? commut2 - =: (b :: SStroke) ? smt - =: qed + \(a :: SStroke) b -> a ≤ b .&& b ≤ a |- a <: b ⨅ a + =: a ⨅ b ? commut2 + =: b + =: qed le_refl <- lemma "a ≤ a" (\A -> a ≤ a) [idemp2] le_trans <- chainLemma "a ≤ b → b ≤ c → a ≤ c" (\ABC -> a ≤ b .=> b ≤ c .=> a ≤ c) $ - \a b c -> a ≤ b .&& b ≤ c |- a <: b ⨅ a ? smt - =: (c ⨅ b) ⨅ a ? smt - =: c ⨅ (b ⨅ a) ? assoc2 - =: (c ⨅ a :: SStroke) ? smt - =: qed + \(a :: SStroke) b c -> a ≤ b .&& b ≤ c |- a <: b ⨅ a + =: (c ⨅ b) ⨅ a + =: c ⨅ (b ⨅ a) ? assoc2 + =: (c ⨅ a) + =: qed lt_iff_le_not_le <- lemma "a < b ↔ a ≤ b ∧ ¬b ≤ a" (\AB -> (a < b) .<=> a ≤ b .&& sNot (b ≤ a)) [sh3] @@ -582,19 +582,19 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = sup_le <- chainLemma "a ≤ c → b ≤ c → a ⊔ b ≤ c" (\ABC -> a ≤ c .=> b ≤ c .=> a ⨆ b ≤ c) $ - \a b c -> a ≤ c .&& b ≤ c |- a ⨆ b <: (c ⨅ a) ⨆ (c ⨅ b) ? smt - =: (c ⨅ (a ⨆ b) :: SStroke) ? distrib2 - =: qed + \(a :: SStroke) b c -> a ≤ c .&& b ≤ c |- a ⨆ b <: (c ⨅ a) ⨆ (c ⨅ b) + =: c ⨅ (a ⨆ b) ? distrib2 + =: qed inf_le_left <- lemma "a ⊓ b ≤ a" (\AB -> a ⨅ b ≤ a) [assoc2, idemp2] inf_le_right <- lemma "a ⊓ b ≤ b" (\AB -> a ⨅ b ≤ b) [commut2, inf_le_left] le_inf <- chainLemma "a ≤ b → a ≤ c → a ≤ b ⊓ c" (\ABC -> a ≤ b .=> a ≤ c .=> a ≤ b ⨅ c) $ - \a b c -> a ≤ b .&& a ≤ c |- a <: b ⨅ a ? smt - =: b ⨅ (c ⨅ a) ? smt - =: (b ⨅ c ⨅ a :: SStroke) ? assoc2 - =: qed + \(a :: SStroke) b c -> a ≤ b .&& a ≤ c |- a <: b ⨅ a + =: b ⨅ (c ⨅ a) + =: (b ⨅ c ⨅ a) ? assoc2 + =: qed le_sup_inf <- lemma "(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z" (\XYZ -> (x ⨆ y) ⨅ (x ⨆ z) ≤ x ⨆ y ⨅ z) @@ -604,18 +604,18 @@ shefferBooleanAlgebra = runKDWith z3{kdOptions = (kdOptions z3) {ribbonLength = top_le_sup_compl <- lemma "⊤ ≤ x ⊔ xᶜ" (\X -> т ≤ x ⨆ ﬧ x) [compl1, le_refl] le_top <- chainLemma "a ≤ ⊤" (\A -> a ≤ т) $ - \a -> sTrue |- a ≤ т <: a .== т ⨅ a ? smt - =: a .== a ⨅ т ? commut2 - =: a .== (a :: SStroke) ? ident2 - =: qed + \(a :: SStroke)-> sTrue |- a ≤ т <: a .== т ⨅ a + =: a .== a ⨅ т ? commut2 + =: a .== a ? ident2 + =: qed bot_le <- chainLemma "⊥ ≤ a" (\A -> ⲳ ≤ a) $ - \a -> sTrue |- ⲳ ≤ a <: ⲳ .== a ⨅ (ⲳ :: SStroke) ? smt - =: (ⲳ .== (ⲳ :: SStroke)) ? bound2 - =: qed + \(a :: SStroke) -> sTrue |- ⲳ ≤ a <: ⲳ .== a ⨅ ⲳ + =: (ⲳ .== (ⲳ :: SStroke)) ? bound2 + =: qed - sdiff_eq <- lemma "x \\ y = x ⊓ yᶜ" (\XY -> x \\ y .== x ⨅ ﬧ y) [smt] - himp_eq <- lemma "x ⇨ y = y ⊔ xᶜ" (\XY -> x ⇨ y .== y ⨆ ﬧ x) [smt] + sdiff_eq <- lemma "x \\ y = x ⊓ yᶜ" (\XY -> x \\ y .== x ⨅ ﬧ y) [] + himp_eq <- lemma "x ⇨ y = y ⊔ xᶜ" (\XY -> x ⇨ y .== y ⨆ ﬧ x) [] pure BooleanAlgebraProof { le_refl {- ∀ (a : α), a ≤ a -} = le_refl diff --git a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs index 3646e094..db9ba95e 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs @@ -76,7 +76,7 @@ sqrt2IsIrrational = runKD $ do oddSquaredIsOdd <- chainLemma "oddSquaredIsOdd" (\(Forall @"a" a) -> odd a .=> odd (sq a)) (\a -> odd a |- let k = some "w" (\kv -> a .== 2*kv+1) - in sq a <: sq (2 * k + 1) ? smt + in sq a <: sq (2 * k + 1) =: qed) -- Prove that if a perfect square is even, then it be the square of an even number. For z3, the above proof @@ -90,7 +90,7 @@ sqrt2IsIrrational = runKD $ do evenSquaredIsMult4 <- chainLemma "evenSquaredIsMult4" (\(Forall @"a" a) -> even a .=> 4 `sDivides` sq a) (\a -> even a |- let k = some "w" (\kv -> a .== 2*kv) - in sq a <: sq (k * 2) ? smt + in sq a <: sq (k * 2) =: qed) -- Define what it means to be co-prime. Note that we use euclidian notion of modulus here