twee-lib-2.2: An equational theorem prover

Safe HaskellNone
LanguageHaskell2010

Twee.Proof

Contents

Description

Equational proofs which are checked for correctedness.

Synopsis

Constructing proofs

data Proof f Source #

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.

Instances
Eq (Proof f) Source # 
Instance details

Defined in Twee.Proof

Methods

(==) :: Proof f -> Proof f -> Bool #

(/=) :: Proof f -> Proof f -> Bool #

Ord (Proof f) Source # 
Instance details

Defined in Twee.Proof

Methods

compare :: Proof f -> Proof f -> Ordering #

(<) :: Proof f -> Proof f -> Bool #

(<=) :: Proof f -> Proof f -> Bool #

(>) :: Proof f -> Proof f -> Bool #

(>=) :: Proof f -> Proof f -> Bool #

max :: Proof f -> Proof f -> Proof f #

min :: Proof f -> Proof f -> Proof f #

Show (Proof f) Source # 
Instance details

Defined in Twee.Proof

Methods

showsPrec :: Int -> Proof f -> ShowS #

show :: Proof f -> String #

showList :: [Proof f] -> ShowS #

Function f => Pretty (Proof f) Source # 
Instance details

Defined in Twee.Proof

f ~ g => Has (ActiveRule f) (Proof g) Source # 
Instance details

Defined in Twee

Methods

the :: ActiveRule f -> Proof g Source #

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.

Constructors

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. Refl t proves t = t.

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 # 
Instance details

Defined in Twee.Proof

Methods

(==) :: Derivation f -> Derivation f -> Bool #

(/=) :: Derivation f -> Derivation f -> Bool #

Show (Derivation f) Source # 
Instance details

Defined in Twee.Proof

PrettyTerm f => Pretty (Derivation f) Source # 
Instance details

Defined in Twee.Proof

Symbolic (Derivation f) Source # 
Instance details

Defined in Twee.Proof

Associated Types

type ConstantOf (Derivation f) :: Type Source #

type ConstantOf (Derivation f) Source # 
Instance details

Defined in Twee.Proof

type ConstantOf (Derivation f) = f

data Axiom f Source #

Constructors

Axiom 

Fields

  • axiom_number :: !Int

    The number of the axiom. Has no semantic meaning; for convenience only.

  • axiom_name :: !String

    A description of the axiom. Has no semantic meaning; for convenience only.

  • axiom_eqn :: !(Equation f)

    The equation which the axiom asserts.

Instances
Eq (Axiom f) Source # 
Instance details

Defined in Twee.Proof

Methods

(==) :: Axiom f -> Axiom f -> Bool #

(/=) :: Axiom f -> Axiom f -> Bool #

Ord (Axiom f) Source # 
Instance details

Defined in Twee.Proof

Methods

compare :: Axiom f -> Axiom f -> Ordering #

(<) :: Axiom f -> Axiom f -> Bool #

(<=) :: Axiom f -> Axiom f -> Bool #

(>) :: Axiom f -> Axiom f -> Bool #

(>=) :: Axiom f -> Axiom f -> Bool #

max :: Axiom f -> Axiom f -> Axiom f #

min :: Axiom f -> Axiom f -> Axiom f #

Show (Axiom f) Source # 
Instance details

Defined in Twee.Proof

Methods

showsPrec :: Int -> Axiom f -> ShowS #

show :: Axiom f -> String #

showList :: [Axiom f] -> ShowS #

PrettyTerm f => Pretty (Axiom f) Source # 
Instance details

Defined in Twee.Proof

certify :: PrettyTerm 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.

Smart constructors for derivations

congPath :: [Int] -> Term f -> Derivation f -> Derivation f Source #

Applies a derivation at a particular path in a term.

Analysing proofs

simplify :: Minimal f => (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f Source #

Simplify a derivation.

After simplification, a derivation has the following properties:

  • Symm is pushed down next to Lemma and Axiom
  • Refl only occurs inside Cong or at the top level
  • Trans is right-associated and is pushed inside Cong if possible

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.

Pretty-printing proofs

data Config Source #

Options for proof presentation.

Constructors

Config 

Fields

defaultConfig :: Config Source #

The default configuration.

data Presentation f Source #

A proof, with all axioms and lemmas explicitly listed.

Constructors

Presentation 

Fields

Instances
Show (Presentation f) Source # 
Instance details

Defined in Twee.Proof

Function f => Pretty (Presentation f) Source # 
Instance details

Defined in Twee.Proof

data ProvedGoal f Source #

Instances
Show (ProvedGoal f) Source # 
Instance details

Defined in Twee.Proof

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 -> Presentation f -> Doc Source #

Print a presented proof.

present :: Function f => Config -> [ProvedGoal f] -> Presentation f Source #

Simplify and present a proof.

describeEquation :: PrettyTerm f => String -> String -> Maybe String -> Equation f -> Doc Source #

Format an equation nicely.

Used both here and in the main file.