Library Coq.Numbers.Integer.Abstract.ZDivEucl
Euclidean Division for integers, Euclid convention
We use here the "usual" formulation of the Euclid Theorem
forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b|
The outcome of the modulo function is hence always positive.
This corresponds to convention "E" in the following paper:
R. Boute, "The Euclidean definition of the functions div and mod",
ACM Transactions on Programming Languages and Systems,
Vol. 14, No.2, pp. 127-144, April 1992.
See files
ZDivTrunc and
ZDivFloor for others conventions.
We simply extend NZDiv with a bound for modulo that holds
regardless of the sign of a and b. This new specification
subsume mod_bound_pos, which nonetheless stays there for
subtyping. Note also that ZAxiomSig now already contain
a div and a modulo (that follow the Floor convention).
We just ignore them here.
We put notations in a scope, to avoid warnings about
redefinitions of notations
Another formulation of the main equation
Uniqueness theorems
Sign rules
Lemma div_opp_r :
forall a b,
b~=0
-> a/(-b) == -(a/b).
Lemma mod_opp_r :
forall a b,
b~=0
-> a mod (-b) == a mod b.
Lemma div_opp_l_z :
forall a b,
b~=0
-> a mod b == 0
->
(-a)/b == -(a/b).
Lemma div_opp_l_nz :
forall a b,
b~=0
-> a mod b ~= 0
->
(-a)/b == -(a/b)-sgn b.
Lemma mod_opp_l_z :
forall a b,
b~=0
-> a mod b == 0
->
(-a) mod b == 0.
Lemma mod_opp_l_nz :
forall a b,
b~=0
-> a mod b ~= 0
->
(-a) mod b == abs b - (a mod b).
Lemma div_opp_opp_z :
forall a b,
b~=0
-> a mod b == 0
->
(-a)/(-b) == a/b.
Lemma div_opp_opp_nz :
forall a b,
b~=0
-> a mod b ~= 0
->
(-a)/(-b) == a/b + sgn(
b).
Lemma mod_opp_opp_z :
forall a b,
b~=0
-> a mod b == 0
->
(-a) mod (-b) == 0.
Lemma mod_opp_opp_nz :
forall a b,
b~=0
-> a mod b ~= 0
->
(-a) mod (-b) == abs b - a mod b.
A division by itself returns 1
A division of a small number by a bigger one yields zero.
Same situation, in term of modulo:
Basic values of divisions and modulo.
Order results about mod and div
A modulo cannot grow beyond its starting point.
As soon as the divisor is strictly greater than 1,
the division is strictly decreasing.
le is compatible with a positive division.
In this convention,
div performs Rounding-Toward-Bottom
when divisor is positive, and Rounding-Toward-Top otherwise.
Since we cannot speak of rational values here, we express this
fact by multiplying back by
b, and this leads to a nice
unique statement.
Giving a reversed bound is slightly more complex
NB: The three previous properties could be used as
specifications for
div.
Inequality
mul_div_le is exact iff the modulo is zero.
Some additional inequalities about div.
A division respects opposite monotonicity for the divisor
Relations between usual operations and mod and div
Cancellations.
With the current convention, the following isn't always true
when
c<0:
-3*-1 / -2*-1 = 3/2 = 1 while
-3/-2 = 2
Operations modulo.
With the current convention, the following result isn't always
true with a negative intermediate divisor. For instance
3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) and
3/(-2)/2 = -1 <> 0 = 3 / (-2*2) .
Similarly, the following result doesn't always hold when b<0.
For instance 3 mod (-2*-2)) = 3 while
3 mod (-2) + (-2)*((3/-2) mod -2) = -1.
A last inequality:
mod is related to divisibility