Source code for proveit.logic.booleans.booleans

from proveit import (Function, Literal, ProofFailure, UnusableProof,
                     defaults, prover, relation_prover, equality_prover)
from proveit.logic.irreducible_value import IrreducibleValue
from proveit.logic.sets.membership import SetMembership, SetNonmembership
from proveit import A, C, P, Q


[docs]class BooleanSet(Literal): def __init__(self, *, styles=None): Literal.__init__( self, string_format='BOOLEAN', latex_format=r'\mathbb{B}', styles=styles)
[docs] def membership_object(self, element): return BooleanMembership(element)
[docs] def nonmembership_object(self, element): return BooleanNonmembership(element)
[docs] @prover def forall_evaluation(self, forall_stmt, **defaults_config): ''' Given a forall statement over the BOOLEAN domain, evaluate to TRUE or FALSE if possible. ''' from proveit.logic import Forall, Equals, SimplificationError from . import false_eq_false, true_eq_true from . import forall_bool_eval_true, forall_bool_eval_false_via_t_f, \ forall_bool_eval_false_via_f_f, forall_bool_eval_false_via_f_t from . import TRUE, FALSE, Boolean from .conjunction import compose assert(isinstance(forall_stmt, Forall) ), "May only apply forall_evaluation method of BOOLEAN to a forall statement" assert(forall_stmt.domain == Boolean), "May only apply forall_evaluation method of BOOLEAN to a forall " \ "statement with the BOOLEAN domain" with defaults.temporary() as temp_defaults: temp_defaults.preserved_exprs = defaults.preserved_exprs.union([forall_stmt.instance_expr]) instance_list = list(forall_stmt.instance_param_lists()) instance_var = instance_list[0][0] instance_expr = forall_stmt.instance_expr P_op = Function(P, instance_var) true_instance = instance_expr.basic_replaced( {instance_var: TRUE}) false_instance = instance_expr.basic_replaced( {instance_var: FALSE}) temp_defaults.auto_simplify = False if true_instance == TRUE and false_instance == FALSE: # special case of Forall_{A in BOOLEAN} A false_eq_false # FALSE = FALSE true_eq_true # TRUE = TRUE return forall_bool_eval_false_via_t_f.instantiate( {P_op: instance_expr}).derive_conclusion() else: # must evaluate for the TRUE and FALSE case separately eval_true_instance = true_instance.evaluation() eval_false_instance = false_instance.evaluation() if not isinstance( eval_true_instance.expr, Equals) or not isinstance( eval_false_instance.expr, Equals): raise SimplificationError( 'Quantified instances must produce equalities as ' 'evaluations') # proper evaluations for both cases (TRUE and FALSE) true_case_val = eval_true_instance.rhs false_case_val = eval_false_instance.rhs if true_case_val == TRUE and false_case_val == TRUE: # both cases are TRUE, so the forall over the # boolean set is TRUE compose([eval_true_instance.derive_via_boolean_equality(), eval_false_instance.derive_via_boolean_equality()]) return forall_bool_eval_true.instantiate( {P_op: instance_expr, A: instance_var}) else: # one case is FALSE, so the forall over the boolean set is # FALSE compose([eval_true_instance, eval_false_instance]) if true_case_val == FALSE and false_case_val == FALSE: impl = forall_bool_eval_false_via_f_f.instantiate( {P_op: instance_expr, A: instance_var}) elif true_case_val == FALSE and false_case_val == TRUE: impl = forall_bool_eval_false_via_f_t.instantiate( {P_op: instance_expr, A: instance_var}) elif true_case_val == TRUE and false_case_val == FALSE: impl = forall_bool_eval_false_via_t_f.instantiate( {P_op: instance_expr, A: instance_var}) else: raise SimplificationError( 'Quantified instance evaluations must be TRUE or FALSE') return impl.derive_conclusion()
[docs] @prover def unfold_forall(self, forall_stmt, **defaults_config): ''' Given forall_{A in Boolean} P(A), derive and return [P(TRUE) and P(FALSE)]. ''' from proveit.logic import Forall from . import unfold_forall_over_bool from . import Boolean assert(isinstance(forall_stmt, Forall) ), "May only apply unfold_forall method of Boolean to a forall statement" assert(forall_stmt.domain == Boolean), "May only apply unfold_forall method of Boolean to a forall statement with the Boolean domain" Px = Function(P, forall_stmt.instance_var) _Px = forall_stmt.instance_expr _A = forall_stmt.instance_var return unfold_forall_over_bool.instantiate( {Px: _Px, A: _A}).derive_consequent()
@prover def prove_by_cases(self, forall_stmt, **defaults_config): ''' Given forall_{A in Boolean} P(A), conclude and return it from [P(TRUE) and P(FALSE)]. ''' from proveit.logic import Forall, And from . import forall_over_bool_by_cases, conditioned_forall_over_bool_by_cases from . import Boolean assert(isinstance(forall_stmt, Forall)), ( "May only apply prove_by_cases method of Boolean to a " "forall statement") assert(forall_stmt.domain == Boolean), ( "May only apply prove_by_cases method of Boolean " "to a forall statement with the Boolean domain") if forall_stmt.conditions.num_entries() > 1: if forall_stmt.conditions.is_double(): condition = forall_stmt.conditions[1] else: condition = And(*forall_stmt.conditions[1:].entries) Qx = Function(Q, forall_stmt.instance_param) _Qx = condition Px = Function(P, forall_stmt.instance_param) _Px = forall_stmt.instance_expr _A = forall_stmt.instance_param # We may need to auto-simplify in order to flatten the # conditions (if there are multiple conditions beyond the # domain condition), but we must preserve the different # parts. preserved_exprs = {forall_stmt, forall_stmt.instance_expr} preserved_exprs.update(forall_stmt.conditions) return conditioned_forall_over_bool_by_cases.instantiate( {Qx: _Qx, Px: _Px, A: _A}, num_forall_eliminations=1, preserved_exprs=preserved_exprs, auto_simplify=True) else: # forall_{A in Boolean} P(A), assuming P(TRUE) and P(FALSE) Px = Function(P, forall_stmt.instance_param) _Px = forall_stmt.instance_expr _A = forall_stmt.instance_param return forall_over_bool_by_cases.instantiate( {Px: _Px, A: _A}, num_forall_eliminations=1, preserve_expr=forall_stmt)
class BooleanMembership(SetMembership): ''' Defines methods that apply to InSet(element, Boolean) objects via InSet.__getattr__ which calls Boolean.membership_object(element) to return a BooleanMembership object. ''' def __init__(self, element): from . import Boolean SetMembership.__init__(self, element, Boolean) def side_effects(self, judgment): ''' Yield side-effect methods to try when the element is proven to be in the Boolean set by calling 'in_bool_side_effects' on the element if it has such a method. Edited by JML on 6/27/19 to add fold_is_bool side_effect ''' from proveit.logic.booleans import unfold_is_bool, fold_is_bool if hasattr(self.element, 'in_bool_side_effects'): for side_effect in self.element.in_bool_side_effects(judgment): yield side_effect # don't automatically do unfold_is_bool_explicit if unfold_is_bool is # unusable -- avoids infinite recursion if unfold_is_bool.is_usable(): yield self.unfold def _readily_provable(self): ''' This Boolean membership is readily provable if the element is readily provable or disprovable. ''' element = self.element if element.readily_provable() or element.readily_disprovable(): return True if hasattr(element, 'readily_in_bool'): return element.readily_in_bool() return False @prover def conclude(self, **defaults_config): ''' Try to deduce that the given element is in the Boolean set under the given assumptions. ''' from . import in_bool_if_true, in_bool_if_false element = self.element # if the element is already proven or disproven, use in_bool_if_true or # in_bool_if_false if element.proven(): return in_bool_if_true.instantiate({A: element}) if element.disproven(): return in_bool_if_false.instantiate({A: element}) # Use 'deduce_in_bool' if the element has that method. if hasattr(element, 'deduce_in_bool'): return element.deduce_in_bool() raise ProofFailure(in_bool(element), defaults.assumptions, str( element) + ' not proven to be equal to TRUE or FALSE.') @equality_prover('defined', 'define') def definition(self, **defaults_config): ''' Deduce [(element in Boolean) = [(element = TRUE) or (element = FALSE)]. ''' from . import in_bool_def return in_bool_def.instantiate({A: self.element}) @prover def unfold(self, **defaults_config): ''' From in_bool(Element), derive and return [element or not(element)] if unfold_is_bool is usable. It it is not, instead try to derive and return [(element=TRUE) or (element=FALSE)]. ''' from . import unfold_is_bool, unfold_is_bool_explicit if unfold_is_bool.is_usable(): # [element or not(element)] assuming in_bool(element) return unfold_is_bool.instantiate( {A: self.element}) else: # [(element = TRUE) or (element = FALSE)] assuming in_bool(element) return unfold_is_bool_explicit.instantiate( {A: self.element}) @prover def fold(self, **defaults_config): ''' From [(element=TRUE) or (element=FALSE)], derive in_bool(Element). Created by JML on 6/27/19 for fold_is_bool side_effect ''' from . import fold_is_bool if fold_is_bool.is_usable(): return fold_is_bool.instantiate( {A: self.element}, preserve_expr=in_bool(self.element)) @prover def derive_via_excluded_middle(self, consequent, **defaults_config): ''' Derive the consequent from (element in Boolean) given element => consequent and Not(element) => consequent. ''' from . import from_excluded_middle return from_excluded_middle.instantiate( {A: self.element, C: consequent}, preserve_expr=consequent) def readily_in_bool(self): return True @relation_prover def deduce_in_bool(self, **defaults_config): from . import in_bool_is_bool return in_bool_is_bool.instantiate({A: self.element}) class BooleanNonmembership(SetNonmembership): def __init__(self, element): from . import Boolean SetNonmembership.__init__(self, element, Boolean) @equality_prover("defined", "define") def definition(self, element, **defaults_config): ''' Derive [(element not in Boolean) = [(element != TRUE) and (element != FALSE)]. ''' from . import not_in_bool_equiv return not_in_bool_equiv.instantiate({A: element})
[docs]class TrueLiteral(Literal, IrreducibleValue): def __init__(self, *, styles=None): Literal.__init__(self, string_format='TRUE', latex_format=r'\top', styles=styles)
[docs] @prover def conclude(self, **defaults_config): from . import true_axiom return true_axiom
[docs] @prover def eval_equality(self, other, **defaults_config): from . import true_eq_true, true_not_false from . import TRUE, FALSE if other == TRUE: return true_eq_true.evaluation() elif other == FALSE: return true_not_false.unfold().equate_negated_to_false()
def readily_not_equal(self, other): ''' Return True iff 'other' is FALSE. ''' from . import FALSE if other==FALSE: return True return False @relation_prover def deduce_not_equal(self, other, **defaults_config): from . import true_not_false from . import TRUE, FALSE if other == FALSE: return true_not_false if other == TRUE: raise ProofFailure( "Cannot prove TRUE != TRUE since that statement is false") raise ProofFailure( "Inequality between TRUE and a non-boolean not defined") def readily_in_bool(self): return True
[docs] @prover def deduce_in_bool(self, **defaults_config): from . import true_is_bool return true_is_bool
[docs]class FalseLiteral(Literal, IrreducibleValue): def __init__(self, *, styles=None): Literal.__init__(self, string_format='FALSE', latex_format=r'\bot', styles=styles)
[docs] @prover def eval_equality(self, other, **defaults_config): from . import false_not_true from . import false_eq_false from . import TRUE, FALSE if other == FALSE: return false_eq_false.evaluation() elif other == TRUE: return false_not_true.unfold().equate_negated_to_false()
[docs] @prover def conclude_negation(self, **defaults_config): from proveit.logic.booleans.negation import not_false return not_false # the negation of FALSE
def readily_not_equal(self, other): ''' Return True iff 'other' is TRUE. ''' from . import TRUE if other==TRUE: return True return False @relation_prover def deduce_not_equal(self, other, **defaults_config): from _.theorems_ import false_not_true from . import TRUE, FALSE if other == TRUE: return false_not_true if other == FALSE: raise ProofFailure( "Cannot prove FALSE != FALSE since that statement is false") raise ProofFailure( "Inequality between FALSE and a non-boolean not defined") def readily_in_bool(self): return True
[docs] @prover def deduce_in_bool(self, **defaults_config): from . import false_is_bool return false_is_bool
[docs] @prover def deny_assumption(self, assumption_to_deny, **defaults_config): ''' If FALSE can be proven under a set of assumptions, any one of those assumptions may be proven untrue given the other assumptions. ''' impl = self.prove().as_implication(assumption_to_deny) # Exclude the assumption_to_deny from the assumptions return impl.deny_antecedent(assumptions=[ assumption for assumption in defaults.assumptions if assumption != assumption_to_deny])
[docs]def in_bool(*elements): from proveit.logic.sets import InSet from . import Boolean if len(elements) == 1: return InSet(elements[0], Boolean) return [InSet(element, Boolean) for element in elements]