Source code for proveit.numbers.addition.add

import math
import bisect
from collections import deque, Counter

from proveit import (Expression, Judgment, Literal, Operation, ExprTuple,
                     ExprRange, defaults, StyleOptions, 
                     prover, relation_prover, equality_prover,
                     auto_prover, auto_relation_prover, auto_equality_prover,
                     maybe_fenced_latex, ProofFailure, InnerExpr,
                     UnsatisfiedPrerequisites,
                     SimplificationDirectives, TransRelUpdater)
from proveit.util import OrderedSet
from proveit import a, b, c, d, e, i, j, k, l, n, x, y, free_vars
from proveit.logic import (And, Equals, NotEquals,
                           EvaluationError, InSet)
from proveit.logic.irreducible_value import is_irreducible_value
from proveit.numbers import (NumberOperation, standard_number_set,
                             pos_number_set, neg_number_set, 
                             nonneg_number_set, nonpos_number_set,
                             nonzero_number_set,
                             union_number_set, deduce_number_set,
                             readily_provable_number_set)
from proveit.numbers.numerals.decimals import DIGITS
import proveit.numbers.numerals.decimals
from proveit.abstract_algebra.generic_methods import (
        apply_commutation_thm, apply_association_thm, 
        apply_disassociation_thm, group_commutation, pairwise_evaluation,
        deduce_equality_via_commutation, generic_permutation,
        sorting_operands, sorting_and_combining_like_operands,
        common_likeness_key)
from proveit import TransRelUpdater
from proveit.numbers import (ZeroSet, Integer, IntegerNeg, IntegerNonPos,
                             Natural, NaturalPos, IntegerNonZero,
                             Rational, RationalPos, RationalNonZero,
                             RationalNeg, RationalNonNeg,
                             RationalNonPos,
                             Real, RealPos, RealNeg, RealNonNeg,
                             RealNonPos, RealNonZero, Complex, 
                             ComplexNonZero)


[docs]class Add(NumberOperation): # operator of the Add operation _operator_ = Literal(string_format='+', theory=__file__) # The 'order_key' simplification directive can be used # to sort terms in a particular order. By default, there # is no sorting -- it keeps the original order as much as # possible but still combines like terms. _simplification_directives_ = SimplificationDirectives( ungroup = True, combine_like_terms = True, combine_like_denoms = False, order_key_fn = lambda term : 0) def __init__(self, *operands, styles=None): r''' Add together any number of operands. ''' NumberOperation.__init__(self, Add._operator_, operands, styles=styles) self.terms = self.operands @staticmethod def _isNegatedOperand(operand): ''' Returns True iff the given operand is negated directly or an iteration with a negated body ''' from proveit.numbers import Neg return isinstance( operand, Neg) or ( isinstance( operand, ExprRange) and isinstance( operand.lambda_map.body, Neg)) def _formatted(self, format_type, **kwargs): ''' Override Operation._formatted so to enable subtraction notation where desired. ''' from proveit import ExprRange from proveit.numbers import Neg # Where should we use subtraction notation subtraction_positions = [] for _k, operand in enumerate(self.operands.entries): if isinstance(operand, Neg): if operand.use_subtraction_notation(): subtraction_positions.append(_k) elif isinstance(operand, ExprRange): if isinstance(operand.body, Neg): if operand.body.use_subtraction_notation(): subtraction_positions.append(_k) if len(subtraction_positions) > 0: operators = [] operands = list(self.operands.entries) for operand in operands: if isinstance(operand, ExprRange): # Make the operator an ExprRange in correspondence # with the operands ExprRange operators.append( ExprRange( operand.lambda_map.parameter_or_parameters, self.operator, operand.true_start_index, operand.true_end_index)) else: operators.append(self.operator) implicit_first_operator = True # the first operator is implicit if it is a '+' for pos in subtraction_positions: if pos >= len(operands): continue operand = operands[pos] if pos == 0: implicit_first_operator = False if isinstance(operand, Neg): # format negated operand using subtraction notation operators[pos] = Neg._operator_ operands[pos] = operand.operand elif isinstance(operand, ExprRange): if isinstance(operand.lambda_map.body, Neg): # format iteration with negation using subtraction # notation operators[pos] = ExprRange( operand.lambda_map.parameter, Neg._operator_, operand.true_start_index, operand.true_end_index) operands[pos] = ExprRange( operand.lambda_map.parameter, operand.lambda_map.body.operand, operand.true_start_index, operand.true_end_index) .with_styles( **operand.get_styles()) elif pos == 0: # not negated after all -- revert to the "implicit first # operator" default implicit_first_operator = False return Operation._formatted_operation( format_type, operators, operands, implicit_first_operator=implicit_first_operator, wrap_positions=self.wrap_positions(), justification=self.get_style('justification', 'left'), **kwargs) else: return Operation._formatted_operation( format_type, self.operator, self.operands, wrap_positions=self.wrap_positions(), justification=self.get_style('justification', 'left'), **kwargs)
[docs] def remake_constructor(self): from proveit.numbers import Neg if (self.operands.is_double() and isinstance(self.operands[1], Neg) and self.operands[1].use_subtraction_notation()): return 'subtract' # use a different constructor if using the subtraction style return Operation.remake_constructor(self)
[docs] def remake_arguments(self): ''' Yield the argument values or (name, value) pairs that could be used to recreate the Operation. ''' from proveit.numbers import Neg if (self.operands.is_double() and isinstance(self.operands[1], Neg) and self.operands[1].use_subtraction_notation()): yield self.operands[0] assert isinstance( self.operands[1], Neg), "The second operand must be negated" yield self.operands[1].operand else: for operand in self.operands: yield operand
[docs] def equality_side_effects(self, judgment): ''' If the right side is irreducible and the left side is binary, a + b = c, derive the commutation b + a = c and if neither a nor b is a Neg, also derive the following: -a - b = -c c - b = a b - c = -a ''' from proveit.numbers import Neg if not isinstance(judgment, Judgment): raise ValueError("Expecting 'judgment' to be a Judgment.") if not isinstance(judgment.expr, Equals): raise ValueError("Expecting the judgment to be an equality.") addition = judgment.lhs if not isinstance(addition, Add): raise ValueError( "Expecting lhs of judgment to be of an Add expression.") if is_irreducible_value(judgment.rhs): if addition.terms.is_double(): # deduce the commutation form: b+a=c from a+b=c if addition.terms[0] != addition.terms[1]: yield (lambda : judgment.inner_expr().lhs.commute(0, 1)) if all(not isinstance(term, Neg) for term in addition.terms): # From a+b=c # deduce the negations form: -a-b=-c # the subtraction form: c-b=a # and the reversed subtraction form: b-c = -a yield (lambda : self.equation_negation(judgment.rhs)) yield (lambda : self.equation_subtraction(judgment.rhs)) yield (lambda : self.equation_reversed_subtraction( judgment.rhs))
def _build_canonical_form(self): ''' Returns a form of this Add with operands in their canonical forms, nested addition is ungrouped, and "common" terms that are the same except coefficient factors are combined, and these terms are all ordered deterministically according to hash values of the non-coefficient parts of the terms. Example: (2/3)*a*b + c + 1 - (-1/4)*a*b + c + (1/3) -> (4/3) + (11/12) a*b + 2 c The order of the terms is arbitrary but deterministic (sorted by hash value). ''' from proveit.numbers import (zero, one, Neg, Mult, is_numeric_rational, numeric_rational_ints, simplified_numeric_rational) from proveit.numbers.multiplication.mult import ( coefficient_and_remainder) if self.terms.num_entries() == 0: return zero # Add operation with no operands remainder_to_rational_coef = dict() contains_only_numeric_rationals = True # Generate canonical forms of terms and ungroup nested # addition: def gen_coef_and_remainders(expr): for term in expr.terms: canonical_term = term.canonical_form() if isinstance(canonical_term, Neg): # Negation should distribute through Add # in its canonical form. assert not isinstance(canonical_term.operand, Add) if isinstance(canonical_term, Add): for _coeff_and_remainder in gen_coef_and_remainders( canonical_term): yield _coeff_and_remainder # for sub_term in canonical_term.terms: # yield coefficient_and_remainder(sub_term) elif isinstance(canonical_term, ExprRange): yield (one, Add(canonical_term)) else: yield coefficient_and_remainder(canonical_term) for coef, remainder in gen_coef_and_remainders(self): if coef == zero: continue if remainder != one: contains_only_numeric_rationals = False if remainder in remainder_to_rational_coef: prev_coef = remainder_to_rational_coef[remainder] if isinstance(prev_coef, Add): remainder_to_rational_coef[remainder] = Add( *prev_coef.terms.entries, coef) else: remainder_to_rational_coef[remainder] = Add( prev_coef, coef) else: remainder_to_rational_coef[remainder] = coef if len(remainder_to_rational_coef) == 0: return zero # Add() = 0 if len(remainder_to_rational_coef) == 1: # special case to avoid infinite recursion remainder, coeff = next(iter(remainder_to_rational_coef.items())) if coeff == one: return remainder if contains_only_numeric_rationals: # This is a sum of only numeric rationals. Just # compute it. assert len(remainder_to_rational_coef)==1 assert one in remainder_to_rational_coef expr = remainder_to_rational_coef[one] if not isinstance(expr, Add): assert is_numeric_rational(expr) return expr sum_as_expr = zero for term in expr.terms: # Add to the cumulative sum. # (a/b) + (c/d) = (a*d + c*b)/(b*d) _a, _b = numeric_rational_ints(sum_as_expr) _c, _d = numeric_rational_ints(term) sum_as_expr = simplified_numeric_rational(_a*_d+_c*_b, _b*_d) return sum_as_expr terms = [] for remainder in sorted(remainder_to_rational_coef.keys(), key=hash): if remainder==one: # We'll save the constant (numeric rational) for the # last term (consistent with the 'quick simplified' # form). continue coef = remainder_to_rational_coef[remainder].canonical_form() if coef == zero: continue if coef == one: term = remainder elif isinstance(remainder, Mult): term = Mult(coef, *remainder.factors.entries) else: term = Mult(coef, remainder) canonical_term = term.canonical_form() terms.append(canonical_term) if one in remainder_to_rational_coef: # Add the numeric rational as the last term. coef = remainder_to_rational_coef[one].canonical_form() if coef != zero: terms.append(coef) if len(terms) == 0: return zero elif len(terms) == 1: return terms[0] else: return Add(*terms) return Add(*sorted([operand.canonical_form() for operand in self.operands.entries], key=hash)) @prover def equation_negation(self, rhs, **defaults_config): ''' From (a + b) = rhs, derive and return -(a-b) = -rhs ''' from proveit.numbers.addition.subtraction import negated_add if not self.terms.is_double(): raise NotImplementedError( "Add.equation_negation implemented only when there are two " "and only two added terms") _a, _b = self.terms[0], self.terms[1] deduction = negated_add.instantiate( {a: _a, b: _b, c: rhs}, auto_simplify=False) return deduction @prover def equation_subtraction(self, rhs, **defaults_config): ''' From (a + b) = rhs, derive and return rhs - b = a. ''' from proveit.numbers.addition.subtraction import subtract_from_add if not self.terms.is_double(): raise NotImplementedError( "Add.deduce_subtraction implemented only when there are " "two and only two added terms") _a, _b = self.terms[0], self.terms[1] deduction = subtract_from_add.instantiate( {a: _a, b: _b, c: rhs}, auto_simplify=False) return deduction @prover def equation_reversed_subtraction(self, rhs, **defaults_config): ''' From (a + b) = rhs, derive and return b - rhs = -a. ''' from proveit.numbers.addition.subtraction import subtract_from_add_reversed if not self.terms.is_double(): raise NotImplementedError( "Add.decude_reversed_subtraction implemented only when " "there are two and only two added terms") deduction = subtract_from_add_reversed.instantiate( {a: self.terms[0], b: self.terms[1], c: rhs}, auto_simplify=False) return deduction
[docs] @equality_prover('multiplied', 'multiply') def conversion_to_multiplication(self, **defaults_config): ''' From the addition of the same values, derive and return the equivalence as a multiplication. For example, a + a + a = 3 * a ''' from proveit import ExprRange from proveit.numbers import one from proveit.numbers.multiplication import ( mult_def_rev, repeated_addition_to_mult) operands = self.operands if (operands.num_entries() == 1 and isinstance(operands[0], ExprRange) and operands[0].is_parameter_independent): expr_range = operands[0] replacements = [] start_index = operands[0].true_start_index if start_index != one: # change the indexing to start from 1. replacement = operands[0].shift_equivalence( new_start=one).derive_reversed() _n = replacement.rhs.entries[0].true_end_index replacements.append(replacement) else: _n = expr_range.true_end_index # x + x + ..(n-3)x.. + x = x*n return repeated_addition_to_mult.instantiate( {x: expr_range.body, n: _n}, replacements=replacements) # Obtain the first element; all other elements should equal # this. for operand in operands: if isinstance(operand, ExprRange): _x = operand.first() else: _x = operand _n = operands.num_elements() _a = operands # a1 + a2 + ..(n-3)x.. + an = x*n if each a1,a2,..,an equals x. return mult_def_rev.instantiate({n: _n, a: _a, x: _x})
[docs] @equality_prover('all_canceled', 'all_cancel') def cancelations(self, **defaults_config): ''' Deduce and return an equality between self and a form in which all simple cancellations are performed (where there are exact negations that occur). ''' from proveit.numbers import Neg expr = self # A convenience to allow successive update to the equation via # transitivities. (starting with self=self). eq = TransRelUpdater(self) neg_operand_indices = dict() for _i, operand in enumerate(self.operands.entries): if isinstance(operand, Neg): neg_operand_indices.setdefault( operand.operand.canonical_form(), OrderedSet()).add(_i) canceled_indices = [] for _i, operand in enumerate(self.operands.entries): if isinstance(operand, Neg): continue operand_cf = operand.canonical_form() if operand_cf in neg_operand_indices: indices = neg_operand_indices[operand_cf] _j = indices.pop() if len(indices) == 0: # no more indices to use in the future neg_operand_indices.pop(operand_cf) # By finding where i and j will be inserted into the # canceled_indices array, we can figure out how much # they need to shift by to compensate for previous # cancelations. i_shift = bisect.bisect_left(canceled_indices, _i) j_shift = bisect.bisect_left(canceled_indices, _j) # Insert the last one first so we don't need to # compensate: if _i < _j: canceled_indices.insert(j_shift, _j) canceled_indices.insert(i_shift, _i) else: canceled_indices.insert(i_shift, _i) canceled_indices.insert(j_shift, _j) expr = eq.update(expr.cancelation( _i - i_shift, _j - j_shift, preserve_all=True)) return eq.relation
[docs] @equality_prover('canceled', 'cancel') def cancelation(self, idx1, idx2, **defaults_config): ''' Attempt a simple cancelation between operands at index i and j. If one of these operands is the negation of the other, deduce and return an equality between self and a form in which these operands are canceled. ''' import proveit.numbers.addition.subtraction as sub_pkg from proveit.numbers import Neg if idx1 > idx2: # choose i to be less than j return self.cancelation(idx2, idx1) if isinstance(self.operands[idx2], Neg): basic_thm = sub_pkg.add_cancel_basic triple_thms = ( sub_pkg.add_cancel_triple_12, sub_pkg.add_cancel_triple_13, sub_pkg.add_cancel_triple_23) general_thm = sub_pkg.add_cancel_general _a = self.operands[idx1] _b = self.operands[idx2].operand elif isinstance(self.operands[idx1], Neg): basic_thm = sub_pkg.add_cancel_reverse triple_thms = ( sub_pkg.add_cancel_triple_21, sub_pkg.add_cancel_triple_31, sub_pkg.add_cancel_triple_32) general_thm = sub_pkg.add_cancel_general_rev _a = self.operands[idx1].operand _b = self.operands[idx2] else: raise ValueError("Unable to cancel %s and %s; " "neither is in an explicitly negated form." %(self.operands[idx1], self.operands[idx2])) if self.operands.is_double(): return basic_thm.instantiate({a:_a, b:_b}) elif (not self.operands.contains_range() and self.operands.num_entries() == 3): # _k is the 3rd index, completing i and j in the set {0,1,2}. _k = {0, 1, 2}.difference([idx1, idx2]).pop() thm = triple_thms[2 - _k] return thm.instantiate({a:_a, b:_b, c: self.operands[_k]}) else: _b, _d = _a, _b _a = self.operands[:idx1] _c = self.operands[idx1 + 1:idx2] _e = self.operands[idx2 + 1:] _i = _a.num_elements() _j = _c.num_elements() _k = _e.num_elements() return general_thm.instantiate( {i: _i, j: _j, k: _k, a: _a, b: _b, c: _c, d: _d, e: _e})
[docs] @equality_prover('eliminated_zeros', 'eliminate_zeros') def zero_eliminations(self, **defaults_config): ''' Derive and return this Add expression equal to a form in which all zero's are eliminated. ''' from proveit.numbers import zero expr = self # A convenience to allow successive update to the equation via # transitivities (starting with self=self). eq = TransRelUpdater(self) # Work in reverse order so indices don't need to be updated. for rev_idx, operand in enumerate(reversed(self.operands.entries)): if operand == zero: idx = self.operands.num_entries() - rev_idx - 1 expr = eq.update(expr.zero_elimination( idx, preserve_all=True)) if not isinstance(expr, Add): # can't do an elimination if reduced to a single term. break return eq.relation
[docs] @equality_prover('eliminated_zero', 'eliminate_zero') def zero_elimination(self, idx, **defaults_config): ''' Derive and return this Add expression equal to a form in which a specific zero operand (at the given index) is eliminated. ''' from proveit.numbers import zero from . import elim_zero_left, elim_zero_right, elim_zero_any if self.operands[idx] != zero: raise ValueError( "Operand at the index %d expected to be zero for %s" % (idx, str(self))) if self.operands.is_double(): if idx == 0: return elim_zero_left.instantiate({a: self.operands[1]}) else: return elim_zero_right.instantiate({a: self.operands[0]}) _a = self.operands[:idx] _b = self.operands[idx + 1:] _i = _a.num_elements() _j = _b.num_elements() return elim_zero_any.instantiate({i: _i, j: _j, a: _a, b: _b})
@equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Returns a proven simplification equation for this Add expression assuming the operands have been simplified. Perform a number of possible simplifications of an Add expression after the operands have been simplified. Disassociate grouped terms, eliminate zero terms, cancel common terms that are subtracted, combine like terms, convert repeated addition to multiplication, etc. ''' from proveit.numbers import (one, Add, Div, Neg, Mult, is_numeric_int, is_numeric_rational) from proveit.numbers.multiplication.mult import ( coefficient_and_remainder) from . import empty_addition, unary_add_reduction if self.operands.num_entries() == 0: # [+]() = 0 return empty_addition if self.operands.is_single(): return unary_add_reduction.instantiate({a:self.operands[0]}, preserve_all=True) # If all operands are negated, factor out the negation. if all(isinstance(operand, Neg) for operand in self.operands): negated = Neg( Add(*[operand.operand for operand in self.operands])) neg_distribution = negated.distribution(auto_simplify=False) neg_factored = neg_distribution.derive_reversed() return neg_factored.inner_expr().rhs.simplify() expr = self # for convenience updating our equation eq = TransRelUpdater(expr) if Add._simplification_directives_.ungroup: # ungroup the expression (disassociate nested additions). _n = 0 length = expr.operands.num_entries() - 1 # loop through all operands while _n < length: operand = expr.operands[_n] if (isinstance(operand, ExprRange) and operand.is_parameter_independent): # A range of repeated terms may be simplified to # a multiplication, but we need to group it first. inner_simplification = ( Add(operand).shallow_simplification()) expr = eq.update(expr.association( _n, 1, replacements=[inner_simplification], auto_simplify=False)) if (isinstance(operand, Add) or (isinstance(operand, Neg) and isinstance(operand.operand, Add))): # if it is grouped, ungroup it expr = eq.update(expr.disassociation( _n, preserve_all=True)) length = expr.operands.num_entries() _n += 1 # See if there are any parameter-independent expression # ranges to be converted to multiplication: # x + x + ..(n-3)x.. + x = x*n for _k, operand in enumerate(expr.operands): if isinstance(operand, ExprRange) and ( operand.is_parameter_independent): if expr.operands.num_entries(): return expr.conversion_to_multiplication( preserve_expr=operand.body, auto_simplify=True) expr_range_term = Add(expr.operands[_k]) replacement = expr_range_term.conversion_to_multiplication( preserve_expr=operand.body, auto_simplify=True) expr = eq.update(expr.inner_expr().associated( _k, 1, replacements=[replacement])) # eliminate zeros where possible expr = eq.update(expr.zero_eliminations(preserve_all=True)) if not isinstance(expr, Add): # eliminated all but one term return eq.relation # perform cancelations where possible expr = eq.update(expr.cancelations(preserve_all=True)) if not isinstance(expr, Add): # canceled all but one term return eq.relation # Check for any double-negations. # Normally, this would have been dealt with in the initial # reduction, but can emerge after disassociating a subtraction. for _i in range(expr.operands.num_entries()): if (isinstance(expr.operands[_i], Neg) and isinstance(expr.operands[_i].operand, Neg)): inner_expr = expr.inner_expr().operands[_i] expr = eq.update( inner_expr.double_neg_simplification( preserve_all=True)) # If all operands are irreducible, perform the evaluation. terms = self.terms if all(is_irreducible_value(term) for term in terms): if self.operands.is_double(): if all(is_numeric_int(term) for term in terms): # Evaluate the addition of two literal integers. evaluation = self._integer_binary_eval() return evaluation elif all(is_numeric_rational(term) for term in terms): # Evaluate the addition of two literal rationals. evaluation = self._rational_binary_eval() return evaluation else: # In the future, handle adding irreducible # complex numbers and/or irrationals as # appropriate. pass else: # Do a pairwise addition of irreducible terms. return pairwise_evaluation(self) order_key_fn = Add._simplification_directives_.order_key_fn if Add._simplification_directives_.combine_like_terms and ( not must_evaluate): # Like terms are ones whose that are the same # apart from literal, rational coefficients. likeness_key_fn = lambda term : ( coefficient_and_remainder(term)[1]) if Add._simplification_directives_.combine_like_denoms: # likeness_key_fn = lambda term : ( # Div(one, term.denominator) if isinstance(term, Div) # else likeness_key_fn(term)) likeness_key_fn = lambda term : ( Div(one, term.denominator) if isinstance(term, Div) else coefficient_and_remainder(term)[1]) # Sort and combine like operands. expr = eq.update(sorting_and_combining_like_operands( expr, order_key_fn=order_key_fn, likeness_key_fn=likeness_key_fn, preserve_likeness_keys=True, auto_simplify=True)) else: # See if we should reorder the terms. expr = eq.update(sorting_operands(expr, order_key_fn=order_key_fn, auto_simplify=False)) if expr != self: # Try starting over with a call to shallow_simplification # (an evaluation may already be known). eq.update(expr.shallow_simplification( must_evaluate=must_evaluate)) return eq.relation if all(is_irreducible_value(term) for term in self.terms): raise NotImplementedError( "Addition evaluation only implemented for rationals: %s" %self) if must_evaluate: # The simplification of the operands may not have # worked hard enough. Let's work harder if we # must evaluate. for term in self.terms: if not is_irreducible_value(term): term.evaluation() # Start over now that the terms are all evaluated to # irreductible values. return self.evaluation() return eq.relation def quick_simplified(self): ''' Return a simplified version of this Add expression without any proof. In particular, negations are distributed nested additions are ungrouped, integers are extracted, added, and placed at the end, and cancelations are made on individual terms as well as expression ranges or portions of expression ranges. We freely assume terms represent numbers and expression ranges are well-formed. This quick-n-dirty approach can be good enough for the purposes of displaying expressions involving expression ranges. See also the quick_simplified_index function defined in number_operation.py. ''' from proveit.numbers import is_numeric_int, num, Neg # Extract any literal integers and expand nested sums. # While we are at it, determing the extremal shifts at the # heads and tails of expression ranges. terms = [] # split into sign, abs_term pairs int_sum = 0 remaining_terms = deque(self.terms) sign=1 # Map non-shifted head to latest shift of ExprRange terms: latest_head_shift = dict() # (Lambda, index expr) -> int # Map non-shiftted tail to earliest shift of ExprRange terms: earliest_tail_shift = dict() # (Lambda, index expr) -> int all_abs_terms = set() def expandable_range(term): if not isinstance(term, ExprRange): return False # Currently this doesn't expand ExprRange bodies that # are Add or Neg which would themselves be expanded. # This algorithm needs to be redesigned to handle such # fancy cases. if isinstance(term.body, Add) or isinstance(term.body, Neg): return False return True while len(remaining_terms): term = remaining_terms.popleft() if term == Neg: # Just an indication to switch the sign back. sign = -sign continue if is_numeric_int(term): int_sum += sign*term.as_int() continue if isinstance(term, Neg): # Switch the sign and indicate to switch the sign # back later. sign = -sign remaining_terms.appendleft(Neg) remaining_terms.appendleft(term.operand) continue if isinstance(term, Add): remaining_terms.extendleft(reversed(term.terms.entries)) continue if expandable_range(term): start_base, start_shift = split_int_shift( term.true_start_index) end_base, end_shift = split_int_shift(term.true_end_index) lambda_map = term.lambda_map latest_head_shift[(lambda_map, start_base)] = max( start_shift, latest_head_shift.get( (lambda_map, start_base), start_shift)) earliest_tail_shift[(lambda_map, end_base)] = min( end_shift, earliest_tail_shift.get( (lambda_map, end_base), end_shift)) all_abs_terms.add(term) terms.append((sign, term)) term = None # Extend the "latest heads" and "earliest tails" if there # are individual terms that match them so we can maximize # cancelations. for extremal_shifts, step in ((latest_head_shift, 1), (earliest_tail_shift, -1)): for (lambda_map, base), shift in extremal_shifts.items(): while True: index = Add(base, num(shift)).quick_simplified() _expr = lambda_map.apply(index) if _expr in all_abs_terms: shift += step if (lambda_map.parameter not in free_vars(lambda_map.body)): # avoid an infinite loop break else: break extremal_shifts[(lambda_map, base)] = shift # Expand ExprRange heads and tails to their extremal shifts if len(latest_head_shift) > 0: old_terms = terms terms = [] for sign, abs_term in old_terms: if expandable_range(abs_term): start_base, start_shift = split_int_shift(abs_term.true_start_index) end_base, end_shift = split_int_shift(abs_term.true_end_index) lambda_map = abs_term.lambda_map latest_start = latest_head_shift[(lambda_map, start_base)] earliest_end = earliest_tail_shift[(lambda_map, end_base)] if start_base == end_base: # For finite ranges, expand all elements. latest_start = end_shift+1 # Peel off elements before the latest start. shift = start_shift while shift < latest_start: index = Add(start_base, num(shift)).quick_simplified() terms.append((sign, lambda_map.apply(index))) shift += 1 if start_base == end_base and shift > end_shift: continue # already expanded all elements. start_index = Add(start_base, num(latest_start)).quick_simplified() end_index = Add(end_base, num(earliest_end)).quick_simplified() terms.append((sign, ExprRange(abs_term.parameter, abs_term.body, start_index, end_index))) shift = earliest_end + 1 # Peel off elements after the earliest end. while shift <= end_shift: index = Add(end_base, num(shift)).quick_simplified() terms.append((sign, lambda_map.apply(index))) shift += 1 else: terms.append((sign, abs_term)) # Do cancelations of opposite terms. # Also check for clearly empty ExprRanges. abs_term_to_neg_idx = dict() abs_term_to_pos_idx = dict() cancelation_indices = set() for idx, (sign, abs_term) in enumerate(terms): if sign == -1: if abs_term in abs_term_to_pos_idx: # Neg term cancels with previous positive term. other_idx = abs_term_to_pos_idx.pop(abs_term) cancelation_indices.add(idx) cancelation_indices.add(other_idx) else: # Store for possible cancelation ahead. abs_term_to_neg_idx[abs_term] = idx else: if abs_term in abs_term_to_neg_idx: # Positive term cancels with previous Neg term. other_idx = abs_term_to_neg_idx.pop(abs_term) cancelation_indices.add(idx) cancelation_indices.add(other_idx) else: # Store for possible cancelation ahead. abs_term_to_pos_idx[abs_term] = idx terms = [term for idx, term in enumerate(terms) if idx not in cancelation_indices] # Re-extend heads and tails of ExprRanges that may have been # split apart, now that we've had a chance to find cancelations. if len(latest_head_shift) > 0 and len(terms) > 0: # Try to prepend heads going in reverse old_terms = terms reversed_terms = [] following_term = None for sign, abs_term in reversed(old_terms): if following_term is not None: if (sign==following_term[0] and expandable_range(following_term[1])): # See if the current term prepends the head of # the following range. start_base, start_shift = split_int_shift( following_term[1].true_start_index) lambda_map = following_term[1].lambda_map index = Add(start_base, num(start_shift-1)).quick_simplified() if abs_term == lambda_map.apply(index): # Prepend the head. following_term[1] = ExprRange( following_term[1].parameter, following_term[1].body, index, following_term[1].true_end_index) continue reversed_terms.append(following_term) following_term = [sign, abs_term] reversed_terms.append(following_term) # get the last one # Try to extend tails, reversing again. terms = [] prev_term = None for sign, abs_term in reversed(reversed_terms): if prev_term is not None: if (sign==prev_term[0] and expandable_range(prev_term[1])): # See if the current term extends the tail of # the previous range. end_base, end_shift = split_int_shift( prev_term[1].true_end_index) lambda_map = prev_term[1].lambda_map index = Add(end_base, num(end_shift+1)).quick_simplified() if abs_term == lambda_map.apply(index): # Extend the tail. prev_term[1] = ExprRange( prev_term[1].parameter, prev_term[1].body, prev_term[1].true_start_index, index) continue terms.append(prev_term) prev_term = [sign, abs_term] terms.append(prev_term) # get the last one # Merge the sign and abs_term into each term. for idx, (sign, abs_term) in enumerate(terms): if sign==1: terms[idx] = abs_term else: assert sign==-1 if isinstance(abs_term, ExprRange): terms[idx] = Neg(Add(abs_term)) else: terms[idx] = Neg(abs_term) if int_sum == 0: if len(terms) == 0: return num(0) if len(terms) == 1 and not isinstance(terms[0], ExprRange): return terms[0] return Add(*terms) else: if len(terms) == 0: return num(int_sum) return Add(*(terms + [num(int_sum)])) def quick_simplification(self): ''' Return a simplification of this Add expression without any proof. See Add.quick_simplified for more details. ''' return Equals(self, self.quick_simplified()) def _integer_binary_eval(self): ''' Evaluate the sum of possibly negated single digit numbers. ''' from proveit.numbers import is_numeric_int, num from proveit.numbers.numerals import DecimalSequence terms = self.terms assert terms.is_double() assert all(is_numeric_int(term) for term in terms) _a, _b = terms _a, _b = _a.as_int(), _b.as_int() if _a < 0 and _b < 0: # evaluate -a-b via a+b _a, _b = -_a, -_b if _a < 0: # evaluate -a+b via (a-b)+b or (b-a)+a _a = -_a if _a > _b: _a, _b = _a - _b, _b else: _a, _b = _b - _a, _a elif _b < 0: # evaluate a-b via (a-b)+b or (b-a)+a _b = -_b if _a > _b: _a, _b = _a - _b, _b else: _a, _b = _b - _a, _a assert _a >= 0 and _b >= 0 if not all(term in DIGITS for term in (num(_a), num(_b))): # multi-digit addition return DecimalSequence.add_eval(_a, _b) with defaults.temporary() as temp_defaults: # We rely upon side-effect automation here. temp_defaults.sideeffect_automation = True # for single digit addition, import the theorem that provides # the evaluation proveit.numbers.numerals.decimals.__getattr__( 'add_%d_%d' % (_a, _b)) return self.evaluation() def _rational_binary_eval(self): ''' Evaluate the sum of possibly literal rational numbers. The evaluation must be irreducible which means that the result (right hand side of the proven equation) must be an integer or a (possibly negated) fraction with no common divisors between the numerator and denominator other than 1. ''' from proveit.numbers import (Div, num, is_numeric_rational, numeric_rational_ints) from . import rational_pair_addition terms = self.terms if not terms.is_double() or ( not all(is_numeric_rational(term) for term in terms)): raise ValueError( "_rational_binary_eval only applicable for binary addition " "of rationals") _a, _b = numeric_rational_ints(terms[0]) _c, _d = numeric_rational_ints(terms[1]) _a, _b, _c, _d = num(_a), num(_b), num(_c), num(_d) # Replace the irreducible forms with the original forms. replacements = [Equals(Div(_a, _b), terms[0]).prove(), Equals(Div(_c, _d), terms[1]).prove()] # Combine the sum using # (a/b) + (c/d) = (a*d + b*c)/(b*d) # Applying automatic simplifications should evaluate the # numerator and denominator and then reduce it to an # irreducible form. return rational_pair_addition.instantiate( {a:_a, b:_b, c:_c, d:_d}, auto_simplify=True, replacements=replacements, preserve_expr=self)
[docs] def subtraction_folding(self, term_idx=None, assumptions=frozenset()): ''' Given a negated term, term_idx or the first negated term if term_idx is None, deduce the equivalence between self and a Subtract form (with the specified negated term on the right of the subtraction). Assumptions may be necessary to deduce operands being in the set of Complex numbers. ''' from proveit.numbers import Neg from proveit.numbers.addition.subtraction.theorems import add_neg_as_subtract if term_idx is None: for _k, term in enumerate(self.terms.entries): if isinstance(term, Neg): term_idx = _k break if term_idx is None: raise ValueError( "No negated term, can't provide the subtraction folding.") if not isinstance(self.terms[term_idx], Neg): raise ValueError( "Specified term is not negated, can't provide the subtraction folding.") expr = self if term_idx != -1 and term_idx != expr.terms.num_entries() - 1: # put the negative term at the end expr = expr.commute(term_idx, term_idx + 1, -1) if expr.terms.num_entries() > 2: # group all of the other terms expr = expr.group(0, -1) return add_neg_as_subtract.instantiate( {x: expr.operands[0], y: expr.operands[-1].operand})
""" def deduce_in_natural_pos_directly(self, assumptions=frozenset(), ruled_out_sets=frozenset(), dont_try_pos=False, dont_try_neg=False): ''' If all of the terms are in Natural and just one is positive, then the sum is positive. ''' from proveit.numbers.number_sets import DeduceInNumberSetException, deduce_positive from . import add_nat_pos_closure from proveit.numbers import NaturalPos, num # first make sure all the terms are in Natural for _k, term in enumerate(self.operands): #try: # found one positive term to make the sum positive deduce_positive(term, assumptions) return add_nat_pos_closure.instantiate({i:num(_k), n:num(self.operands.num_entries()-_k-1), a:self.operands[:_k], b:term, c:self.operands[_k+1:]}, assumptions=assumptions) #except: # pass # need to have one of the elements positive for the sum to be positive raise DeduceInNumberSetException(self, NaturalPos, assumptions) """
[docs] @relation_prover def deduce_in_number_set(self, number_set, **defaults_config): ''' given a number set, attempt to prove that the given expression is in that number set using the appropriate closure theorem ''' import proveit.numbers.addition as add_pkg from proveit.numbers.addition.subtraction import ( subtract_nat_closure_bin, sub_one_is_nat) from proveit.numbers import (zero, one, Neg, greater, Less, LessEq, greater_eq) from proveit.logic import InSet if number_set == ZeroSet: if self.operands.is_double(): return add_pkg.add_zero_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_zero_closure.instantiate({i:_i, a: _a}) if number_set == Integer: if self.operands.is_double(): return add_pkg.add_int_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_int_closure.instantiate({i:_i, a: _a}) if number_set == Rational: if self.operands.is_double(): return add_pkg.add_rational_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_rational_closure.instantiate({i: _i, a: _a}) if number_set == Real: if self.operands.is_double(): return add_pkg.add_real_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_real_closure.instantiate({i: _i, a: _a}) if number_set == Complex: if self.operands.is_double(): return add_pkg.add_complex_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_complex_closure.instantiate({i: _i, a: _a}) # Prove what we can in preparation. for operand in self.operands: deduce_number_set(operand) # Handle special cases when all operands are in # the desired number set. if all(InSet(operand, number_set).proven() for operand in self.operands): if number_set == Natural: if self.operands.is_double(): return add_pkg.add_nat_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_nat_closure.instantiate({i: _i, a: _a}) if number_set == NaturalPos: if self.operands.is_double(): return add_pkg.add_nat_pos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_nat_pos_closure.instantiate({i: _i, a: _a}) if number_set == IntegerNeg: if self.operands.is_double(): return add_pkg.add_int_neg_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_int_neg_closure.instantiate({i: _i, a: _a}) if number_set == IntegerNonPos: if self.operands.is_double(): return add_pkg.add_int_nonpos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_int_nonpos_closure.instantiate({i: _i, a: _a}) if number_set == RationalPos: if self.operands.is_double(): return add_pkg.add_rational_pos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_rational_pos_closure.instantiate({i: _i, a: _a}) if number_set == RationalNeg: if self.operands.is_double(): return add_pkg.add_rational_neg_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() add_pkg.add_rational_neg_closure.instantiate({i: _i, a: _a}) if number_set == RationalNonNeg: if self.operands.is_double(): return add_pkg.add_rational_nonneg_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_rational_nonneg_closure.instantiate({i:_i, a: _a}) if number_set == RationalNonPos: if self.operands.is_double(): return add_pkg.add_rational_nonpos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_rational_nonpos_closure.instantiate({i:_i, a: _a}) if number_set == RealPos: if self.operands.is_double(): return add_pkg.add_real_pos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_real_pos_closure.instantiate({i: _i, a: _a}) if number_set == RealNeg: if self.operands.is_double(): return add_pkg.add_real_neg_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_real_neg_closure.instantiate({i: _i, a: _a}) if number_set == RealNonNeg: if self.operands.is_double(): return add_pkg.add_real_nonneg_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_real_nonneg_closure.instantiate({i:_i, a: _a}) if number_set == RealNonPos: if self.operands.is_double(): return add_pkg.add_real_nonpos_closure_bin.instantiate( {a: self.operands[0], b: self.operands[1]}) _a = self.operands _i = _a.num_elements() return add_pkg.add_real_nonpos_closure.instantiate({i:_i, a: _a}) # Try special case where one term is positive and the # rest are non-negative. if number_set in {NaturalPos, RationalPos, RealPos}: val = None for _i, operand in enumerate(self.operands.entries): if greater(operand, zero).readily_provable(): val = _i elif not greater_eq(operand, zero).readily_provable(): # Not non-negative val = None break # Forget it. if val is not None: if number_set == NaturalPos: temp_thm = add_pkg.add_nat_pos_from_nonneg elif number_set == RationalPos: temp_thm = add_pkg.add_rational_pos_from_nonneg else: temp_thm = add_pkg.add_real_pos_from_nonneg _a, _b, _c = (self.operands[:val], self.operands[val], self.operands[val + 1:]) _i = _a.num_elements() _j = _c.num_elements() return temp_thm.instantiate( {i: _i, j: _j, a: _a, b: _b, c: _c}) # Try special case where one term is negative and the # rest are non-positive. if number_set in {IntegerNeg, RationalNeg, RealNeg}: val = None for _i, operand in enumerate(self.operands.entries): if greater(operand, zero).readily_provable(): val = _i elif not greater_eq(operand, zero).readily_provable(): # Not non-negative val = None break # Forget it. if val is not None: if number_set == NaturalPos: temp_thm = add_pkg.add_int_neg_from_nonpos elif number_set == RationalPos: temp_thm = add_pkg.add_rational_neg_from_nonpos else: temp_thm = add_pkg.add_real_neg_from_nonpos _a, _b, _c = (self.operands[:val], self.operands[val], self.operands[val + 1:]) _i = _a.num_elements() _j = _c.num_elements() return temp_thm.instantiate( {i: _i, j: _j, a: _a, b: _b, c: _c}) # Handle positive, negative, nonpos, nonneg, or nonzero major_number_set = None if number_set in {IntegerNonZero, RationalNonZero, RealNonZero, ComplexNonZero}: # Prove it is not zero and prove it is in the corresponding # major number set (Integer, Rational, Real, or Complex) self.deduce_not_equal(zero, try_deduce_number_set=False) to_major_number_set = {IntegerNonZero:Integer, RationalNonZero:Rational, RealNonZero:Real, ComplexNonZero:Complex} major_number_set = to_major_number_set[number_set] if number_set in {NaturalPos, RationalPos, RealPos}: # Prove it is positive and prove it is in the corresponding # major number set (Integer, Rational, Real) self.deduce_positive(try_deduce_number_set=False) to_major_number_set = {NaturalPos:Integer, RationalPos:Rational, RealPos:Real} major_number_set = to_major_number_set[number_set] if number_set in {IntegerNeg, RationalNeg, RealNeg}: # Prove it is negative and prove it is in the corresponding # major number set (Integer, Rational, Real) self.deduce_negative(try_deduce_number_set=False) to_major_number_set = {IntegerNeg:Integer, RationalNeg:Rational, RealNeg:Real} major_number_set = to_major_number_set[number_set] if number_set in {IntegerNonPos, RationalNonPos, RealNonPos}: # Prove it is non-positive and prove it is in the # corresponding major number set (Integer, Rational, Real) self.deduce_non_positive(try_deduce_number_set=False) to_major_number_set = {IntegerNonPos:Integer, RationalNonPos:Rational, RealNonPos:Real} major_number_set = to_major_number_set[number_set] if number_set in {Natural, RationalNonNeg, RealNonNeg}: # Prove it is non-positive and prove it is in the # corresponding major number set (Integer, Rational, Real) self.deduce_non_negative(try_deduce_number_set=False) to_major_number_set = {Natural:Integer, RationalNonNeg:Rational, RealNonNeg:Real} major_number_set = to_major_number_set[number_set] if major_number_set is not None: self.deduce_in_number_set(major_number_set) # Now it should just go through. return InSet(self, number_set).conclude_as_last_resort() raise NotImplementedError( "'deduce_in_number_set' on %s not implemented for the %s set" % (self, number_set))
def deduce_positive(self, *, try_deduce_number_set=True, **defaults_config): ''' Prove the sum is positive. ''' from proveit.numbers import greater, zero, Neg from .subtraction import pos_difference if greater(self, zero).proven(): # Already known (don't use readily_provable). return greater(self, zero).prove() if self.terms.is_double() and isinstance(self.terms[1], Neg): # (a - b) with a > b => (a - b) is positive _a, _b = self.terms[0], self.terms[1].operand if greater(_a, _b).readily_provable(): return pos_difference.instantiate({a:_a, b:_b}) if try_deduce_number_set: # Try 'deduce_number_set'. deduce_number_set(self) # Last resort attempt return greater(self, zero).prove() @relation_prover def deduce_negative(self, *, try_deduce_number_set=True, **defaults_config): ''' Prove the sum is negative. ''' from proveit.numbers import Less, zero, Neg from .subtraction import neg_difference if Less(self, zero).proven(): # Already known (don't use readily_provable). return Less(self, zero).prove() if self.terms.is_double() and isinstance(self.terms[1], Neg): # (a - b) with a < b => (a - b) is negative _a, _b = self.terms[0], self.terms[1].operand if Less(_a, _b).readily_provable(): return neg_difference.instantiate({a:_a, b:_b}) if try_deduce_number_set: # Try 'deduce_number_set'. deduce_number_set(self) # Last resort attempt return Less(self, zero).prove() def deduce_non_positive(self, *, try_deduce_number_set=True, **defaults_config): ''' Prove the sum is non-positive. ''' from proveit.numbers import LessEq, zero, Neg from .subtraction import nonpos_difference if LessEq(self, zero).proven(): # Already known (don't use readily_provable). return LessEq(self, zero).prove() if self.terms.is_double() and isinstance(self.terms[1], Neg): # (a - b) with a <= b => (a - b) is non-positive _a, _b = self.terms[0], self.terms[1].operand if LessEq(_a, _b).readily_provable(): return nonpos_difference.instantiate({a:_a, b:_b}) if try_deduce_number_set: # Try 'deduce_number_set'. deduce_number_set(self) # Last resort attempt return LessEq(self, zero).prove() def deduce_non_negative(self, *, try_deduce_number_set=True, **defaults_config): ''' Prove the sum is non-negative. ''' from proveit.numbers import greater_eq, zero, Neg from .subtraction import nonneg_difference if greater_eq(self, zero).proven(): # Already known (don't use readily_provable). return greater_eq(self, zero).prove() if self.terms.is_double() and isinstance(self.terms[1], Neg): # (a - b) with a >= b => (a - b) is non-negative _a, _b = self.terms[0], self.terms[1].operand if greater_eq(_a, _b).readily_provable(): return nonneg_difference.instantiate({a:_a, b:_b}) if try_deduce_number_set: # Try 'deduce_number_set'. deduce_number_set(self) # Last resort attempt return greater_eq(self, zero).prove() def readily_provable_number_set(self): ''' Return the most restrictive number set we can readily prove contains the evaluation of this number operation. ''' from proveit.numbers import (Neg, greater, greater_eq, Less, LessEq) nonzero_to_full_number_set = { IntegerNonZero:Integer, RationalNonZero:Rational, RealNonZero:Real, ComplexNonZero:Complex} operands = self.operands if operands.num_entries() == 0: return ZeroSet # [+]() = 0 list_of_operand_sets = [] # find a minimal std number set for operand any_positive = False any_negative = False for operand in operands: operand_ns = readily_provable_number_set(operand) if RealPos.readily_includes(operand_ns): any_positive = True if RealNeg.readily_includes(operand_ns): any_negative = True list_of_operand_sets.append(operand_ns) # Find the number set that number_set = union_number_set(*list_of_operand_sets) if number_set in nonzero_to_full_number_set: # Adding non-zero operands provides no guarantee that the # result will be non-zero (unlike adding positives, # negatives, nonpositives, or nonnegatives). number_set = nonzero_to_full_number_set[number_set] restriction = None if RealPos.readily_includes(number_set): restriction = pos_number_set # must be positive elif RealNeg.readily_includes(number_set): restriction = neg_number_set # must be negative elif RealNonNeg.readily_includes(number_set): if any_positive: restriction = pos_number_set # must be positive else: restriction = nonneg_number_set # must be non-negative elif RealNonPos.readily_includes(number_set): if any_negative: restriction = neg_number_set # must be negative else: restriction = nonpos_number_set # must be non-positive if restriction not in (pos_number_set, neg_number_set): # Check for the special case of a - b where we know # a > b, a < b, a ≥ b, a ≤ b, or a ≠ b if self.terms.is_double() and isinstance(self.terms[1], Neg): _a, _b = self.terms[0], self.terms[1].operand if greater(_a, _b).readily_provable(): restriction = pos_number_set # positive elif greater_eq(_a, _b).readily_provable(): restriction = nonneg_number_set # non-negative elif Less(_a, _b).readily_provable(): restriction = neg_number_set # negative elif LessEq(_a, _b).readily_provable(): restriction = nonpos_number_set # non-positive elif NotEquals(_a, _b).readily_provable(): restriction = nonzero_number_set # non-zero # Use the positive, negative, non-negative, non-positive, or # non-zero restriction. if restriction is not None: return restriction[number_set] return number_set # IS THIS NECESSARY?
[docs] @prover def deduce_difference_in_natural(self, **defaults_config): from proveit.numbers import Neg from proveit.numbers.number_sets.integers import difference_is_nat if not self.terms.is_double(): raise ValueError("deduce_difference_in_natural only applicable " "when there are two terms, got %s" % self) if not isinstance(self.terms[1], Neg): raise ValueError("deduce_difference_in_natural only applicable " "for a subtraction, got %s" % self) thm = difference_is_nat return thm.instantiate({a: self.terms[0], b: self.terms[1].operand})
# IS THIS NECESSARY?
[docs] @prover def deduce_difference_in_natural_pos(self, **defaults_config): from proveit.numbers import Neg from proveit.numbers.number_sets.integers import difference_is_nat_pos if not self.terms.is_double(): raise ValueError( "deduce_difference_in_natural_pos only applicable " "when there are two terms, got %s" % self) if not isinstance(self.terms[1], Neg): raise ValueError( "deduce_difference_in_natural_pos only applicable " "for a subtraction, got %s" % self) thm = difference_is_nat_pos return thm.instantiate({a: self.terms[0], b: self.terms[1].operand})
def index(self, the_term, also_return_num=False): ''' Return the starting index of the_term, which may be a single operand, a list of consecutive operands, or a Add expression that represents the sum of the list of consecutive operands. If also_return_num is True, return a tuple of the index and number of operands for the_term. ''' if isinstance(the_term, Add): the_term = the_term.operands.entries if (hasattr(the_term, '__getitem__') and hasattr(the_term, '__len__')): # multiple operands in the_term first_term = the_term[0] num = len(the_term) idx = -1 try: while True: idx = self.operands.index(first_term, start=idx + 1) if self.operands[idx:idx + num].entries == tuple(the_term): break # found it all! except ValueError: raise ValueError("Term is absent!") else: num = 1 try: idx = self.operands.index(the_term) except ValueError: raise ValueError("Term is absent!") return (idx, num) if also_return_num else idx def readily_factorable(self, factor): ''' Return True iff 'factor' is factorable from 'self' in an obvious manner. For this Add, it is readily factorable if it is readily factorable from all terms. ''' from proveit.numbers import readily_factorable if self == factor: return True for term in self.terms: if not readily_factorable(term, factor): return False return True
[docs] @auto_equality_prover('factorized', 'factor') def factorization(self, the_factors, pull="left", group_factors=True, group_remainder=True, **defaults_config): ''' Factor out the factor(s) from this sum, pulling it either to the "left" or "right". If group_factors is True, the factors are grouped together as a sub-product. In the Add case, the remainder will always be grouped (we have 'group_remainder' as a parameter just for recursion compatibility). ''' from proveit.numbers.multiplication import distribute_through_sum from proveit.numbers import one, Mult if pull not in ('left', 'right'): raise ValueError("'pull' must be 'left' or 'right'") expr = self # for convenience updating our equation eq = TransRelUpdater(expr) replacements = list(defaults.replacements) _b = [] if not isinstance(the_factors, Expression): # If 'the_factors' is not an Expression, assume it is # an iterable and make it a Mult. the_factors = Mult(*the_factors) # factor the_factor from each term for _i in range(expr.terms.num_entries()): term = expr.terms[_i] if term == the_factors: if pull == 'left': replacements.append(Mult(term, one).one_elimination(1)) else: replacements.append(Mult(one, term).one_elimination(0)) _b.append(one) else: if not hasattr(term, 'factorization'): raise ValueError( "Factor, %s, is not present in the term at " "index %d of %s!" % (the_factors, _i, self)) term_factorization = term.factorization( the_factors, pull, group_factors=group_factors, group_remainder=True) if not isinstance(term_factorization.rhs, Mult): raise ValueError( "Expecting right hand side of each factorization " "to be a product. Instead obtained: {0} for term " "number {1} (0-based index).". format(term_factorization.rhs, _i)) if pull == 'left': # the grouped remainder on the right _b.append(term_factorization.rhs.operands[-1]) else: # the grouped remainder on the left _b.append(term_factorization.rhs.operands[0]) # substitute in the factorized term expr = eq.update(term_factorization.substitution( expr.inner_expr().terms[_i])) if not group_factors and isinstance(the_factors, Mult): factor_sub = the_factors.operands else: factor_sub = ExprTuple(the_factors) if pull == 'left': _a = factor_sub _c = ExprTuple() else: _a = ExprTuple() _c = factor_sub _b = ExprTuple(*_b) _i = _a.num_elements() _j = _b.num_elements() _k = _c.num_elements() distribution = distribute_through_sum.instantiate( {i: _i, j: _j, k: _k, a: _a, b: _b, c: _c}, preserve_expr=expr, replacements=replacements) eq.update(distribution.derive_reversed()) return eq.relation
@equality_prover('combined_terms', 'combine_terms') def combining_terms(self, **defaults_config): ''' Combine terms, adding their literal, rational coefficients. Alias for `combining_operands`. ''' from proveit.numbers import one, Div from proveit.numbers.multiplication.mult import ( coefficient_and_remainder) # Obtain the common term "remainder" (sans coefficient), # raising a ValueError if the terms are not all like terms. likeness_key_fn = lambda term : ( coefficient_and_remainder(term)[1]) try: key = common_likeness_key(self, likeness_key_fn=likeness_key_fn) if isinstance(key, ExprRange): raise ValueError except ValueError as _e: if any( not( isinstance(term, Div) or (isinstance(term, ExprRange) and isinstance(term.body, Div))) for term in self.terms): return _e # testing new denominator def to accommodate ExprRange? # denominator = common_likeness_key( # self, likeness_key_fn = lambda term: term.denominator) denominator = common_likeness_key( self, likeness_key_fn = ( lambda term: term.denominator if isinstance(term, Div) else term.body.denominator)) # the following handles both a set of fracs and an # ExprRange of fracs and any combination of the two numerator_terms = self.terms.map_elements( lambda term: term.numerator) # create our desired combination of like fractions combined = Div(Add(*numerator_terms), denominator) replacements = list(defaults.replacements) if defaults.auto_simplify: combined_simp = combined.simplification() if combined_simp.lhs != combined_simp.rhs: replacements.append(combined_simp) return (combined.distribution(preserve_all=True). derive_reversed(replacements=replacements)) if key != one: # Factor out the common part from the coefficients. return self.factorization(key, pull="right") # All of the operands are rational, literals. if defaults.auto_simplify: # Simplify if auto-simplification is on. return self.simplification() else: return Equals(self, self).conclude_via_reflexivity() @equality_prover('combined_operands', 'combine_operands') def combining_operands(self, **defaults_config): ''' Combine terms, adding their literal, rational coeffiicents. Alias for `combining_terms`. ''' return self.combining_terms()
[docs] @equality_prover('commuted', 'commute') def commutation(self, init_idx=None, final_idx=None, **defaults_config): ''' Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (a + b + ... + y + z) = (a + ... + y + b + z) via init_idx = 1 and final_idx = -2. ''' from . import commutation, leftward_commutation, rightward_commutation return apply_commutation_thm( self, init_idx, final_idx, commutation, leftward_commutation, rightward_commutation)
[docs] @equality_prover('group_commuted', 'group_commute') def group_commutation(self, init_idx, final_idx, length, disassociate=True, **defaults_config): ''' Given numerical operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassocate is True, it will be disassociated afterwards. ''' return group_commutation( self, init_idx, final_idx, length, disassociate=disassociate)
@equality_prover('moved', 'move') def permutation_move(self, init_idx=None, final_idx=None, **defaults_config): ''' Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (a + b + ... + y + z) = (a + ... + y + b + z) via init_idx = 1 and final_idx = -2. ''' return self.commutation(init_idx, final_idx) @equality_prover('permuted', 'permute') def permutation(self, new_order=None, cycles=None, **defaults_config): ''' Deduce that this Add expression is equal to an Add in which the terms at indices 0, 1, …, n-1 have been reordered as specified EITHER by the new_order list OR by the cycles list parameter. For example, (a+b+c+d).permutation_general(new_order=[0, 2, 3, 1]) and (a+b+c+d).permutation_general(cycles=[(1, 2, 3)]) would both return ⊢ (a+b+c+d) = (a+c+d+b). ''' return generic_permutation(self, new_order, cycles)
[docs] @equality_prover('associated', 'associate') def association(self, start_idx, length, **defaults_config): ''' Given numerical operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (a + b + ... + y + z) = (a + b ... + (l + ... + m) + ... + y + z) ''' from . import association eq = apply_association_thm( self, start_idx, length, association) ''' # DON'T WORRY ABOUT RESETTING THE STYLE FOR THE MOMENT. # set the subraction style as appropriate given what we started with: subtraction_positions = self.subtraction_positions() eq.inner_expr().lhs.with_subtraction_at(*subtraction_positions) beg_positions = [p for p in subtraction_positions if p < start_idx] inner_positions = [p-start_idx for p in subtraction_positions if start_idx <= p < start_idx+length] end_positions = [p-length for p in subtraction_positions if p > start_idx+length] eq.inner_expr().rhs.operands[start_idx].with_subtraction_at(*inner_positions) eq.inner_expr().rhs.operands[start_idx].with_subtraction_at(*(beg_positions + end_positions)) ''' return eq
[docs] @equality_prover('disassociated', 'disassociate') def disassociation(self, idx, **defaults_config): ''' Given numerical operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (a + b ... + (l + ... + m) + ... + y+ z) = (a + b + ... + y + z) ''' from proveit.core_expr_types import Len from proveit.numbers import Neg from . import disassociation from .subtraction import subtraction_disassociation if (isinstance(self.operands[idx], Neg) and isinstance(self.operands[idx].operand, Add)): subtraction_terms = self.operands[idx].operand.operands _a = self.operands[:idx] _b = subtraction_terms _c = self.operands[idx + 1:] _i = Len(_a).computed() _j = Len(_b).computed() _k = Len(_c).computed() return subtraction_disassociation.instantiate( {i: _i, j: _j, k: _k, a: _a, b: _b, c: _c}) eq = apply_disassociation_thm(self, idx, disassociation) ''' # DON'T WORRY ABOUT RESETTING THE STYLE FOR THE MOMENT. # set the subraction style as appropriate given what we started with: subtraction_positions = self.subtraction_positions() inner_positions = self.operand[idx].subtraction_positions() inner_num_operands = len(self.operand[idx]) eq.inner_expr().lhs.operands[idx].with_subtraction_at(*inner_positions) eq.inner_expr().lhs.with_subtraction_at(*subtraction_positions) new_positions = [p for p in subtraction_positions if p < idx] new_positions.extend([p+idx for p in inner_positions]) new_positions.extend([p+inner_num_operands for p in subtraction_positions if p > idx]) eq.inner_expr().rhs.with_subtraction_at(*new_positions) ''' return eq
@relation_prover def bound_via_operand_bound(self, operand_relation, **defaults_config): ''' Alias for bound_via_term_bound. Also see NumberOperation.deduce_bound. ''' return self.bound_via_term_bound(operand_relation) @relation_prover def bound_via_term_bound(self, term_relation, **defaults_config): ''' Deduce a bound of this sum via the bound on one of its terms. For example a + b + c + d < a + z + c + d given b < z. Also see NumberOperation.deduce_bound. ''' from proveit.numbers import NumberOrderingRelation, Less if isinstance(term_relation, Judgment): term_relation = term_relation.expr if not isinstance(term_relation, NumberOrderingRelation): raise TypeError("'term_relation' expected to be a number " "relation (<, >, ≤, or ≥)") idx = None for side in term_relation.operands: try: idx, num = self.index(side, also_return_num=True) break except ValueError: pass if idx is None: raise TypeError("'term_relation' expected to be a relation " "for one of the terms; neither term of %s " "appears in the %s relation." %(self, term_relation)) expr = self eq = TransRelUpdater(expr) if num > 1: expr = eq.update(expr.association(idx, num,)) if expr.operands.is_double(): # Handle the binary cases. assert 0 <= idx < 2 if idx == 0: relation = term_relation.right_add_both_sides(expr.terms[1]) elif idx == 1: relation = term_relation.left_add_both_sides(expr.terms[0]) expr = eq.update(relation) else: thm = None if isinstance(term_relation, Less): # We can use the strong bound. from . import strong_bound_via_term_bound thm = strong_bound_via_term_bound else: # We may only use the weak bound. from . import weak_bound_via_term_bound thm = weak_bound_via_term_bound _a = self.terms[:idx] _b = self.terms[idx+1:] _i = _a.num_elements() _j = _b.num_elements() _x = term_relation.normal_lhs _y = term_relation.normal_rhs expr = eq.update(thm.instantiate( {i: _i, j: _j, a: _a, b: _b, x: _x, y: _y})) if num > 1 and isinstance(expr.terms[idx], Add): expr = eq.update(expr.disassociation(idx)) relation = eq.relation if relation.lhs != self: relation = relation.with_direction_reversed() assert relation.lhs == self return relation @relation_prover def bound_by_term(self, term_or_idx, use_weak_bound=False, **defaults_config): ''' Deduce that this sum is bound by the given term (or term at the given index). For example, a + b + c + d ≥ b provided that a ≥ 0, c ≥ 0, and d ≥ 0. To use this method, we must know that the other terms are all in RealPos, RealNeg, RealNonNeg, or RealNonPos and will call deduce_weak_upper_bound_by_term, deduce_strong_upper_bound_by_term, deduce_weak_lower_bound_by_term, deduce_strong_lower_bound_by_term accordingly. ''' from proveit.numbers import RealPos, RealNeg, RealNonNeg, RealNonPos relevant_number_sets = {RealPos, RealNeg, RealNonNeg, RealNonPos} for _k, term_entry in enumerate(self.terms.entries): if _k == term_or_idx or term_entry == term_or_idx: # skip the term doing the bounding. continue for number_set in list(relevant_number_sets): if isinstance(term_entry, ExprRange): in_number_set = And(ExprRange( term_entry.parameter, InSet(term_entry.body, number_set), term_entry.true_start_index, term_entry.true_end_index)) else: in_number_set = InSet(term_entry, number_set) if not in_number_set.readily_provable(): relevant_number_sets.discard(number_set) if len(relevant_number_sets) == 0: raise UnsatisfiedPrerequisites( "In order to use Add.bound_by_term, the " "'other' terms must all be known to be contained " "in RealPos, RealNeg, RealNonNeg, RealNonPos") if not use_weak_bound: # If a strong bound is applicable, use that. if RealPos in relevant_number_sets: return self.deduce_strong_lower_bound_by_term(term_or_idx) if RealNeg in relevant_number_sets: return self.deduce_strong_upper_bound_by_term(term_or_idx) if RealNonNeg in relevant_number_sets: return self.deduce_weak_lower_bound_by_term(term_or_idx) if RealNonPos in relevant_number_sets: return self.deduce_weak_upper_bound_by_term(term_or_idx) @relation_prover def deduce_weak_lower_bound_by_term( self, term_or_idx, **defaults_config): ''' Deduce that this sum is greater than or equal to the term at the given index. ''' from . import term_as_weak_lower_bound return self._deduce_specific_bound_by_term( term_as_weak_lower_bound, term_or_idx) @relation_prover def deduce_weak_upper_bound_by_term( self, term_or_idx, **defaults_config): ''' Deduce that this sum is less than or equal to the term at the given index. ''' from . import term_as_weak_upper_bound return self._deduce_specific_bound_by_term( term_as_weak_upper_bound, term_or_idx) @relation_prover def deduce_strong_lower_bound_by_term( self, term_or_idx, **defaults_config): ''' Deduce that this sum is greater than the term at the given index. ''' from . import term_as_strong_lower_bound return self._deduce_specific_bound_by_term( term_as_strong_lower_bound, term_or_idx) @relation_prover def deduce_strong_upper_bound_by_term( self, term_or_idx, **defaults_config): ''' Deduce that this sum is less than the term at the given index. ''' from . import term_as_strong_upper_bound return self._deduce_specific_bound_by_term( term_as_strong_upper_bound, term_or_idx) def _deduce_specific_bound_by_term(self, thm, term_or_idx): ''' Helper method for deduce_weak_lower_bound_by_term, deduce_weak_upper_bound_by_term, deduce_strong_lower_bound_by_term, and deduce_strong_lower_bound_by_term. ''' if isinstance(term_or_idx, Expression): try: idx = self.terms.index(term_or_idx) except ValueError: raise ValueError( "'term_or_idx' must be one of the terms of %s " "or an index for one of the terms."%self) else: if not isinstance(term_or_idx, int): raise TypeError( "'term_or_idx' must be an Expression or int") idx = term_or_idx _a = self.terms[:idx] _b = self.terms[idx] _c = self.terms[idx + 1:] _i = _a.num_elements() _j = _c.num_elements() return thm.instantiate({i: _i, j: _j, a: _a, b: _b, c: _c}) @relation_prover def deduce_not_equal(self, other, *, try_deduce_number_set=True, **defaults_config): ''' Attempt to prove that self is not equal to other. ''' from proveit.numbers import zero, Neg if other == zero: if self.terms.is_double(): if isinstance(self.terms[1], Neg): from .subtraction import nonzero_difference_if_different _a = self.terms[0] _b = self.terms[1].operand if NotEquals(_a, _b).readily_provable(): # If we know (or can readily prove) that # _a != _b then we can prove _a - _b != 0. return nonzero_difference_if_different.instantiate( {a:_a, b:_b}) if try_deduce_number_set: # Try deducing the number set. number_set = readily_provable_number_set(self) if ComplexNonZero.readily_includes(number_set): deduce_number_set(self) return NotEquals(self, zero).prove() if NotEquals(self, other).readily_provable(): # Readily provable. return NotEquals(self, other).prove() # If it isn't a special case treated here, just use # conclude-as-folded. return NotEquals(self, other).conclude_as_folded()
[docs]def subtract(a, b): ''' Return the a-b expression (which is internally a+(-b)). ''' from proveit.numbers import Neg if isinstance(b, ExprRange): b = ExprRange(b.lambda_map.parameter_or_parameters, Neg(b.lambda_map.body), b.true_start_index, b.true_end_index, b.get_styles()) # The default style will use subtractions where appropriate. return Add(a, b) return Add(a, Neg(b))
[docs]def dist_subtract(a, b): ''' Returns the distributed a-b expression. That is, if a or b are Add expressions, combine all of the terms into a single Add expression (not nested). For example, with a:x-y, b:c+d-e+g, it would return x-y-c-d+e-g. ''' from proveit.numbers import Neg if isinstance(b, Add): bterms = [term.operand if isinstance(term, Neg) else Neg(term) for term in b.terms] elif isinstance(b, ExprRange): bterms = [ExprRange(b.lambda_map.parameter_or_parameters, Neg(b.lambda_map.body), b.true_start_index, b.true_end_index, b.get_styles())] else: bterms = [Neg(b)] if isinstance(a, Add): aterms = a.terms else: aterms = [a] # The default style will use subtractions where appropriate. return Add(*(aterms + bterms))
[docs]def dist_add(*terms): ''' Returns the distributed sum of expression. That is, if any of the terms are Add expressions, expand them. For example, dist_add(x-y, c+d-e+g) would return x-y+c+d-e+g. ''' expanded_terms = [] for term in terms: if isinstance(term, Add): expanded_terms.extend(term.terms) else: expanded_terms.append(term) return Add(*expanded_terms)
def split_int_shift(expr): ''' If the expression contains an additive integer shift term, return the remaining terms and the shift independently as a pair. Otherwise, return the expression paired with a zero shift. ''' from proveit.numbers import is_numeric_int, zero, Neg if isinstance(expr, Neg): expr = Add(expr) # wrap in an Add so we can do quick_simplified if isinstance(expr, Add): expr = expr.quick_simplified() if (isinstance(expr, Add) and is_numeric_int(expr.terms[-1])): shift = expr.terms[-1].as_int() if expr.terms.num_entries() == 1: return shift elif (expr.terms.num_entries() == 2 and not isinstance(expr.terms[0], ExprRange)): return expr.terms[0], shift else: return Add(*expr.terms[:-1].entries), shift if is_numeric_int(expr): return zero, expr.as_int() return expr, 0