Library Coq.ZArith.Zquot


Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.

Local Open Scope Z_scope.

This file provides results about the Round-Toward-Zero Euclidean division Zquotrem, whose projections are Zquot and Zrem. Definition of this division can be found in file BinIntDef.
This division and the one defined in Zdiv agree only on positive numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor).
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.

Relation between division on N and on Z.


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

Lemma Nmod_Zrem : forall a b:N,
  Z.of_N (a mod b) = Z.rem (Z.of_N a) (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.

Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).

Then, the inequalities constraining the remainder: The remainder is bounded by the divisor, in term of absolute values

Theorem Zrem_lt : forall a b:Z, b<>0 ->
  Z.abs (Z.rem a b) < Z.abs 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 Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.

This can also be said in a simplier way:

Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a.

Reformulation of Zquot_lt and Zrem_sgn in 2 then 4 particular cases.

Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.

Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.

Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.

Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.

Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.

Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.

Division and Opposite



Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b).

Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b).

Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b).

Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b.

Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b.

Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b).

Unicity results


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

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

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

Theorem Zquot_mod_unique_full:
 forall a b q r, Remainder a b r ->
   a = b*q + r -> q = a÷b /\ r = Z.rem a b.

Theorem Zquot_unique_full:
 forall a b q r, Remainder a b r ->
  a = b*q + r -> q = a÷b.

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

Theorem Zrem_unique_full:
 forall a b q r, Remainder a b r ->
  a = b*q + r -> r = Z.rem a b.

Theorem Zrem_unique:
 forall a b q r, 0 <= a -> 0 <= r < b ->
   a = b*q + r -> r = Z.rem a b.

Basic values of divisions and modulo.


Lemma Zrem_0_l: forall a, Z.rem 0 a = 0.

Lemma Zrem_0_r: forall a, Z.rem a 0 = a.

Lemma Zquot_0_l: forall a, 0÷a = 0.

Lemma Zquot_0_r: forall a, a÷0 = 0.

Lemma Zrem_1_r: forall a, Z.rem a 1 = 0.

Lemma Zquot_1_r: forall a, a÷1 = a.

Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r
 : zarith.

Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0.

Lemma Zrem_1_l: forall a, 1 < a -> Z.rem 1 a = 1.

Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1.

Ltac zero_or_not a :=
  destruct (Z.eq_dec a 0);
  [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r;
   auto with zarith|].

Lemma Z_rem_same : forall a, Z.rem a a = 0.

Lemma Z_rem_mult : forall a b, Z.rem (a*b) b = 0.

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

Order results about Zrem and Zquot



Lemma Z_quot_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 Z_quot_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 Zquot_small: forall a b, 0 <= a < b -> a÷b = 0.

Same situation, in term of modulo:

Theorem Zrem_small: forall a n, 0 <= a < n -> Z.rem a n = a.

Zge is compatible with a positive division.

Lemma Z_quot_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 Z_mult_quot_le : forall a b:Z, 0 <= a -> 0 <= b*(a÷b) <= a.

Lemma Z_mult_quot_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 Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Z.rem a b = 0.

A modulo cannot grow beyond its starting point.

Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Z.rem a b <= a.

Some additionnal inequalities about Zdiv.

Theorem Zquot_le_upper_bound:
  forall a b q, 0 < b -> a <= q*b -> a÷b <= q.

Theorem Zquot_lt_upper_bound:
  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q.

Theorem Zquot_le_lower_bound:
  forall a b q, 0 < b -> q*b <= a -> q <= a÷b.

Theorem Zquot_sgn: forall a b,
  0 <= Z.sgn (a÷b) * Z.sgn a * Z.sgn 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) rem 2 = -1 <> 1 = 9 rem 2

Lemma Z_rem_plus : forall a b c:Z,
 0 <= (a+b*c) * a ->
 Z.rem (a + b * c) c = Z.rem a c.

Lemma Z_quot_plus : forall a b c:Z,
 0 <= (a+b*c) * a -> c<>0 ->
 (a + b * c) ÷ c = a ÷ c + b.

Theorem Z_quot_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 Zquot_mult_cancel_r : forall a b c:Z,
 c<>0 -> (a*c)÷(b*c) = a÷b.

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

Lemma Zmult_rem_distr_l: forall a b c,
  Z.rem (c*a) (c*b) = c * (Z.rem a b).

Lemma Zmult_rem_distr_r: forall a b c,
  Z.rem (a*c) (b*c) = (Z.rem a b) * c.

Operations modulo.

Theorem Zrem_rem: forall a n, Z.rem (Z.rem a n) n = Z.rem a n.

Theorem Zmult_rem: forall a b n,
 Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n.

addition and modulo
Generally speaking, unlike with Zdiv, we don't have (a+b) rem n = (a rem n + b rem n) rem n for any a and b. For instance, take (8 + (-10)) rem 3 = -2 whereas (8 rem 3 + (-10 rem 3)) rem 3 = 1.

Theorem Zplus_rem: forall a b n,
 0 <= a * b ->
 Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n.

Lemma Zplus_rem_idemp_l: forall a b n,
 0 <= a * b ->
 Z.rem (Z.rem a n + b) n = Z.rem (a + b) n.

Lemma Zplus_rem_idemp_r: forall a b n,
 0 <= a*b ->
 Z.rem (b + Z.rem a n) n = Z.rem (b + a) n.

Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n.

Lemma Zmult_rem_idemp_r: forall a b n, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n.

Unlike with Zdiv, the following result is true without restrictions.

Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c).

A last inequality:

Theorem Zquot_mult_le:
 forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b.

Z.rem is related to divisibility (see more in Znumtheory)

Lemma Zrem_divides : forall a b,
 Z.rem a b = 0 <-> exists c, a = b*c.

Particular case : dividing by 2 is related with parity

Lemma Zquot2_odd_remainder : forall a,
 Remainder a 2 (if Z.odd a then Z.sgn a else 0).

Notation Zquot2_quot := Zquot2_quot (only parsing).

Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0.

Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a.

Lemma Zeven_rem : forall a, Z.even a = Zeq_bool (Z.rem a 2) 0.

Lemma Zodd_rem : forall a, Z.odd a = negb (Zeq_bool (Z.rem a 2) 0).

Interaction with "historic" Zdiv

They agree at least on positive numbers:

Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
  a÷b = a/b /\ Z.rem a b = a mod b.

Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
  a÷b = a/b.

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

Modulos are null at the same places

Theorem Zrem_Zmod_zero : forall a b, b<>0 ->
 (Z.rem a b = 0 <-> a mod b = 0).