from proveit import (defaults, Literal, Operation, ProofFailure,
UnsatisfiedPrerequisites, USE_DEFAULTS,
relation_prover, prover)
from proveit.logic import IrreducibleValue, Equals, NotEquals
from proveit import a, b
import math
[docs]class Numeral(Literal, IrreducibleValue):
_inNaturalStmts = None # initializes when needed
_inNaturalPosStmts = None # initializes when needed
_inDigitsStmts = None # initializes when needed
_notZeroStmts = None # initializes when needed
_positiveStmts = None # initializes when needed
def __init__(self, n, string_format=None, latex_format=None, *,
styles=None):
if string_format is None:
string_format = str(n)
Literal.__init__(
self, string_format, extra_core_info=[str(n)],
theory=__file__, styles=styles)
if not isinstance(n, int):
raise ValueError("'n' of a Numeral must be an integer")
self.n = n
[docs] @prover
def eval_equality(self, other, **defaults_config):
if other == self:
return Equals(self, self).prove().evaluation()
self_neq_other = self.deduce_not_equal(other)
return self_neq_other.unfold().equate_negated_to_false()
def readily_not_equal(self, other):
'''
Return True iff self and other are numeric rationals that are
not equal to each other.
'''
return not_equal_numeric_rationals(self, other.canonical_form())
@relation_prover
def deduce_not_equal(self, other, **defaults_config):
'''
Prove and return self ≠ other if other is a numeric
rational.
'''
if is_numeric_rational(other):
return deduce_not_equal_numeric_rationals(self, other)
raise NotImplementedError(
"Numeral.deduce_not_equal only implemented for "
"comparing numeric rationals, not %s"%other)
@relation_prover
def deduce_equal_or_not(self, other, **defaults_config):
from proveit.numbers import Less
relation = Less.sort([self, other]).expr
if isinstance(relation, Equals):
return relation
if NotEquals(self, other).proven():
return self.deduce_not_equal(other)
raise UnsatisfiedPrerequisites(
"Unable to determine whether or not %s = %s"
%(self, other))
[docs] def remake_arguments(self):
'''
Yield the argument values that could be used to recreate this DigitLiteral.
'''
yield self.n
if self.string_format != str(self.n):
yield '"' + self.string_format + '"'
if self.latex_format != self.string_format:
yield ('latex_format', 'r"' + self.latex_format + '"')
[docs] def as_int(self):
return self.n
[docs] @staticmethod
def make_literal(string_format, latex_format, *,
extra_core_info, theory, styles):
'''
Make the DigitLiteral that matches the core information.
'''
from proveit import Theory
assert theory == Theory(__file__), (
"Expecting a different Theory for a DigitLiteral: "
"%s vs %s" % (theory.name, Theory(__file__).name))
n = int(extra_core_info[0])
return Numeral(n, string_format, latex_format, styles=styles)
def readily_provable_number_set(self):
'''
We can prove this numeral is in {0} or in NaturalPos.
We can also prove this is in Digits, but that is less useful
for this purpose.
'''
from proveit.numbers import zero, ZeroSet, NaturalPos
if self == zero:
return ZeroSet
else:
return NaturalPos
[docs] @prover
def deduce_in_number_set(self, number_set, **defaults_config):
from proveit.logic import Set
from proveit.numbers import (zero, ZeroSet, Natural, NaturalPos,
Digits, IntegerNonPos,
RationalNonPos, RealNonPos)
from proveit.logic import InSet, SubsetEq
if self == zero and number_set == ZeroSet:
return InSet(zero, Set(zero)).conclude_as_folded()
if number_set == Natural:
return self.deduce_in_natural()
elif number_set == NaturalPos:
return self.deduce_in_natural_pos()
elif number_set == IntegerNonPos:
if self.n > 0:
raise ProofFailure(
InSet(self, number_set), defaults.assumptions,
"%s is positive"%self)
return InSet(self, number_set).conclude_as_last_resort()
elif number_set == Digits:
return self.deduce_in_digits()
else:
try:
# Do this to avoid infinite recursion -- if
# we already know this numeral is in the NaturalPos set
# we should know how to prove that it is in any
# number set that contains the natural numbers.
if self.n > 0:
InSet(self, NaturalPos).prove(automation=False)
else:
InSet(self, Natural).prove(automation=False)
InSet(self, IntegerNonPos).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.
if self.n > 0:
self.deduce_in_natural_pos()
else:
self.deduce_in_natural()
self.deduce_in_integer_nonpos()
if self.n > 0:
sub_rel = SubsetEq(NaturalPos, number_set)
else:
if number_set in (RationalNonPos, RealNonPos):
sub_rel = SubsetEq(IntegerNonPos, number_set)
# Allow automation for this minor thing even
# if automation has been disabled coming into this.
sub_rel.prove(automation=True)
else:
sub_rel = SubsetEq(Natural, number_set)
# Prove membership via inclusion:
return sub_rel.derive_superset_membership(self)
[docs] @prover
def deduce_in_natural(self, **defaults_config):
if Numeral._inNaturalStmts is None:
from proveit.numbers.number_sets.natural_numbers import zero_in_nats
from .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]
@prover
def deduce_in_integer_nonpos(self, **defaults_config):
from proveit.logic import InSet
from proveit.numbers import IntegerNonPos
if self.n != 0:
raise ProofFailure(InSet(self, IntegerNonPos), defaults.assumptions,
"%s is positive"%self)
from proveit.numbers.number_sets.integers import zero_is_nonpos_int
return zero_is_nonpos_int
'''
def deduce_not_zero(self):
if Numeral._notZeroStmts is None:
from .decimals import one_not_zero, two_not_zero, three_not_zero, four_not_zero, five_not_zero
from .decimals import six_not_zero, seven_not_zero, eight_not_zero, nine_not_zero
Numeral._notZeroStmts = {1:one_not_zero, 2:two_not_zero, 3:three_not_zero, 4:four_not_zero, 5:five_not_zero, 6:six_not_zero, 7:seven_not_zero, 8:eight_not_zero, 9:nine_not_zero}
return Numeral._notZeroStmts[self.n]
'''
[docs] @prover
def deduce_in_natural_pos(self, **defaults_config):
if Numeral._inNaturalPosStmts is None:
from .decimals import posnat1, posnat2, posnat3, posnat4, posnat5
from .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]
[docs] @prover
def deduce_in_digits(self, **defaults_config):
if Numeral._inDigitsStmts is None:
from .decimals import digit0, digit1, digit2, digit3, digit4, digit5
from .decimals import digit6, digit7, digit8, digit9
Numeral._inDigitsStmts = {
0: digit0,
1: digit1,
2: digit2,
3: digit3,
4: digit4,
5: digit5,
6: digit6,
7: digit7,
8: digit8,
9: digit9}
if self.n < 0 or self.n > 9:
raise ProofFailure(self, [],
"Cannot prove %d in Digits" % self.n)
return Numeral._inDigitsStmts[self.n]
[docs] @prover
def deduce_positive(self, **defaults_config):
if Numeral._positiveStmts is None:
from .decimals import posnat1, posnat2, posnat3, posnat4, posnat5
from .decimals import posnat6, posnat7, posnat8, posnat9
Numeral._positiveStmts = {
1: posnat1,
2: posnat2,
3: posnat3,
4: posnat4,
5: posnat5,
6: posnat6,
7: posnat7,
8: posnat8,
9: posnat9}
return Numeral._positiveStmts[self.n]
class NumeralSequence(Operation, IrreducibleValue):
"""
Base class of BinarySequence, DecimalSequence, and HexSequence.
"""
def __init__(self, operator, *digits, styles=None):
Operation.__init__(self, operator, digits, styles=styles)
self.digits = self.operands
def is_irreducible_value(self):
'''
Only really an irreducible value if each digit is a Numeral.
'''
return (not self.digits.is_single() and
all(isinstance(digit, Numeral) for digit in self.digits))
@prover
def eval_equality(self, other, **defaults_config):
if other == self:
return Equals(self, self).conclude_via_reflexivity()
self_neq_other = self.deduce_not_equal(other)
return self_neq_other.unfold().equate_negated_to_false()
@prover
def deduce_not_equal(self, other, **defaults_config):
# same method works for Numeral and NumeralSequence.
return Numeral.deduce_not_equals(self, other)
def _prefix(self, format_type):
raise NotImplementedError("'_prefix' must be implemented for each "
"NumeralSequence")
def _formatted(self, format_type, operator=None, **kwargs):
from proveit import ExprRange
outstr = ''
fence = False
if operator is None:
operator = ' ~ '
prefix = self._prefix(format_type)
if (self.digits.is_single() or
not all(isinstance(digit, Numeral) for
digit in self.digits)):
# for binary, we use #b(...)
# for hex, we use #x(...)
# for decimal, #(...)
if format_type == 'latex':
outstr += r'\texttt{\#}'
else:
outstr += '#'
outstr += prefix
outstr += '('
fence = True
else:
if prefix != '':
# for binary, we use 0b
# for hex, we use 0x
# for decimal, no prefix
if format_type == 'latex':
outstr += r'\texttt{0}'
else:
outstr += '0'
outstr += prefix
for i, digit in enumerate(self.digits):
if i != 0 and fence:
add = operator
else:
add = ''
if isinstance(digit, Operation):
outstr += add + digit.formatted(format_type, fence=True)
elif isinstance(digit, ExprRange):
outstr += add + digit.formatted(format_type, operator=operator)
else:
outstr += add + digit.formatted(format_type)
if fence:
outstr += r')'
return outstr
def _function_formatted(self, format_type, **kwargs):
return self._formatted(format_type, **kwargs)
[docs]def is_numeric_natural(expr):
'''
Return True iff the 'expr' represents an explicit, numeric natural
number.
'''
if isinstance(expr, Numeral):
return True
elif isinstance(expr, NumeralSequence):
return expr.is_irreducible_value()
return False
[docs]def is_numeric_int(expr):
'''
Return True iff the 'expr' represents an explicit, numeric integer.
'''
from proveit.numbers import Neg
return is_numeric_natural(expr) or (
isinstance(expr, Neg) and is_numeric_natural(expr.operand))
[docs]def is_numeric_rational(expr):
'''
Return True iff 'expr' represents an explicit, numeric rational
number (as a numeric integer or fraction of numeric integers
with a nonzero denominator).
'''
from proveit.numbers import Neg, Div, zero
if isinstance(expr, Neg) and is_numeric_rational(expr.operand):
return True
if isinstance(expr, Div):
return (is_numeric_int(expr.numerator) and
is_numeric_int(expr.denominator) and
expr.denominator != zero)
return is_numeric_int(expr)
[docs]def numeric_rational_ints(expr):
'''
Return the integer numerator and denominator of a numeric rational.
Never returns a negative denominator (multiplies top and bottom
by -1 to avoid that).
'''
from proveit.numbers import Neg, Div
sign = 1
while isinstance(expr, Neg):
sign *= -1
expr = expr.operand
if isinstance(expr, Div):
numer, denom = expr.numerator.as_int(), expr.denominator.as_int()
if denom < 0:
# The denominator is negative; multiply top and bottom
# by negative 1.
return -numer, -denom
return numer*sign, denom
return expr.as_int()*sign, 1
[docs]def simplified_numeric_rational(numer_int, denom_int):
'''
Given a numerator and a denominator as integers, return
an Expression of the equivalent irreducible rational.
'''
from proveit.numbers import num, Div, Neg
# Extract the sign.
sign = 1
if numer_int < 0:
sign *= -1
numer_int *= -1
if denom_int < 0:
sign *= -1
denom_int *= -1
# Find the greatest common divisor and divide it out.
gcd = int(math.gcd(numer_int, denom_int))
numer_int = numer_int // gcd
denom_int = denom_int // gcd
# Build and return the expression.
if denom_int == 1:
rational = num(numer_int)
else:
rational = Div(num(numer_int), num(denom_int))
if sign == -1:
return Neg(rational)
return rational
[docs]def not_equal_numeric_rationals(a, b):
'''
Return True iff a and b are numeric rational expressions that
are not equal to each other.
'''
if is_numeric_rational(a) and is_numeric_rational(b):
if numeric_rational_ints(a) != numeric_rational_ints(b):
return True
return False
'''
Comparators for numeric integers/rationals.
'''
[docs]def less_numeric_ints(a, b):
'''
Return True iff a < b.
a and b must be numeric integer expressions.
'''
if not (is_numeric_int(a) and is_numeric_int(b)):
raise ValueError("Both arguments to 'less_numeric_ints' should "
"be numeric ints, got %s and %s"%(a, b))
return a.as_int() < b.as_int()
[docs]def less_eq_numeric_ints(a, b):
'''
Return True iff a ≤ b.
a and b must be numeric integer expressions.
'''
if not (is_numeric_int(a) and is_numeric_int(b)):
raise ValueError("Both arguments to 'less_numeric_ints' should "
"be numeric ints, got %s and %s"%(a, b))
return a.as_int() <= b.as_int()
def _compare_numeric_rationals(a, b, comparator):
'''
Helper for less_numeric_rationals and less_eq_numeric_rationals.
'''
if not (is_numeric_rational(a) and is_numeric_rational(b)):
raise ValueError(
"Both arguments to '_compare_numeric_rationals' should "
"be numeric rationals, got %s and %s"%(a, b))
a_numer, a_denom = numeric_rational_ints(a)
b_numer, b_denom = numeric_rational_ints(b)
assert a_denom > 0
assert b_denom > 0
# Multiply both sides by both denominators:
return comparator(a_numer*b_denom, b_numer*a_denom)
[docs]def less_numeric_rationals(a, b):
'''
Return True iff a < b.
a and b must be numeric rational expressions.
'''
return _compare_numeric_rationals(a, b, lambda x, y: x < y)
[docs]def less_eq_numeric_rationals(a, b):
'''
Return True iff a ≤ b.
a and b must be numeric rational expressions.
'''
return _compare_numeric_rationals(a, b, lambda x, y: x <= y)
[docs]@prover
def deduce_not_equal_numeric_rationals(lhs, rhs, **defaults_config):
'''
Assuming a and b are numeric rationals, prove and return that
a ≠ b.
'''
from proveit.numbers.ordering import less_is_not_eq
if less_numeric_rationals(lhs.canonical_form(), rhs.canonical_form()):
_a, _b = lhs, rhs
else:
_a, _b = rhs, lhs
not_eq_stmt = less_is_not_eq.instantiate({a: _a, b: _b})
if not_eq_stmt.lhs != lhs:
# We need to reverse the statement.
return not_eq_stmt.derive_reversed()
return not_eq_stmt