Safe Haskell | None |
---|---|
Language | Haskell2010 |
Equational proofs which are checked for correctedness.
Synopsis
- data Proof f
- data Derivation f
- = UseLemma !(Proof f) !(Subst f)
- | UseAxiom !(Axiom f) !(Subst f)
- | Refl !(Term f)
- | Symm !(Derivation f)
- | Trans !(Derivation f) !(Derivation f)
- | Cong !(Fun f) ![Derivation f]
- data Axiom f = Axiom {
- axiom_number :: !Int
- axiom_name :: !String
- axiom_eqn :: !(Equation f)
- certify :: Function f => Derivation f -> Proof f
- equation :: Proof f -> Equation f
- derivation :: Proof f -> Derivation f
- lemma :: Proof f -> Subst f -> Derivation f
- autoSubst :: Equation f -> Subst f
- simpleLemma :: Function f => Proof f -> Derivation f
- axiom :: Axiom f -> Derivation f
- symm :: Derivation f -> Derivation f
- trans :: Derivation f -> Derivation f -> Derivation f
- cong :: Fun f -> [Derivation f] -> Derivation f
- congPath :: [Int] -> Term f -> Derivation f -> Derivation f
- simplify :: Function f => Derivation f -> Derivation f
- steps :: Function f => Derivation f -> [Derivation f]
- usedLemmas :: Derivation f -> [Proof f]
- usedAxioms :: Derivation f -> [Axiom f]
- usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
- usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]
- groundAxiomsAndSubsts :: Function f => Derivation f -> Map (Axiom f) (Set (Subst f))
- eliminateDefinitions :: Function f => [Axiom f] -> Derivation f -> Derivation f
- eliminateDefinitionsFromGoal :: Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f
- data Config f = Config {
- cfg_all_lemmas :: !Bool
- cfg_no_lemmas :: !Bool
- cfg_ground_proof :: !Bool
- cfg_show_instances :: !Bool
- cfg_use_colour :: !Bool
- cfg_show_uses_of_axioms :: Axiom f -> Bool
- defaultConfig :: Config f
- data Presentation f = Presentation {
- pres_axioms :: [Axiom f]
- pres_lemmas :: [Proof f]
- pres_goals :: [ProvedGoal f]
- data ProvedGoal f = ProvedGoal {
- pg_number :: Int
- pg_name :: String
- pg_proof :: Proof f
- pg_goal_hint :: Equation f
- pg_witness_hint :: Subst f
- provedGoal :: Int -> String -> Proof f -> ProvedGoal f
- checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f
- pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
- present :: Function f => Config f -> [ProvedGoal f] -> Presentation f
- describeEquation :: Function f => String -> String -> Maybe String -> Equation f -> Doc
Constructing proofs
A checked proof. If you have a value of type Proof f
,
it should jolly well represent a valid proof!
The only way to construct a Proof f
is by using certify
.
data Derivation f Source #
A derivation is an unchecked proof. It might be wrong!
The way to check it is to call certify
to turn it into a Proof
.
UseLemma !(Proof f) !(Subst f) | Apply an existing rule (with proof!) to the root of a term |
UseAxiom !(Axiom f) !(Subst f) | Apply an axiom to the root of a term |
Refl !(Term f) | Reflexivity. |
Symm !(Derivation f) | Symmetry |
Trans !(Derivation f) !(Derivation f) | Transivitity |
Cong !(Fun f) ![Derivation f] | Congruence. Parallel, i.e., takes a function symbol and one derivation for each argument of that function. |
Instances
Eq (Derivation f) Source # | |
Defined in Twee.Proof (==) :: Derivation f -> Derivation f -> Bool # (/=) :: Derivation f -> Derivation f -> Bool # | |
(Labelled f, Show f) => Show (Derivation f) Source # | |
Defined in Twee.Proof showsPrec :: Int -> Derivation f -> ShowS # show :: Derivation f -> String # showList :: [Derivation f] -> ShowS # | |
(Labelled f, PrettyTerm f) => Pretty (Derivation f) Source # | |
Defined in Twee.Proof pPrintPrec :: PrettyLevel -> Rational -> Derivation f -> Doc # pPrint :: Derivation f -> Doc # pPrintList :: PrettyLevel -> [Derivation f] -> Doc # | |
Symbolic (Derivation f) Source # | |
Defined in Twee.Proof type ConstantOf (Derivation f) Source # termsDL :: Derivation f -> DList (TermListOf (Derivation f)) Source # subst_ :: (Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f Source # | |
type ConstantOf (Derivation f) Source # | |
Defined in Twee.Proof |
Axiom | |
|
certify :: Function f => Derivation f -> Proof f Source #
Checks a Derivation
and, if it is correct, returns a
certified Proof
.
If the Derivation
is incorrect, throws an exception.
derivation :: Proof f -> Derivation f Source #
Smart constructors for derivations
simpleLemma :: Function f => Proof f -> Derivation f Source #
axiom :: Axiom f -> Derivation f Source #
symm :: Derivation f -> Derivation f Source #
trans :: Derivation f -> Derivation f -> Derivation f Source #
cong :: Fun f -> [Derivation f] -> Derivation f Source #
congPath :: [Int] -> Term f -> Derivation f -> Derivation f Source #
Applies a derivation at a particular path in a term.
Analysing proofs
simplify :: Function f => Derivation f -> Derivation f Source #
Simplify a derivation so that: * Symm occurs innermost * Trans is right-associated * Each Cong has at least one non-Refl argument * Refl is not used unnecessarily
steps :: Function f => Derivation f -> [Derivation f] Source #
Transform a derivation into a list of single steps. Each step has the following form: * Trans does not occur * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom * Each Cong has exactly one non-Refl argument (no parallel rewriting) * Refl only occurs as an argument to Cong
usedLemmas :: Derivation f -> [Proof f] Source #
Find all lemmas which are used in a derivation.
usedAxioms :: Derivation f -> [Axiom f] Source #
Find all axioms which are used in a derivation.
usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)] Source #
Find all lemmas which are used in a derivation, together with the substitutions used.
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)] Source #
Find all axioms which are used in a derivation, together with the substitutions used.
groundAxiomsAndSubsts :: Function f => Derivation f -> Map (Axiom f) (Set (Subst f)) Source #
Find all ground instances of axioms which are used in the expanded form of a derivation (no lemmas).
eliminateDefinitions :: Function f => [Axiom f] -> Derivation f -> Derivation f Source #
eliminateDefinitionsFromGoal :: Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f Source #
Pretty-printing proofs
Options for proof presentation.
Config | |
|
defaultConfig :: Config f Source #
The default configuration.
data Presentation f Source #
A proof, with all axioms and lemmas explicitly listed.
Presentation | |
|
Instances
(Labelled f, Show f) => Show (Presentation f) Source # | |
Defined in Twee.Proof showsPrec :: Int -> Presentation f -> ShowS # show :: Presentation f -> String # showList :: [Presentation f] -> ShowS # | |
Function f => Pretty (Presentation f) Source # | |
Defined in Twee.Proof pPrintPrec :: PrettyLevel -> Rational -> Presentation f -> Doc # pPrint :: Presentation f -> Doc # pPrintList :: PrettyLevel -> [Presentation f] -> Doc # |
data ProvedGoal f Source #
ProvedGoal | |
|
Instances
(Labelled f, Show f) => Show (ProvedGoal f) Source # | |
Defined in Twee.Proof showsPrec :: Int -> ProvedGoal f -> ShowS # show :: ProvedGoal f -> String # showList :: [ProvedGoal f] -> ShowS # |
provedGoal :: Int -> String -> Proof f -> ProvedGoal f Source #
Construct a ProvedGoal
.
checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f Source #
Check that pg_goal/pg_witness match up with pg_proof.
pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc Source #
Print a presented proof.
present :: Function f => Config f -> [ProvedGoal f] -> Presentation f Source #
Simplify and present a proof.