Judgment

class proveit.Judgment(expression, assumptions, *, num_lit_gen=0)

Bases: object

Attributes Summary

in_progress_to_derive_sideeffects
presumed_theorems_and_theories
presuming_theorem_and_theory_exclusions
qed_in_progress
theorem_being_proven

Methods Summary

as_impl(self, hypothesis)	Abbreviation for as_implication.
as_implication(self, hypothesis)	Performs a “deduction” derivation step, forming an implication statement with the given hypothesis and self.expr as the conclusion.
as_theorem_or_axiom(self)	Assuming this Judgment represents a Theorem or Axiom, return the Theorem or Axiom object.
begin_proof(self, theorem)	Begin a proof for a theorem.
derive_side_effects(self)	Derive any side-effects that are obvious consequences arising from this truth.
eliminate(self, \*skolem_constants, …)	Performs a Skolem constant elimination derivation step on this Judgment (KT), where this KT has the form S |– alpha and the set S of assumptions includes one or more assumptions involving one or more Skolem constants sk1, …, skn specified by skolem_constants, where the Skolem constant-related assumptions were previously generated using the Exists.choose(sk1, …, skn) method.
evaluation(self)	Prove that the Judgement expression equals TRUE under the assumptions of the Judgment.
find_judgment(expression, assumptions)	Try to find a Judgment for this expression that applies to the given set of assumptions (its assumptions are a subset of the given assumptions).
forget_judgments()	Forget all Judgment’s and all Assumption proof objects.
generalize(self, …[, domain_lists, …])	Performs a generalization derivation step.
inner_expr(self[, assumptions])	Return an InnerExpr object to wrap the Judgment and access any inner sub-expression (including assumptions or inner expressions of assumptions) for the purpose of replacing the inner expression, changing its style, or relabeling variables.
instantiate(self[, repl_map, …])	Performs an instantiation derivation step to be proven under the given assumptions, in addition to the assumptions of the Judgment.
is_usable(self)	Returns True iff this Judgment has a “usable” proof.
latex(self[, perform_usability_check])	Display the turnstile notation to show that the judgment on the right derives from the set of assumptions on the left.
order_of_appearance(self, sub_expressions)	Yields the given sub-Expressions in the order in which they appear in this Judgment.
print_dependents(self)	Provided that this Judgment is known to represent a theorem or axiom, print all theorems that are known to depend on it directly or indirectly.
print_requirements(self)	Provided that this Judgment is known to represent a proven theorem, print the set of axioms that are required directly or indirectly inits proof as well as any required theorems that are unproven (if it has not yet been proven completely).
proof(self)	Returns the most up-to-date proof of this Judgment.
raise_unusable_proof(self)
string(self[, perform_usability_check])	Display the turnstile notation to show that the judgment on the right derives from the set of assumptions on the left.
with_matching_styles(self, expr, assumptions)	Return the Judgment with the styles matching those of the given expression and assumptions.

Attributes Documentation

in_progress_to_derive_sideeffects = {}

presumed_theorems_and_theories = None

presuming_theorem_and_theory_exclusions = None

qed_in_progress = False

theorem_being_proven = None

Methods Documentation

as_impl(self, hypothesis)

Abbreviation for as_implication.

as_implication(self, hypothesis)

Performs a “deduction” derivation step, forming an implication statement with the given hypothesis and self.expr as the conclusion. The hypothesis is removed from the set of the conclusion statement’s assumptions for the implication statement’s assumptions.

as_theorem_or_axiom(self)

Assuming this Judgment represents a Theorem or Axiom, return the Theorem or Axiom object.

begin_proof(self, theorem)

Begin a proof for a theorem. Only use other theorems that are in the presuming list of theorems/packages or theorems that are required, directly or indirectly, in proofs of theorems that are explicitly listed (these are implicitly presumed). If there exists any presumed theorem that has a direct or indirect dependence upon this theorem then a CircularLogic exception is raised.

derive_side_effects(self)

Derive any side-effects that are obvious consequences arising from this truth. Called after the corresponding Proof is complete.

eliminate(self, \*skolem_constants, \*\*defaults_config)

Performs a Skolem constant elimination derivation step on this Judgment (KT), where this KT has the form S |– alpha and the set S of assumptions includes one or more assumptions involving one or more Skolem constants sk1, …, skn specified by skolem_constants, where the Skolem constant-related assumptions were previously generated using the Exists.choose(sk1, …, skn) method.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

evaluation(self)

Prove that the Judgement expression equals TRUE under the assumptions of the Judgment.

static find_judgment(expression, assumptions)

Try to find a Judgment for this expression that applies to the given set of assumptions (its assumptions are a subset of the given assumptions). Return None if there is no match.

static forget_judgments()

Forget all Judgment’s and all Assumption proof objects. This is used for demonstration purposes in the tutorial, but should not generally be needed.

generalize(self, forall_var_or_vars_or_var_lists, \*, domain_lists=None, domain=None, conditions=(), antecedent=None)

Performs a generalization derivation step. Returns the proven generalized Judgment. Can introduce any number of nested Forall operations to wrap the original statement, corresponding to the number of given forall_var_lists and domains. A single variable list or single variable and a single domain may be provided to introduce a single Forall wrapper.

This will also handle “literal” generalization in which literals are converted to variables (with the same formatting), corresponding axioms and/or theorems are converted to assumptions, and these variables are then generalized in one step. To do this, simply supply Literal expressions in place of Variables in the forall_var_or_vars_or_var_lists. There may even be a mixture of Literals and Variables. There are important limitations regarding literal generalization. There must not be any axiom or theorem requirement using that Literal that isn’t masked by a condition, or a LiteralGeneralizationFailure will be raised. That is, all needed axioms/theorems which use that Literal must be converted to an assumption (with the Literal converted to a Variable) and then included in the conditions (or antecedent).

If an antecedent is provided, it plays the role of an extra condition but is placed in an implication instead of a Conditional.

inner_expr(self, assumptions=None)

Return an InnerExpr object to wrap the Judgment and access any inner sub-expression (including assumptions or inner expressions of assumptions) for the purpose of replacing the inner expression, changing its style, or relabeling variables.

instantiate(self, repl_map=None, \*, num_forall_eliminations=None, simplify_only_where_marked=False, markers_and_marked_expr=None, \*\*defaults_config)

Performs an instantiation derivation step to be proven under the given assumptions, in addition to the assumptions of the Judgment. This may instantiate Variables that are universally quantified immediately to the right of the Judgment turnstile according to the “replacement” map (repl_map), eliminating the quantifier as the corresponding variables are instantiated. It may eliminate any number of nested Forall operations, instantiating the instance Variables according to repl_map, going to the depth for which the instance variables occur as keys in repl_map or according to num_forall_eliminations if it is specified.

For Variables that map to Variables in the replacement map, this is handled as a relabeling across both sides of the turnstile as well as “internal” Lambda map parameters. For Variables that map to non-Variables, the replacement only occurs within an eliminated quantifier and will not penetrate into internal Lambda maps that use that Variable as a parameter.

Replacements are made simultaneously. For example, the {x:y, y:x} mapping will swap x and y variables.

If equality ‘replacements’ are specified or ‘auto_simplify’ is True (in proveit.defaults which may be temporarily set via keyword arguments), equality replacements may be made in the process via equality judgements where the left-hand-side is the expression being replaced and the right-hand-side is the replacement.

If simplify_only_where_marked= is True, Prove-It will only simplify “marked” parts of an expression. ‘markers_and_marked_expr’ must then be a tuple: Variable markers, and an expression that matches pre-simplified instantiated expression except where marked with the markers. Only sub-expressions containing a marker may be simplified (if auto_simplify=True).

Returns the proven instantiated Judgment, or throws an exception if the proof fails. For the proof to succeed, all conditions of eliminated Forall operations, after replacements are made, must be proven. Furthermore, there may be additional requirements when iterated parameters are instantiated (see Lambda.apply for details). Automation may be used in attempting to prove these requirements provided proveit.defaults.conclude_automation=True.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

is_usable(self)

Returns True iff this Judgment has a “usable” proof. Proofs may be unusable when proving a theorem that is restricted with respect to which theorems may be used (to avoid circular logic).

latex(self, perform_usability_check=True)

Display the turnstile notation to show that the judgment on the right derives from the set of assumptions on the left.

order_of_appearance(self, sub_expressions)

Yields the given sub-Expressions in the order in which they appear in this Judgment. There may be repeats.

print_dependents(self)

Provided that this Judgment is known to represent a theorem or axiom, print all theorems that are known to depend on it directly or indirectly.

print_requirements(self)

Provided that this Judgment is known to represent a proven theorem, print the set of axioms that are required directly or indirectly inits proof as well as any required theorems that are unproven (if it has not yet been proven completely).

proof(self)

Returns the most up-to-date proof of this Judgment.

raise_unusable_proof(self)

string(self, perform_usability_check=True)

Display the turnstile notation to show that the judgment on the right derives from the set of assumptions on the left.

with_matching_styles(self, expr, assumptions)

Return the Judgment with the styles matching those of the given expression and assumptions.