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

In [1]:
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

In [2]:
%begin theorems

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

In [3]:
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):

In [4]:
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):

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

mod_int_closure (conjecture without proof):

In [6]:
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):

In [7]:
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):

In [8]:
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):

In [9]:
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):

In [10]:
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):

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

mod_real_closure (conjecture without proof):

In [12]:
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):

In [13]:
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):

In [14]:
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):

In [15]:
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):

In [16]:
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):

In [17]:
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):

In [18]:
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):

In [19]:
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):

In [20]:
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}$.

In [21]:
redundant_mod_elimination = Forall(
(a, b), Equals(Mod(Mod(a, b), b), Mod(a, b)),
domains=(Real, RealPos))

redundant_mod_elimination (conjecture without proof):

In [22]:
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),
domain=RealPos),
domain=Real),
domain=Natural)

redundant_mod_elimination_in_sum (conjecture without proof):

In [23]:
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):

In [24]:
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),
domain=RealPos),
domain=Real),
domain=Natural)

redundant_mod_elimination_in_sum_in_modabs (conjecture without proof):

In [25]:
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):

In [26]:
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):

In [27]:
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):

In [28]:
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):

In [29]:
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):

In [30]:
image_size_indep_of_left_shift = Forall(
L, Forall(
S, Forall(
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):

In [31]:
image_size_indep_of_right_shift = Forall(
L, Forall(
S, Forall(
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):

In [32]:
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):

In [33]:
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):

In [34]:
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):

In [35]:
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):

In [36]:
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):

In [37]:
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):

In [38]:
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):

In [39]:
interval_left_shift_bijection = Forall(
N, Forall(
(a, b, c),
Bijections(Interval(a, b),
Interval(zero, subtract(N, one)))),
domain=Integer),
domain=NaturalPos)

interval_left_shift_bijection (conjecture without proof):

In [40]:
interval_right_shift_bijection = Forall(
N, Forall(
(a, b, c),

%end theorems

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