logo

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