Source code for proveit.logic.booleans.implication.iff

from proveit import (Literal, Operation, defaults, USE_DEFAULTS, 
                     ProofFailure, prover, relation_prover, equality_prover)
from proveit.logic.booleans.conjunction import compose
from .implies import Implies
from proveit import A, B, C
from proveit import TransitiveRelation

# if and only if: A => B and B => A


[docs]class Iff(TransitiveRelation): # The operator of the Iff operation _operator_ = Literal( string_format='<=>', latex_format=r'\Leftrightarrow', theory=__file__) # map left-hand-sides to Subset Judgments # (populated in TransitivityRelation.derive_side_effects) known_left_sides = dict() # map right-hand-sides to Subset Judgments # (populated in TransitivityRelation.derive_side_effects) known_right_sides = dict() def __init__(self, A, B, *, styles=None): TransitiveRelation.__init__(self, Iff._operator_, A, B, styles=styles) self.A = A self.B = B
[docs] def 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. ''' for side_effect in TransitiveRelation.side_effects(self, judgment): yield side_effect yield self.derive_left_implication # B=>A given A<=>B yield self.derive_right_implication # A=>B given A<=>B yield self.derive_reversed # B<=>A given A<=>B # A=B given A<=>B (assuming A and B are in booleans) yield self.derive_equality
def _readily_provable(self): ''' A <=> B is readily provable if A => B and B => A are rediable provable or if A and B are both readily provable or both readily disprovable. ''' return ((Implies(self.A, self.B).readily_provable() and Implies(self.B, self.A).readily_provable()) or (self.A.readily_provable() and self.B.readily_provable()) or ( self.A.readily_disprovable() and (self.B.readily_disprovable()))) def _readily_disprovable(self): ''' A <=> B is readily provable if A => B is readily disprovable or B => A is readily disprovable or if A is readily provable and B is readily disprovable or vice-versa. ''' return (Implies(self.A, self.B).readily_disprovable() or Implies(self.B, self.A).readily_disprovable() or (self.A.readily_disprovable() and self.B.readily_provable()) or (self.A.readily_provable() and ( self.B.readily_disprovable())))
[docs] @prover def 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). ''' from . import iff_t_t, iff_t_f, iff_f_t, iff_f_f, true_iff_true, false_iff_false if self in {true_iff_true, false_iff_false}: # should be proven via one of the imported theorems as a # simple special case try: self.shallow_simplification() # self.evaluation() except BaseException: return self.prove() if self.A.readily_provable() and self.B.readily_provable(): # A <=> B because A and B are both true. from . import iff_via_both_true if iff_via_both_true.is_usable(): return iff_via_both_true.instantiate({A:self.A, B:self.B}) if self.A.readily_disprovable() and self.B.readily_disprovable(): # A <=> B because A and B are both false. from . import iff_via_both_false if iff_via_both_false.is_usable(): return iff_via_both_false.instantiate({A:self.A, B:self.B}) # Introduce the Iff via implications each way as a direct # consequence of the definition. return self.conclude_by_definition()
[docs] @prover def 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. ''' from proveit.logic.booleans import FALSE, TRUE if self.A == TRUE and self.B == FALSE: from . import true_iff_false_negated return true_iff_false_negated elif self.B == TRUE and self.A == FALSE: from . import false_iff_true_negated return false_iff_true_negated elif self.A.readily_provable() and self.B.readily_disprovable(): from . import not_iff_via_not_right return not_iff_via_not_right.instantiate({A:self.A, B:self.B}) elif self.A.readily_disprovable() and self.B.readily_provable(): from . import not_iff_via_not_left return not_iff_via_not_left.instantiate({A:self.A, B:self.B}) elif Implies(self.A, self.B).readily_disprovable(): from . import not_iff_via_not_right_impl return not_iff_via_not_right_impl.instantiate({A:self.A, B:self.B}) elif Implies(self.B, self.A).readily_disprovable(): from . import not_iff_via_not_left_impl return not_iff_via_not_left_impl.instantiate({A:self.A, B:self.B}) raise ProofFailure(self, defaults.assumptions, "Unable to automatically conclude by " "standard means.")
[docs] @prover def derive_left_implication(self, **defaults_config): ''' From (A<=>B) derive and return B=>A. ''' from . import iff_implies_left return iff_implies_left.instantiate( {A: self.A, B: self.B})
[docs] @prover def derive_left(self, **defaults_config): ''' From (A<=>B) derive and return A assuming B. ''' from . import left_from_iff return left_from_iff.instantiate( {A: self.A, B: self.B})
[docs] @prover def derive_right_implication(self, **defaults_config): ''' From (A<=>B) derive and return A=>B. ''' from . import iff_implies_right return iff_implies_right.instantiate( {A: self.A, B: self.B})
[docs] @prover def derive_right(self, **defaults_config): ''' From (A<=>B) derive and return B assuming A. ''' from . import right_from_iff return right_from_iff.instantiate( {A: self.A, B: self.B})
[docs] @prover def derive_reversed(self, **defaults_config): ''' From (A<=>B) derive and return (B<=>A). ''' from . import iff_symmetry return iff_symmetry.instantiate( {A: self.A, B: self.B})
[docs] @prover def 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. ''' from . import iff_transitivity assert isinstance(other_iff, Iff) if self.B == other_iff.A: # from A <=> B, B <=> C, derive A <=> C return iff_transitivity.instantiate( {A: self.A, B: self.B, C: other_iff.B}, preserve_all=True) elif self.A == other_iff.A: # from y = x and y = z, derive x = z return self.derive_reversed().apply_transitivity(other_iff) elif self.A == other_iff.B: # from y = x and z = y, derive x = z return self.derive_reversed().apply_transitivity( other_iff.derive_reversed()) elif self.B == other_iff.B: # from x = y and z = y, derive x = z return self.apply_transitivity( other_iff.derive_reversed()) else: assert False, ('transitivity cannot be applied unless there ' 'is something in common in the equalities')
[docs] @equality_prover("defined", "define") def definition(self, **defaults_config): ''' Return (A <=> B) = [(A => B) and (B => A)] where self represents (A <=> B). ''' from . import iff_def return iff_def.instantiate({A: self.A, B: self.B})
[docs] @prover def conclude_by_definition(self, **defaults_config): ''' Conclude (A <=> B) assuming both (A => B), (B => A). ''' from . import iff_def, iff_intro if iff_intro.is_usable(): return iff_intro.instantiate({A: self.A, B: self.B}) return (iff_def.instantiate({A: self.A, B: self.B}) .derive_left_via_equality())
@equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' If the operands that to TRUE or FALSE, we can evaluate this expression as TRUE or FALSE. ''' from proveit.logic import TRUE, FALSE # Load in truth-table evaluations from . import iff_t_t, iff_t_f, iff_f_t, iff_f_f if must_evaluate: start_over = False for operand in self.operands: if operand not in (TRUE, FALSE): # The simplification of the operands may not have # worked hard enough. Let's work harder if we # must evaluate. operand.evaluation() start_over = True if start_over: return self.evaluation() # May now be able to evaluate via loaded truth tables. return Operation.shallow_simplification( self, must_evaluate=must_evaluate) def readily_in_bool(self): ''' Returns True if we can readily prove that the operands are provably boolean and therefore this Iff is boolean. ''' from proveit.logic import in_bool return (in_bool(self.A).readily_provable() and in_bool(self.B).readily_provable())
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): ''' Attempt to deduce, then return, that this 'iff' expression is in the set of BOOLEANS. ''' from . import iff_closure return iff_closure.instantiate( {A: self.A, B: self.B})
[docs] @prover def derive_equality(self, **defaults_config): ''' From (A <=> B), derive (A = B) assuming A and B in BOOLEANS. ''' from . import eq_from_iff, eq_from_mutual_impl # We must be able to prove this Iff to do this derivation -- # then either eq_from_iff or eq_from_mutual_impl can be used. self.prove() # eq_from_mutual_impl may make for a shorter proof; do it both # ways (if both are usable) if not eq_from_iff.is_usable(): return eq_from_mutual_impl.instantiate( {A: self.A, B: self.B}) eq_from_mutual_impl.instantiate( {A: self.A, B: self.B}) return eq_from_iff.instantiate( {A: self.A, B: self.B})