Source code for proveit.numbers.modular.mod

from proveit import (defaults, Literal, Operation, ProofFailure, 
                     relation_prover, equality_prover)
# from proveit.numbers.number_sets import Integer, Real
from proveit import a, b, c, i, j, x, L
from proveit.logic import Equals, InSet, SubsetEq
from proveit.relation import TransRelUpdater
from proveit.numbers import (NumberOperation, Add, ZeroSet,
                             deduce_number_set,
                             readily_provable_number_set)

[docs]class Mod(NumberOperation): # operator of the Mod operation. _operator_ = Literal(string_format='mod', latex_format=r'~\textup{mod}~', theory=__file__) def __init__(self, dividend, divisor, *, styles=None): NumberOperation.__init__(self, Mod._operator_, (dividend, divisor), styles=styles) self.dividend = self.operands[0] self.divisor = self.operands[1] @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Returns a proven simplification equation for this Mod expression assuming the operands have been simplified. Specifically, performs reductions of the form (x mod L) = x where applicable and [(a mod L + b) mod L] = [(a + b) mod L]. ''' from . import (int_mod_elimination, real_mod_elimination, redundant_mod_elimination, redundant_mod_elimination_in_sum) from proveit.numbers import ( NaturalPos, RealPos, Interval, IntervalCO, subtract, zero, one) deduce_number_set(self.dividend) divisor_ns = readily_provable_number_set(self.divisor) if (NaturalPos.readily_includes(divisor_ns) and InSet(self.dividend, Interval(zero, subtract(self.divisor, one))).proven()): # (x mod L) = x if L in N+ and x in {0 .. L-1} return int_mod_elimination.instantiate( {x:self.dividend, L:self.divisor}) if (RealPos.readily_includes(divisor_ns) and InSet(self.dividend, IntervalCO(zero, self.divisor)).proven()): # (x mod L) = x if L in R+ and x in [0, L) return real_mod_elimination.instantiate( {x:self.dividend, L:self.divisor}) return Mod._redundant_mod_elimination( self, redundant_mod_elimination, redundant_mod_elimination_in_sum) @staticmethod def _redundant_mod_elimination( expr, mod_elimination_thm, mod_elimination_in_sum_thm): ''' For use by Mod and ModAbs for shallow_simplification. Examples: If expr = Mod(Mod(a, b), b), then calling Mod._redundant_mod_elimination(expr, redundant_mod_elimination_in_modabs, redundant_mod_elimination_in_sum_in_modabs) returns Mod(a, b). If expr = Mod( Add(Mod(a, b), c), b ) = ((a mod b) + c) mod b, then calling Mod._redundant_mod_elimination(expr, redundant_mod_elimination_in_modabs, redundant_mod_elimination_in_sum_in_modabs) returns Mod(Add(a, c), b) i.e. (a+c) mod b ''' dividend = expr.dividend divisor = expr.divisor if isinstance(dividend, Mod) and dividend.divisor==divisor: # [(a mod b) mod b] = [a mod b] return mod_elimination_thm.instantiate( {a:dividend.dividend, b:divisor}) elif isinstance(dividend, Add): # Eliminate 'mod L' from each term. eq = TransRelUpdater(expr) _L = divisor mod_terms = [] for _k, term in enumerate(dividend.terms): if isinstance(term, Mod) and term.divisor==_L: mod_terms.append(_k) for _k in mod_terms: # Use preserve_all=True for all but the last term. preserve_all = (_k != mod_terms[-1]) _a = expr.dividend.terms[:_k] _b = expr.dividend.terms[_k].dividend _c = expr.dividend.terms[_k+1:] _i = _a.num_elements() _j = _c.num_elements() expr = eq.update( mod_elimination_in_sum_thm .instantiate( {i:_i, j:_j, a:_a, b:_b, c:_c, L:_L}, preserve_all=preserve_all)) return eq.relation return Equals(expr, expr).conclude_via_reflexivity() # def deduce_in_interval(self, assumptions=frozenset()): # from . import mod_in_interval, mod_in_interval_c_o # from number_sets import deduce_in_integer, deduce_in_real # try: # # if the operands are integers, then we can deduce that # # a mod b is in 0..(b-1) # deduce_in_integer(self.operands, assumptions) # return mod_in_interval.instantiate( # {a:self.dividend, b:self.divisor}).checked(assumptions) # except: # # if the operands are reals, then we can deduce that a mod b is in [0, b) # deduce_in_real(self.operands, assumptions) # return mod_in_interval_c_o.instantiate({a:self.dividend, # b:self.divisor}).checked(assumptions)
[docs] @relation_prover def deduce_in_interval(self, **defaults_config): ''' Prove that the "x mod b" is in the interval [0, b). ''' from . import (mod_in_interval, mod_natpos_in_interval, mod_in_interval_c_o) from proveit.numbers import Integer, NaturalPos # from number_sets import deduce_in_integer, deduce_in_real dividend_ns = readily_provable_number_set(self.dividend) divisor_ns = readily_provable_number_set(self.divisor) int_dividend = Integer.readily_includes(dividend_ns) if (int_dividend and NaturalPos.readily_includes(divisor_ns)): return mod_natpos_in_interval.instantiate( {a: self.dividend, b: self.divisor}) elif (int_dividend and Integer.readily_includes(divisor_ns)): # if the operands are integers, then we can deduce that # a mod b is an integer in the set {0,1,...,(b-1)} return mod_in_interval.instantiate( {a: self.dividend, b: self.divisor}) else: # if the operands are reals, then we can deduce that # a mod b is in half-open real interval [0, b) return mod_in_interval_c_o.instantiate( {a: self.dividend, b: self.divisor})
[docs] @relation_prover def deduce_in_number_set(self, number_set, **defaults_config): ''' Given a number set number_set (such as Integer, Real, etc), attempt to prove that the given Mod expression is in that number set using the appropriate closure theorem. ''' import proveit.numbers.modular as mod_pkg from proveit.numbers import (Integer, Natural, Real, Interval, RealInterval) if (isinstance(number_set, Interval) or isinstance(number_set, RealInterval)): if isinstance(number_set, Interval): # To prove that it is in an integer interval through # standard means, we'll need to know that the dividend # and divisor are integers. InSet(self.dividend, Integer).prove() InSet(self.divisor, Integer).prove() in_mod_interval = self.deduce_in_interval() mod_interval = in_mod_interval.domain if mod_interval == number_set: return in_mod_interval # To prove by standard means, 'mod_interval' must be a # subset of 'number_set'. set_relation = SubsetEq(mod_interval, number_set).prove() return set_relation.derive_superset_membership(self) thm = None if number_set == ZeroSet: divisor_ns = readily_provable_number_set(self.divisor) if Integer.readily_includes(divisor_ns): thm = mod_pkg.mod_in_zero_set_int else: thm = mod_pkg.mod_in_zero_set elif number_set == Integer: thm = mod_pkg.mod_int_closure elif number_set == Natural: thm = mod_pkg.mod_int_to_nat_closure elif number_set == Real: thm = mod_pkg.mod_real_closure if thm is not None: return thm.instantiate({a: self.dividend, b: self.divisor}) raise NotImplementedError( "'Mod.deduce_in_number_set()' not implemented for the %s set" % str(number_set))
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 (zero, one, Interval, IntervalCO, Abs, subtract, NaturalPos, Integer) _b = self.divisor # from number_sets import deduce_in_integer, deduce_in_real dividend_ns = readily_provable_number_set(self.dividend) if dividend_ns == ZeroSet: # 0 mod N = 0 return ZeroSet divisor_ns = readily_provable_number_set(self.divisor) int_dividend = Integer.readily_includes(dividend_ns) if (int_dividend and NaturalPos.readily_includes(divisor_ns)): return Interval(zero, subtract(_b, one)) elif (int_dividend and Integer.readily_includes(divisor_ns)): # if the operands are integers, then we can deduce that # a mod b is an integer in the set {0,1,...,(b-1)} return Interval(zero, subtract(Abs(_b), one)) else: # if the operands are reals, then we can deduce that # a mod b is in half-open real interval [0, b) return IntervalCO(zero, _b)