Iff

class proveit.logic.Iff(A, B, *, styles=None)

Bases: proveit.TransitiveRelation

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

apply_transitivity(self, other_iff, …)	From A <=> B (self) and the given B <=> C (other_iff) derive and return (A <=> C) assuming self and other_iff.
conclude(self, \*\*defaults_config)	Try to automatically conclude this Iff given both operands are true, both operands are false, or by proving implications in both direction (the definition).
conclude_by_definition(self, \*\*defaults_config)	Conclude (A <=> B) assuming both (A => B), (B => A).
conclude_negation(self, \*\*defaults_config)	Try to automatically conclude the negation of Iff given one operand is true and the other is false or by proving the implication in one of the directions is False.
deduce_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that this ‘iff’ expression is in the set of BOOLEANS.
definition(self, \*\*defaults_config)	Return (A <=> B) = [(A => B) and (B => A)] where self represents (A <=> B).
derive_equality(self, \*\*defaults_config)	From (A <=> B), derive (A = B) assuming A and B in BOOLEANS.
derive_left(self, \*\*defaults_config)	From (A<=>B) derive and return A assuming B.
derive_left_implication(self, …)	From (A<=>B) derive and return B=>A.
derive_reversed(self, \*\*defaults_config)	From (A<=>B) derive and return (B<=>A).
derive_right(self, \*\*defaults_config)	From (A<=>B) derive and return B assuming A.
derive_right_implication(self, …)	From (A<=>B) derive and return A=>B.
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
side_effects(self, judgment)	Yield the TransitiveRelation side-effects (which also records known_left_sides and known_right_sides).

Attributes Documentation

known_left_sides = {}

known_right_sides = {}

Methods Documentation

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

From A <=> B (self) and the given B <=> C (other_iff) derive and return (A <=> C) assuming self and other_iff. Also works more generally as long as there is a common side to the equations.

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

conclude(self, \*\*defaults_config)

Try to automatically conclude this Iff given both operands are true, both operands are false, or by proving implications in both direction (the definition).

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

conclude_by_definition(self, \*\*defaults_config)

Conclude (A <=> B) assuming both (A => B), (B => A).

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

conclude_negation(self, \*\*defaults_config)

Try to automatically conclude the negation of Iff given one operand is true and the other is false or by proving the implication in one of the directions is False.

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

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this ‘iff’ expression is in the set of BOOLEANS.

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

definition(self, \*\*defaults_config)

Return (A <=> B) = [(A => B) and (B => A)] where self represents (A <=> B).

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

‘defined’ returns the right-hand side of ‘definition’. ‘define’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘definition’ for the inner expression.

derive_equality(self, \*\*defaults_config)

From (A <=> B), derive (A = B) assuming A and B in BOOLEANS.

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

derive_left(self, \*\*defaults_config)

From (A<=>B) derive and return A assuming B.

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

derive_left_implication(self, \*\*defaults_config)

From (A<=>B) derive and return B=>A.

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

derive_reversed(self, \*\*defaults_config)

From (A<=>B) derive and return (B<=>A).

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

derive_right(self, \*\*defaults_config)

From (A<=>B) derive and return B assuming A.

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

derive_right_implication(self, \*\*defaults_config)

From (A<=>B) derive and return A=>B.

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.

side_effects(self, judgment)

Yield the TransitiveRelation side-effects (which also records known_left_sides and known_right_sides). Also derive the left and right implications, derive the reversed version and attempt to derive equality.