Safe Haskell  SafeInferred 

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
(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 #  
Eq (Derivation f) Source #  
Defined in Twee.Proof (==) :: Derivation f > Derivation f > Bool # (/=) :: Derivation f > Derivation f > Bool #  
(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 rightassociated * Each Cong has at least one nonRefl 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 nonRefl 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 #
Prettyprinting 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.