Equals

class proveit.logic.Equals(a, b, *, styles=None)

Bases: proveit.relation.equiv_relation.EquivRelation

Attributes Summary

initializing
inversions
known_equalities
known_evaluation_sets
known_simplifications

Methods Summary

StrongRelationClass()
WeakRelationClass()
affirm_via_contradiction(self, conclusion, …)	From (A=FALSE), derive the conclusion provided that the negated conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.
apply_transitivity(self, other, …)	From x = y (self) and y = z (other) derive and return x = z.
conclude(self, \*\*defaults_config)	Attempt to conclude the equality various ways: simple reflexivity (x=x), via an evaluation (if one side is an irreducible).
conclude_boolean_equality(self, …)	Prove and return self of the form
conclude_via_reflexivity(self, …)	Prove and return self of the form x = x.
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this equality statement is in the Boolean set.
deduce_not_equals(self, \*\*defaults_config)	Deduce x != y assuming not(x = y), where self is x=y.
deny_via_contradiction(self, conclusion, …)	From (A=FALSE), derive the negated conclusion provided that the conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.
derive_contradiction(self, \*\*defaults_config)	From A=FALSE, and assuming A, derive FALSE.
derive_is_in_singleton(self, \*\*defaults_config)	From (x = y), derive (x in {y}).
derive_left_via_equality(self, …)	From A = B, derive A (the Right-Hand-Side) assuming B.
derive_reversed(self, \*\*defaults_config)	From x = y derive y = x.
derive_right_via_equality(self, …)	From A = B, derive B (the Right-Hand-Side) assuming A.
derive_via_boolean_equality(self, …)	From A = TRUE derive A, or from A = FALSE derive Not(A).
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
invert(lambda_map, rhs[, assumptions])	Given some x -> f(x) map and a right-hand-side, find the x for which f(x) = rhs amongst known equalities under the given assumptions.
known_relations_from_left(expr, \*[, …])	For each Judgment that is an Equals involving the given expression on the left hand side, yield the Judgment and the right hand side.
known_relations_from_right(expr, \*[, …])	For each Judgment that is an Equals involving the given expression on the right hand side, yield the Judgment and the left hand side.
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically for a negated equation.
other_side(self, expr)	Returns the ‘other’ side of the of the equation if the given expr is on one side.
reversed(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘symmetrization’.
side_effects(self, judgment)	Derive the reversed form.
sub_left_side_into(self, lambda_map, …)	From x = y, and given P(y), derive P(x) assuming P(y).
sub_right_side_into(self, lambda_map, …)	From x = y, and given P(x), derive P(y) assuming P(x).
substitution(self, lambda_map, …)	From x = y, and given f(x), derive f(x)=f(y).

Attributes Documentation

initializing = {}

inversions = {}

known_equalities = {[not](FALSE): OrderedSet([|- [not](FALSE) = TRUE, |- TRUE = [not](FALSE)]), TRUE: OrderedSet([|- [not](FALSE) = TRUE, |- TRUE = [not](FALSE), {_a = TRUE} |- _a = TRUE, {A = TRUE} |- A = TRUE, |- TRUE = TRUE]), _b: OrderedSet([{_b = _a} |- _b = _a, {_b = _a} |- _a = _b]), _a: OrderedSet([{_b = _a} |- _b = _a, {_b = _a} |- _a = _b, {_a = TRUE} |- _a = TRUE, {_a = FALSE} |- _a = FALSE]), x: OrderedSet([{x = y} |- x = y, {x = y} |- y = x]), y: OrderedSet([{x = y} |- x = y, {x = y} |- y = x]), A: OrderedSet([{A = TRUE} |- A = TRUE, {A = FALSE} |- A = FALSE]), [not](TRUE): OrderedSet([|- [not](TRUE) = FALSE, |- FALSE = [not](TRUE)]), FALSE: OrderedSet([|- [not](TRUE) = FALSE, |- FALSE = [not](TRUE), {_a = FALSE} |- _a = FALSE, {A = FALSE} |- A = FALSE, |- FALSE = FALSE]), BOOLEAN: OrderedSet([|- BOOLEAN = {TRUE, FALSE}, |- {TRUE, FALSE} = BOOLEAN]), {TRUE, FALSE}: OrderedSet([|- BOOLEAN = {TRUE, FALSE}, |- {TRUE, FALSE} = BOOLEAN]), -0: OrderedSet([|- (-0) = 0, |- 0 = (-0)]), 0: OrderedSet([|- (-0) = 0, |- 0 = (-0)])}

known_evaluation_sets = {[not](FALSE): {|- [not](FALSE) = TRUE}, _a: {{_a = TRUE} |- _a = TRUE, {_a = FALSE} |- _a = FALSE}, A: {{A = FALSE} |- A = FALSE, {A = TRUE} |- A = TRUE}, [not](TRUE): {|- [not](TRUE) = FALSE}, TRUE: {|- TRUE = TRUE}, FALSE: {|- FALSE = FALSE}, -0: {|- (-0) = 0}}

known_simplifications = {}

Methods Documentation

classmethod StrongRelationClass()

classmethod WeakRelationClass()

affirm_via_contradiction(self, conclusion, \*\*defaults_config)

From (A=FALSE), derive the conclusion provided that the negated conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.

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

apply_transitivity(self, other, \*\*defaults_config)

From x = y (self) and y = z (other) derive and return x = z. Also works more generally as long as there is a common side to the equations. If “other” is not an equality, reverse roles and call ‘apply_transitivity’ from the “other” side.

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

conclude(self, \*\*defaults_config)

Attempt to conclude the equality various ways: simple reflexivity (x=x), via an evaluation (if one side is an irreducible). Use conclude_via_transitivity for transitivity cases.

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

conclude_boolean_equality(self, \*\*defaults_config)

Prove and return self of the form

A=TRUE given A, A=FALSE given Not(A), or [Not(A)=FALSE] given A.

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

conclude_via_reflexivity(self, \*\*defaults_config)

Prove and return self of the form x = x.

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

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this equality statement is in the Boolean set.

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

deduce_not_equals(self, \*\*defaults_config)

Deduce x != y assuming not(x = y), where self is x=y.

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

deny_via_contradiction(self, conclusion, \*\*defaults_config)

From (A=FALSE), derive the negated conclusion provided that the conclusion implies both (A=FALSE) as well as A, and the conclusion is a Boolean.

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

derive_contradiction(self, \*\*defaults_config)

From A=FALSE, and assuming A, derive FALSE.

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

derive_is_in_singleton(self, \*\*defaults_config)

From (x = y), derive (x in {y}).

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

derive_left_via_equality(self, \*\*defaults_config)

From A = B, derive A (the Right-Hand-Side) assuming B.

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

derive_reversed(self, \*\*defaults_config)

From x = y derive y = x. This derivation is an automatic side-effect.

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

derive_right_via_equality(self, \*\*defaults_config)

From A = B, derive B (the Right-Hand-Side) assuming A.

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

derive_via_boolean_equality(self, \*\*defaults_config)

From A = TRUE derive A, or from A = FALSE derive Not(A). This derivation is an automatic side-effect. Note, see derive_stmt_eq_true or Not.equate_negated_to_false for the reverse process.

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

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value. This Operation.evaluation version simplifies the operands and then calls shallow_simplification with must_evaluat=True.

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

‘evaluated’ returns the right-hand side of ‘evaluation’. ‘evaluate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘evaluation’ for the inner expression.

static invert(lambda_map, rhs, assumptions=None)

Given some x -> f(x) map and a right-hand-side, find the x for which f(x) = rhs amongst known equalities under the given assumptions. Return this x if one is found; return None otherwise.

static known_relations_from_left(expr, \*, assumptions=None, include_canonical_forms=True)

For each Judgment that is an Equals involving the given expression on the left hand side, yield the Judgment and the right hand side. By default, canonical forms will also be included (as an Expression rather than a Judgment) if the equality has not yet actually been proven.

static known_relations_from_right(expr, \*, assumptions=None, include_canonical_forms=True)

For each Judgment that is an Equals involving the given expression on the right hand side, yield the Judgment and the left hand side. By default, canonical forms will also be included (as an Expression rather than a Judgment) if the equality has not yet actually been proven.

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for a negated equation.

other_side(self, expr)

Returns the ‘other’ side of the of the equation if the given expr is on one side.

reversed(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘symmetrization’.

side_effects(self, judgment)

Derive the reversed form. If the rhs is TRUE/FALSE derive the lhs or its negation. Derive FALSE if the rhs is FALSE and the lhs is readily provable. Apply ‘equality_side_effects’ ifthe lhs has a method with this name.

sub_left_side_into(self, lambda_map, \*\*defaults_config)

From x = y, and given P(y), derive P(x) assuming P(y). P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression to upon which to perform a global replacement of self.rhs.

Note: auto-simplification may only affect sub-expressions touched by the substitution.

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

sub_right_side_into(self, lambda_map, \*\*defaults_config)

From x = y, and given P(x), derive P(y) assuming P(x). P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression to upon which to perform a global replacement of self.lhs.

Note: auto-simplification may only affect sub-expressions touched by the substitution.

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

substitution(self, lambda_map, \*\*defaults_config)

From x = y, and given f(x), derive f(x)=f(y). f(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression upon which to perform a global replacement of self.lhs.

Note: auto-simplification may only affect sub-expressions touched by the substitution.

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