logo

Demonstrations for the theory of proveit.numbers.divisibility

In [1]:
import proveit
from proveit import defaults, free_vars, used_vars, ProofFailure
from proveit import a, b, c, n, x, y
from proveit.logic import Equals, InSet, NotEquals
from proveit.numbers import one, zero, two, three, four, five, six, Complex, Integer, NaturalPos
from proveit.numbers import Add, Divides, DividesProper, Exp, GCD, Mult
from proveit.numbers.divisibility  import divides_def
from proveit.numbers.divisibility import divides_is_bool
%begin demonstrations

Divisibility (Divides) $x\rvert y$ and Greatest Common Divisor (GCD)

Introduction

Divisibility of one number by another is a common concern throughout various fields of mathematics $\dots$ The notation $x\rvert y$, read as “x divides y,” indicates that $x$ is a factor of $y$, or $y$ is a multiple of $x$, and is often defined as meaning there exists some integer $k$ such that $y=kx$. As we'll see further below in the section on axioms, in Prove-It we define $x\rvert y$ as meaning that $\frac{y}{x} \in \mathbb{Z}$. This ``_demonstrations_`` notebook explores $x\rvert y$ expressions and related methods.

Simple Expressions Involving the Divides Class $x\rvert y$

Expressions involving divisibility claims are easy to construct using the Divides() class. Here are some basic examples of such expressions:

In [2]:
# a simple divisibility claim
Divides(x, y)
In [3]:
# some other examples, some true, some false, some indeterminant
example_1, example_2, example_3, example_4, example_5 = (
    Divides(two, four), Divides(x, x), Divides(a, Add(b, c)),
    Divides(six, three), Divides(x, Mult(x,y)))
example_1:
example_2:
example_3:
example_4:
example_5:

Common Attributes of a Subset expression

Consider ``example_5`` from above, $x\rvert(xy)$, which is true for all $x\ne 0$, and look at some of its attributes.

We can look at the construction of such an expression by calling expr_info() to see the tabular representation of the expression's underlying directed acyclic graph (DAG) representation:</font>

In [4]:
example_5.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple6, 3
3Operationoperator: 4
operands: 5
4Literal
5ExprTuple6, 7
6Variable
7Variable

We can access the left-hand and right-hand sides of such expressions in terms of operands:

In [5]:
example_5.operands
In [6]:
example_5.operands[0]
In [7]:
example_5.operands[1]

We can access the “divides” operator itself:

In [8]:
example_5.operator

If and when needed, we can check for an expression being an instance of the Divides class:

In [9]:
isinstance(example_5, Divides)

True

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

In [10]:
used_vars(example_5)
In [11]:
free_vars(example_5)

Axioms

Currently there is a single ``axiom`` for the divisibility theory, establishing the basic definition for $x\rvert y$ (see [divisibility axioms](./_axioms_.ipynb) page.) for updates).

In [12]:
# def of x|y
divides_def
 ⊢  

Divisibility $x\rvert y$ involving non-zero integers $x$ and $y$ is often defined as $(x\rvert y) = \exists_{k\in\mathbb{Z}}[y = kx]$. The axiomatic definition shown above is essentially the same, implicitly disallowing $x=0$ by the nature of the fraction $\frac{y}{x}$, but also allowing $y=0$.

Theorems & Conjectures

The `number/divisbility` theory has a handful of related theorems and conjectures established, with a number of other possibilities still open for development. Some illustrative examples of the theorems are shown below, and the remainder can be found in the [divisibility theorems notebook](./\_theorems\_.ipynb).

In [13]:
from proveit.numbers.divisibility import (
        divides_is_bool, divides_transitivity, divides_reflexivity,
        divides_anti_symmetry, euclids_lemma, divides_sum, non_zero_divides_zero)
In [14]:
# divisibility claims are Boolean
divides_is_bool
 ⊢  
In [15]:
# divisbility is transitive
divides_transitivity
 ⊢  
In [16]:
# divisbility is reflexive
divides_reflexivity
 ⊢  
In [17]:
# divisbility manifests a form of antisymmetry
divides_anti_symmetry
 ⊢  
In [18]:
# when dealing with integers, we can make some important claims
euclids_lemma
 ⊢  
In [19]:
# divisibility across sums of divisible pieces
divides_sum
 ⊢  
In [20]:
# everything (non-zero) divides zero
non_zero_divides_zero
 ⊢  

Demonstrations

1. TBA.

TBA

2. TBA.

TBA

3. TBA.

TBA

Miscellaneous Testing

The material below was developed to test various divisbility-related methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.

In [21]:
divides_is_bool
 ⊢  
In [22]:
# notice that .instance_params and .instance_vars often appear to
# provide the same information for the quantified params/vars:
# really the correct thing
params_example, vars_example = (
    divides_is_bool.instance_params,
    divides_is_bool.instance_vars)
params_example:
vars_example:
In [23]:
# But when we have ranges of params like A1 … An
# instance_vars would give A (used more commonly for internal stuff)
# while instance_params would give A1 … An, and is typically what we want
from proveit.logic import Forall
from proveit.core_expr_types import (a_1_to_i, a_1_to_m, b_1_to_j, b_1_to_n,
                                              c_1_to_j, c_1_to_k, c_1_to_n,
                                              d_1_to_k, y_1_to_n)
example_forall = Forall(a_1_to_i, x)
example_forall:
In [24]:
params_example, vars_example = (
    example_forall.instance_params,
    example_forall.instance_var_or_vars)
params_example:
vars_example:
In [25]:
two_divides_four = Divides(two, four)
two_divides_four:
In [26]:
two_divides_four.operands
In [27]:
two_divides_four.lhs
In [28]:
two_divides_four.deduce_in_bool()
 ⊢  
In [29]:
two_divides_four_proper = DividesProper(two, four)
two_divides_four_proper:
In [30]:
InSet(x, Complex).proven(assumptions=[InSet(x, Complex)])

True
In [31]:
Divides(x, x).conclude(assumptions=[InSet(x, Complex), NotEquals(x, zero)])
,  ⊢  
In [32]:
try:
    Divides(two, two).conclude()
except ProofFailure as e:
    print("Proof Failure: {}".format(e))
In [33]:
InSet(two, Complex).prove()
 ⊢  
In [34]:
NotEquals(two, zero).prove()
 ⊢  
In [35]:
Divides(two, two).conclude()
 ⊢  
In [36]:
Divides(two, two).proven()

True
In [37]:
two_divides_zero = Divides(two, zero)
two_divides_zero:
In [38]:
two_divides_zero.conclude()
 ⊢  
In [39]:
Divides(x, zero).conclude(assumptions=[InSet(x, Complex), NotEquals(x, zero)])
,  ⊢  

Equality in Divides.conclude() (x|x)

In [40]:
# testing general Divide.conclude() method with x|x where we
# have no information about x
try:
    Divides(x, x).conclude()
except Exception as e:
    print("Exception! {0}".format(e))

Exception! Unable to prove x | x:
In Divides.conclude() we tried:
Case: lhs = rhs. Although lhs = rhs = x, either x is not known to be non-zero or x is not known to be in the complex numbers (or both). Try proving one or both of those claims first.
Case: x|xy. This possible case returned the following error message: conclude_via_factor only applies for an explicit Mult expression on the rhs of the Divides, but received x on the right side. 
Case: (x^n) | (y^n). Does not appear applicable.
Case: transitivity search. In attempting to use conclude_via_transitivity(), obtained the following error message: 'Divides' object has no attribute 'conclude_via_equality'.
In [41]:
# testing general Divide.conclude() method with x|x where we
# now have sufficient information about x
Divides(x, x).conclude(assumptions=[NotEquals(x, zero), InSet(x, Complex)])
,  ⊢  

x|xy in Divides.conclude_via_factor() (which is then used in the Divides.conclude() method

In [42]:
# Divides(x, Mult(x, y)).conclude_via_factor(assumptions=[InSet(x, Integer), InSet(y, Integer), NotEquals(x, zero)])
In [43]:
# Divides(x, Mult(y, x)).conclude_via_factor(assumptions=[InSet(x, Integer), InSet(y, Integer), NotEquals(x, zero)])
In [44]:
Divides(x, Mult(x, y)).conclude(assumptions=[InSet(x, Integer), InSet(y, Integer), NotEquals(x, zero)])
, ,  ⊢  

Transitivity in Divides.conclude()

Using Divides.conclude() to indirectly utilize transitivity, given the right assumptions:

In [45]:
Divides(x, y).conclude(assumptions=[Divides(x, a), Divides(a, y)])
,  ⊢  
In [46]:
defaults.assumptions = [Divides(x, a), Divides(a, y)]
defaults.assumptions:
In [47]:
Divides(x, y).conclude()
,  ⊢  

Divisibility called from the Mult class?

In [48]:
Mult(two, three).deduce_divided_by(two, auto_simplify=False)
 ⊢  
In [49]:
Mult(two, three).deduce_divided_by(two)
 ⊢  
In [50]:
Mult(two, three).deduce_divided_by(three, auto_simplify=False)
 ⊢  
In [51]:
Mult(two, three).deduce_divided_by(three)
 ⊢  
In [52]:
# Then a case where the divisibility is clearly not true:
try:
    Mult(two, three).deduce_divided_by(four)
except Exception as e:
    print("Exception! {0}".format(e))

Exception! In Mult(2, 3).deduce_divided_by(4), the supplied divisor 4 does not appear to be equal to either of the multiplicands 2 or 3.

Testing Divides.eliminate_common_factor()

In [53]:
Divides(Mult(two, three), Mult(two, five)).prove(assumptions=[Divides(Mult(two, three), Mult(two, five))])
 ⊢  
In [54]:
Divides(Mult(two, three), Mult(two, five)).eliminate_common_factors(assumptions=[Divides(Mult(two, three), Mult(two, five))])
 ⊢  
In [55]:
Divides(Mult(two, three, four), Mult(two, four, five)).eliminate_common_factors(
    assumptions=[Divides(Mult(two, three, four), Mult(two, four, five))])
 ⊢  

Testing Divides side_effects

In [56]:
Divides(two, Mult(two, Exp(two, two))).conclude(assumptions=[InSet(Exp(two, two), Integer)])
 ⊢  
In [57]:
Divides(Exp(x, n), Exp(y,n)).prove(
    assumptions=[Divides(Exp(x, n), Exp(y,n)), InSet(x, Integer), InSet(y, Integer), InSet(n, NaturalPos)])
 ⊢  
In [58]:
from proveit.numbers.divisibility import common_factor_elimination
common_factor_elimination
 ⊢  
In [59]:
Divides(x, y).prove(
    assumptions=[Divides(Exp(x, two), Exp(y,two)), InSet(x, Integer), InSet(y, Integer)])
, ,  ⊢  
In [60]:
Divides(Mult(two, x), Mult(two, y)).prove(assumptions=[Divides(Mult(two, x), Mult(two, y))])
 ⊢  
In [61]:
Divides(x, y).prove()
,  ⊢  
In [62]:
# Divides(x, y).prove(
#     assumptions=[Divides(Mult(two, x), Mult(two, y)), InSet(x, Integer), InSet(y, Integer)])

GCD

In [63]:
GCD(x, y)
In [64]:
GCD(x, y).operands

GCD.deduce_relatively_prime()

In [65]:
try:
    GCD(x, y).deduce_relatively_prime()
except Exception as e:
    print("Exception! {0}".format(e))

Exception! Proof step failed assuming {x | a, a | y}:
Attempting to instantiate |- forall_{a, b in NaturalPos | gcd(a, b) = 1} [forall_{p in NaturalPos | p > 1} [not]((p | a) and (p | b))] with {a: x, b: y}:
Unsatisfied condition: x in NaturalPos. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [66]:
GCD(x, y).deduce_relatively_prime(
    assumptions=[Equals(GCD(x,y), one), InSet(x, NaturalPos), InSet(y, NaturalPos)])
, ,  ⊢  
In [67]:
%end demonstrations