# Demonstrations for the theory of proveit.numbers.modular¶

In [1]:
import proveit
from proveit import a, b, c, d, x, L
from proveit.logic import Equals, InSet
from proveit.numbers import NaturalPos, Real, RealPos, Interval, IntervalCO
from proveit.numbers import Abs, Add, ModAbs, Mod, subtract, one, zero
%begin demonstrations


# Modular Arithmetic $a \thinspace\text{mod}\thinspace b$, $|a|_{\text{mod}\thinspace b}$¶

## Introduction [under construction] ¶

Some introductory comments here about the importance of modular arithmetic and its representation within Prove-It.

## Simple Expressions Involving Modular Arithmetic ($a \thinspace\text{mod}\thinspace b$ or $|a| \thinspace\text{mod}\thinspace b$)¶

It is straightforward to construct modular arithmetic expressions and absolute value expressions. Here are some basic examples of such expressions:

In [2]:
# basic modular expression
Mod(a, b)

In [3]:
# basic ModAbs expression
ModAbs(a, b)


## Common Attributes of a Mod Expression ¶

Let's define a simple Mod expression, $(a+b) \thinspace\text{mod}\thinspace c$, and look at some of its attributes.

In [4]:
a_plus_b_mod_c = Mod(Add(a, b), c)

a_plus_b_mod_c:
In [5]:
a_mod_b = Mod(a, b)

a_mod_b:

We can use the expr_info() method to look at the how our mod expression is structured:

In [6]:
a_plus_b_mod_c.expr_info()

core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Operationoperator: 5
operands: 6
4Variable
5Literal
6ExprTuple7, 8
7Variable
8Variable

The operator for a Mod expression is simply the mod string:

In [7]:
a_plus_b_mod_c.operator


We can get a tuple of the operands and a list of the variables. We can also get a separate list of the *free* variables in the expression (of course, in this expression, all the variables are also free variables):

In [8]:
a_plus_b_mod_c.operands

In [9]:
from proveit import used_vars, free_vars
used_vars(a_plus_b_mod_c)

In [10]:
free_vars(a_mod_b)


We can replace selected variables in our expression with other variables:

In [11]:
a_plus_b_mod_c.basic_replaced({a:d})


And if needed we can reach down further into the expression to extract and manipulate specific pieces of the expression:

In [12]:
new = a_plus_b_mod_c.operands[0].basic_replaced({a:d})

new:

## Axioms ¶

The axioms for modular arithmetic …

## Demonstrations ¶

1. TBA.

We begin with some simple expressions ….

2. TBA.

3. TBA.

## Simplifications¶

In [13]:
Mod(x, L).simplification(assumptions=[InSet(L, NaturalPos), InSet(x, Interval(zero, subtract(L, one)))])

In [14]:
Mod(x, L).simplification(assumptions=[InSet(L, RealPos), InSet(x, IntervalCO(zero, L))])

In [15]:
Mod(Mod(x, L), L).simplification(assumptions=[InSet(L, RealPos), InSet(x, Real)])

In [16]:
ModAbs(Mod(x, L), L).simplification(assumptions=[InSet(L, RealPos), InSet(x, Real)])


## Misc Testing ¶

Some temporary testing while the modular theory and demonstrations page are developed (this material can be deleted later once the demonstrations page is more established).

Testing Mod.deduce_in_number_set() method for constants and variables.

In [17]:
from proveit.logic import InSet, NotEquals
from proveit.numbers import zero, two, three, Integer, Natural, NaturalPos, Real

In [18]:
three_mod_two = Mod(three, two)

three_mod_two:
In [19]:
a_mod_b = Mod(a, b)

a_mod_b:

Testing Mod.deduce_in_interval() method.

In [20]:
three_mod_two.deduce_in_interval()

In [21]:
a_mod_b.deduce_in_interval(
assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢

Testing Mod.deduce_in_number_set() method.

In [22]:
# deduce that int mod int is in the Integer set
three_mod_two.deduce_in_number_set(Integer)

In [23]:
# deduce that int mod int is in the Integer set
a_mod_b.deduce_in_number_set(
Integer,
assumptions=[InSet(a, Integer), InSet(b, Integer), NotEquals(b, zero)])

, ,  ⊢
In [24]:
# deduce that int mod int is in the Natural set
three_mod_two.deduce_in_number_set(Natural)

In [25]:
# deduce that int mod int is in the Real set
three_mod_two.deduce_in_number_set(Real)

In [26]:
# deduce that int mod int is in the Real set
a_mod_b.deduce_in_number_set(
Real,
assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [27]:
# What happens if we try to deduce into an incorrect set?
try:
three_mod_two.deduce_in_number_set(NaturalPos)
except Exception as e:
print("EXCEPTION: ", e)

EXCEPTION:  'Mod.deduce_in_number_set()' not implemented for the NaturalPos set


Testing ModAbs methods.

In [28]:
abs_three_mod_two = ModAbs(three, two)

abs_three_mod_two:
In [29]:
abs_a_mod_b = ModAbs(a, b)

abs_a_mod_b:
In [30]:
str(abs_three_mod_two)

'|3|_{mod 2}'
In [31]:
abs_three_mod_two.deduce_in_number_set(Integer)

In [32]:
abs_three_mod_two.deduce_in_number_set(Real)

In [33]:
# what happens if we try to deduce into an incorrect set?
try:
abs_three_mod_two.deduce_in_number_set(Natural)
except Exception as the_exception:
print("EXCEPTION: ", the_exception)

EXCEPTION:  'ModAbs.deduce_in_number_set()' not implemented for the Natural set


Set some temporary assumptions for testing ModAbs methods:

In [34]:
from proveit import a, b, N
from proveit.numbers import Abs, Div, LessEq, subtract
temp_assumptions = [InSet(a, Real), InSet(b, Real), InSet(N, RealPos)]

temp_assumptions:

#### ModAbs.difference_reversal()¶

In [35]:
ModAbs(subtract(a, b), N).difference_reversal(assumptions=temp_assumptions)

, ,  ⊢

#### Some simplification examples: removing redundant mods and removing abs¶

In [36]:
# actually this is still an oversight; should do something like
# |(|a| mod N)| mod N = |a| mod N (I think)
ModAbs(Add(ModAbs(a, N), b), N).simplification()

In [37]:
ModAbs(Add(Mod(a, N), b), N).simplification(assumptions=temp_assumptions)

, ,  ⊢
In [38]:
ModAbs(Add(Mod(a, N), b), N).simplification(
assumptions=temp_assumptions+[LessEq(Abs(Add(a, b)), Div(N, two))])

, , ,  ⊢
In [39]:
ModAbs(Add(a, b), N).simplification(
assumptions=temp_assumptions+[LessEq(Abs(Add(a, b)), Div(N, two))])

, , ,  ⊢

The following example eliminates a redundant (mod N) inside, then eliminates the unnecessary (mod N) outside, and finally eliminates the absolute value altogether:

In [40]:
from proveit.numbers import greater
ModAbs(Add(Mod(a, N), b), N).simplification(
assumptions=(
temp_assumptions+
[LessEq(Abs(Add(a, b)), Div(N, two)), greater(Add(a, b), zero)]))

, , , ,  ⊢
In [41]:
%end demonstrations