Source code for proveit.logic.equality.equals

from proveit import (Expression, Judgment, as_expression, 
                     defaults, USE_DEFAULTS, ProofFailure,
                     UnsatisfiedPrerequisites,
                     Conditional, ExprTuple, equality_prover, InnerExpr,
                     InnerExprGenerator, free_vars)
from proveit.util import OrderedSet
from proveit import Literal, Operation, Lambda, ArgumentExtractionError
from proveit.relation import EquivRelation, TransitivityException
from proveit import relation_prover, prover
from proveit.logic.irreducible_value import is_irreducible_value
from proveit import a, b, c, d, k, A, B, P, Q, f, n, x, y, z

[docs]class Equals(EquivRelation): # operator of the Equals operation _operator_ = Literal(string_format='=', theory=__file__) # Map Expressions to sets of Judgments of equalities that involve # the Expression on the left hand or right hand side. known_equalities = dict() # Map each Expression/defaults._simplification_directives_id # combination to a single known_equality deemed to effect a # simplification according to the simplification directives of # the id. known_simplifications = dict() # Specific simplifications that simplify the inner expression to # IrreducibleValue objects. known_evaluation_sets = dict() # Record found inversions. See the invert method. # Maps (lambda_map, rhs) pairs to a list of # (known_equality, inversion) pairs, recording previous results # of the invert method for future reference. inversions = dict() # Record the Equals objects being initialized (to avoid infinite # recursion while automatically deducing an equality is in Boolean). initializing = set() def __init__(self, a, b, *, styles=None): EquivRelation.__init__(self, Equals._operator_, a, b, styles=styles) ''' # May be better not to be proactive but we need to see if this # breaks anything. if self not in Equals.initializing: Equals.initializing.add(self) try: self.deduce_in_bool() # proactively prove (a=b) in Boolean. except: # may fail before the relevent _axioms_ have been generated pass # and that's okay Equals.initializing.remove(self) ''' def _record_as_proven(self, judgment): ''' 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. ''' Equals.known_equalities.setdefault( self.lhs, OrderedSet()).add(judgment) Equals.known_equalities.setdefault( self.rhs, OrderedSet()).add(judgment) if is_irreducible_value(self.rhs): # With an irreducible right hand side, remember this as # an evaluation. assert isinstance(judgment.expr, Equals) Equals.known_evaluation_sets.setdefault( self.lhs, set()).add(judgment)
[docs] def 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. ''' from proveit.logic.booleans import TRUE, FALSE if self.lhs == self.rhs: # Don't bother with side-effects for reflexive equalities. return # automatically derive the reversed form which is equivalent yield self.derive_reversed if self.rhs == FALSE: if self.lhs.proven(): # readily provable doesn't seem to work here # derive FALSE given lhs=FALSE and lhs. yield self.derive_contradiction # Use this form after merging in 'Expression.proven' commite: # if self.lhs.proven(): # If lhs is proven using default assumptions. # # derive FALSE given lhs=FALSE and lhs. # yield self.derive_contradiction if self.rhs in (TRUE, FALSE): # automatically derive A from A=TRUE or Not(A) from A=FALSE yield self.derive_via_boolean_equality if hasattr(self.lhs, 'equality_side_effects'): for side_effect in self.lhs.equality_side_effects(judgment): yield side_effect
[docs] def negation_side_effects(self, judgment): ''' Side-effect derivations to attempt automatically for a negated equation. ''' yield self.deduce_not_equals # A != B from not(A=B)
def _readily_provable(self, try_readily_equal=True, check_transitive_pair=None): ''' Return True iff this equality is readily provable: * The lhs and rhs have the same canonical form; * The lhs has a '_readily_equal' method that returns True. * One side is TRUE/FALSE and the other side is provable/disprovable., * The sides mutually imply each other and each side is provably boolean. * There is a known (indirect) equality through the known equalities and/or canonical forms. 'check_transitive_pair' isn't used since this is already essentially more powerful via indirect known equalities and/or canonical forms (this should be revisited/tested to make sure we can conclude everything that is readily provable and that this isn't too slow). ''' from proveit.logic import TRUE, FALSE, Iff, in_bool lhs, rhs = self.lhs, self.rhs if lhs == rhs: return True if try_readily_equal: if hasattr(lhs, 'readily_equal'): if lhs.readily_equal(rhs): return True if hasattr(rhs, 'readily_equal'): if rhs.readily_equal(lhs): return True if lhs.canonical_form() == rhs.canonical_form(): return True if (lhs == TRUE and rhs.readily_provable()) or ( rhs == TRUE and lhs.readily_provable()): return True if (lhs == FALSE and rhs.readily_disprovable()) or ( rhs == FALSE and lhs.readily_disprovable()): return True if not isinstance(lhs, ExprTuple) and ( not isinstance(rhs, ExprTuple) and Iff(lhs, rhs).readily_provable() and in_bool(lhs).readily_provable() and in_bool(rhs).readily_provable()): from proveit.logic.booleans.implication import eq_from_iff if eq_from_iff.is_usable(): return True for eq_expr in Equals.yield_known_equal_expressions(lhs): if eq_expr == rhs: return True return False def _readily_disprovable(self): ''' Equals is disprovable if NotEquals is provable. ''' from .not_equals import NotEquals return NotEquals(self.lhs, self.rhs).readily_provable()
[docs] @prover def 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. ''' from proveit.logic import TRUE, FALSE, Iff, in_bool lhs, rhs = self.lhs, self.rhs if lhs == rhs: # Trivial x=x return self.conclude_via_reflexivity() if (lhs in (TRUE, FALSE)) or (rhs in (TRUE, FALSE)): try: # Try to conclude as TRUE or FALSE. return self.conclude_boolean_equality() except ProofFailure: pass if hasattr(lhs, 'readily_equal') and ( lhs.readily_equal(rhs)): # Use an Expression-specific deduce_equal return lhs.deduce_equal(rhs) if hasattr(rhs, 'readily_equal') and ( rhs.readily_equal(lhs)): # Use an Expression-specific deduce_equal in reverse. return rhs.deduce_equal(lhs).derive_reversed() if lhs.canonical_form() == rhs.canonical_form() and ( not lhs._is_effective_relation() or self.canonical_form() == Expression._build_canonical_form(self)): # If the canonical forms are the same, we should be able # to prove equality via 'deduce_canonically_equal'. return lhs.deduce_canonically_equal(rhs) if not isinstance(lhs, ExprTuple) and ( not isinstance(rhs, ExprTuple) and Iff(lhs, rhs).readily_provable() and in_bool(lhs).readily_provable() and in_bool(rhs).readily_provable()): # There is mutual implication both sides are known to be # boolean. Conclude equality via mutual implication. self.conclude_via_mutual_implication() # Try the 'deduce_equal' method. If NotImplementedError # or UnsatisfiedPrerequisites is raised, we'll move on. if hasattr(lhs, 'deduce_equal'): try: return lhs.deduce_equal(rhs) except (NotImplementedError, UnsatisfiedPrerequisites): # 'deduce_equal' not implemented for this # particular case, so carry on with default approach. pass # Try to prove equality via standard EquiRelation # strategies (simplify both sides then try transitivity). return EquivRelation.conclude(self, check_transitive_pair=False)
@prover def conclude_negation(self, **defaults_config): ''' Attempt to conclude the negation of this equality. ''' from proveit.logic import NotEquals return NotEquals(self.lhs, self.rhs).unfold() @prover def conclude_via_mutual_implication(self, **defaults_config): ''' Prove A = B via A <=> B. ''' from proveit.logic import Iff lhs, rhs = self.lhs, self.rhs return Iff(lhs, rhs).derive_equality() @prover def conclude_via_direct_substitution(self, **defaults_config): ''' Prove that this Equals expression is true by directly and greedily substituting sub-expressions that differ but are known, or readily provable, to be equal 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'. ''' from proveit import ExprRange if self.proven(): # Already known. Done. return self.prove() def raise_different_structures(): raise ValueError("%s and %s have different structures " "and cannot be equated via direct " "substitution"%(self.lhs, self.rhs)) lhs_inner_gen = InnerExprGenerator(self.lhs) rhs_inner_gen = InnerExprGenerator(self.rhs) lambda_body = self.lhs lambda_parameters = [] # Equating all entries (elements and ranges). all_equalities_lhs = [] all_equalities_rhs = [] replacements = [] while True: try: next_inner_lhs = next(lhs_inner_gen) except StopIteration: try: next_inner_rhs = next(rhs_inner_gen) except StopIteration: break # lhs finished before rhs: raise_different_structures() try: next_inner_rhs = next(rhs_inner_gen) except StopIteration: # rhs finished before lhs: raise_different_structures() inner_expr_path = next_inner_lhs.inner_expr_path if (inner_expr_path != next_inner_rhs.inner_expr_path): raise_different_structures() # Check if the lhs/rhs InnerExpr objects correspond to the # same sub-expression or sub-expressions that are known to # be equal. lhs_sub_expr = next_inner_lhs.cur_sub_expr() rhs_sub_expr = next_inner_rhs.cur_sub_expr() assumptions = (next_inner_lhs.assumptions + tuple(next_inner_lhs.conditions)) if lhs_sub_expr == rhs_sub_expr: # These sub-expressions are the same, so we can # skip over this entire branch. lhs_inner_gen.skip_over_branch() rhs_inner_gen.skip_over_branch() continue if isinstance(lhs_sub_expr, ExprRange) or ( isinstance(rhs_sub_expr, ExprRange)): equality = None else: equality = Equals(lhs_sub_expr, rhs_sub_expr) if isinstance(lhs_sub_expr, Lambda) and ( isinstance(rhs_sub_expr, Lambda)): # Don't replace Lambda's directly, replace their bodies # and make sure their parameters are the same. if lhs_sub_expr.parameters != rhs_sub_expr.parameters: raise_different_structures() equality = None if isinstance(lhs_sub_expr, ExprTuple) and ( isinstance(rhs_sub_expr, ExprTuple) and lhs_sub_expr.num_entries() == rhs_sub_expr.num_entries()): # Don't replace an entire ExprTuple if we can replace # individual entries. equal_entrywise = True for left_entry, right_entry in zip(lhs_sub_expr.entries, rhs_sub_expr.entries): if left_entry == right_entry: continue # identical entries. if isinstance(left_entry, ExprRange) or ( isinstance(right_entry, ExprRange)): # If there are non-identical expression ranges, # replace the entire ExprTuple if possible. equal_entrywise = False break if not Equals(left_entry, right_entry).proven( assumptions=assumptions): equal_entrywise = False break if equal_entrywise: equality = None if equality is not None and equality != self and ( equality.readily_provable(assumptions=assumptions)): # These sub-expressions are known to be equal, # so let's replace the corresponding location # with a lambda parameter for our lambda expression. # Create the InnerExpr for the lambda_body for # the current inner expression path and use this # to create the new lambda_body and extend the # parameters. lambda_body_inner_expr = InnerExpr( lambda_body, inner_expr_path=inner_expr_path) params = free_vars(equality).intersection( lambda_body_inner_expr.parameters) # If any assumptions are required that are introduced # by inner conditions, we need to equate Conditionals. inner_conditions = set(next_inner_lhs.conditions).intersection( next_inner_rhs.conditions) conditions = [] equality = equality.prove(assumptions=assumptions) for assumption in equality.assumptions: if assumption in inner_conditions: conditions.append(assumption) if len(conditions) > 0: # Wrap sub-expressions in Conditionals. lhs_sub_expr = Conditional(lhs_sub_expr, conditions) rhs_sub_expr = Conditional(rhs_sub_expr, conditions) # Make sure we replace the Conditional with # its value where the condition is redundant. replacement = lhs_sub_expr.satisfied_condition_reduction( assumptions=conditions) replacements.append(replacement) replacement = rhs_sub_expr.satisfied_condition_reduction( assumptions=conditions) replacements.append(replacement) if len(params) > 0: # We are substituting an inner scope with inner # parameters. # Generalize the equality over the parameters # with appropriate conditions. universal_eq = equality.generalize(params, conditions=conditions) lhs_lambda = Lambda(params, lhs_sub_expr) equality = lhs_lambda.substitution(universal_eq) elif len(conditions) > 0: # No parameters but using Conditionals. equality = Equals(lhs_sub_expr, rhs_sub_expr).prove() repl_lambda = lambda_body_inner_expr.repl_lambda( params_of_param=params) lambda_body = repl_lambda.body lambda_parameters.extend(repl_lambda.parameters.entries) # We can skip over this branch now. lhs_inner_gen.skip_over_branch() rhs_inner_gen.skip_over_branch() all_equalities_lhs.append(equality.lhs) all_equalities_rhs.append(equality.rhs) else: # These sub-expressions are different. They could # have known equalities at a deeper level, but let's # make sure they have the same structure. if (lhs_sub_expr.core_info() != rhs_sub_expr.core_info() or (lhs_sub_expr.num_sub_expr() != rhs_sub_expr.num_sub_expr())): raise_different_structures() # Make the lambda map to use for substitutions. lambda_map = Lambda(lambda_parameters, lambda_body) if (len(all_equalities_lhs)==1 and not isinstance(all_equalities_lhs[0], ExprRange)): # Just one, basic equality which we already know. return equality.substitution(lambda_map, replacements=replacements) else: # Multi-operand substitution. tuple_eq = Equals(ExprTuple(*all_equalities_lhs), ExprTuple(*all_equalities_rhs)) return tuple_eq.substitution( lambda_map, replacements=replacements) """ (0 = (t - ((t - 1) + 1)), t - ((t - 1) + 1) if 0 = (t - ((t - 1) + 1))) = (TRUE, 0 if 0 = (t - ((t - 1) + 1))) {MULTI_QUDIT_GATE(CONTROL, {t - ((t - 1) + 1), t}) if 0 = (t - ((t - 1) + 1)). = {MULTI_QUDIT_GATE(CONTROL, {0, t}) if TRUE. [{0 = (t - ((t - 1) + 1))} |- {t - ((t - 1) + 1) if 0 = (t - ((t - 1) + 1)). = (t - ((t - 1) + 1)), {0 = (t - ((t - 1) + 1))} |- {0 if 0 = (t - ((t - 1) + 1)). = 0] """ """ Abandoning, but keeping a stub in case we want to revisit this: @prover def conclude_via_substitutions(self, *equalities, **defaults_config): ''' Prove that this Equals expression is true by using the supplied proven equalities and performing substitutions. This is the "Equivalence Closure Problem" which Deepak Kapur has written papers on: Journal of Systems Science and Complexity volume 32, pages 317–355 (2019), https://10.4230/LIPIcs.FSCD.2021.15 https://doi.org/10.1007/3-540-62950-5_59 His algorithms are O(n log n) for binary functions and O(n^2) in general. ''' """ @staticmethod def yield_directly_known_eq_exprs(expr, *, assumptions=USE_DEFAULTS, include_canonical_forms=True): ''' Generate expressions that are directly known to be equal to the given expression. If 'include_canonical_form' is True, also include expressions that are presumed to be equal to the given one by having the same canonical form. ''' known_equalities = Equals.known_equalities.get(expr, tuple()) # No need to report the expression we started with. reported = set([expr]) for eq_judgment in known_equalities: if eq_judgment.is_applicable(assumptions): for _expr in (eq_judgment.lhs, eq_judgment.rhs): if _expr not in reported: reported.add(_expr) yield _expr if include_canonical_forms: cf = expr.canonical_form() for expr in Expression.canonical_form_to_exprs[cf]: if expr not in reported: reported.add(expr) yield expr
[docs] @staticmethod def known_relations_from_left(expr, *, assumptions=USE_DEFAULTS, 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. ''' for other_expr in Equals.yield_directly_known_eq_exprs( expr, assumptions=assumptions, include_canonical_forms=include_canonical_forms): eq = Equals(expr, other_expr) yield (eq, eq.rhs)
[docs] @staticmethod def known_relations_from_right(expr, *, assumptions=USE_DEFAULTS, 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. ''' for other_expr in Equals.yield_directly_known_eq_exprs( expr, assumptions=assumptions, include_canonical_forms=include_canonical_forms): eq = Equals(other_expr, expr) yield (eq, eq.lhs)
[docs] @prover def conclude_via_reflexivity(self, **defaults_config): ''' Prove and return self of the form x = x. ''' from . import equals_reflexivity assert self.lhs == self.rhs return equals_reflexivity.instantiate({x: self.lhs})
[docs] @prover def derive_reversed(self, **defaults_config): ''' From x = y derive y = x. This derivation is an automatic side-effect. ''' from . import equals_reversal return equals_reversal.instantiate({x: self.lhs, y: self.rhs})
def reversed(self): ''' Return an Equals expression with the right side and left side reversed from this one. This is not a derivation: see derive_reversed(). ''' return Equals(self.rhs, self.lhs) @equality_prover("reversed", "reverse") def symmetrization(self, **defaults_config): ''' Prove (x = y) = (y = x). ''' from . import equals_symmetry return equals_symmetry.instantiate({y:self.lhs, x:self.rhs}) @staticmethod def yield_known_equal_expressions(expr, *, exceptions=None, include_canonical_forms=True, assumptions=USE_DEFAULTS): ''' 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. If 'include_canonical_forms' is True, also account for presumed equalities by having the same canonical form. ''' # Make sure we derive assumption side-effects first. from proveit import Assumption Assumption.make_assumptions() to_process = OrderedSet() to_process.add(expr) processed = set() while len(to_process) > 0: expr = to_process.pop() if expr in processed: continue if (exceptions is not None and expr in exceptions): # Skip this 'exception'. continue yield expr processed.add(expr) for expr in Equals.yield_directly_known_eq_exprs( expr, assumptions=assumptions, include_canonical_forms=include_canonical_forms): if expr not in processed: to_process.add(expr)
[docs] @prover def deduce_not_equals(self, **defaults_config): r''' Deduce x != y assuming not(x = y), where self is x=y. ''' from .not_equals import NotEquals return NotEquals(self.lhs, self.rhs).conclude_as_folded()
''' # This isn't right. def deduce_negated(self, i, assumptions=USE_DEFAULTS): from proveit.logic.booleans.conjunction import falsified_and_if_not_right, falsified_and_if_not_left, falsified_and_if_neither if i == 0: # Deduce Not(A and B) from Not(A). return falsified_and_if_not_right.instantiate( {A: self.operands[0], B: self.operands[1]}, assumptions=assumptions) if i == 1: return falsified_and_if_not_left.instantiate( {A: self.operands[0], B: self.operands[1]}, assumptions=assumptions) else: return falsified_and_if_neither.instantiate( {A: self.operands[0], B: self.operands[1]}, assumptions=assumptions) '''
[docs] @prover def 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. ''' from . import equals_transitivity other = as_expression(other) if not isinstance(other, Equals): # If the other relation is not "Equals", call from the "other" # side. return other.apply_transitivity(self) other_equality = other # We can assume that y=x will be a Judgment if x=y is a Judgment # because it is derived as a side-effect. if self.rhs == other_equality.lhs: return equals_transitivity.instantiate( {x: self.lhs, y: self.rhs, z: other_equality.rhs}, preserve_all=True) elif self.rhs == other_equality.rhs: return equals_transitivity.instantiate( {x: self.lhs, y: self.rhs, z: other_equality.lhs}, preserve_all=True) elif self.lhs == other_equality.lhs: return equals_transitivity.instantiate( {x: self.rhs, y: self.lhs, z: other_equality.rhs}, preserve_all=True) elif self.lhs == other_equality.rhs: return equals_transitivity.instantiate( {x: self.rhs, y: self.lhs, z: other_equality.lhs}, preserve_all=True) else: raise TransitivityException( None, defaults.assumptions, 'Transitivity cannot be applied unless there is something in common in the equalities: %s vs %s' % (str(self), str(other)))
@staticmethod @prover def relate_across_chain_transitively(*elements, **defaults_config): ''' Use transitivity to relate the first element to the last element through a chain of relations through all of the elements in order. ''' from proveit import ExprRange num_elements = len(elements) if num_elements == 0: raise TransitivityException( None, defaults.assumptions, 'Empty chain of elements to relate') if num_elements == 1: # Trivial case of a single element equal to itself. elem = elements[0] return Equals(elem, elem).conclude_via_reflexivity() elif num_elements == 2: # Simple case of a single relation. return Equals(*elements).prove() elif num_elements == 3: # x=y and y=z => x=z return Equals(*elements[:2]).apply_transitivity( Equals(*elements[1:])) elif num_elements == 4: # a=b, b=c, c=d => a=d from . import four_chain_transitivity _a, _b, _c, _d = elements return four_chain_transitivity.instantiate( {a:_a, b:_b, c:_c, d:_d}) else: raise NotImplementedError( "There are issues instantiating transitivity_chain " "that need to be resolved; may require ExprRange " "fixes") """ # A chain with more than 4 elements from proveit import IndexedVar from proveit.numbers import subtract, one, quick_simplified_index from proveit.numbers import Add from proveit.core_expr_types import x_1_to_np1 from . import transitivity_chain _x = ExprTuple(*elements) if isinstance(_x[0], ExprRange) or isinstance(_x[1], ExprRange): raise NotImplementedError( "'relate_across_chain_transitively' not implemented " "when there is an ExprRange at as the first or last " "of the entries, though it should be possible.") _np1 = quick_simplified_index(_x.num_elements()) _n = quick_simplified_index(subtract(_x.num_elements(), one)) x_full = ExprTuple(x_1_to_np1).basic_replaced({n:_n}) # We really need to simplify instantiating this sort of # thing. (see Issue #264) print(ExprRange(k, k, one, _np1).partition(_n)) #print(ExprRange(k, k, one, _np1).partition( # one).inner_expr().rhs[1].shifted( # new_start=one)) print(ExprRange(k, k, one, _np1).partition(one)) x_split1 = x_full[0].partitioned(_n) #x_split2 = x_full[0].partition(one).inner_expr().rhs[1].shift( # new_start=one).rhs # (x_1, x_{1+1}, ..., x_{n+1}) x_split2 = x_full[0].partitioned(one) return transitivity_chain.instantiate( {n:_n, x:_x, x_split1:_x, x_split2:_x}) """
[docs] @prover def 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. ''' from proveit.logic import TRUE, FALSE from proveit.logic.booleans import eq_true_elim from proveit.logic import Not if self.rhs == TRUE: return eq_true_elim.instantiate({A: self.lhs}) # A elif self.rhs == FALSE: # Not(A) return Not(self.lhs).conclude_via_falsified_negation()
[docs] @prover def derive_contradiction(self, **defaults_config): ''' From A=FALSE, and assuming A, derive FALSE. ''' from proveit.logic import FALSE from . import contradiction_via_falsification if self.rhs == FALSE: return contradiction_via_falsification.instantiate( {A: self.lhs}) raise ValueError( 'Equals.derive_contradiction is only applicable if the ' 'right-hand-side is FALSE')
[docs] @prover def 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. ''' from proveit.logic.booleans.implication import affirm_via_contradiction return affirm_via_contradiction(self, conclusion)
[docs] @prover def 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. ''' from proveit.logic.booleans.implication import deny_via_contradiction return deny_via_contradiction(self, conclusion)
[docs] @prover def 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. ''' from proveit.logic import TRUE, FALSE, Not from proveit.logic.booleans import eq_true_intro if self.rhs == TRUE: return eq_true_intro.instantiate({A: self.lhs}) elif self.rhs == FALSE: if isinstance(self.lhs, Not): evaluation = self.lhs.evaluation() if evaluation.rhs == self.rhs: return evaluation else: return Not(self.lhs).equate_negated_to_false() elif self.lhs == TRUE or self.lhs == FALSE: return Equals(self.rhs, self.lhs).conclude_boolean_equality( ).derive_reversed() raise ProofFailure( self, defaults.assumptions, "May only conclude via boolean equality if one side of the equality is TRUE or FALSE")
[docs] @prover def derive_is_in_singleton(self, **defaults_config): ''' From (x = y), derive (x in {y}). ''' from proveit.logic.sets.enumeration import fold_singleton return fold_singleton.instantiate({x: self.lhs, y: self.rhs})
@staticmethod def _lambda_expr(lambda_map, expr_being_replaced): from proveit import InnerExpr if isinstance(lambda_map, InnerExpr): lambda_map = lambda_map.repl_lambda() if not isinstance(lambda_map, Lambda): # as a default, do a global replacement lambda_map = Lambda.global_repl(lambda_map, expr_being_replaced) return lambda_map
[docs] @prover # Note: this should NOT be an @equality_prover. def 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. ''' from proveit import Conditional from . import substitution if isinstance(lambda_map, Conditional): conditional = lambda_map if self.lhs == conditional.value: # Return the substitution equality for swapping out # the value of a conditional which may implicitly # assume that the condition is satisfied. return conditional.value_substitution(self) lambda_map = Equals._lambda_expr(lambda_map, self.lhs) extra_kwargs = {'simplify_only_where_marked': True, 'markers_and_marked_expr': ( lambda_map.parameter_vars, Equals(lambda_map.body, lambda_map.body))} if not lambda_map.parameters.is_single(): # We must use operands_substitution for ExprTuple # substitution. from proveit.core_expr_types.operations import \ operands_substitution, operands_substitution_via_tuple _n = lambda_map.parameters.num_elements() if self.proven(): # If we know the tuples are equal, use the theorem # with this equality as a prerequisite. return operands_substitution_via_tuple.instantiate( {n: _n, f: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) # Otherwise, we'll use the axiom in which the prerequisite # is that the individual elements are equal. return operands_substitution.instantiate( {n: _n, f: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) # Regular single-operand substitution: return substitution.instantiate( {f: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs)
[docs] @prover def 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. ''' from . import sub_left_side_into from . import (substitute_truth, substitute_in_true, substitute_falsehood, substitute_in_false) from proveit.logic import TRUE, FALSE lambda_map = Equals._lambda_expr(lambda_map, self.rhs) # Check if we want to use the reverse equality for a shorter # proof. reversed_eq = Equals(self.rhs, self.lhs) if reversed_eq.proven(): if (reversed_eq.prove().proof().num_steps() < self.prove().proof().num_steps()): # Reverse it for a shorter proof. return reversed_eq.sub_right_side_into(lambda_map) extra_kwargs = {'simplify_only_where_marked': True, 'markers_and_marked_expr': (lambda_map.parameter_vars, lambda_map.body)} if not lambda_map.parameters.is_single(): # We must use sub_in_left_operands for ExprTuple # substitution. from proveit.logic.equality import \ sub_in_left_operands, sub_in_left_operands_via_tuple _n = lambda_map.parameters.num_elements() if self.proven(): # If we know the tuples are equal, use the theorem # with this equality as a prerequisite. return sub_in_left_operands_via_tuple.instantiate( {n: _n, P: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) return sub_in_left_operands.instantiate( {n: _n, P: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) try: # try some alternative proofs that may be shorter, if # they are usable if self.rhs == TRUE: # substitute_truth may provide a shorter proof # option substitute_truth.instantiate( {x: self.lhs, P: lambda_map}, **extra_kwargs) elif self.lhs == TRUE: # substitute_in_true may provide a shorter proof # option substitute_in_true.instantiate( {x: self.rhs, P: lambda_map}, **extra_kwargs) elif self.rhs == FALSE: # substitute_falsehood may provide a shorter proof # option substitute_falsehood.instantiate( {x: self.lhs, P: lambda_map}, **extra_kwargs) elif self.lhs == FALSE: # substitute_in_false may provide a shorter proof # option substitute_in_false.instantiate( {x: self.rhs, P: lambda_map}, **extra_kwargs) except BaseException: pass return sub_left_side_into.instantiate( {x: self.lhs, y: self.rhs, P: lambda_map}, **extra_kwargs)
[docs] @prover def 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. ''' from . import sub_right_side_into from . import (substitute_truth, substitute_in_true, substitute_falsehood, substitute_in_false) from proveit.logic import TRUE, FALSE # Check if we want to use the reverse equality for a shorter # proof. reversed_eq = Equals(self.rhs, self.lhs) if reversed_eq.proven(): if (reversed_eq.prove().proof().num_steps() < self.prove().proof().num_steps()): # Reverse it for a shorter proof. return reversed_eq.sub_left_side_into(lambda_map) lambda_map = Equals._lambda_expr(lambda_map, self.lhs) extra_kwargs = {'simplify_only_where_marked': True, 'markers_and_marked_expr': (lambda_map.parameter_vars, lambda_map.body)} if not lambda_map.parameters.is_single(): # We must use sub_in_right_operands for ExprTuple # substitution. from proveit.logic.equality import \ sub_in_right_operands, sub_in_right_operands_via_tuple _n = lambda_map.parameters.num_elements() if self.proven(): # If we know the tuples are equal, use the theorem # with this equality as a prerequisite. return sub_in_right_operands_via_tuple.instantiate( {n: _n, P: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) return sub_in_right_operands.instantiate( {n: _n, P: lambda_map, x: self.lhs, y: self.rhs}, **extra_kwargs) try: # try some alternative proofs that may be shorter, if # they are usable if self.lhs == TRUE: # substitute_truth may provide a shorter proof # options substitute_truth.instantiate( {x: self.rhs, P: lambda_map}, **extra_kwargs) elif self.rhs == TRUE: # substitute_in_true may provide a shorter proof # options substitute_in_true.instantiate( {x: self.lhs, P: lambda_map}, **extra_kwargs) elif self.lhs == FALSE: # substitute_falsehood may provide a shorter proof # options substitute_falsehood.instantiate( {x: self.rhs, P: lambda_map}, **extra_kwargs) elif self.rhs == FALSE: # substitute_in_false may provide a shorter proof # options substitute_in_false.instantiate( {x: self.lhs, P: lambda_map}, **extra_kwargs) except BaseException: pass return sub_right_side_into.instantiate( {x: self.lhs, y: self.rhs, P: lambda_map}, **extra_kwargs)
[docs] @prover def derive_right_via_equality(self, **defaults_config): ''' From A = B, derive B (the Right-Hand-Side) assuming A. ''' from . import rhs_via_equality return rhs_via_equality.instantiate({P: self.lhs, Q: self.rhs})
[docs] @prover def derive_left_via_equality(self, **defaults_config): ''' From A = B, derive A (the Right-Hand-Side) assuming B. ''' from . import lhs_via_equality return lhs_via_equality.instantiate({P: self.lhs, Q: self.rhs})
[docs] def other_side(self, expr): ''' Returns the 'other' side of the of the equation if the given expr is on one side. ''' if expr == self.lhs: return self.rhs elif expr == self.rhs: return self.lhs raise ValueError( 'The given expression is expected to be one of the sides of the equation')
def readily_in_bool(self): return True # equality is always boolean
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): ''' Deduce and return that this equality statement is in the Boolean set. ''' from . import equality_in_bool return equality_in_bool.instantiate({x: self.lhs, y: self.rhs}, preserve_all=True)
@equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Given equality operands that are the same or are irreducible values, return this expression equated to TRUE or FALSE. ''' if self.lhs == self.rhs: # prove equality is true by reflexivity return evaluate_truth(self.conclude_via_reflexivity().expr) if (is_irreducible_value(self.lhs) and is_irreducible_value(self.rhs)): # Irreducible values must know how to evaluate the equality # between each other, where appropriate. return self.lhs.eval_equality(self.rhs) if must_evaluate: # If we need an evaluation, this should do the trick: deduce_equal_or_not(self.lhs, self.rhs) return self.evaluation() return Operation.shallow_simplification(self) @staticmethod @prover def get_known_evaluation(expr, **defaults_config): ''' Return an applicable evaluation for the given expression if one is explicitly known; otherwise raise UnsatisfiedPrerequisites. Also see Equals.get_readily_provable_evaluation. ''' return Equals.get_readily_provable_evaluation(expr, automation=False) @staticmethod @prover def get_readily_provable_evaluation( expr, *, use_canonical_forms=True, **defaults_config): ''' Return an applicable evaluation for the given expression if one is readily provable; otherwise raise UnsatisfiedPrerequisites. If conclude_automation is True, we are allowed to derive an evaluation via transitivity through any number of known equalities and/or expressions with the same canonical form (if use_canonical_forms is also True), excluding equalities with any "preserved" expressions (in defaults.preserved_exprs) whose evaluations are to be disregarded. ''' if is_irreducible_value(expr): return Equals(expr, expr).conclude_via_reflexivity() if expr in Equals.known_evaluation_sets: evaluations = Equals.known_evaluation_sets[expr] candidates = [] for judgment in evaluations: if judgment.is_applicable(defaults.assumptions): # Found existing evaluation suitable for the # assumptions candidates.append(judgment) if len(candidates) >= 1: # Return the "best" candidate with respect to fewest # number of steps. def min_key(judgment): return judgment.proof().num_steps() return min(candidates, key=min_key) if defaults.conclude_automation: # An evaluation isn't directly known, but we may know # something equal to this that has an evaluation and # therefore we have an evaluation by transitivity and/or # same canonical forms as long as 'automation' is allowed. for eq_expr in Equals.yield_known_equal_expressions( expr, exceptions=defaults.preserved_exprs, include_canonical_forms=use_canonical_forms): eq_evaluation = None if eq_expr.proven(): eq_evaluation = evaluate_truth(eq_expr) elif eq_expr.disproven(): eq_evaluation = evaluate_falsehood(eq_expr) elif eq_expr != expr: eq_evaluation = Equals.get_known_evaluation(eq_expr) if eq_evaluation is not None: if expr == eq_expr: return eq_evaluation _eq = Equals(expr, eq_expr) if use_canonical_forms and ( expr.canonical_form()==eq_expr.canonical_form()): # deduce equality via same canonical form _eq = expr.deduce_canonically_equal(eq_expr) else: _eq = _eq.conclude_via_transitivity() return _eq.apply_transitivity(eq_evaluation) raise UnsatisfiedPrerequisites( "No readily provable evaluation")
[docs] @staticmethod def invert(lambda_map, rhs, assumptions=USE_DEFAULTS): ''' 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. ''' from proveit._core_.proof import Assumption # Make sure we derive assumption side-effects first. Assumption.make_assumptions() if (lambda_map, rhs) in Equals.inversions: # Previous solution(s) exist. Use one if the assumptions are # sufficient. for known_equality, inversion in Equals.inversions[( lambda_map, rhs)]: if known_equality.is_applicable(assumptions): return inversion # The mapping may be a trivial identity: f(x) = f(x) try: x = lambda_map.extract_argument(rhs) # Found a trivial inversion. Store it for future reference. known_equality = Equals(rhs, rhs).prove() Equals.inversions.setdefault( (lambda_map, rhs), []).append( (known_equality, x)) return x # Return the found inversion. except ArgumentExtractionError: pass # well, it was worth a try # Search among known relations for a solution. for known_equality, lhs in Equals.known_relations_from_right( rhs, assumptions): try: x = lambda_map.extract_argument(lhs) # Found an inversion. Store it for future reference. Equals.inversions.setdefault( (lambda_map, rhs), []).append( (known_equality, x)) return x # Return the found inversion. except ArgumentExtractionError: pass # not a match. keep looking. raise InversionError( "No inversion found to map %s onto %s" % (str(lambda_map), str(rhs)))
""" def conclude_via_reduction(expr, assumptions): ''' Attempts to prove that the given expression is TRUE under the given assumptions via evaluating that the expression is equal to true. Returns the resulting Judgment if successful. ''' from proveit.lambda_map import SubExprRepl if not isinstance(expr, Operation): # Can only really do reduction on an Operation. But we can # try to do a proof by evaluation. expr.evaluation(assumptions) return expr.prove(assumptions) # reduce the operands reduced_expr = reduce_operands(expr, assumptions) # prove the reduced version judgment = reduced_expr.prove(assumptions) # now rebuild the original via sub_left_side_into (for a shorter proof than substitutions) for k, operand in enumerate(expr.operands): # for each operand, replace it with the original sub_expr_repl = SubExprRepl(judgment).operands[k] judgment = operand.evaluation(assumptions=assumptions).sub_left_side_into(sub_expr_repl, assumptions) assert judgment.expr == expr, 'Equivalence substitutions did not work out as they should have' return judgment """ """ def default_simplification(inner_expr, in_place=False, must_evaluate=False, operands_only=False, assumptions=USE_DEFAULTS, automation=USE_DEFAULTS): ''' Default attempt to simplify the given inner expression under the given assumptions. If successful, returns a Judgment (using a subset of the given assumptions) that expresses an equality between the expression (on the left) and one with a simplified form for the "inner" part (in some canonical sense determined by the Operation). If in_place is True, the top-level expression must be a Judgment and the simplified Judgment is derived instead of an equivalence relation. If must_evaluate=True, the simplified form must be an irreducible value (see is_irreducible_value). Specifically, this method checks to see if an appropriate simplification/evaluation has already been proven. If not, but if it is an Operation, call the simplification/evaluation method on all operands, make these substitions, then call simplification/evaluation on the expression with operands substituted for simplified forms. It also treats, as a special case, evaluating the expression to be true if it is in the set of assumptions [also see Judgment.evaluation and evaluate_truth]. If operands_only = True, only simplify the operands of the inner expression. ''' # among other things, convert any assumptions=None # to assumptions=() to avoid len(None) errors assumptions = defaults.checked_assumptions(assumptions) if automation is USE_DEFAULTS: automation = defaults.automation from proveit.logic import TRUE, FALSE from proveit.logic.booleans import true_axiom top_level = inner_expr.expr_hierarchy[0] inner = inner_expr.expr_hierarchy[-1] if operands_only: # Just do the reduction of the operands at the level below the # "inner expression" reduced_inner_expr = reduce_operands( inner_expr, in_place, must_evaluate) if in_place: try: return reduced_inner_expr.expr_hierarchy[0].prove( automation=False) except BaseException: assert False try: eq = Equals(top_level, reduced_inner_expr.expr_hierarchy[0]) return eq.prove(automation=False) except BaseException: assert False def inner_simplification(inner_equivalence): if in_place: return inner_equivalence.sub_right_side_into(inner_expr) return inner_equivalence.substitution(inner_expr) if is_irreducible_value(inner): return Equals(inner, inner).prove() # See if the expression is already known to be true as a special # case. try: inner.prove(assumptions, automation=False) true_eval = evaluate_truth(inner, assumptions) # A=TRUE given A if inner == top_level: if in_place: return true_axiom else: return true_eval return inner_simplification(true_eval) except BaseException: pass # See if the negation of the expression is already known to be true # as a special case. try: inner.disprove(assumptions, automation=False) false_eval = evaluate_falsehood( inner, assumptions) # A=FALSE given Not(A) return inner_simplification(false_eval) except BaseException: pass # ================================================================ # # See if the expression already has a proven simplification # # ================================================================ # # construct the key for the known_simplifications dictionary known_simplifications_key = (inner, defaults.sorted_assumptions) if (must_evaluate and inner in Equals.known_evaluation_sets): evaluations = Equals.known_evaluation_sets[inner] candidates = [] for judgment in evaluations: if judgment.is_applicable(assumptions): # Found existing evaluation suitable for the assumptions candidates.append(judgment) if len(candidates) >= 1: # Return the "best" candidate with respect to fewest number # of steps. def min_key(judgment): return judgment.proof().num_steps() simplification = min(candidates, key=min_key) return inner_simplification(simplification) elif (not must_evaluate and known_simplifications_key in Equals.known_simplifications): simplification = Equals.known_simplifications[known_simplifications_key] if simplification.is_usable(): return inner_simplification(simplification) # ================================================================ # if not defaults.automation: msg = 'Unknown evaluation (without automation): ' + str(inner) raise SimplificationError(msg) # See if the expression is equal to something that has an evaluation # or is already known to be true. if inner in Equals.known_equalities: for known_eq in Equals.known_equalities[inner]: try: if known_eq.is_applicable(assumptions): if in_place: # Should first substitute in the known # equivalence then simplify that. if inner == known_eq.lhs: known_eq.sub_right_side_into(inner_expr) elif inner == known_eq.rhs: known_eq.sub_left_side_into(inner_expr) # Use must_evaluate=True. Simply being equal to # something simplified isn't necessarily the # appropriate simplification for "inner" itself. alt_inner = known_eq.other_side(inner).inner_expr() equiv_simp = \ default_simplification(alt_inner, in_place=in_place, must_evaluate=True, automation=False) if in_place: # Returns Judgment with simplification: return equiv_simp inner_equiv = known_eq.apply_transitivity(equiv_simp) if inner == top_level: return inner_equiv return inner_equiv.substitution(inner_expr) except SimplificationError: pass # try to simplify via reduction if not isinstance(inner, Operation): if must_evaluate: raise EvaluationError('Unknown evaluation: ' + str(inner)) else: # don't know how to simplify, so keep it the same return inner_simplification(Equals(inner, inner).prove()) reduced_inner_expr = reduce_operands(inner_expr, in_place, must_evaluate) if reduced_inner_expr == inner_expr: if must_evaluate: # Since it wasn't irreducible to begin with, it must change # in order to evaluate. raise SimplificationError('Unable to evaluate: ' + str(inner)) else: raise SimplificationError('Unable to simplify: ' + str(inner)) # evaluate/simplify the reduced inner expression inner = reduced_inner_expr.expr_hierarchy[-1] if must_evaluate: inner_equiv = inner.evaluation() else: inner_equiv = inner.simplification() value = inner_equiv.rhs if value == TRUE: # Attempt to evaluate via proving the expression; # This should result in a shorter proof if allowed # (e.g., if theorems are usable). try: evaluate_truth(inner) except BaseException: pass if value == FALSE: # Attempt to evaluate via disproving the expression; # This should result in a shorter proof if allowed # (e.g., if theorems are usable). try: evaluate_falsehood(inner) except BaseException: pass reduced_simplification = inner_simplification(inner_equiv) if in_place: simplification = reduced_simplification else: # Via transitivity, go from the original expression to the # reduced expression (simplified inner operands) and then the # final simplification (simplified inner expression). reduced_top_level = reduced_inner_expr.expr_hierarchy[0] eq1 = Equals(top_level, reduced_top_level) eq1.prove(automation=False) eq2 = Equals(reduced_top_level, reduced_simplification.rhs) eq2.prove(automation=False) simplification = eq1.apply_transitivity(eq2) if not in_place and top_level == inner: # Store direct simplifications in the known_simplifications # dictionary for next time. Equals.known_simplifications[known_simplifications_key] = simplification if is_irreducible_value(value): # also store it in the known_evaluation_sets dictionary for # next time, since it evaluated to an irreducible value. Equals.known_evaluation_sets.setdefault( top_level, set()).add(simplification) return simplification """
[docs]@prover def evaluate_truth(expr, **defaults_config): ''' Attempts to prove that the given expression equals TRUE under the given assumptions via proving the expression. Returns the resulting Judgment evaluation if successful. ''' from proveit.logic import TRUE return Equals(expr, TRUE).conclude_boolean_equality()
[docs]@prover def evaluate_falsehood(expr, **defaults_config): ''' Attempts to prove that the given expression equals FALSE under the given assumptions via disproving the expression. Returns the resulting Judgment evaluation if successful. ''' from proveit.logic import FALSE return Equals(expr, FALSE).conclude_boolean_equality()
[docs]@prover def deduce_equal_or_not(lhs, rhs, **defaults_config): ''' Prove and return that lhs=rhs or lhs≠rhs or raise an UnsatisfiedPrerequisites or NotImplementedError if neither of these is readily known. ''' from proveit.logic import NotEquals if Equals(lhs, rhs).proven(): return Equals(lhs, rhs).prove() if lhs == rhs: return Equals(lhs, rhs).conclude_via_reflexivity() if NotEquals(lhs, rhs).proven(): return NotEquals(lhs, rhs).prove() if lhs.canonical_form() == rhs.canonical_form(): return lhs.deduce_canonically_equal(rhs) if hasattr(lhs, 'deduce_equal_or_not'): return lhs.deduce_equal_or_not(rhs) if hasattr(rhs, 'deduce_equal_or_not'): return rhs.deduce_equal_or_not(lhs).derive_reversed() raise UnsatisfiedPrerequisites( "We cannot readily prove whether or not %s=%s" %(lhs, rhs))
[docs]def evaluation_or_simplification(expr, return_none_if_trivial=False): ''' Return a nontrivial evaluation of the given expression if possible; otherwise return a nontrivial simplification if possible. If we can't obtain one or the expression is already irreducible or simplified, return the trivial reflection or None if return_none_if_trivial is True. ''' def trivial_form(): if return_none_if_trivial: return None return Equals(expr, expr).conclude_via_reflexivity() if is_irreducible_value(expr): # This is already irreducible; nothing more to do. return trivial_form() try: # First try an evaluation -- this is best and it # should fail quickly when it can't be done. return expr.evaluation() except (SimplificationError, ProofFailure, UnsatisfiedPrerequisites, NotImplementedError): pass try: # If we weren't able to do an evaluation, try a # simplification. simplification = expr.simplification() if simplification.lhs != simplification.rhs: return simplification except (SimplificationError, ProofFailure, UnsatisfiedPrerequisites, NotImplementedError): pass return trivial_form()
[docs]class SimplificationError(Exception): def __init__(self, message): self.message = message def __str__(self): return self.message
[docs]class EvaluationError(SimplificationError): def __init__(self, expr, assumptions=None): if assumptions is None: assumptions = defaults.assumptions self.message = ("Evaluation of %s under assumptions %s is not known" % (expr, assumptions)) def __str__(self): return self.message
class InversionError(Exception): def __init__(self, message): self.message = message def __str__(self): return self.message