from proveit import (as_expression, defaults, Literal,
UnsatisfiedPrerequisites,
ProofFailure, TransitiveRelation,
TransitivityException, USE_DEFAULTS,
prover, relation_prover)
from proveit import a, b, k
from proveit.logic import Equals, InSet, NotEquals
from proveit.numbers import zero, Complex, Integer, NaturalPos
class DividesRelation(TransitiveRelation):
def __init__(self, operator, lhs, rhs, *, styles):
TransitiveRelation.__init__(self, operator, lhs, rhs,
styles=styles)
self.divisor = self.lhs
self.dividend = self.rhs
def side_effects(self, judgment):
'''
In addition to the TransitiveRelation side-effects, also
attempt (where applicable) eliminate_dividen_exponent,
eliminate_common_exponent, and eliminate_common_factor.
'''
from proveit.numbers import two, Exp, Mult
for side_effect in TransitiveRelation.side_effects(self, judgment):
yield side_effect
# For each of the following, use the default assumptions to
# verify some conditions before yielding the side effect method
# (i.e. check using .readily_provable())
# for 2|(b^n), derive 2|b.
# (can be generalized to any prime number).
if self.lhs==two and isinstance(self.rhs, Exp):
if (InSet(self.rhs.base, Integer).readily_provable() and
InSet(self.rhs.exponent, Integer).readily_provable()):
yield self.eliminate_dividend_exponent
# for (a^n)|(b^n)
if (isinstance(self.rhs, Exp) and
isinstance(self.lhs, Exp) and
self.lhs.exponent==self.rhs.exponent):
if (InSet(self.lhs.base, Integer).readily_provable() and
InSet(self.rhs.base, Integer).readily_provable() and
InSet(self.lhs.exponent, NaturalPos).readily_provable()):
yield self.eliminate_common_exponent
# for (ka)|(kb)
if (isinstance(self.lhs, Mult) and isinstance(self.rhs, Mult)):
operands_intersection = (set(self.lhs.operands).
intersection(set(self.lhs.operands)))
if(len(operands_intersection) > 0):
yield self.eliminate_common_factors
@staticmethod
def WeakRelationClass():
# Divides is weaker than DividesProper (in development)
# analogous to <= being weaker than <
return Divides # Divides is weaker than DividesProper
@staticmethod
def StrongRelationClass():
# DividesProper (in development) is stronger than Divides.
# DividesProper(x, y) is like Divides(x, y) but requires x != y
return DividesProper # DividesProper is stronger than Divides
[docs]class Divides(DividesRelation):
'''
Divides(x, y) represents the claim that x divides y (i.e. x|y)
(equivalently, x is a factor of y, y is a multiple of x, or
y/x is an integer). The axiomatic definition in Prove-It uses
x|y = (y/x in Z), with no prerequisites on x and y. Extending
DividesRelation allows us to have not only this weak relation
class but also a strong relation class, DividesProper, the pair
combined then allowing the calling of
Divides.conclude_via_transitivity()
utilizing the TransitiveRelation.conclude_via_transitivity() method.
'''
_operator_ = Literal(
string_format='|', latex_format=r'\rvert', theory=__file__
)
# map left-hand-sides to "Divides" Judgments
# (populated in TransitivityRelation.side_effects)
known_left_sides = dict()
# map right-hand-sides to "Divides" Judgments
# (populated in TransitivityRelation.side_effects)
known_right_sides = dict()
def __init__(self, a, b, *, styles=None):
DividesRelation.__init__(self, Divides._operator_, a, b,
styles=styles)
[docs] @prover
def conclude(self, **defaults_config):
'''
Attempt to conclude the divisibility claim in various ways:
(1) simple reflexivity (x|x);
(2) simple x|0 for x ≠ 0;
(3) simple x|xy or x|yx scenario
(4) x^n | y^n if x|y is known or assumed
(5) x|y if (x^n)|(y^n) is known or assumed
(6) via transitivity.
'''
from proveit.numbers import Exp
#-- -------------------------------------------------------- --#
#-- Case (1): x|x with x != 0 known or assumed --#
#-- -------------------------------------------------------- --#
from proveit.logic import InSet
from proveit.numbers import (ComplexNonZero,
readily_provable_number_set)
err_str = "In Divides.conclude() we tried:\n"
lhs_ns = readily_provable_number_set(self.lhs, default=Complex)
if self.lhs == self.rhs:
if ComplexNonZero.readily_includes(lhs_ns):
# Trivial x|x with complex x ≠ 0
return self.conclude_via_reflexivity()
else:
err_str = err_str + (
"Case: lhs = rhs. "
"Although lhs = rhs = {0}, either {0} is not known to "
"be non-zero or {0} is not known to be in the complex "
"numbers (or both). Try proving one or both of those "
"claims first.\n".format(self.lhs))
# raise ProofFailure(self, assumptions, err_str)
#-- -------------------------------------------------------- --#
#-- Case (2): x|0 with x != 0 known or assumed --#
#-- -------------------------------------------------------- --#
if self.rhs == zero:
if ComplexNonZero.readily_includes(lhs_ns):
# We have 0/x with complex x ≠ 0
return self.conclude_via_zero_factor()
else:
err_str = err_str + (
"Case: rhs = 0. "
"Although rhs = 0, either the lhs {0} is not known to "
"be non-zero or {0} is not known to be in the complex "
"numbers (or both). Try proving one or both of those "
"claims first.\n".format(self.lhs))
#-- -------------------------------------------------------- --#
#-- Case (3): very simple version of x|xy or x|yx --#
#-- -------------------------------------------------------- --#
# return self.conclude_via_factor(assumptions)
try:
return self.conclude_via_factor()
except Exception as e:
err_str = err_str + (
"Case: x|xy. This possible case returned the following "
"error message: {0} \n".format(e))
pass
#-- -------------------------------------------------------- --#
#-- Case (4): x^n|y^n if x|y --#
#-- -------------------------------------------------------- --#
if (isinstance(self.lhs, Exp) and isinstance(self.rhs, Exp) and
Equals(self.lhs.exponent, self.rhs.exponent) and
Divides(self.lhs.base, self.rhs.base).proven()):
if (InSet(self.lhs.base, Integer).readily_provable() and
InSet(self.rhs.base, Integer).readily_provable() and
InSet(self.lhs.exponent, NaturalPos).readily_provable()):
return (Divides(self.lhs.base, self.rhs.base).
introduce_common_exponent(self.lhs.exponent))
else:
err_str = err_str + (
"Case: (x^n) | (y^n). One or more of the conditions "
"(such as domain requirements or x|y) were not "
"already proven. Check the conditions for the "
"common_exponent_introduction theorem in the "
"number/divisibility package.\n")
else:
err_str = err_str + (
"Case: (x^n) | (y^n). Does not appear applicable.\n")
"""
# This case should be handled on the "side-effect" end.
#-- -------------------------------------------------------- --#
#-- Case (5): x|y if x^n|y^n (for some small pos nat n) --#
#-- -------------------------------------------------------- --#
possible_exps = range(2,10)
for e in possible_exps:
# print("exp = {}".format(e))
if (Divides(Exp(self.lhs, num(e)), Exp(self.rhs, num(e))).
proven(assumptions)):
# print(" Divides found for exp = {}".format(test_exp))
return (Divides(Exp(self.lhs, test_exp),
Exp(self.rhs, test_exp)).
eliminate_common_exponent(assumptions=assumptions))
err_str = err_str + (
"Case: x|y where we already have (x^n)|(y^n). "
"Does not appear applicable.\n")
"""
#-- -------------------------------------------------------- --#
#-- Case (6): x|z with x|y and y|z known or assumed --#
#-- -------------------------------------------------------- --#
# Seek out the appropriate x|y and y|z and use transitivity
# to get x|z, utilizing the conclude_via_transitivity() method
# available for instances of TransitiveRelation
try:
return self.conclude_via_transitivity()
except Exception as e:
err_str = err_str + (
"Case: transitivity search. In attempting to use "
"conclude_via_transitivity(), obtained the following "
"error message: {0}.".format(e))
pass
raise ProofFailure(self, defaults.assumptions, err_str)
[docs] @prover
def conclude_via_reflexivity(self, **defaults_config):
'''
Prove and return self of the form x|x with x ≠ 0.
'''
from . import divides_reflexivity
_x = divides_reflexivity.instance_var
assert self.lhs == self.rhs
return divides_reflexivity.instantiate({_x: self.lhs})
[docs] @prover
def conclude_via_zero_factor(self, **defaults_config):
'''
Prove and return self of the form x|0 for x ≠ 0
'''
from . import non_zero_divides_zero
_x = non_zero_divides_zero.instance_var
return non_zero_divides_zero.instantiate({_x: self.lhs})
[docs] @prover
def conclude_via_factor(self, **defaults_config):
'''
Prove and return self of the form x|xy for x ≠ 0 and y in Ints
'''
from proveit.numbers import Mult
if isinstance(self.rhs, Mult):
if self.rhs.operands.is_double():
# should check to make sure none of the operands
# are actually ExprRanges (later!)
if self.lhs == self.rhs.operands[0]:
# apply left version
from . import left_factor_divisibility
_x, _y = left_factor_divisibility.instance_params
return left_factor_divisibility.instantiate(
{_x: self.lhs, _y: self.rhs.operands[1]})
elif self.lhs == self.rhs.operands[1]:
# apply right version
from . import right_factor_divisibility
_x, _y = right_factor_divisibility.instance_params
return right_factor_divisibility.instantiate(
{_x: self.lhs, _y: self.rhs.operands[0]})
else:
raise ValueError(
"conclude_via_factor only applies for an explicit "
"factor appearing on both sides of the Divides. "
"{0} does not appear in {1} as an explicit factor.".
format(self.lhs, self.rhs))
else:
raise NotImplementedError(
"conclude_via_factor implemented only for binary "
"multiplication.")
else:
raise ValueError(
"conclude_via_factor only applies for an explicit "
"Mult expression on the rhs of the Divides, "
"but received {0} on the right side.".
format(self.rhs))
[docs] @prover
def eliminate_dividend_exponent(self, **defaults_config):
'''
From k|a^n (self), derive and return k|a if k is prime
and a and n are integers. Currently, this is only implement
for k=2. This method is called from the
DividesRelation.side_effects() method.
'''
from proveit.numbers import two, Exp
from . import even__if__power_is_even
if not isinstance(self.rhs, Exp):
raise ValueError(
"'eliminate_dividend_exponent' is only applicable "
"when the dividend is raised to an integer power.")
if self.lhs != two:
raise NotImplementedError(
"'eliminate_dividend_exponent' currently only implemented "
"for a divisor of 2, but should eventually be "
"generalized for any prime divisor.")
a_, n_ = even__if__power_is_even.instance_params
return even__if__power_is_even.instantiate(
{a_: self.rhs.base, n_: self.rhs.exponent})
[docs] @prover
def eliminate_common_exponent(self, **defaults_config):
'''
From self of the form (k^n)|(a^n), derive and return k|a.
k, a, must be integers, with n a positive integer. This method
is called from the DividesRelation side_effects() method.
'''
from proveit.numbers import Exp
if (isinstance(self.lhs, Exp) and
isinstance(self.rhs, Exp) and
self.lhs.exponent == self.rhs.exponent):
k = self.lhs.base
a = self.rhs.base
n = self.lhs.exponent
if (InSet(k, Integer).readily_provable() and
InSet(a, Integer).readily_provable() and
InSet(n, NaturalPos).readily_provable()):
from . import common_exponent_elimination
_k, _a, _n = common_exponent_elimination.instance_params
return common_exponent_elimination.instantiate(
{_k: k, _a: a, _n: n})
else:
err_msg = ("In using Divides.eliminate_common_exponent(), "
"the exponent ({0}) must already be known to be "
"a positive natural and each base ({1}, {2}) "
"must already been know to be an integer.".
format(n, k, a))
else:
err_msg = ("In using Divides.eliminate_common_exponent(), "
"the lhs {0} and rhs {1} must both be exponential.".
format(self.lhs, self.rhs))
raise ValueError(err_msg)
[docs] @prover
def introduce_common_exponent(self, exponent, **defaults_config):
'''
From self of the form (k)|(a), with integers k and a, derive
and return k^n|a^n where n = exponent is a positive natural.
'''
from . import common_exponent_introduction
_k, _a, _n = common_exponent_introduction.instance_params
return common_exponent_introduction.instantiate(
{_k: self.lhs, _a: self.rhs, _n: exponent})
@prover
def eliminate_common_factors(self, **defaults_config):
'''
Eliminate all factors in common between the divisor and the
dividend. For example, from (k a)|(k b), derive and return a|b.
k must be a non-zero complex number.
'''
from . import common_factor_elimination
from proveit.numbers import Mult, one, ComplexNonZero
if self.lhs == self.rhs:
# From x | x return 1 | 1. It's vacuous, but whatever.
return Divides(one, one).prove()
elif (isinstance(self.lhs, Mult) and
isinstance(self.rhs, Mult)):
# Handle the basic case in which the divisor and
# the dividend are each the product of two factors and
# the first of these is in common between them.
if (self.lhs.operands.is_double() and
self.rhs.operands.is_double()):
lhs1 = self.lhs.operands[0]
lhs2 = self.lhs.operands[1]
rhs1 = self.rhs.operands[0]
rhs2 = self.rhs.operands[1]
if lhs1 == rhs1 and InSet(lhs1,
ComplexNonZero).readily_provable():
return common_factor_elimination.instantiate(
{a: lhs2, b: rhs2, k: lhs1})
# Try to convert it to the basic case via factorization
# and try again.
rhs_factors = set(self.rhs.operands.entries)
common_factors = [factor for factor in self.lhs.factors
if factor in rhs_factors]
# Pull the common factors out to the front.
if len(common_factors) == 0:
return self.prove() # No common factors to eliminate.
lhs_factorization = self.lhs.factorization(
common_factors, pull='left',
group_factors=True, group_remainder=True,
preserve_all=True)
rhs_factorization = self.rhs.factorization(
common_factors, pull='left',
group_factors=True, group_remainder=True,
preserve_all=True)
# Prove this "divides" but the substitute factorized forms.
divides_proof = self.prove()
if lhs_factorization.lhs != lhs_factorization.rhs:
divides_proof = lhs_factorization.sub_right_side_into(
divides_proof)
if rhs_factorization.lhs != rhs_factorization.rhs:
divides_proof = rhs_factorization.sub_right_side_into(
divides_proof)
lhs1, lhs2 = lhs_factorization.rhs.operands
rhs1, rhs2 = rhs_factorization.rhs.operands
return common_factor_elimination.instantiate(
{a: lhs2, b: rhs2, k: lhs1})
elif isinstance(self.lhs, Mult) and self.rhs in self.lhs.factors:
# From (k z) | k return z | 1. Why not?
dividend = Mult(self.rhs, one)
divides = Divides(self.lhs, dividend)
divides_proof = divides.eliminate_common_factors()
return divides_proof.inner_expr().lhs.dividend.one_elimination(1)
elif isinstance(self.rhs, Mult) and self.lhs in self.rhs.factors:
# From (k z) | k return z | 1. Why not?
divisor = Mult(self.lhs, one)
divides = Divides(divisor, self.rhs)
divides_proof = divides.eliminate_common_factors()
return divides_proof.inner_expr().lhs.divisor.one_elimination(1)
# There are no common factors.
return self.prove()
[docs] @prover
def apply_transitivity(self, other, **defaults_config):
'''
From x|y (self) and y|z (other) derive and return x|z.
Will also check for y|z (self) and x|y (other) to return x|z.
'''
from . import divides_transitivity
_x, _y, _z = divides_transitivity.instance_params
other = as_expression(other)
if not isinstance(other, Divides):
raise ValueError(
"Unsupported transitivity operand: Divides.apply_transitivity() "
"method requires another Divides expression for transitivity "
"to be applied. Instead, received the following input: {0}.". format(other))
if self.rhs == other.lhs:
return divides_transitivity.instantiate(
{_x: self.lhs, _y: self.rhs, _z: other.rhs},
preserve_all=True)
if self.lhs == other.rhs:
return divides_transitivity.instantiate(
{_x: other.lhs, _y: other.rhs, _z: self.rhs},
preserve_all=True)
else:
raise TransitivityException(
self, defaults.assumptions,
'Transitivity cannot be applied unless the lhs of one of '
'Divides expressions is equal to the rhs of the other '
'Divides expression. Instead we have: {0} vs {1}'.
format(self, other))
def readily_in_bool(self):
'''
A Divides operation is always boolean (but could only be
true for numbers).
'''
return True
[docs] @relation_prover
def deduce_in_bool(self, **defaults_config):
'''
Deduce and return that this 'Divides' expression is in
the Boolean set.
'''
from . import divides_is_bool
_x, _y = divides_is_bool.instance_params
return divides_is_bool.instantiate(
{_x: self.operands[0], _y: self.operands[1]})
[docs]class DividesProper(DividesRelation):
'''
DividesProper(x, y) represents the claim that x divides y
(i.e. x|y) but x != y. x|y is equivalent to saying that x is a
factor of y, y is a multiple of x, or y/x is an integer).
This class is still under development, with the class stub located
here so that we have a 'strong relation' class version of Divides
that can be called from the DividesRelation class, which in turn
allows us to use the TransitiveRelation.concude_via_transitivity()
method.
'''
_operator_ = Literal(
string_format='|', latex_format=r'{\rvert_{P}}', theory=__file__
)
# map left-hand-sides to "Divides" Judgments
# (populated in TransitivityRelation.side_effects)
known_left_sides = dict()
# map right-hand-sides to "Divides" Judgments
# (populated in TransitivityRelation.side_effects)
known_right_sides = dict()
def __init__(self, a, b, *, styles=None):
DividesRelation.__init__(self, DividesProper._operator_, a, b,
styles=styles)