twee-lib-2.4.2: An equational theorem prover

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
 (Labelled f, Show f) => Show (Proof f) Source # Instance detailsDefined in Twee.Proof MethodsshowsPrec :: Int -> Proof f -> ShowS #show :: Proof f -> String #showList :: [Proof f] -> ShowS # Eq (Proof f) Source # Instance detailsDefined in Twee.Proof Methods(==) :: Proof f -> Proof f -> Bool #(/=) :: Proof f -> Proof f -> Bool # Ord (Proof f) Source # Instance detailsDefined in Twee.Proof Methodscompare :: 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 # Function f => Pretty (Proof f) Source # Instance detailsDefined in Twee.Proof MethodspPrintPrec :: PrettyLevel -> Rational -> Proof f -> Doc #pPrint :: Proof f -> Doc #pPrintList :: PrettyLevel -> [Proof f] -> Doc #

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
 (Labelled f, Show f) => Show (Derivation f) Source # Instance detailsDefined in Twee.Proof MethodsshowsPrec :: Int -> Derivation f -> ShowS #show :: Derivation f -> String #showList :: [Derivation f] -> ShowS # Eq (Derivation f) Source # Instance detailsDefined in Twee.Proof Methods(==) :: Derivation f -> Derivation f -> Bool #(/=) :: Derivation f -> Derivation f -> Bool # (Labelled f, PrettyTerm f) => Pretty (Derivation f) Source # Instance detailsDefined in Twee.Proof MethodspPrint :: Derivation f -> Doc #pPrintList :: PrettyLevel -> [Derivation f] -> Doc # Source # Instance detailsDefined in Twee.Proof Associated Typestype ConstantOf (Derivation f) Source # Methodssubst_ :: (Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f Source # type ConstantOf (Derivation f) Source # Instance detailsDefined in Twee.Proof type ConstantOf (Derivation f) = f

data Axiom f Source #

Constructors

 Axiom Fieldsaxiom_number :: !IntThe number of the axiom. Has no semantic meaning; for convenience only.axiom_name :: !StringA description of the axiom. Has no semantic meaning; for convenience only.axiom_eqn :: !(Equation f)The equation which the axiom asserts.

#### Instances

Instances details
 (Labelled f, Show f) => Show (Axiom f) Source # Instance detailsDefined in Twee.Proof MethodsshowsPrec :: Int -> Axiom f -> ShowS #show :: Axiom f -> String #showList :: [Axiom f] -> ShowS # Eq (Axiom f) Source # Instance detailsDefined in Twee.Proof Methods(==) :: Axiom f -> Axiom f -> Bool #(/=) :: Axiom f -> Axiom f -> Bool # Ord (Axiom f) Source # Instance detailsDefined in Twee.Proof Methodscompare :: 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, PrettyTerm f) => Pretty (Axiom f) Source # Instance detailsDefined in Twee.Proof MethodspPrintPrec :: PrettyLevel -> Rational -> Axiom f -> Doc #pPrint :: Axiom f -> Doc #pPrintList :: PrettyLevel -> [Axiom f] -> Doc #

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 Fieldscfg_all_lemmas :: !BoolNever inline lemmas.cfg_no_lemmas :: !BoolInline all lemmas.cfg_ground_proof :: !BoolMake the proof ground.cfg_show_instances :: !BoolPrint out explicit substitutions.cfg_use_colour :: !BoolPrint out proofs in colour.cfg_show_uses_of_axioms :: Axiom f -> BoolPrint out which instances of some axioms were used.

The default configuration.

data Presentation f Source #

A proof, with all axioms and lemmas explicitly listed.

Constructors

 Presentation Fieldspres_axioms :: [Axiom f]The used axioms.pres_lemmas :: [Proof f]The used lemmas.pres_goals :: [ProvedGoal f]The goals proved.

#### Instances

Instances details
 (Labelled f, Show f) => Show (Presentation f) Source # Instance detailsDefined in Twee.Proof MethodsshowsPrec :: Int -> Presentation f -> ShowS #show :: Presentation f -> String #showList :: [Presentation f] -> ShowS # Function f => Pretty (Presentation f) Source # Instance detailsDefined in Twee.Proof MethodspPrint :: Presentation f -> Doc #pPrintList :: PrettyLevel -> [Presentation f] -> Doc #

data ProvedGoal f Source #

Constructors

 ProvedGoal Fieldspg_number :: Int pg_name :: String pg_proof :: Proof f pg_goal_hint :: Equation f pg_witness_hint :: Subst f

#### Instances

Instances details
 (Labelled f, Show f) => Show (ProvedGoal f) Source # Instance detailsDefined in Twee.Proof MethodsshowsPrec :: Int -> ProvedGoal f -> ShowS #show :: ProvedGoal f -> String #showList :: [ProvedGoal f] -> ShowS #

provedGoal :: Int -> String -> Proof f -> ProvedGoal f Source #

Construct a ProvedGoal.

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.

Format an equation nicely.

Used both here and in the main file.