Source code for proveit.numbers.modular.mod_abs

from proveit import (defaults, Literal, Operation, 
                     relation_prover, equality_prover,
                     SimplificationDirectives)
from proveit import a, b, c, i, j, x, L, N
from proveit.logic import Equals
from proveit.relation import TransRelUpdater
from proveit.numbers import (
        two, Abs, Add, Div, Integer, LessEq, NumberOperation,
        readily_provable_number_set, Real, ZeroSet)
from .mod import Mod

[docs]class ModAbs(NumberOperation): # operator of the ModAbs operation. _operator_ = Literal(string_format='ModAbs', theory=__file__) # The eliminate_mod simplification directive controls the # simplification of an expression like |x|_{mod L} to |x| when # we know or can readily prove that |x| <= L/2. _simplification_directives_ = SimplificationDirectives( eliminate_mod = True) def __init__(self, value, divisor, *, styles=None): Operation.__init__(self, ModAbs._operator_, (value, divisor), styles=styles) self.dividend = self.value = value self.divisor = divisor
[docs] def string(self, **kwargs): return ('|' + self.value.string(fence=False) + '|_{mod ' + self.divisor.string(fence=False) + '}')
[docs] def latex(self, **kwargs): return (r'\left|' + self.value.latex(fence=False) + r'\right|_{\textup{mod}\thinspace ' + self.divisor.latex(fence=False) + r'}')
@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 |a mod L + b|_{mod L} = |a + b|_{mod L}, and if we know (or can readily prove) that |x| <= L/2, then performs reductions of the form |x|_{mod L} = |x| ''' from . import (redundant_mod_elimination_in_modabs, redundant_mod_elimination_in_sum_in_modabs) eq = TransRelUpdater(self) # eq is then self = self # (1) First deal with |a mod L + b|_{mod L} expr = eq.update(Mod._redundant_mod_elimination( self, redundant_mod_elimination_in_modabs, redundant_mod_elimination_in_sum_in_modabs)) # (2) IF we still have a ModAbs of the form |x|_{mod L}, # and the simplification directive 'eliminate_mod' is True, # further simplify to just |x| if we can readily prove that # |x| <= L/2 if (ModAbs._simplification_directives_.eliminate_mod and isinstance(eq.relation.rhs, ModAbs)): _dividend = eq.relation.rhs.dividend _divisor = eq.relation.rhs.divisor if LessEq(Abs(_dividend), Div(_divisor, two)).readily_provable(): from . import mod_abs_x_reduce_to_abs_x _x_sub = _dividend _N_sub = _divisor eq.update(mod_abs_x_reduce_to_abs_x.instantiate( {x: _x_sub, N: _N_sub})) return eq.relation @equality_prover('reversed_difference', 'reverse_difference') def difference_reversal(self, **defaults_config): ''' Derive |a - b|_{N} = |b - a|_{N}. ''' from proveit.numbers import Add, Neg from . import mod_abs_diff_reversal if not (isinstance(self.value, Add) and self.value.operands.is_double() and isinstance(self.value.operands[1], Neg)): raise ValueError( "ModAbs.difference_reversal is only applicable for " "an expression of the form |a - b|_{N}, not {0}". format(self)) _a_sub = self.value.operands[0] _b_sub = self.value.operands[1].operand _N_sub = self.divisor return mod_abs_diff_reversal.instantiate( {a:_a_sub, b:_b_sub, N: _N_sub})
[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 ModAbs expression is in that number set using the appropriate closure theorem. ''' import proveit.numbers.modular as mod_pkg thm = None if number_set == ZeroSet: divisor_ns = readily_provable_number_set(self.divisor) if Integer.readily_includes(divisor_ns): thm = mod_pkg.mod_abs_in_zero_set_int else: thm = mod_pkg.mod_abs_in_zero_set elif number_set == Integer: thm = mod_pkg.mod_abs_int_closure elif number_set == Real: thm = mod_pkg.mod_abs_real_closure if thm is not None: return thm.instantiate({a: self.value, b: self.divisor}) raise NotImplementedError( "'ModAbs.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. ''' value_ns = readily_provable_number_set(self.value) divisor_ns = readily_provable_number_set(self.divisor) if value_ns == ZeroSet: return ZeroSet # |0|_{mod b} = 0 elif value_ns.readily_includes(Integer) and ( divisor_ns.readily_includes(Integer)): return Integer else: return Real