Library Coq.ZArith.ZOdiv
This file provides results about the Round-Toward-Zero Euclidean
division ZOdiv_eucl, whose projections are ZOdiv and ZOmod.
Definition of this division can be found in file ZOdiv_def.
This division and the one defined in Zdiv agree only on positive
numbers. Otherwise, Zdiv performs Round-Toward-Bottom.
The current approach is compatible with the division of usual
programming languages such as Ocaml. In addition, it has nicer
properties with respect to opposite and other usual operations.
Since ZOdiv and Zdiv are not meant to be used concurrently,
we reuse the same notation.
Infix "/" :=
ZOdiv :
Z_scope.
Infix "mod" :=
ZOmod (
at level 40,
no associativity) :
Z_scope.
Infix "/" :=
Ndiv :
N_scope.
Infix "mod" :=
Nmod (
at level 40,
no associativity) :
N_scope.
Auxiliary results on the ad-hoc comparison NPgeb.
Relation between division on N and on Z.
Characterization of this euclidean division.
First, the usual equation a=q*b+r. Notice that a mod 0
has been chosen to be a, so this equation holds even for b=0.
Then, the inequalities constraining the remainder.
The remainder is bounded by the divisor, in term of absolute values
The sign of the remainder is the one of a. Due to the possible
nullity of a, a general result is to be stated in the following form:
This can also be said in a simplier way:
Reformulation of ZOdiv_lt and ZOmod_sgn in 2
then 4 particular cases.
Basic values of divisions and modulo.
Lemma ZOmod_0_l:
forall a, 0
mod a = 0.
Lemma ZOmod_0_r:
forall a,
a mod 0
= a.
Lemma ZOdiv_0_l:
forall a, 0
/a = 0.
Lemma ZOdiv_0_r:
forall a,
a/0
= 0.
Lemma ZOmod_1_r:
forall a,
a mod 1
= 0.
Lemma ZOdiv_1_r:
forall a,
a/1
= a.
Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r
:
zarith.
Lemma ZOdiv_1_l:
forall a, 1
< a -> 1
/a = 0.
Lemma ZOmod_1_l:
forall a, 1
< a -> 1
mod a = 1.
Lemma ZO_div_same :
forall a:
Z,
a<>0 ->
a/a = 1.
Lemma ZO_mod_same :
forall a,
a mod a = 0.
Lemma ZO_mod_mult :
forall a b,
(a*b) mod b = 0.
Lemma ZO_div_mult :
forall a b:
Z,
b <> 0 ->
(a*b)/b = a.
Order results about ZOmod and ZOdiv
As soon as the divisor is greater or equal than 2,
the division is strictly decreasing.
A division of a small number by a bigger one yields zero.
Same situation, in term of modulo:
Zge is compatible with a positive division.
With our choice of division, rounding of (a/b) is always done toward zero:
The previous inequalities between b*(a/b) and a are exact
iff the modulo is zero.
A modulo cannot grow beyond its starting point.
Some additionnal inequalities about Zdiv.
Relations between usual operations and Zmod and Zdiv
First, a result that used to be always valid with Zdiv,
but must be restricted here.
For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2
Cancellations.
Operations modulo.
addition and modulo
Generally speaking, unlike with Zdiv, we don't have
(a+b) mod n = (a mod n + b mod n) mod n
for any a and b.
For instance, take (8 + (-10)) mod 3 = -2 whereas
(8 mod 3 + (-10 mod 3)) mod 3 = 1.
Unlike with Zdiv, the following result is true without restrictions.
A last inequality:
ZOmod is related to divisibility (see more in Znumtheory)
Interaction with "historic" Zdiv
They agree at least on positive numbers:
Modulos are null at the same places