twee-lib-2.4.1: An equational theorem prover
Safe HaskellNone
LanguageHaskell2010

Twee.Proof

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

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

(Labelled f, Show 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

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

Instances details
Eq (Derivation f) Source # 
Instance details

Defined in Twee.Proof

Methods

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

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

(Labelled f, Show f) => Show (Derivation f) Source # 
Instance details

Defined in Twee.Proof

(Labelled f, 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) 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

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

(Labelled f, Show 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 #

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

Defined in Twee.Proof

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.

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 :: 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).

Pretty-printing proofs

data Config f Source #

Options for proof presentation.

Constructors

Config 

Fields

defaultConfig :: Config f Source #

The default configuration.

data Presentation f Source #

A proof, with all axioms and lemmas explicitly listed.

Constructors

Presentation 

Fields

Instances

Instances details
(Labelled f, Show f) => 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

Instances details
(Labelled f, Show f) => 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 f -> Presentation f -> Doc Source #

Print a presented proof.

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

Simplify and present a proof.

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

Format an equation nicely.

Used both here and in the main file.