from proveit import (Literal, Operation, ExprRange, defaults,
UnsatisfiedPrerequisites,
prover, relation_prover, equality_prover)
from proveit import a, b, c, d, k, m, n, x
from proveit.logic import is_irreducible_value
from proveit.numbers.number_sets.number_set import NumberSet, NumberMembership
from proveit.numbers.numerals.numeral import NumeralSequence, Numeral
from proveit.numbers.numerals import zero, one, two, three, four, five, six, seven, eight, nine
DIGITS = [zero, one, two, three, four, five, six, seven, eight, nine]
[docs]class DecimalSequence(NumeralSequence):
# operator of the DecimalSequence operation.
_operator_ = Literal(string_format='Decimal', theory=__file__)
def __init__(self, *digits, styles=None):
NumeralSequence.__init__(self, DecimalSequence._operator_, *digits,
styles=styles)
for digit in self.digits:
if is_irreducible_value(digit) and digit not in DIGITS:
raise Exception(
'A DecimalSequence may only be composed of 0-9 digits')
def _prefix(self, format_type):
# No prefix for a DecimalSequence (unlike binary or hex
# which needs a prefix to indicate type of number it is).
return ""
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
"""
If the DecimalSequence contains an ExprRange representing a
repeated digit, expand it appropriately.
"""
from proveit import ExprRange
if self.digits.is_single():
return self.single_digit_reduction()
for digit in self.digits:
if isinstance(digit, ExprRange):
# if at least one digit is an ExprRange, we can try to
# reduce it to an ExprTuple
return self.digit_repetition_reduction()
[docs] def as_int(self):
if all(digit in DIGITS for digit in self.digits):
return eval(self.formatted('string'))
raise ValueError("Cannot convert %s to an integer; its digits "
"are not all irreducible")
[docs] @relation_prover
def deduce_in_number_set(self, number_set, **defaults_config):
from proveit.numbers import Natural, NaturalPos
from proveit.logic import InSet
if number_set == Natural:
return self.deduce_in_natural()
elif number_set == NaturalPos:
return self.deduce_in_natural_pos()
else:
try:
# Do this to avoid infinite recursion -- if
# we already know this numeral is in NaturalPos
# we should know how to prove that it is in any
# number set that contains the natural numbers.
if self.as_int() > 0:
InSet(self, NaturalPos).prove(automation=False)
else:
InSet(self, Natural).prove(automation=False)
except BaseException:
# Try to prove that it is in the given number
# set after proving that the numeral is in
# the Natural set and the NaturalPos set.
self.deduce_in_natural()
if self.as_int() > 0:
self.deduce_in_natural_pos()
return InSet(self, number_set).conclude()
[docs] @relation_prover
def deduce_in_natural(self, **defaults_config):
from . import deci_sequence_is_nat
return deci_sequence_is_nat.instantiate(
{n: self.operands.num_elements(), a: self.digits})
# if Numeral._inNaturalStmts is None:
# from proveit.numbers.number_sets.integers import zero_in_nats
# from proveit.numbers.numerals.decimals import nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9
# Numeral._inNaturalStmts = {0: zero_in_nats, 1: nat1, 2: nat2, 3: nat3, 4: nat4, 5: nat5, 6: nat6, 7: nat7,
# 8: nat8, 9: nat9}
# return Numeral._inNaturalStmts[self.n]
[docs] @relation_prover
def deduce_in_natural_pos(self, **defaults_config):
from . import deci_sequence_is_nat_pos
_a = self.digits[0]
_b = self.digits[1:]
return deci_sequence_is_nat_pos.instantiate(
{n: _b.num_elements(), a:_a, b:_b})
# from proveit import ProofFailure
# if Numeral._inNaturalPosStmts is None:
# from proveit.numbers.numerals.decimals import posnat1, posnat2, posnat3, posnat4, posnat5
# from proveit.numbers.numerals.decimals import posnat6, posnat7, posnat8, posnat9
# Numeral._inNaturalPosStmts = {1: posnat1, 2: posnat2, 3: posnat3, 4: posnat4, 5: posnat5, 6: posnat6,
# 7: posnat7, 8: posnat8, 9: posnat9}
# if self.n <= 0:
# raise ProofFailure(self, [],
# "Cannot prove %d in NaturalPos" % self.n)
# return Numeral._inNaturalPosStmts[self.n]
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.logic import InSet
from proveit.numbers import Natural, NaturalPos
_a = self.digits[0]
if isinstance(_a, ExprRange):
# Checking for positivity is not implement for an ExprRange
# of digits.
#return Natural
return None # Not implemented for anything yet.
if InSet(_a, NaturalPos).readily_provable():
return NaturalPos
else:
return Natural
@equality_prover('single_digit_reduced', 'single_digit_reduce')
def single_digit_reduction(self, **defaults_config):
from . import single_digit_reduction
if not self.digits.is_single():
raise ValueError("single_digit_reduction is only applicable "
"when there is a single digit in the "
"DecimalSequence; not satisfied by %s"%self)
return single_digit_reduction.instantiate({n:self.digits[0]})
@equality_prover('digit_repetition_reduced', 'digit_repetition_reduce')
def digit_repetition_reduction(self, **defaults_config):
'''
Tries to reduce a decimal sequence containing an ExprRange.
For example, reduce #(3 4 2 .. 4 repeats .. 2 3) to 3422223
'''
from proveit import TransRelUpdater
from proveit.core_expr_types.tuples import n_repeats_reduction
from proveit.numbers.numerals.decimals import deci_sequence_reduction_ER
expr = self
# A convenience to allow successive update to the equation via transitivities.
# (starting with self=self).
eq = TransRelUpdater(self)
idx = 0
for i, digit in enumerate(self.digits):
# i is the current index in the original expression
# idx is the current index in the transformed expression (eq.relation)
if (isinstance(digit, ExprRange) and
isinstance(digit.body, Numeral)):
import proveit.numbers.numerals.decimals
# _m = expr.digits[:i].num_elements(assumptions)
# _n = digit.true_end_index
# _k = expr.digits[i + 1:].num_elements(assumptions)
# _a = expr.digits[:i]
# _b = digit.body
# _d = expr.digits[i + 1:]
_m = eq.relation.rhs.digits[:idx].num_elements()
_n = digit.true_end_index
_k = expr.digits[i + 1:].num_elements()
_a = eq.relation.rhs.digits[:idx]
_b = digit.body
_d = expr.digits[i + 1:]
# if digit.true_end_index.as_int() >= 10:
# Automatically reduce an Expression range of
# a single numeral to an Expression tuple
# (3 .. 4 repeats.. 3) = 3333
# #(2 3 4 (5 ..3 repeats.. 5) 6 7 8) = 234555678
while _n.as_int() > 9:
_x = digit.body
_c = n_repeats_reduction.instantiate(
{n: _n, x: _x}, preserve_all=True).rhs
eq.update(deci_sequence_reduction_ER.instantiate(
{m: _m, n: _n, k: _k, a: _a, b: _b, c: _c, d: _d},
preserve_all=True))
_n = num(_n.as_int() - 1)
idx += 1
#_n = digit.true_end_index
len_thm = proveit.numbers.numerals.decimals \
.__getattr__('reduce_%s_repeats' % _n)
_x = digit.body
_c = len_thm.instantiate({x: _x}).rhs
idx += _n.as_int()
eq.update(deci_sequence_reduction_ER.instantiate(
{m: _m, n: _n, k: _k, a: _a, b: _b, c: _c, d: _d},
preserve_all=True))
else:
idx += 1
return eq.relation
@staticmethod
@prover
def add_eval(num1, num2, **defaults_config):
'''
evaluates the addition of two integers
'''
from . import md_only_nine_add_one, md_nine_add_one
if not isinstance(num1, int) or not isinstance(num2, int):
raise ValueError("'num1' and 'num2' should be integers")
num1 = num(num1)
num2 = num(num2)
if num2 == one:
# if the second number (num2) is one, we set it equal to the first number and then assume the
# first number to be one and the second number to not be one. SHOULD BE DELETED once addition works
# for numbers greater than one.
num2 = num1
elif num2 != one:
raise NotImplementedError(
"Currently, add_eval only works for the addition of Decimal "
"Sequences and one, not %s, %s" %
(str(num1), str(num2)))
if all(digit == nine for digit in num2.digits):
# every digit is 9
return md_only_nine_add_one.instantiate(
{k: num2.digits.num_elements()})
elif num2.digits[-1] == nine:
# the last digit is nine
count = 0
idx = -1
while num2.digits[idx] == nine or (
isinstance(
num2.digits[idx],
ExprRange) and num2.digits[idx].body == nine):
if isinstance(num2.digits[idx], ExprRange):
count += num2.digits[idx].true_end_index
else:
count += 1
idx -= 1
length = num2.digits.num_elements()
_m = num(length.as_int() - count - 1)
_k = num(count)
_a = num2.digits[:-(count + 1)]
_b = num2.digits[-(count + 1)]
return md_nine_add_one.instantiate(
{m: _m, k: _k, a: _a, b: _b})
else:
# the last digit is not nine
_m = num(num2.digits.num_elements().as_int() - 1)
_k = num(0)
_a = num2.digits[:-1]
_b = num2.digits[-1]
eq = md_nine_add_one.instantiate(
{m: _m, k: _k, a: _a, b: _b})
return eq.inner_expr(
).rhs.operands[-1].evaluate()
@staticmethod
@prover
def mult_eval(num1, num2, **defaults_config):
'''
evaluates the multiplication of two integers
'''
if not isinstance(num1, int) or not isinstance(num2, int):
raise ValueError("'num1' and 'num2' should be integers")
raise NotImplementedError("multi-digit multiplication has not "
"been implemented yet")
'''
# Shouldn't be needed given new auto-simplification approach.
@prover
def evaluate_add_digit(self, **defaults_config):
"""
Evaluates each addition within the DecimalSequence
"""
from proveit import TransRelUpdater, ExprTuple
from proveit.numbers import Add
from . import deci_sequence_reduction
expr = self
# A convenience to allow successive update to the equation via transitivities.
# (starting with self=self).
eq = TransRelUpdater(self, assumptions)
for i, digit in enumerate(self.digits):
if isinstance(digit, Add):
# only implemented for addition.
_m = expr.digits[:i].num_elements(assumptions=assumptions)
_n = digit.operands.num_elements(assumptions=assumptions)
_k = expr.digits[i + 1:].num_elements(assumptions=assumptions)
# _a = expr.inner_expr().operands[:i]
_b = digit.operands
_c = digit.evaluation(assumptions=assumptions).rhs
# _d = expr.inner_expr().operands[i + 1:]
_a = expr.digits[:i]
_d = expr.digits[i + 1:]
expr = eq.update(deci_sequence_reduction.instantiate(
{m: _m, n: _n, k: _k, a: _a, b: _b, c: _c, d: _d}, assumptions=assumptions))
return eq.relation
'''
class DigitSet(NumberSet):
def __init__(self, *, styles=None):
NumberSet.__init__(
self, 'Digits', r'\mathbb{N}^{\leq 9}',
theory=__file__, styles=styles)
@prover
def deduce_member_lower_bound(self, member, **defaults_config):
from . import digits_lower_bound
return digits_lower_bound.instantiate({n: member})
@prover
def deduce_member_upper_bound(self, member, **defaults_config):
from . import digits_upper_bound
return digits_upper_bound.instantiate({n: member})
def membership_object(self, element):
return DeciMembership(element, self)
class DeciMembership(NumberMembership):
'''
Defines methods that apply to membership of a decimal sequence.
'''
def __init__(self, element, number_set):
NumberMembership.__init__(self, element, number_set)
@prover
def conclude(self, **defaults_config):
from proveit import ProofFailure
from . import n_in_digits
# if we know the element is 0-9, then we can show it is a digit
try:
return NumberMembership.conclude(self)
except ProofFailure:
return n_in_digits.instantiate({n: self.element})
# if isinstance(self.element, numeral) and 0 <= self.element.as_int() <= 9:
# _n = self.element.as_int()
# thm = proveit.numbers.numerals.decimals \
# .__getattr__('digit%s' % _n)
# return thm
# else:
# return n_in_digits.instantiate({n: self.element},
# assumptions=assumptions)
def side_effects(self, judgment):
'''
Yield side-effects when proving 'n in Digit' for a given n.
'''
yield self.derive_element_lower_bound
yield self.derive_element_upper_bound
@prover
def derive_element_lower_bound(self, **defaults_config):
return self.domain.deduce_member_lower_bound(self.element)
@prover
def derive_element_upper_bound(self, **defaults_config):
return self.domain.deduce_member_upper_bound(self.element)
[docs]def num(x):
from proveit.numbers import Neg
if x < 0:
return Neg(num(abs(x)))
if isinstance(x, int):
if x < 10:
if x == 0:
return zero
elif x == 1:
return one
elif x == 2:
return two
elif x == 3:
return three
elif x == 4:
return four
elif x == 5:
return five
elif x == 6:
return six
elif x == 7:
return seven
elif x == 8:
return eight
elif x == 9:
return nine
else:
return DecimalSequence(*[num(int(digit)) for digit in str(x)])
else:
assert False, 'num not implemented for anything except integers currently. plans to take in strings or floats with specified precision'