module Proof:sig..end
Functions to manipulate proof expressions
val is_true : Expr.expr -> boolIndicates whether the term is a Proof for the expression 'true'.
val is_asserted : Expr.expr -> boolIndicates whether the term is a proof for a fact asserted by the user.
val is_goal : Expr.expr -> boolIndicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
val is_oeq : Expr.expr -> boolIndicates whether the term is a binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
val is_modus_ponens : Expr.expr -> boolIndicates whether the term is proof via modus ponens
Given a proof for p and a proof for (implies p q), produces a proof for q.
T1: p
T2: (implies p q)
mp T1 T2: q
The second antecedents may also be a proof for (iff p q).
val is_reflexivity : Expr.expr -> boolIndicates whether the term is a proof for (R t t), where R is a reflexive relation. This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.
val is_symmetry : Expr.expr -> boolIndicates whether the term is proof by symmetricity of a relation
Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
T1: (R t s)
symmetry T1: (R s t)
T1 is the antecedent of this proof object.
val is_transitivity : Expr.expr -> boolIndicates whether the term is a proof by transitivity of a relation
Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
for (R t u).
T1: (R t s)
T2: (R s u)
trans T1 T2: (R t u)
val is_Transitivity_star : Expr.expr -> boolIndicates whether the term is a proof by condensed transitivity of a relation
Condensed transitivity proof.
It combines several symmetry and transitivity proofs.
Example:
T1: (R a b)
T2: (R c b)
T3: (R c d)
trans* T1 T2 T3: (R a d)
R must be a symmetric and transitive relation.
Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.
val is_monotonicity : Expr.expr -> boolIndicates whether the term is a monotonicity proof object.
T1: (R t_1 s_1)
...
Tn: (R t_n s_n)
monotonicity T1 ... Tn: (R (f t_1 ... t_n) (f s_1 ... s_n))
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are suppressed to save space.
val is_quant_intro : Expr.expr -> boolIndicates whether the term is a quant-intro proof
Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
T1: (~ p q)
quant-intro T1: (~ (forall (x) p) (forall (x) q))
val is_distributivity : Expr.expr -> boolIndicates whether the term is a distributivity proof object.
Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.
This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.
val is_and_elimination : Expr.expr -> boolIndicates whether the term is a proof by elimination of AND
Given a proof for (and l_1 ... l_n), produces a proof for l_i
T1: (and l_1 ... l_n)
and-elim T1: l_i
val is_or_elimination : Expr.expr -> boolIndicates whether the term is a proof by elimination of not-or
Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
T1: (not (or l_1 ... l_n))
not-or-elim T1: (not l_i)
val is_rewrite : Expr.expr -> boolIndicates whether the term is a proof by rewriting
A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.
This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.
Examples: (= (+ ( x : expr ) 0) x) (= (+ ( x : expr ) 1 2) (+ 3 x)) (iff (or ( x : expr ) false) x)
val is_rewrite_star : Expr.expr -> boolIndicates whether the term is a proof by rewriting
A proof for rewriting an expression t into an expression s. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases. The cases are:
val is_pull_quant : Expr.expr -> boolIndicates whether the term is a proof for pulling quantifiers out.
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
val is_push_quant : Expr.expr -> boolIndicates whether the term is a proof for pushing quantifiers in.
A proof for:
(iff (forall (x_1 ... x_m) (and p_1x_1 ... x_m ... p_nx_1 ... x_m))
(and (forall (x_1 ... x_m) p_1x_1 ... x_m)
...
(forall (x_1 ... x_m) p_nx_1 ... x_m)))
This proof object has no antecedents
val is_elim_unused_vars : Expr.expr -> boolIndicates whether the term is a proof for elimination of unused variables.
A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) px_1 ... x_n)
(forall (x_1 ... x_n) px_1 ... x_n))
It is used to justify the elimination of unused variables. This proof object has no antecedents.
val is_der : Expr.expr -> boolIndicates whether the term is a proof for destructive equality resolution
A proof for destructive equality resolution:
(iff (forall (x) (or (not (= ( x : expr ) t)) Px)) Pt)
if ( x : expr ) does not occur in t.
This proof object has no antecedents.
Several variables can be eliminated simultaneously.
val is_quant_inst : Expr.expr -> boolIndicates whether the term is a proof for quantifier instantiation
A proof of (or (not (forall (x) (P x))) (P a))
val is_hypothesis : Expr.expr -> boolIndicates whether the term is a hypothesis marker. Mark a hypothesis in a natural deduction style proof.
val is_lemma : Expr.expr -> boolIndicates whether the term is a proof by lemma
T1: false
lemma T1: (or (not l_1) ... (not l_n))
This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.
val is_unit_resolution : Expr.expr -> boolIndicates whether the term is a proof by unit resolution
T1: (or l_1 ... l_n l_1' ... l_m')
T2: (not l_1)
...
T(n+1): (not l_n)
unit-resolution T1 ... T(n+1): (or l_1' ... l_m')
val is_iff_true : Expr.expr -> boolIndicates whether the term is a proof by iff-true
T1: p
iff-true T1: (iff p true)
val is_iff_false : Expr.expr -> boolIndicates whether the term is a proof by iff-false
T1: (not p)
iff-false T1: (iff p false)
val is_commutativity : Expr.expr -> boolIndicates whether the term is a proof by commutativity
comm: (= (f a b) (f b a))
f is a commutative operator.
This proof object has no antecedents. Remark: if f is bool, then = is iff.
val is_def_axiom : Expr.expr -> boolIndicates whether the term is a proof for Tseitin-like axioms
Proof object used to justify Tseitin's like axioms:
(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)
This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).
val is_def_intro : Expr.expr -> boolIndicates whether the term is a proof for introduction of a name
Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:
When e is of Boolean type:
def-intro: (and (or n (not e)) (or (not n) e))
or:
def-intro: (or (not n) e)
when e only occurs positively.
When e is of the form (ite cond th el):
def-intro: (and (or (not cond) (= n th)) (or cond (= n el)))
Otherwise:
def-intro: (= n e)
val is_apply_def : Expr.expr -> boolIndicates whether the term is a proof for application of a definition
apply-def T1: F ~ n
F is 'equivalent' to n, given that T1 is a proof that
n is a name for F.
val is_iff_oeq : Expr.expr -> boolIndicates whether the term is a proof iff-oeq
T1: (iff p q)
iff~ T1: (~ p q)
val is_nnf_pos : Expr.expr -> boolIndicates whether the term is a proof for a positive NNF step
Proof for a (positive) NNF step. Example:
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
nnf-pos T1 T2 T3 T4: (~ (iff s_1 s_2)
(and (or r_1 r_2') (or r_1' r_2)))
The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
(a) When creating the NNF of a positive force quantifier.
The quantifier is retained (unless the bound variables are eliminated).
Example
T1: q ~ q_new
nnf-pos T1: (~ (forall (x T) q) (forall (x T) q_new))
(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.
val is_nnf_neg : Expr.expr -> boolIndicates whether the term is a proof for a negative NNF step
Proof for a (negative) NNF step. Examples:
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
nnf-neg T1 ... Tn: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
and
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
nnf-neg T1 ... Tn: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
and
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
nnf-neg T1 T2 T3 T4: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
val is_skolemize : Expr.expr -> boolIndicates whether the term is a proof for a Skolemization step
Proof for:
sk: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y)))
sk: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y))
This proof object has no antecedents.
val is_modus_ponens_oeq : Expr.expr -> boolIndicates whether the term is a proof by modus ponens for equi-satisfiability.
Modus ponens style rule for equi-satisfiability.
T1: p
T2: (~ p q)
mp~ T1 T2: q
val is_theory_lemma : Expr.expr -> boolIndicates whether the term is a proof for theory lemma
Generic proof for theory lemmas.
The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: