from proveit import (Expression, Literal, Lambda, Function, Operation,
OperationOverInstances, InnerExpr,
Judgment, free_vars, maybe_fenced, USE_DEFAULTS,
ProofFailure, defaults,
prover, relation_prover, equality_prover,
auto_prover, auto_relation_prover, auto_equality_prover,
SimplificationDirectives, UnsatisfiedPrerequisites)
from proveit import a, b, c, f, i, j, k, l, m, x, Q, S
from proveit.logic import Forall, InSet
from proveit.numbers import one, Add, Neg, subtract
from proveit.numbers import (ZeroSet, Complex, Integer, Interval, Natural,
NaturalPos, Rational, Real, RealInterval,
readily_provable_number_set)
from proveit.numbers.ordering import Less, LessEq
from proveit import TransRelUpdater
[docs]class Sum(OperationOverInstances):
# operator of the Sum operation.
_operator_ = Literal(
string_format='Sum',
latex_format=r'\sum',
theory=__file__)
_init_argname_mapping_ = {'index_or_indices': 'instance_param_or_params',
'summand': 'instance_expr'}
_simplification_directives_ = SimplificationDirectives(
pull_out_index_indep_factors=True)
def __init__(self, index_or_indices, summand, *,
domain=None, domains=None, condition=None,
conditions=None, styles=None, _lambda_map=None):
r'''
Sum summand over indices over domains.
Arguments serve analogous roles to Forall arguments (found in
basiclogic.booleanss):
indices: instance vars
summand: instance_expressions
domains: conditions (except no longer optional)
'''
if (domains is not None):
raise NotImplementedError("Sum class not yet implemented for "
"multiple domains nor for multiple "
"indices.")
OperationOverInstances.__init__(
self, Sum._operator_, index_or_indices, summand,
domain=domain, domains=domains, condition=condition,
conditions=conditions, styles=styles, _lambda_map=_lambda_map)
if hasattr(self, 'instance_param'):
self.index = self.instance_param
if hasattr(self, 'instance_params'):
self.indices = self.instance_params
self.summand = self.instance_expr
"""
# think about this later
if isinstance(self.domain,RealInterval):
raise ValueError('Sum cannot sum over non-discrete set (e.g. Interval)')
elif self.domain == Real:
raise ValueError('Sum cannot sum over Real.')
elif self.domain == Integer:
self.domain = Interval(Neg(infinity),infinity)
elif self.domain == Natural:
self.domain = Interval(zero,infinity)
"""
def _build_canonical_form(self):
'''
Returns a canonical form of this Sum with any
index-independent factors pulled out in front.
'''
from proveit.numbers import Mult
canonical_summand = self.summand.canonical_form()
if isinstance(canonical_summand, Mult):
# Pull any index-independent scalar factors in front.
index_indep_factors = []
index_dep_factors = []
for factor in canonical_summand.factors:
if free_vars(factor).isdisjoint(self.indices):
index_indep_factors.append(factor)
else:
index_dep_factors.append(factor)
if len(index_indep_factors) > 0:
# Pulling out some index-independent scalar factors.
if len(index_dep_factors) > 0:
# Keeping some index-dependent scalar factors
# within the VecSum.
canonical_summand = Mult(
*index_dep_factors).canonical_form()
else:
canonical_summand = one
# Build/return the Mult with the Sum.
_sum = Sum(self.indices, canonical_summand,
conditions=self.conditions.canonical_form())
return Mult(
Mult(*index_indep_factors), _sum).canonical_form()
# Build the canonical VecSum.
return Sum(self.indices, canonical_summand,
conditions=self.conditions.canonical_form())
[docs] @relation_prover
def deduce_in_number_set(self, number_set, **defaults_config):
from . import (summation_zero_closure, summation_nat_closure,
summation_nat_pos_closure, summation_int_closure,
summation_real_closure, summation_complex_closure)
_x = self.instance_param
_f = Lambda(_x, self.instance_expr)
_Q = Lambda(_x, self.condition)
if number_set == ZeroSet:
thm = summation_zero_closure
elif number_set == Natural:
thm = summation_nat_closure
elif number_set == NaturalPos:
thm = summation_nat_pos_closure
elif number_set == Integer:
thm = summation_int_closure
elif number_set == Real:
thm = summation_real_closure
elif number_set == Complex:
thm = summation_complex_closure
else:
raise NotImplementedError(
"'Sum.deduce_in_number_set' not implemented for the %s set"
% str(number_set))
impl = thm.instantiate({ x: _x, f: _f, Q: _Q})
antecedent = impl.antecedent
if not antecedent.proven():
# Conclude the antecedent via generalization.
antecedent.conclude_via_generalization()
return impl.derive_consequent()
def readily_provable_number_set(self):
'''
Return the most restrictive number set we can readily
prove contains the evaluation of this number operation.
'''
with defaults.temporary() as tmp_defaults:
tmp_defaults.assumptions = defaults.assumptions + tuple(
self.conditions)
summand_ns = readily_provable_number_set(self.summand)
if summand_ns is None:
return None
if summand_ns == ZeroSet:
return ZeroSet
if summand_ns in (Natural, NaturalPos, Integer, Real, Complex):
# We have proven closure for these.
# ToDo: implement more closure.
return summand_ns
if Integer.readily_includes(summand_ns): return Integer
if Rational.readily_includes(summand_ns): return Rational
if Real.readily_includes(summand_ns): return Real
return Complex
def _formatted(self, format_type, **kwargs):
# MUST BE UPDATED TO DEAL WITH 'joining' NESTED LEVELS
fence = kwargs['fence'] if 'fence' in kwargs else False
explicit_conds = self.explicit_conditions()
if isinstance(self.domain, Interval) and len(explicit_conds)==0:
formatted_operator = self.operator.formatted(format_type)
formatted_index = self.index.formatted(format_type)
formatted_lower = self.domain.lower_bound.formatted(format_type)
formatted_upper = self.domain.upper_bound.formatted(format_type)
formatted_summand = self.summand.formatted(format_type, fence=True)
formatted_inner = "%s_{%s = %s}^{%s} %s"%(
formatted_operator, formatted_index,
formatted_lower, formatted_upper, formatted_summand)
return maybe_fenced(format_type, formatted_inner, fence=fence)
else:
return OperationOverInstances._formatted(self, format_type,
fence=fence)
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
'''
Returns a proven simplification equation for this Sum
expression assuming the operands have been simplified.
For the trivial case of summing over only one item (currently
implemented just for a Interval where the endpoints are equal),
derive and return this summation expression equated with the
simplified form of the single term.
Assumptions may be necessary to deduce necessary conditions
for the simplification.
NEEDS UPDATING
'''
from proveit.logic import TRUE, Equals
from proveit.numbers import Mult
from . import sum_single, trivial_sum
summand = self.summand
if (isinstance(self.domain,Interval) and
self.domain.lower_bound == self.domain.upper_bound):
if hasattr(self, 'index'):
return sum_single.instantiate(
{Function(f, self.index): summand,
a: self.domain.lower_bound})
if (isinstance(self.domain,Interval) and
self.instance_param not in free_vars(summand)
and self.non_domain_condition()==TRUE):
# Trivial sum: summand independent of parameter.
_a = self.domain.lower_bound
_b = self.domain.upper_bound
_x = summand
return trivial_sum.instantiate(
{a:_a, b:_b, x:_x})
if Sum._simplification_directives_.pull_out_index_indep_factors:
if isinstance(summand, Mult):
index_indep_factors = []
for factor in summand.factors:
if free_vars(factor).isdisjoint(self.indices):
index_indep_factors.append(factor)
if len(index_indep_factors) > 0:
return self.factorization(
index_indep_factors, pull='left',
group_factors=False)
return Equals(self, self).conclude_via_reflexivity()
#raise SimplificationError(
# "Sum simplification only implemented for a summation over an "
# "integer Interval of one instance variable where the upper "
# "and lower bounds are the same.")
@equality_prover('geom_sum_reduced', 'geom_sum_reduce')
def geom_sum_reduction(self, **defaults_config):
r'''
If this summation is in the form of a geometric sum
(finite or infinite), equate it to an analytical form.
Examples:
∑_{n=0}^{∞} x^n = 1 / (1 - x)
∑_{n=j}^{k} x^n = (x^{k + 1} - x^j) / (x - 1)
'''
from . import inf_geom_sum, gen_finite_geom_sum
from proveit.numbers import zero, infinity
try:
# self.r = extract_exp_base(self.summand)
_x_sub = self.summand.base
except BaseException:
raise ValueError("Summand not an exponential!")
if not isinstance(self.domain, Interval):
raise ValueError("Not explicitly summing over Interval!")
else:
if (self.domain.lower_bound == zero and
self.domain.upper_bound == infinity):
# We're in the infinite geom sum domain!
_m = self.indices[0]
return inf_geom_sum.instantiate({x: _x_sub, m: _m})
else:
# We're in the finite geom sum domain!
_x, _j, _k = gen_finite_geom_sum.all_instance_params()
# _i = gen_finite_geom_sum.instance_expr.instance_expr.lhs.indices
_i = gen_finite_geom_sum.instance_expr.instance_expr.lhs.index
# _i_sub = self.indices[0]
_i_sub = self.index
_j_sub = self.domain.lower_bound
_k_sub = self.domain.upper_bound
return gen_finite_geom_sum.instantiate(
{x: _x_sub, _i: _i_sub, j: _j_sub, _k: _k_sub})
# else:
# print "Not a geometric sum!"
@equality_prover('shifted', 'shift')
def shifting(self, shift_amount, **defaults_config):
'''
Shift the summation indices by the shift_amount, and shift
the summand by a corresponding compensating amount, deducing
and returning the equivalence of this summation with the
index-shifted version.
This shift() method is implemented only for a Sum with a single
index and only when the domain is an integer Interval.
Eventually this should also be implemented for domains of
Natural, NaturalPos, etc.
Example: Let S = Sum(i, i+2, Interval(0, 10)). Then S.shift(one)
will return |- S = Sum(i, i+1, Interval(1, 11)).
'''
if not hasattr(self, 'index'):
raise NotImplementedError(
"Sum.shifting() only implemented for summations with a single "
"index over an Interval. The sum {} has indices {}."
.format(self, self.indices))
# The following constraint can eventually be modified to deal
# with a domain like all Natural … but for now limited to
# integer Interval domain.
if not isinstance(self.domain, Interval):
raise NotImplementedError(
"Sum.shifting() only implemented for summations with a single "
"index over an Interval. The sum {} has domain {}."
.format(self, self.domain))
from . import index_shift
_x = self.index
_a = self.domain.lower_bound
_b = self.domain.upper_bound
_c = shift_amount
f_op, f_op_sub = Function(f, self.index), self.summand
"""
# SHOULD BE HANDLED VIA AUTO-SIMPLIFICATION NOW.
# Create some (possible) reduction formulas for the shifted
# components, which will then be passed through to the
# instantiation as "reductions" for simpifying the final form
# of the indices and summand. Notice that when attempting to
# simplify the summand, we need to send along the assumption
# about the index domain. If the (supposed) reduction is
# trivial (like |– x = x), the eventual instantiation process
# will ignore/eliminate it.
replacements = list(defaults.replacements)
if (simplify_idx):
lower_bound_shifted = (
Add(_a, _c).simplification(
shallow=True, assumptions=assumptions))
replacements.append(lower_bound_shifted)
upper_bound_shifted = (
Add(_b, _c).simplification(
shallow=True, assumptions=assumptions))
replacements.append(upper_bound_shifted)
if (simplify_summand):
summand_shifted = f_op_sub.basic_replaced({_i:subtract(_i, _c)})
summand_shifted = (
summand_shifted.simplification(shallow=True,
assumptions=[*assumptions, InSet(_i, Interval(_a, _b))]))
replacements.append(summand_shifted)
"""
return index_shift.instantiate(
{f_op: f_op_sub, x: _x, a: _a, b: _b, c: _c})
@equality_prover('negated_index', 'negate_index')
def index_negation(self, **defaults_config):
from . import index_negate
_x = self.index
_a = self.domain.lower_bound
_b = self.domain.upper_bound
# We could make this more general eventually
# (to handle multiple indices or domains other than Intervals),
# but we only have a simple version implemented for now.
if not hasattr(self, 'index'):
raise NotImplementedError(
"Sum.index_negation() only implemented for summations with a single "
"index over an Interval. The sum {} has indices {}."
.format(self, self.indices))
if not isinstance(self.domain, Interval):
raise NotImplementedError(
"Sum.shifting() only implemented for summations with a single "
"index over an Interval. The sum {} has domain {}."
.format(self, self.domain))
f_op, f_op_sub = Function(f, self.index), self.summand
return index_negate.instantiate(
{f_op: f_op_sub, x: _x, a: _a, b: _b})
@prover
def joining(self, second_summation, **defaults_config):
'''
Join the "second summation" with "this" (self) summation,
deducing and returning the equivalence of the sum of the self
and second_summation with the joined summation.
Both summations must be over integer Intervals.
The relation between the first summation upper bound, UB1,
and the second summation lower bound, LB2, must be *explicitly*
either UB1 = LB2-1 or LB2=UB1+1 *or* easily-derivable
mathematical equivalents of those equalities.
Example usage: let S1 = Sum(i, i^2, Interval(1,10)) and
S2 = Sum(i, i^2, Interval(1,10)). Then S1.join(S2) returns
|- S1 + S2 = Sum(i, i^2, Interval(1,20))
'''
if (not isinstance(self.domain,Interval) or
not isinstance(second_summation.domain,Interval)):
raise NotImplementedError(
"Sum.join() is only implemented for summations with a "
"single index over an integer Interval. The sum {0} has "
"indices {1} and domain {2}; the sum {3} has indices "
"{4} and domain {5}.".
format(self, self.indices, self.domain, second_summation,
second_summation.indices, second_summation.domain))
if self.summand != second_summation.summand:
raise ValueError(
"Sum joining using Sum.join() is only allowed when the "
"summands are identical. The sum {0} has summand {1} "
"while the sum {2} has summand {3}. If the summands are "
"equal but do not appear identical, you will have to "
"establish an appropriate substituion before calling the "
"Sum.join() method.".
format(self, self.summand, second_summation,
second_summation.summand))
from . import sum_split_after, sum_split_before
from proveit import a
_i = self.index
_a1 = self.domain.lower_bound
_b1 = self.domain.upper_bound
_a2 = second_summation.domain.lower_bound
_b2 = second_summation.domain.upper_bound
f_op, f_op_sub = Function(f, self.index), self.summand
# Create low-effort, simplified versions of transition index
# values, if possible
_b1_plus_1_simplified = Add(_b1, one).shallow_simplified()
_a2_minus_1_simplified = subtract(_a2, one).shallow_simplified()
# This breaks into four cases (despite the temptation to
# combine some of the cases):
if (_b1 == subtract(_a2, one)):
# UB1 == LB2 - 1 (literally)
sum_split = sum_split_before
split_index = _a2
elif (_a2 == Add(_b1, one)):
# LB2 == UB1 + 1 (literally)
sum_split = sum_split_after
split_index = _b1
elif (_b1 == _a2_minus_1_simplified):
# UB1 == LB2 - 1 (after simplification)
sum_split = sum_split_before
split_index = _a2
elif (_a2 == _b1_plus_1_simplified):
# LB2 == UB1 + 1 (after simplification)
sum_split = sum_split_after
split_index = _b1
else:
raise UnsatisfiedPrerequisites(
"Sum joining using Sum.join() only implemented for when "
"there is an explicit (or easily verified) increment "
"of one unit from the first summation's upper bound "
"to the second summation's lower bound (or decrement "
"of one unit from second summation's lower bound to "
"first summation's upper bound). We have first "
"summation upper bound of {0} with the second summation "
"lower bound of {1}. If these appear to have the "
"necessary relationship, you might need to prove this "
"before calling the Sum.join() method.".
format(_b1, _a2))
# Preserve the original summations that will be on the
# left side of the equation.
preserved_exprs = set(defaults.preserved_exprs)
preserved_exprs.add(self)
preserved_exprs.add(second_summation)
return sum_split.instantiate(
{f_op: f_op_sub, a: _a1, b: split_index, c: _b2, x: _i},
preserved_exprs=preserved_exprs).derive_reversed()
@equality_prover('partitioned', 'split')
def partition(self, split_index, side='after', **defaults_config):
r'''
Split summation over one integral Interval {a ... c} into two
summations. If side == 'after', it splits into a summation over
{a ... split_index} plus a summation over {split_index+1 ... c}.
If side == 'before', it splits into a summation over
{a ... split_index-1} plus a summation over {split_index ... c},
deducing and returning the equivalence of this summation with
the split version. When the simplify_idx is True, a shallow
simplification is applied to the new indices (for example,
a new index of i = 4 + 1 may be expressed as i = 5).
Eventually plan to accept and act on user-supplied reductions
as well, but not implemented at this time.
This split() method is implemented only for a Sum with a single
index and only when the domain is an integer Interval.
Eventually this should also be implemented for domains of
Natural, NaturalPos, etc.
As special cases, split_index==a with side == 'after' splits
off the first single term. Also, split_index==c with
side == 'before' splits off the last single term.
Example usage: Let S = Sum(i, i+2, Interval(0, 10)). Then
S.split(four, side='after') will return
|- S = Sum(i, i+2, Interval(0, 4)) +
Sum(i, i+2, Interval(5, 10))
'''
# The following constraint can eventually be modified to allow
# a domain like Natural or NaturalPos, but for now limited
# to integer Interval domain.
if (not isinstance(self.domain, Interval) or
not hasattr(self, 'index')):
raise NotImplementedError(
"Sum.partition() only implemented for summations with a single "
"index over an integer Interval. The sum {} has indices {} "
"and domain {}."
.format(self, self.indices, self.domain))
# Special cases: splitting off last or first item
if side == 'before' and self.domain.upper_bound == split_index:
return self.partition_last()
if side == 'after' and self.domain.lower_bound == split_index:
return self.partition_first()
_i = self.index
_a = self.domain.lower_bound
_b = split_index
_c = self.domain.upper_bound
f_op, f_op_sub = Function(f, self.index), self.summand
"""
# SHOULD BE HANDLED VIA AUTO-SIMPLIFICATION NOW.
# Create a (possible) reduction formula for the split
# components' index expression, which will then be passed
# through to the instantiation as a "reduction" for simpifying
# the final form of the indices. If the (supposed) reduction is
# trivial (like |– x = x), the eventual instantiation process
# will ignore/eliminate it.
if (simplify_idx):
# 2 Cases to consider: side = 'after' vs. side = 'before'
if side == 'after':
# simplify lower index expr for 2nd sum of split
new_idx = Add(_b, one).simplification(
shallow=True, assumptions=assumptions)
else:
# simplify upper index expr for 1st sum of split
new_idx = subtract(_b, one).simplification(
shallow=True, assumptions=assumptions)
user_reductions = [*user_reductions, new_idx]
"""
from . import sum_split_after, sum_split_before
sum_split = sum_split_after if side == 'after' else sum_split_before
return sum_split.instantiate(
{f_op: f_op_sub, a: _a, b: _b, c: _c, x: _i})
@equality_prover('last_partitioned', 'split_last')
def partition_last(self, **defaults_config):
'''
Split a summation over an integral Interval {a ... c} into a
sum of: a new summation over the integral Interval {a ... (c-1)}
and the final term evaluated at the upper bound, deducing and
returning the equivalence of this summation with
the new split version. When the simplify_idx is True, a shallow
simplification is applied to the new indices (for example,
a new index of i = 4 + 1 may be expressed as i = 5). When the
simplify_summand = True, a shallow simplification is applied to
the upper term that has been peeled off by itself.
Eventually plan to accept and act on user-supplied reductions
as well, but not implemented at this time.
This split_off_last() method is implemented only for a Sum
with a single index and only when the domain is an integer
Interval. Eventually this should also be implemented for
domains of Natural, NaturalPos, etc. split_off_last() is called
from Sum.split() for special cases.
Example usage: Let S = Sum(i, i+2, Interval(0, 10)). Then
S.split_off_last() will return
|- S = Sum(i, i+2, Interval(0, 9)) + 12
'''
if isinstance(self.domain, Interval) and hasattr(self, 'index'):
from . import sum_split_last
_i = self.index
_a = self.domain.lower_bound
_b = self.domain.upper_bound
f_op, f_op_sub = Function(f, self.index), self.summand
"""
# SHOULD BE HANDLED VIA AUTO-SIMPLIFICATION NOW.
# Create (possible) reduction formulas for the upper
# index expression of the resulting sum, and for the
# resulting final term extracted from the sum, which will
# then be passed through to the instantiation as reductions
# for simpifying the final form of the indices and split-off
# term. If any (supposed) reduction is trivial
# (like |– x = x), the eventual instantiation process will
# ignore/eliminate it.
if (simplify_idx):
# Just 1 case to address:
# simplify upper index of resulting remaining sum
new_idx = subtract(_b, one).simplification(
shallow=True, assumptions=assumptions)
user_reductions = [*user_reductions, new_idx]
if simplify_summand:
# Simplify the summand for the last item
new_summand = f_op_sub.basic_replaced({_i: _b})
new_summand = new_summand.simplification(shallow=True,
assumptions=assumptions)
user_reductions = [*user_reductions, new_summand]
"""
return sum_split_last.instantiate(
{f_op: f_op_sub, a: _a, b: _b, x: _i})
raise UnsatisfiedPrerequisites(
"Sum.partition_last() only implemented for summations with a "
"single index over an integer Interval. The sum {} has "
"index or indices {} and domain {}."
.format(self, self.indices, self.domain))
@equality_prover('first_partitioned', 'split_first')
def partition_first(self, **defaults_config):
'''
Split a summation over an integral Interval {a ... c} into a
sum of: the first term in the sum and a new summation over the
integral Interval {a+1 ... c}, deducing and
returning the equivalence of this summation with
the new split version. When the simplify_idx is True, a shallow
simplification is applied to the new indices (for example,
a new index of i = 4 + 1 may be expressed as i = 5). When the
simplify_summand = True, a shallow simplification is applied to
the lower term that has been peeled off by itself.
Eventually plan to accept and act on user-supplied reductions
as well, but not implemented at this time.
This split_off_last() method is implemented only for a Sum
with a single index and only when the domain is an integer
Interval. Eventually this should also be implemented for
domains of Natural, NaturalPos, etc. split_off_last() is called
from Sum.split() for special cases.
Example usage: Let S = Sum(i, i+2, Interval(1, 10)). Then
S.split_off_first() will return
|- S = 3 + Sum(i, i+2, Interval(2, 10))
'''
if isinstance(self.domain, Interval) and hasattr(self, 'index'):
from . import sum_split_first
_i = self.index
_a = self.domain.lower_bound
_b = self.domain.upper_bound
f_op, f_op_sub = Function(f, self.index), self.summand
"""
# SHOULD BE HANDLED VIA AUTO-SIMPLIFICATION NOW.
# Create (possible) reduction formulas for the lower
# index expression of the resulting sum, and for the
# resulting first term extracted from the sum, which will
# then be passed through to the instantiation as reductions
# for simpifying the final form of the indices and split-off
# term. If any (supposed) reduction is trivial
# (like |– x = x), the eventual instantiation process will
# ignore/eliminate it.
if simplify_idx:
# Just 1 case to address:
# simplify lower index of resulting remaining sum
new_idx = Add(_a, one).simplification(
shallow=True, assumptions=assumptions)
user_reductions = [*user_reductions, new_idx]
if simplify_summand:
# Simplify the summand for the first item
new_summand = f_op_sub.basic_replaced({_i: _a})
new_summand = new_summand.simplification(shallow=True,
assumptions=assumptions)
user_reductions = [*user_reductions, new_summand]
"""
return sum_split_first.instantiate(
{f_op: f_op_sub, a: _a, b: _b, x: _i})
raise NotImplementedError(
"Sum.split_off_first() only implemented for summations with a "
"single index over an integer Interval. The sum {} has "
"index or indices {} and domain {}."
.format(self, self.indices, self.domain))
[docs] @auto_equality_prover('factorized', 'factor')
def factorization(self, the_factors, pull="left", group_factors=True,
group_remainder=None, **defaults_config):
'''
Return the proven factorization (equality with the factored
form) from pulling the factor(s) from this summation to the
"left" or "right".
If group_factors is True, the factors will be grouped together
as a sub-product. group_remainder is not relevant kept for
compatibility with other factor methods.
'''
from proveit import ExprTuple, var_range, IndexedVar
from proveit.numbers.multiplication import distribute_through_summation
from proveit.numbers import Mult, one
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)
if not free_vars(the_factors).isdisjoint(self.instance_params):
raise ValueError(
'Cannot factor anything involving summation indices '
'out of a summation')
expr = self
# for convenience updating our equation
eq = TransRelUpdater(expr)
# We may need to factor the summand within the summation
summand_assumptions = defaults.assumptions + self.conditions.entries
summand_factorization = self.summand.factorization(
the_factors,
pull,
group_factors=group_factors,
group_remainder=True,
assumptions=summand_assumptions)
if summand_factorization.lhs != summand_factorization.rhs:
gen_summand_factorization = summand_factorization.generalize(
self.instance_params, conditions=self.conditions)
expr = eq.update(expr.instance_substitution(
gen_summand_factorization))
if not group_factors and isinstance(the_factors, Mult):
factors = the_factors.factors
else:
factors = ExprTuple(the_factors)
if pull == 'left':
_a = factors
_c = ExprTuple()
summand_remainder = expr.summand.factors[-1]
elif pull == 'right':
_a = ExprTuple()
_c = factors
summand_remainder = expr.summand.factors[0]
else:
raise ValueError("'pull' must be 'left' or 'right', not %s"
%pull)
_b = self.instance_params
_i = _a.num_elements()
_j = _b.num_elements()
_k = _c.num_elements()
_f = Lambda(expr.instance_params, summand_remainder)
_Q = Lambda(expr.instance_params, expr.condition)
_impl = distribute_through_summation.instantiate(
{i: _i, j: _j, k: _k, f:_f, Q:_Q, b:_b})
quantified_eq = _impl.derive_consequent()
eq.update(quantified_eq.instantiate({a: _a, c: _c}))
return eq.relation
[docs] @relation_prover
def deduce_bound(self, summand_relation, **defaults_config):
r'''
Given a universally quantified ordering relation over all
summand instances, return a bounding relation for the
summation. For example, using the summand relation
\forall_{k in {m...n}} (a(k) <= b(k)),
we can prove
\sum_{l=m}^{n} a(l) <= \sum_{l=m}^{n} b(l)
or using the summand relation
\forall_{k in {m...n}} (a(k) < b(k)),
and assuming m <= n, we can prove
\sum_{l=m}^{n} a(l) < \sum_{l=m}^{n} b(l)
'''
from . import (weak_summation_from_summands_bound,
strong_summation_from_summands_bound)
if not (self.instance_params.is_single()):
raise NotImplementedError(
"sum.bound only currently implemented for summations "
"over a single parameter")
if isinstance(summand_relation, Judgment):
summand_relation = summand_relation.expr
if not (isinstance(summand_relation, Forall) and
summand_relation.instance_params.is_single() and
(isinstance(summand_relation.instance_expr, Less) or
isinstance(summand_relation.instance_expr, LessEq))):
raise ValueError("Expecting summand_relation to be a number "
"ordering relation (< or <=) universally "
"quantified over a single parameter, not %s"
%summand_relation)
summand_lambda = Lambda(self.instance_param, self.summand)
lesser_lambda = Lambda(summand_relation.instance_param,
summand_relation.instance_expr.normal_lhs)
greater_lambda = Lambda(summand_relation.instance_param,
summand_relation.instance_expr.normal_rhs)
if summand_lambda not in (lesser_lambda, greater_lambda):
raise ValueError("Expecting summand_relation to be a universally "
"quantified number relation (< or <=) "
"involving the summand {0} not {1}.".
format(self.summand, summand_relation))
_a = lesser_lambda
_b = greater_lambda
_S = self.domain
if isinstance(summand_relation.instance_expr, LessEq):
# Use weak form
sum_rel_impl = weak_summation_from_summands_bound.instantiate(
{a:_a, b:_b, S:_S}, preserve_all=True)
else:
# Use strong form
sum_rel_impl = strong_summation_from_summands_bound.instantiate(
{a:_a, b:_b, S:_S}, preserve_all=True)
sum_relation = sum_rel_impl.derive_consequent()
if summand_lambda == greater_lambda:
return sum_relation.with_direction_reversed()
return sum_relation
@relation_prover
def upper_bound_as_integral(self, **defaults_config):
'''
If the summand is a monotonically decreasing function over the
continuous [a-1, b] interval, when can bound the sum from a to b
by the integra from a-1 to b.
'''
from proveit.numbers import IntervalCC, deduce_as_mon_dec_func
from . import integral_upper_bound_of_sum
# We could make this more general eventually
# (at least to handle multiple indices),
# but we only have a simple version implemented for now.
if not hasattr(self, 'index'):
raise NotImplementedError(
"Sum.upper_bound_as_integral() only implemented for summations with a single "
"index over an Interval. The sum {} has indices {}."
.format(self, self.indices))
if not isinstance(self.domain, Interval):
raise NotImplementedError(
"Sum.upper_bound_as_integral() only implemented for summations with a single "
"index over an Interval. The sum {} has domain {}."
.format(self, self.domain))
_a = self.domain.lower_bound
_b = self.domain.upper_bound
_f = Lambda(self.index, self.summand)
membership = deduce_as_mon_dec_func(_f, domain=IntervalCC(subtract(_a, one), _b))
_S = membership.domain.domain
return integral_upper_bound_of_sum.instantiate({a:_a, b:_b, f:_f, S:_S})