Library Coq.ZArith.ZOdiv


Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing.
Require Export ZOdiv_def.
Require Zdiv.

Open Scope Z_scope.

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.

Lemma NPgeb_Zge : forall (n:N)(p:positive),
  NPgeb n p = true -> Z_of_N n >= Zpos p.

Lemma NPgeb_Zlt : forall (n:N)(p:positive),
  NPgeb n p = false -> Z_of_N n < Zpos p.

Relation between division on N and on Z.


Lemma Ndiv_Z0div : forall a b:N,
  Z_of_N (a/b) = (Z_of_N a / Z_of_N b).

Lemma Nmod_Z0mod : forall a b:N,
  Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b).

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.

Theorem N_div_mod_eq : forall a b,
  a = (b * (Ndiv a b) + (Nmod a b))%N.

Theorem ZO_div_mod_eq : forall a b,
  a = b * (ZOdiv a b) + (ZOmod a b).

Then, the inequalities constraining the remainder.

Theorem Pdiv_eucl_remainder : forall a b:positive,
  Z_of_N (snd (Pdiv_eucl a b)) < Zpos b.

Theorem Nmod_lt : forall (a b:N), b<>0%N ->
  (a mod b < b)%N.

The remainder is bounded by the divisor, in term of absolute values

Theorem ZOmod_lt : forall a b:Z, b<>0 ->
  Zabs (a mod b) < Zabs b.

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:

Theorem ZOmod_sgn : forall a b:Z,
  0 <= Zsgn (a mod b) * Zsgn a.

This can also be said in a simplier way:

Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z.

Theorem ZOmod_sgn2 : forall a b:Z,
  0 <= (a mod b) * a.

Reformulation of ZOdiv_lt and ZOmod_sgn in 2 then 4 particular cases.

Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
  0 <= a mod b < Zabs b.

Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
  -Zabs b < a mod b <= 0.

Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b.

Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b.

Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0.

Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0.

Division and Opposite



Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b).

Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b).

Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b).

Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b.

Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.

Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b).

Unicity results


Definition Remainder a b r :=
  (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0).

Definition Remainder_alt a b r :=
  Zabs r < Zabs b /\ 0 <= r * a.

Lemma Remainder_equiv : forall a b r,
 Remainder a b r <-> Remainder_alt a b r.

Theorem ZOdiv_mod_unique_full:
 forall a b q r, Remainder a b r ->
   a = b*q + r -> q = a/b /\ r = a mod b.

Theorem ZOdiv_unique_full:
 forall a b q r, Remainder a b r ->
  a = b*q + r -> q = a/b.

Theorem ZOdiv_unique:
 forall a b q r, 0 <= a -> 0 <= r < b ->
   a = b*q + r -> q = a/b.

Theorem ZOmod_unique_full:
 forall a b q r, Remainder a b r ->
  a = b*q + r -> r = a mod b.

Theorem ZOmod_unique:
 forall a b q r, 0 <= a -> 0 <= r < b ->
   a = b*q + r -> r = a mod b.

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.

Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c.

Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c.

With our choice of division, rounding of (a/b) is always done toward zero:

Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a.

Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0.

The previous inequalities between b*(a/b) and a are exact iff the modulo is zero.

Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.

Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b).

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.

Theorem ZOdiv_le_upper_bound:
  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.

Theorem ZOdiv_lt_upper_bound:
  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.

Theorem ZOdiv_le_lower_bound:
  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.

Theorem ZOdiv_sgn: forall a b,
  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.

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.

Lemma ZOdiv_mult_cancel_r : forall a b c:Z,
 c<>0 -> (a*c)/(b*c) = a/b.

Lemma ZOdiv_mult_cancel_l : forall a b c:Z,
 c<>0 -> (c*a)/(c*b) = a/b.

Lemma ZOmult_mod_distr_l: forall a b c,
  (c*a) mod (c*b) = c * (a mod b).

Lemma ZOmult_mod_distr_r: forall a b c,
  (a*c) mod (b*c) = (a mod b) * c.

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.

Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c).

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:

Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
  a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b.

Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
  a/b = Zdiv.Zdiv a b.

Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
  a mod b = Zdiv.Zmod a b.

Modulos are null at the same places

Theorem ZOmod_Zmod_zero : forall a b, b<>0 ->
 (a mod b = 0 <-> Zdiv.Zmod a b = 0).