Theorems (or conjectures) for the theory of proveit.numbers.modular

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Lambda, IndexedVar, ExprRange
from proveit import a, b, c, i, j, n, x, y, L, N, S
from proveit.logic import (And, Equals, Forall, Iff, InSet, NotEquals, 
                           SubsetEq, SetOfAll, Card, Bijections)
from proveit.numbers import (Abs, Add, frac, greater_eq, LessEq, Interval, IntervalCO,
                            Mod, ModAbs, Mult, Neg, number_ordering, subtract)
from proveit.numbers import (zero, one, two, ZeroSet, Natural, Integer, NaturalPos, 
                            Real, RealPos, Complex)
from proveit.core_expr_types import a_1_to_n, a_1_to_i, c_1_to_j

%begin theorems

Defining theorems for theory 'proveit.numbers.modular'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

mod_in_zero_set_int = Forall(
    (a, b),
    InSet(Mod(a, b), ZeroSet),
    domain=Integer,
    conditions=[Equals(a, zero)])

mod_in_zero_set_int (conjecture without proof):

mod_in_zero_set = Forall(
    (a, b),
    InSet(Mod(a, b), ZeroSet),
    domain=Real,
    conditions=[Equals(a, zero)])

mod_in_zero_set (conjecture without proof):

mod_int_closure = Forall(
    (a, b),
    InSet(Mod(a, b), Integer),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_int_closure (conjecture without proof):

mod_int_to_nat_closure = Forall(
    (a, b),
    InSet(Mod(a, b), Natural),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_int_to_nat_closure (conjecture without proof):

mod_in_interval = Forall(
    (a, b),
    InSet(Mod(a, b), Interval(zero, subtract(Abs(b), one))),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_in_interval (conjecture without proof):

mod_natpos_in_interval = Forall(
    (a, b),
    InSet(Mod(a, b), Interval(zero, subtract(b, one))),
    domains=(Integer, NaturalPos))

mod_natpos_in_interval (conjecture without proof):

mod_abs_in_zero_set_int = Forall(
    (a, b),
    InSet(ModAbs(a, b), ZeroSet),
    domain=Integer,
    conditions=[Equals(a, zero)])

mod_abs_in_zero_set_int (conjecture without proof):

mod_abs_in_zero_set = Forall(
    (a, b),
    InSet(ModAbs(a, b), ZeroSet),
    domain=Real,
    conditions=[Equals(a, zero)])

mod_abs_in_zero_set (conjecture without proof):

mod_real_closure = Forall(
    (a, b),
    InSet(Mod(a, b), Real),
    domain=Real,
    conditions=[NotEquals(b, zero)])

mod_real_closure (conjecture without proof):

mod_abs_int_closure = Forall(
    (a, b),
    InSet(ModAbs(a, b), Integer),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_abs_int_closure (conjecture without proof):

mod_abs_int_to_nat_closure = Forall(
    (a, b),
    InSet(ModAbs(a, b), Natural),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_abs_int_to_nat_closure (conjecture without proof):

mod_abs_in_interval = Forall(
    (a, b),
    InSet(ModAbs(a, b), Interval(zero, subtract(Abs(b), one))),
    domain=Integer,
    conditions=[NotEquals(b, zero)])

mod_abs_in_interval (conjecture without proof):

mod_abs_real_closure = Forall(
    (a, b),
    InSet(ModAbs(a, b), Real),
    domain=Real,
    conditions=[NotEquals(b, zero)])

mod_abs_real_closure (conjecture without proof):

mod_in_interval_c_o = Forall(
    (a, b),
    InSet(Mod(a, b), IntervalCO(zero, Abs(b))),
    domain=Real,
    conditions=[NotEquals(b, zero)])

mod_in_interval_c_o (conjecture without proof):

mod_abs_scaled = Forall(
    (a, b, c),
    Equals(Mult(a, ModAbs(b, c)), ModAbs(Mult(a, b), Mult(a, c))),
    domain=Real)

mod_abs_scaled (conjecture without proof):

mod_abs_subtract_cancel = Forall(
    (a, b, c),
    LessEq(ModAbs(subtract(Mod(Add(b, a), c), b), c), Abs(a)),
    domain=Real,
    conditions=[NotEquals(c, zero)])

mod_abs_subtract_cancel (conjecture without proof):

int_mod_elimination = Forall(
    L, Forall(
        x, Equals(Mod(x, L), x),
        domain=Interval(zero, subtract(L, one))),
    domain=NaturalPos)

int_mod_elimination (conjecture without proof):

real_mod_elimination = Forall(
    L, Forall(
        x, Equals(Mod(x, L), x),
        domain=IntervalCO(zero, L)),
    domain=RealPos)

real_mod_elimination (conjecture without proof):

Since $((a + n \cdot L)~\textrm{mod}~L) = (a~\textrm{mod}~L)$ and there always exists an integer $n$ such that $(x~\textrm{mod}~L) = (x + n \cdot L)$ then we can also eliminate $\textrm{mod}~L$ from any term within a $\textrm{mod}~L$. That is $((a~\textrm{mod}~L + b)~\textrm{mod}~L) = ((a + b)~\textrm{mod}~L)$. This reasoning also applies to ModAbs: $|a~\textrm{mod}~L + b|_{\textrm{mod}~L} = |a + b|_{~\textrm{mod}~L}$.

redundant_mod_elimination = Forall(
    (a, b), Equals(Mod(Mod(a, b), b), Mod(a, b)),
    domains=(Real, RealPos))

redundant_mod_elimination (conjecture without proof):

redundant_mod_elimination_in_sum = Forall(
    (i, j), Forall(
        (a_1_to_i, b, c_1_to_j), Forall(
            L, Equals(Mod(Add(a_1_to_i, Mod(b, L), c_1_to_j), L), 
                      Mod(Add(a_1_to_i, b, c_1_to_j), L)).with_wrap_after_operator(),
            domain=RealPos),
        domain=Real),
    domain=Natural)

redundant_mod_elimination_in_sum (conjecture without proof):

redundant_mod_elimination_in_modabs = Forall(
    (a, b), Equals(ModAbs(Mod(a, b), b), ModAbs(a, b)),
    domains=(Real, RealPos))

redundant_mod_elimination_in_modabs (conjecture without proof):

redundant_mod_elimination_in_sum_in_modabs = Forall(
    (i, j), Forall(
        (a_1_to_i, b, c_1_to_j), Forall(
            L, Equals(ModAbs(Add(a_1_to_i, Mod(b, L), c_1_to_j), L), 
                      ModAbs(Add(a_1_to_i, b, c_1_to_j), L)).with_wrap_after_operator(),
            domain=RealPos),
        domain=Real),
    domain=Natural)

redundant_mod_elimination_in_sum_in_modabs (conjecture without proof):

mod_abs_of_difference_bound = Forall((a, b, N),
       greater_eq(ModAbs(subtract(a, b), N),
                  subtract(ModAbs(a, N), ModAbs(b, N))),
       domains=[Real, Real, RealPos])

mod_abs_of_difference_bound (conjecture without proof):

mod_abs_x_reduce_to_x = Forall((x, N),
       Equals(ModAbs(x, N), x),
       domains = [Real, RealPos],
       conditions=[number_ordering(LessEq(zero, x), LessEq(x, frac(N, two)))]
      )

mod_abs_x_reduce_to_x (conjecture without proof):

mod_abs_x_reduce_to_abs_x = Forall((x, N),
       Equals(ModAbs(x, N), Abs(x)),
       domains = [Real, RealPos],
       conditions=[LessEq(Abs(x), frac(N, two))]
      )

mod_abs_x_reduce_to_abs_x (conjecture without proof):

mod_abs_diff_reversal = Forall(
    (a, b, N), Equals(ModAbs(subtract(a, b), N), ModAbs(subtract(b, a), N)),
    domains = [Real, Real, RealPos])

mod_abs_diff_reversal (conjecture without proof):

bijective_interval_image_size = Forall(
    N, Forall(
        (a, b),
        Equals(Card(SetOfAll(x, Mod(x, N), domain=Interval(a, b))),
               Card(Interval(a, b))),
        condition=LessEq(Card(Interval(a, b)), N),
        domain=Integer),
    domain=NaturalPos)

bijective_interval_image_size (conjecture without proof):

image_size_indep_of_left_shift = Forall(
    L, Forall(
        S, Forall(
            c, Equals(Card(SetOfAll(x, Mod(Add(c, x), L), 
                                    domain=S)),
                      Card(SetOfAll(x, Mod(x, L), domain=S))),
            domain=Real),
        condition=SubsetEq(S, Real)),
    domain=Real)

image_size_indep_of_left_shift (conjecture without proof):

image_size_indep_of_right_shift = Forall(
    L, Forall(
        S, Forall(
            c, Equals(Card(SetOfAll(x, Mod(Add(x, c), L), 
                                    domain=S)),
                      Card(SetOfAll(x, Mod(x, L), domain=S))),
            domain=Real),
        condition=SubsetEq(S, Real)),
    domain=Real)

image_size_indep_of_right_shift (conjecture without proof):

complete_interval_image = Forall(
    N, Forall((a, b),
              Equals(SetOfAll(x, Mod(x, N), 
                              domain=Interval(a, b)),
                     Interval(zero, subtract(N, one))),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_image (conjecture without proof):

complete_interval_image_size = Forall(
    N, Forall((a, b),
              Equals(Card(SetOfAll(x, Mod(x, N), 
                                   domain=Interval(a, b))),
                     N),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_image_size (conjecture without proof):

complete_interval_left_shift_image = Forall(
    N, Forall((a, b, c),
              Equals(SetOfAll(x, Mod(Add(c, x), N), domain=Interval(a, b)),
                     Interval(zero, subtract(N, one))),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_left_shift_image (conjecture without proof):

complete_interval_left_shift_image_size = Forall(
    N, Forall((a, b, c),
              Equals(Card(SetOfAll(x, Mod(Add(c, x), N), domain=Interval(a, b))),
                     N),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_left_shift_image_size (conjecture without proof):

complete_interval_right_shift_image = Forall(
    N, Forall((a, b, c),
              Equals(SetOfAll(x, Mod(Add(x, c), N), domain=Interval(a, b)),
                     Interval(zero, subtract(N, one))),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_right_shift_image (conjecture without proof):

complete_interval_right_shift_image_size = Forall(
    N, Forall((a, b, c),
              Equals(Card(SetOfAll(x, Mod(Add(x, c), N), domain=Interval(a, b))),
                     N),
              domain=Integer,
              condition=greater_eq(Card(Interval(a, b)), N)),
    domain=NaturalPos)

complete_interval_right_shift_image_size (conjecture without proof):

interval_bijection = Forall(
    N, Forall(
        (a, b, c),
        InSet(Lambda(x, Mod(x, N)), 
              Bijections(Interval(a, b),
                         Interval(zero, subtract(N, one)))),
        domain=Integer),
    domain=NaturalPos)

interval_bijection (conjecture without proof):

interval_left_shift_bijection = Forall(
    N, Forall(
        (a, b, c),
        InSet(Lambda(x, Mod(Add(c, x), N)), 
              Bijections(Interval(a, b),
                         Interval(zero, subtract(N, one)))),
        domain=Integer),
    domain=NaturalPos)

interval_left_shift_bijection (conjecture without proof):

interval_right_shift_bijection = Forall(
    N, Forall(
        (a, b, c),
        InSet(Lambda(x, Mod(Add(x, c), N)), 
              Bijections(Interval(a, b),
                         Interval(zero, subtract(N, one)))),
        domain=Integer),
    domain=NaturalPos)

interval_right_shift_bijection (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.modular