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
Lemma ZO_div_pos:
forall a b, 0 <=
a -> 0 <=
b -> 0 <=
a/b.
As soon as the divisor is greater or equal than 2,
the division is strictly decreasing.
Lemma ZO_div_lt :
forall a b:Z, 0 <
a -> 2 <=
b ->
a/b <
a.
A division of a small number by a bigger one yields zero.
Theorem ZOdiv_small:
forall a b, 0 <=
a <
b ->
a/b = 0.
Same situation, in term of modulo:
Theorem ZOmod_small:
forall a n, 0 <=
a <
n ->
a mod n =
a.
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.
Theorem ZOmod_le:
forall a b, 0 <=
a -> 0 <=
b ->
a mod b <=
a.
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
Lemma ZO_mod_plus :
forall a b c:Z,
0 <= (
a+b*c) *
a ->
(
a +
b *
c)
mod c =
a mod c.
Lemma ZO_div_plus :
forall a b c:Z,
0 <= (
a+b*c) *
a ->
c<>0 ->
(
a +
b *
c) /
c =
a /
c +
b.
Theorem ZO_div_plus_l:
forall a b c :
Z,
0 <= (
a*b+c)*c ->
b<>0 ->
b<>0 -> (
a *
b +
c) /
b =
a +
c /
b.
Cancellations.
Operations modulo.
Theorem ZOmod_mod:
forall a n, (
a mod n)
mod n =
a mod n.
Theorem ZOmult_mod:
forall a b n,
(
a *
b)
mod n = ((
a mod n) * (
b mod n))
mod n.
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.
Theorem ZOplus_mod:
forall a b n,
0 <=
a *
b ->
(
a +
b)
mod n = (
a mod n +
b mod n)
mod n.
Lemma ZOplus_mod_idemp_l:
forall a b n,
0 <=
a *
b ->
(
a mod n +
b)
mod n = (
a +
b)
mod n.
Lemma ZOplus_mod_idemp_r:
forall a b n,
0 <=
a*b ->
(
b +
a mod n)
mod n = (
b +
a)
mod n.
Lemma ZOmult_mod_idemp_l:
forall a b n, (
a mod n *
b)
mod n = (
a *
b)
mod n.
Lemma ZOmult_mod_idemp_r:
forall a b n, (
b * (
a mod n))
mod n = (
b *
a)
mod n.
Unlike with Zdiv, the following result is true without restrictions.
A last inequality:
Theorem ZOdiv_mult_le:
forall a b c, 0<=a -> 0<=b -> 0<=c ->
c*(a/b) <= (
c*a)/b.
ZOmod is related to divisibility (see more in Znumtheory)
Lemma ZOmod_divides :
forall a b,
a mod b = 0 <->
exists c,
a =
b*c.
Interaction with "historic" Zdiv
They agree at least on positive numbers:
Modulos are null at the same places