| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.KnuckleDragger
Description
A lightweight theorem proving like interface, built on top of SBV. Inspired by and modeled after Philip Zucker's tool with the same name, see http://github.com/philzook58/knuckledragger.
See the directory Documentation.SBV.Examples.KnuckleDragger for various examples.
Synopsis
- type Proposition a = (QuantifiedBool a, QNot a, Skolemize (NegatesTo a), Satisfiable (Symbolic (SkolemsTo (NegatesTo a))), Constraint Symbolic (SkolemsTo (NegatesTo a)))
- data Proof
- axiom :: Proposition a => String -> a -> KD Proof
- lemma :: Proposition a => String -> a -> [Proof] -> KD Proof
- lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
- theorem :: Proposition a => String -> a -> [Proof] -> KD Proof
- theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
- chainLemma :: (ChainLemma steps step, Proposition a) => String -> a -> steps -> [Proof] -> KD Proof
- chainLemmaWith :: (ChainLemma steps step, Proposition a) => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
- chainTheorem :: (ChainLemma steps step, Proposition a) => String -> a -> steps -> [Proof] -> KD Proof
- chainTheoremWith :: (ChainLemma steps step, Proposition a) => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
- class Induction a where
- induct :: a -> Proof
- inductAlt1 :: a -> Proof
- inductAlt2 :: a -> Proof
- sorry :: Proof
- data KD a
- runKD :: KD a -> IO a
- runKDWith :: SMTConfig -> KD a -> IO a
Propositions and their proofs
type Proposition a = (QuantifiedBool a, QNot a, Skolemize (NegatesTo a), Satisfiable (Symbolic (SkolemsTo (NegatesTo a))), Constraint Symbolic (SkolemsTo (NegatesTo a))) Source #
Proof for a property. This type is left abstract, i.e., the only way to create on is via a
call to lemma/theorem etc., ensuring soundness. (Note that the trusted-code base here
is still large: The underlying solver, SBV, and KnuckleDragger kernel itself. But this
mechanism ensures we can't create proven things out of thin air, following the standard LCF
methodology.)
Adding axioms/definitions
axiom :: Proposition a => String -> a -> KD Proof Source #
Accept the given definition as a fact. Usually used to introduce definitial axioms,
giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions,
if you assert nonsense, then you get nonsense back. So, calls to axiom should be limited to
definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.
Basic proofs
lemma :: Proposition a => String -> a -> [Proof] -> KD Proof Source #
Prove a given statement, using auxiliaries as helpers. Using the default solver.
lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof Source #
Prove a given statement, using auxiliaries as helpers. Using the given solver.
theorem :: Proposition a => String -> a -> [Proof] -> KD Proof Source #
Prove a given statement, using auxiliaries as helpers. Essentially the same as lemma, except for the name, using the default solver.
theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof Source #
Prove a given statement, using auxiliaries as helpers. Essentially the same as lemmaWith, except for the name.
Chain of reasoning
chainLemma :: (ChainLemma steps step, Proposition a) => String -> a -> steps -> [Proof] -> KD Proof Source #
Prove a property via a series of equality steps, using the default solver.
Let H be a list of already established lemmas. Let P be a property we wanted to prove, named name.
Consider a call of the form chainLemma name P [A, B, C, D] H. Note that H is
a list of already proven facts, ensured by the type signature. We proceed as follows:
- Prove:
H -> A == B - Prove:
H && A == B -> B == C - Prove:
H && A == B && B == C -> C == D - Prove:
H && A == B && B == C && C == D -> P - If all of the above steps succeed, conclude
P.
Note that if the type of steps (i.e., A .. D above) is SBool, then we use implication
as opposed to equality; which better captures line of reasoning.
So, chain-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning in the case of non-boolean steps.
If there are no helpers given (i.e., if H is empty), then this call is equivalent to lemmaWith.
If H is a singleton, then we error-out. A single step in H indicates a user-error, since there's
no sequence of steps to reason about.
chainLemmaWith :: (ChainLemma steps step, Proposition a) => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof Source #
Prove a property via a series of equality steps, using the given solver.
chainTheorem :: (ChainLemma steps step, Proposition a) => String -> a -> steps -> [Proof] -> KD Proof Source #
Same as chainLemma, except tagged as Theorem
chainTheoremWith :: (ChainLemma steps step, Proposition a) => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof Source #
Same as chainLemmaWith, except tagged as Theorem
Induction
class Induction a where Source #
Given a predicate, return an induction principle for it. Typically, we only have one viable induction principle for a given type, but we allow for alternative ones.
Minimal complete definition
Instances
| (SymVal a, SymVal b, SymVal c) => Induction (SBV a -> SBV b -> SBV c -> SInteger -> SBool) Source # | Induction over four argument predicates, with last argument SInteger. |
| (SymVal a, SymVal b, SymVal c, SymVal e) => Induction (SBV a -> SBV b -> SBV c -> SList e -> SBool) Source # | Induction over four argument predicates, with last argument a list. |
| (SymVal a, SymVal b) => Induction (SBV a -> SBV b -> SInteger -> SBool) Source # | Induction over three argument predicates, with last argument SInteger. |
| (SymVal a, SymVal b, SymVal e) => Induction (SBV a -> SBV b -> SList e -> SBool) Source # | Induction over three argument predicates, with last argument a list. |
| SymVal a => Induction (SBV a -> SInteger -> SBool) Source # | Induction over two argument predicates, with the last argument SInteger. |
| (SymVal a, SymVal e) => Induction (SBV a -> SList e -> SBool) Source # | Induction over two argument predicates, with last argument a list. |
| Induction (SInteger -> SBool) Source # | Induction over SInteger. We provide various induction principles here: The first one is over naturals, will only prove predicates that explicitly restrict the argument to >= 0. The second and third ones are induction over the entire range of integers, two different principles that might work better for different problems. |
| SymVal a => Induction (SList a -> SBool) Source # | Induction over lists |
Faking proofs
A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver
cannot deal with, or if we want to postpone the proof for the time being. KnuckleDragger will keep
track of the uses of sorry and will print them appropriately while printing proofs.