Equals

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

Bases: proveit.TransitiveRelation

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

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:

conclude_boolean_equality(self, …)

Prove and return self of the form

conclude_via_direct_substitution(self, …)

Prove that this Equals expression is true by directly and

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

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. This derivation is an automatic

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

get_known_evaluation(expr, \*[, automation])

Return an applicable evaluation (under current defaults) for the given expression if one is known; otherwise return None.

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, assumptions_set)

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, assumptions_set)

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(self)

Return an Equals expression with the right side and left side reversed from this one.

shallow_simplification(self, \*[, must_evaluate])

Given equality operands that are the same or are irreducible

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

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

side_effects(self, judgment)

Record the judgment in Equals.known_equalities, associated from the left hand side and the right hand side.

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). f(x) is provided

yield_known_equal_expressions(expr, \*[, …])

Yield everything known to be equal to the given expression under the given assumptions directly or indirectly through the transitive property of equality.

Attributes Documentation

initializing = {}
inversions = {}
known_equalities = {[not](FALSE): {|- [not](FALSE) = TRUE, |- TRUE = [not](FALSE)}, TRUE: {|- [not](FALSE) = TRUE, |- TRUE = TRUE, |- TRUE = [not](FALSE)}, TRUE = FALSE: {|- FALSE = (TRUE = FALSE), |- (TRUE = FALSE) = FALSE}, FALSE: {|- FALSE = (5 = 4), |- FALSE = (0 = 8), |- (2 = 1) = FALSE, |- FALSE = (8 = 0), |- ([not](TRUE) = TRUE) = FALSE, |- (FALSE = TRUE) = FALSE, |- FALSE = (4 = 3), |- [not](TRUE) = FALSE, |- (4 = 3) = FALSE, |- (0 = 1) = FALSE, |- (9 = 0) = FALSE, |- (0 = e) = FALSE, |- FALSE = (2 = 3), |- FALSE = (0 = i), |- (9 = 8) = FALSE, |- FALSE = (0 = 4), |- FALSE = (3 = 2), |- FALSE = (7 = 8), |- (0 = 4) = FALSE, |- FALSE = (5 = 6), |- (6 = 7) = FALSE, |- (2 = 3) = FALSE, |- (0 = 7) = FALSE, |- (6 = 5) = FALSE, |- FALSE = (e = 0), |- (1 = 2) = FALSE, |- FALSE = (0 = 9), |- FALSE = (0 = 3), |- FALSE = (0 = 7), |- (8 = 9) = FALSE, |- (i = 0) = FALSE, |- FALSE = (6 = 7), |- FALSE = (9 = 0), |- (0 = i) = FALSE, |- (TRUE = FALSE) = FALSE, |- FALSE = (TRUE = FALSE), |- (5 = 0) = FALSE, |- FALSE = (3 = 0), |- FALSE = (6 = 5), |- (0 = 3) = FALSE, |- FALSE = FALSE, |- (8 = 7) = FALSE, |- (3 = 0) = FALSE, |- FALSE = (0 = 5), |- (0 = pi) = FALSE, |- FALSE = (7 = 6), |- (3 = 2) = FALSE, |- FALSE = (7 = 0), |- FALSE = (6 = 0), |- (8 = 0) = FALSE, |- (0 = 8) = FALSE, |- FALSE = (2 = 1), |- (pi = 0) = FALSE, |- FALSE = (FALSE = TRUE), |- (4 = 5) = FALSE, |- FALSE = (2 = 0), |- FALSE = (0 = 1), |- FALSE = (4 = 5), |- (1 = 0) = FALSE, |- (0 = 5) = FALSE, |- (5 = 6) = FALSE, |- FALSE = (0 = e), |- (3 = 4) = FALSE, |- (5 = 4) = FALSE, |- (6 = 0) = FALSE, |- (0 = 9) = FALSE, |- FALSE = (0 = pi), |- FALSE = [not](TRUE), |- FALSE = (i = 0), |- FALSE = (1 = 2), |- FALSE = ([not](TRUE) = TRUE), |- FALSE = (0 = 2), |- (7 = 0) = FALSE, |- FALSE = (4 = 0), |- FALSE = (9 = 8), |- FALSE = (5 = 0), |- (7 = 6) = FALSE, |- (0 = 6) = FALSE, |- (0 = 2) = FALSE, |- FALSE = (pi = 0), |- (2 = 0) = FALSE, |- FALSE = (8 = 9), |- (e = 0) = FALSE, |- (TRUE = [not](TRUE)) = FALSE, |- FALSE = (1 = 0), |- (4 = 0) = FALSE, |- FALSE = (TRUE = [not](TRUE)), |- (7 = 8) = FALSE, |- FALSE = (8 = 7), |- FALSE = (3 = 4), |- FALSE = (0 = 6)}, FALSE = TRUE: {|- FALSE = (FALSE = TRUE), |- (FALSE = TRUE) = FALSE}, [not](TRUE): {|- [not](TRUE) = FALSE, |- FALSE = [not](TRUE)}, TRUE = [not](TRUE): {|- FALSE = (TRUE = [not](TRUE)), |- (TRUE = [not](TRUE)) = FALSE}, [not](TRUE) = TRUE: {|- ([not](TRUE) = TRUE) = FALSE, |- FALSE = ([not](TRUE) = TRUE)}, BOOLEAN: {|- {TRUE, FALSE} = BOOLEAN, |- BOOLEAN = {TRUE, FALSE}}, {TRUE, FALSE}: {|- {TRUE, FALSE} = BOOLEAN, |- BOOLEAN = {TRUE, FALSE}}, 1: {|- 1 = 1}, 0 = 1: {|- FALSE = (0 = 1), |- (0 = 1) = FALSE}, 1 = 0: {|- (1 = 0) = FALSE, |- FALSE = (1 = 0)}, 0 = 2: {|- (0 = 2) = FALSE, |- FALSE = (0 = 2)}, 2 = 0: {|- FALSE = (2 = 0), |- (2 = 0) = FALSE}, 0 = 3: {|- (0 = 3) = FALSE, |- FALSE = (0 = 3)}, 3 = 0: {|- FALSE = (3 = 0), |- (3 = 0) = FALSE}, 0 = 4: {|- (0 = 4) = FALSE, |- FALSE = (0 = 4)}, 4 = 0: {|- (4 = 0) = FALSE, |- FALSE = (4 = 0)}, 0 = 5: {|- FALSE = (0 = 5), |- (0 = 5) = FALSE}, 5 = 0: {|- FALSE = (5 = 0), |- (5 = 0) = FALSE}, 0 = 6: {|- FALSE = (0 = 6), |- (0 = 6) = FALSE}, 6 = 0: {|- FALSE = (6 = 0), |- (6 = 0) = FALSE}, 0 = 7: {|- (0 = 7) = FALSE, |- FALSE = (0 = 7)}, 7 = 0: {|- (7 = 0) = FALSE, |- FALSE = (7 = 0)}, 0 = 8: {|- (0 = 8) = FALSE, |- FALSE = (0 = 8)}, 8 = 0: {|- (8 = 0) = FALSE, |- FALSE = (8 = 0)}, 0 = 9: {|- (0 = 9) = FALSE, |- FALSE = (0 = 9)}, 9 = 0: {|- (9 = 0) = FALSE, |- FALSE = (9 = 0)}, 2 = 1: {|- (2 = 1) = FALSE, |- FALSE = (2 = 1)}, 1 = 2: {|- FALSE = (1 = 2), |- (1 = 2) = FALSE}, 3 = 2: {|- (3 = 2) = FALSE, |- FALSE = (3 = 2)}, 2 = 3: {|- (2 = 3) = FALSE, |- FALSE = (2 = 3)}, 4 = 3: {|- FALSE = (4 = 3), |- (4 = 3) = FALSE}, 3 = 4: {|- (3 = 4) = FALSE, |- FALSE = (3 = 4)}, 5 = 4: {|- (5 = 4) = FALSE, |- FALSE = (5 = 4)}, 4 = 5: {|- FALSE = (4 = 5), |- (4 = 5) = FALSE}, 6 = 5: {|- (6 = 5) = FALSE, |- FALSE = (6 = 5)}, 5 = 6: {|- (5 = 6) = FALSE, |- FALSE = (5 = 6)}, 7 = 6: {|- FALSE = (7 = 6), |- (7 = 6) = FALSE}, 6 = 7: {|- FALSE = (6 = 7), |- (6 = 7) = FALSE}, 8 = 7: {|- FALSE = (8 = 7), |- (8 = 7) = FALSE}, 7 = 8: {|- FALSE = (7 = 8), |- (7 = 8) = FALSE}, 9 = 8: {|- (9 = 8) = FALSE, |- FALSE = (9 = 8)}, 8 = 9: {|- (8 = 9) = FALSE, |- FALSE = (8 = 9)}, -0: {|- 0 = (-0), |- (-0) = 0}, 0: {|- 0 = (-0), |- (-0) = 0}, 0 = e: {|- FALSE = (0 = e), |- (0 = e) = FALSE}, e = 0: {|- (e = 0) = FALSE, |- FALSE = (e = 0)}, 0 = pi: {|- (0 = pi) = FALSE, |- FALSE = (0 = pi)}, pi = 0: {|- FALSE = (pi = 0), |- (pi = 0) = FALSE}, 0 = i: {|- FALSE = (0 = i), |- (0 = i) = FALSE}, i = 0: {|- (i = 0) = FALSE, |- FALSE = (i = 0)}}
known_evaluation_sets = {[not](FALSE): {|- [not](FALSE) = TRUE}, TRUE: {|- TRUE = TRUE}, TRUE = FALSE: {|- (TRUE = FALSE) = FALSE}, FALSE = TRUE: {|- (FALSE = TRUE) = FALSE}, [not](TRUE): {|- [not](TRUE) = FALSE}, TRUE = [not](TRUE): {|- (TRUE = [not](TRUE)) = FALSE}, [not](TRUE) = TRUE: {|- ([not](TRUE) = TRUE) = FALSE}, FALSE: {|- FALSE = FALSE}, 1: {|- 1 = 1}, 0 = 1: {|- (0 = 1) = FALSE}, 1 = 0: {|- (1 = 0) = FALSE}, 0 = 2: {|- (0 = 2) = FALSE}, 2 = 0: {|- (2 = 0) = FALSE}, 0 = 3: {|- (0 = 3) = FALSE}, 3 = 0: {|- (3 = 0) = FALSE}, 0 = 4: {|- (0 = 4) = FALSE}, 4 = 0: {|- (4 = 0) = FALSE}, 0 = 5: {|- (0 = 5) = FALSE}, 5 = 0: {|- (5 = 0) = FALSE}, 0 = 6: {|- (0 = 6) = FALSE}, 6 = 0: {|- (6 = 0) = FALSE}, 0 = 7: {|- (0 = 7) = FALSE}, 7 = 0: {|- (7 = 0) = FALSE}, 0 = 8: {|- (0 = 8) = FALSE}, 8 = 0: {|- (8 = 0) = FALSE}, 0 = 9: {|- (0 = 9) = FALSE}, 9 = 0: {|- (9 = 0) = FALSE}, 2 = 1: {|- (2 = 1) = FALSE}, 1 = 2: {|- (1 = 2) = FALSE}, 3 = 2: {|- (3 = 2) = FALSE}, 2 = 3: {|- (2 = 3) = FALSE}, 4 = 3: {|- (4 = 3) = FALSE}, 3 = 4: {|- (3 = 4) = FALSE}, 5 = 4: {|- (5 = 4) = FALSE}, 4 = 5: {|- (4 = 5) = FALSE}, 6 = 5: {|- (6 = 5) = FALSE}, 5 = 6: {|- (5 = 6) = FALSE}, 7 = 6: {|- (7 = 6) = FALSE}, 6 = 7: {|- (6 = 7) = FALSE}, 8 = 7: {|- (8 = 7) = FALSE}, 7 = 8: {|- (7 = 8) = FALSE}, 9 = 8: {|- (9 = 8) = FALSE}, 8 = 9: {|- (8 = 9) = FALSE}, -0: {|- (-0) = 0}, 0 = e: {|- (0 = e) = FALSE}, e = 0: {|- (e = 0) = FALSE}, 0 = pi: {|- (0 = pi) = FALSE}, pi = 0: {|- (pi = 0) = FALSE}, 0 = i: {|- (0 = i) = FALSE}, i = 0: {|- (i = 0) = FALSE}}
known_simplifications = {}

Methods Documentation

static StrongRelationClass()[source]
static WeakRelationClass()[source]
affirm_via_contradiction(self, conclusion, \*\*defaults_config)[source]

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)[source]

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)[source]

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)[source]
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_direct_substitution(self, \*\*defaults_config)[source]

Prove that this Equals expression is true by directly and greedily equating sub-expressions that differ.

For example, we can prove f(g(a, b), h(c, d)) = f(g(a, b’), h(c, d’)) if b=b’ and d’=d.

However, we cannot use this to prove f(g(a, b), h(c, d)) = f(g(a, b), h’) by simply knowing d=d’ and h(c, d’)=h’. Rather, we must know h(c, d) = h’.

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

conclude_via_reflexivity(self, \*\*defaults_config)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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)[source]

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.

static get_known_evaluation(expr, \*, automation=None)[source]

Return an applicable evaluation (under current defaults) for the given expression if one is known; otherwise return None. If automation is True, we are allow to derive an evaluation via transitivity with through any number of known equalities, excluding equalities with any “preserved” expressions (in defaults.preserved_exprs) whose evaluations are to be disregarded.

static invert(lambda_map, rhs, assumptions=None)[source]

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_set)[source]

For each Judgment that is an Equals involving the given expression on the left hand side, yield the Judgment and the right hand side.

static known_relations_from_right(expr, assumptions_set)[source]

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)[source]

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

other_side(self, expr)[source]

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

reversed(self)[source]

Return an Equals expression with the right side and left side reversed from this one. This is not a derivation: see derive_reversed().

shallow_simplification(self, \*, must_evaluate=False, \*\*defaults_config)[source]

Given equality operands that are the same or are irreducible values, return this expression equated to TRUE or FALSE.

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

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

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

side_effects(self, judgment)[source]

Record the judgment in Equals.known_equalities, associated from the left hand side and the right hand side. This information may be useful for concluding new equations via transitivity. If the right hand side is an “irreducible value” (see is_irreducible_value), also record it in Equals.known_evaluation_sets for use when the evaluation method is called. Some side-effects derivations are also attempted depending upon the form of this equality. If the rhs is an “irreducible value” (see is_irreducible_value), also record the judgment in the Equals.known_evaluation_sets dictionary, for use when the simplification or evaluation method is called. Some side-effects derivations are also attempted depending upon the form of this equality.

sub_left_side_into(self, lambda_map, \*\*defaults_config)[source]

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.

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

sub_right_side_into(self, lambda_map, \*\*defaults_config)[source]

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.

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

substitution(self, lambda_map, \*\*defaults_config)[source]

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.

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

static yield_known_equal_expressions(expr, \*, exceptions=None)[source]

Yield everything known to be equal to the given expression under the given assumptions directly or indirectly through the transitive property of equality. If ‘exceptions’ are provided, disregard known equalities with expressions in the ‘exceptions’ set.