Library Coq.ZArith.Zdiv
Euclidean Division
Defines first of function that allows Coq to normalize.
Then only after proves the main required property.
Definitions of Euclidian operations
Euclidean division of a positive by a integer
(that is supposed to be positive).
Total function than returns an arbitrary value when
divisor is not positive
Euclidean division of integers.
Total function than returns (0,0) when dividing by 0.
The pseudo-code is:
if b = 0 : (0,0)
if b <> 0 and a = 0 : (0,0)
if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in
if r = 0 then (-q,0) else (-(q+1),b-r)
if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)
if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in
if r = 0 then (-q,0) else (-(q+1),b+r)
In other word, when b is non-zero, q is chosen to be the greatest integer
smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when
r is not null).
Definition Zdiv_eucl (
a b:Z) :
Z *
Z :=
match a,
b with
|
Z0,
_ => (0, 0)
|
_,
Z0 => (0, 0)
|
Zpos a',
Zpos _ =>
Zdiv_eucl_POS a' b
|
Zneg a',
Zpos _ =>
let (
q,
r) :=
Zdiv_eucl_POS a' b in
match r with
|
Z0 => (-
q, 0)
|
_ => (- (
q + 1),
b -
r)
end
|
Zneg a',
Zneg b' =>
let (
q,
r) :=
Zdiv_eucl_POS a' (
Zpos b')
in (
q, -
r)
|
Zpos a',
Zneg b' =>
let (
q,
r) :=
Zdiv_eucl_POS a' (
Zpos b')
in
match r with
|
Z0 => (-
q, 0)
|
_ => (- (
q + 1),
b +
r)
end
end.
Division and modulo are projections of Zdiv_eucl
Syntax
Infix "/" :=
Zdiv :
Z_scope.
Infix "mod" :=
Zmod (
at level 40,
no associativity) :
Z_scope.
First a lemma for two positive arguments
Then the usual situation of a positive b and no restriction on a
Theorem Z_div_mod :
forall a b:Z,
b > 0 ->
let (
q,
r) :=
Zdiv_eucl a b in a =
b *
q +
r /\ 0 <=
r <
b.
For stating the fully general result, let's give a short name
to the condition on the remainder.
Definition Remainder r b := 0 <=
r <
b \/
b <
r <= 0.
Another equivalent formulation:
Now comes the fully general result about Euclidean division.
The same results as before, stated separately in terms of Zdiv and Zmod
Lemma Z_mod_remainder :
forall a b:Z,
b<>0 ->
Remainder (
a mod b)
b.
Lemma Z_mod_lt :
forall a b:Z,
b > 0 -> 0 <=
a mod b <
b.
Lemma Z_mod_neg :
forall a b:Z,
b < 0 ->
b <
a mod b <= 0.
Lemma Z_div_mod_eq_full :
forall a b:Z,
b <> 0 ->
a =
b*(a/b) + (
a mod b).
Lemma Z_div_mod_eq :
forall a b:Z,
b > 0 ->
a =
b*(a/b) + (
a mod b).
Lemma Zmod_eq_full :
forall a b:Z,
b<>0 ->
a mod b =
a - (
a/b)*b.
Lemma Zmod_eq :
forall a b:Z,
b>0 ->
a mod b =
a - (
a/b)*b.
Existence theorem
Uniqueness theorems
Basic values of divisions and modulo.
Lemma Zmod_0_l:
forall a, 0
mod a = 0.
Lemma Zmod_0_r:
forall a,
a mod 0 = 0.
Lemma Zdiv_0_l:
forall a, 0/a = 0.
Lemma Zdiv_0_r:
forall a,
a/0 = 0.
Lemma Zmod_1_r:
forall a,
a mod 1 = 0.
Lemma Zdiv_1_r:
forall a,
a/1 =
a.
Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
:
zarith.
Lemma Zdiv_1_l:
forall a, 1 <
a -> 1/a = 0.
Lemma Zmod_1_l:
forall a, 1 <
a -> 1
mod a = 1.
Lemma Z_div_same_full :
forall a:Z,
a<>0 ->
a/a = 1.
Lemma Z_mod_same_full :
forall a,
a mod a = 0.
Lemma Z_mod_mult :
forall a b, (
a*b)
mod b = 0.
Lemma Z_div_mult_full :
forall a b:Z,
b <> 0 -> (
a*b)/b =
a.
Order results about Zmod and Zdiv
Lemma Z_div_pos:
forall a b,
b > 0 -> 0 <=
a -> 0 <=
a/b.
Lemma Z_div_ge0:
forall a b,
b > 0 ->
a >= 0 ->
a/b >=0.
As soon as the divisor is greater or equal than 2,
the division is strictly decreasing.
Lemma Z_div_lt :
forall a b:Z,
b >= 2 ->
a > 0 ->
a/b <
a.
A division of a small number by a bigger one yields zero.
Theorem Zdiv_small:
forall a b, 0 <=
a <
b ->
a/b = 0.
Same situation, in term of modulo:
Theorem Zmod_small:
forall a n, 0 <=
a <
n ->
a mod n =
a.
Zge is compatible with a positive division.
Lemma Z_div_ge :
forall a b c:Z,
c > 0 ->
a >=
b ->
a/c >=
b/c.
Same, with Zle.
Lemma Z_div_le :
forall a b c:Z,
c > 0 ->
a <=
b ->
a/c <=
b/c.
With our choice of division, rounding of (a/b) is always done toward bottom:
The previous inequalities are exact iff the modulo is zero.
A modulo cannot grow beyond its starting point.
Theorem Zmod_le:
forall a b, 0 <
b -> 0 <=
a ->
a mod b <=
a.
Some additionnal inequalities about Zdiv.
A division of respect opposite monotonicity for the divisor
Relations between usual operations and Zmod and Zdiv
Zopp and Zdiv, Zmod.
Due to the choice of convention for our Euclidean division,
some of the relations about Zopp and divisions are rather complex.
Lemma Zdiv_opp_opp :
forall a b:Z, (-a)/(-b) =
a/b.
Lemma Zmod_opp_opp :
forall a b:Z, (-a)
mod (-b) = - (
a mod b).
Lemma Z_mod_zero_opp_full :
forall a b:Z,
a mod b = 0 -> (-a)
mod b = 0.
Lemma Z_mod_nz_opp_full :
forall a b:Z,
a mod b <> 0 ->
(-a)
mod b =
b - (
a mod b).
Lemma Z_mod_zero_opp_r :
forall a b:Z,
a mod b = 0 ->
a mod (-b) = 0.
Lemma Z_mod_nz_opp_r :
forall a b:Z,
a mod b <> 0 ->
a mod (-b) = (
a mod b) -
b.
Lemma Z_div_zero_opp_full :
forall a b:Z,
a mod b = 0 -> (-a)/b = -(a/b).
Lemma Z_div_nz_opp_full :
forall a b:Z,
a mod b <> 0 ->
(-a)/b = -(a/b)-1.
Lemma Z_div_zero_opp_r :
forall a b:Z,
a mod b = 0 ->
a/(-b) = -(a/b).
Lemma Z_div_nz_opp_r :
forall a b:Z,
a mod b <> 0 ->
a/(-b) = -(a/b)-1.
Cancellations.
Operations modulo.
Theorem Zmod_mod:
forall a n, (
a mod n)
mod n =
a mod n.
Theorem Zmult_mod:
forall a b n,
(
a *
b)
mod n = ((
a mod n) * (
b mod n))
mod n.
Theorem Zplus_mod:
forall a b n,
(
a +
b)
mod n = (
a mod n +
b mod n)
mod n.
Theorem Zminus_mod:
forall a b n,
(
a -
b)
mod n = (
a mod n -
b mod n)
mod n.
Lemma Zplus_mod_idemp_l:
forall a b n, (
a mod n +
b)
mod n = (
a +
b)
mod n.
Lemma Zplus_mod_idemp_r:
forall a b n, (
b +
a mod n)
mod n = (
b +
a)
mod n.
Lemma Zminus_mod_idemp_l:
forall a b n, (
a mod n -
b)
mod n = (
a -
b)
mod n.
Lemma Zminus_mod_idemp_r:
forall a b n, (
a -
b mod n)
mod n = (
a -
b)
mod n.
Lemma Zmult_mod_idemp_l:
forall a b n, (
a mod n *
b)
mod n = (
a *
b)
mod n.
Lemma Zmult_mod_idemp_r:
forall a b n, (
b * (
a mod n))
mod n = (
b *
a)
mod n.
For a specific number N, equality modulo N is hence a nice setoid
equivalence, compatible with +, - and *.
Definition eqm N a b := (
a mod N =
b mod N).
Lemma eqm_refl N :
forall a, (
eqm N)
a a.
Lemma eqm_sym N :
forall a b, (
eqm N)
a b -> (
eqm N)
b a.
Lemma eqm_trans N :
forall a b c,
(
eqm N)
a b -> (
eqm N)
b c -> (
eqm N)
a c.
Add Parametric Relation N :
Z (
eqm N)
reflexivity proved by (
eqm_refl N)
symmetry proved by (
eqm_sym N)
transitivity proved by (
eqm_trans N)
as eqm_setoid.
Add Parametric Morphism N :
Zplus
with signature (
eqm N) ==> (
eqm N) ==> (
eqm N)
as Zplus_eqm.
Add Parametric Morphism N :
Zminus
with signature (
eqm N) ==> (
eqm N) ==> (
eqm N)
as Zminus_eqm.
Add Parametric Morphism N :
Zmult
with signature (
eqm N) ==> (
eqm N) ==> (
eqm N)
as Zmult_eqm.
Add Parametric Morphism N :
Zopp
with signature (
eqm N) ==> (
eqm N)
as Zopp_eqm.
Lemma Zmod_eqm N :
forall a, (
eqm N) (
a mod N)
a.
Lemma Zdiv_Zdiv :
forall a b c, 0<=b -> 0<=c -> (
a/b)/c =
a/(b*c).
Unfortunately, the previous result isn't always true on negative numbers.
For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2)
A last inequality:
Theorem Zdiv_mult_le:
forall a b c, 0<=a -> 0<=b -> 0<=c ->
c*(a/b) <= (
c*a)/b.
Zmod is related to divisibility (see more in Znumtheory)
Lemma Zmod_divides :
forall a b,
b<>0 ->
(
a mod b = 0 <->
exists c,
a =
b*c).
Weaker results kept only for compatibility
Lemma Z_mod_same :
forall a,
a > 0 ->
a mod a = 0.
Lemma Z_div_same :
forall a,
a > 0 ->
a/a = 1.
Lemma Z_div_plus :
forall a b c:Z,
c > 0 -> (
a +
b *
c) /
c =
a /
c +
b.
Lemma Z_div_mult :
forall a b:Z,
b > 0 -> (
a*b)/b =
a.
Lemma Z_mod_plus :
forall a b c:Z,
c > 0 -> (
a +
b *
c)
mod c =
a mod c.
Lemma Z_div_exact_1 :
forall a b:Z,
b > 0 ->
a =
b*(a/b) ->
a mod b = 0.
Lemma Z_div_exact_2 :
forall a b:Z,
b > 0 ->
a mod b = 0 ->
a =
b*(a/b).
Lemma Z_mod_zero_opp :
forall a b:Z,
b > 0 ->
a mod b = 0 -> (-a)
mod b = 0.
A direct way to compute Zmod
Another convention is possible for division by negative numbers:
quotient is always the biggest integer smaller than or equal to a/b
remainder is hence always positive or null.
A third convention: Ocaml.
See files ZOdiv_def.v and ZOdiv.v.
Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b).
Hence (-a) mod b = - (a mod b)
a mod (-b) = a mod b
And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b).