Library Coq.ZArith.Zdiv




Euclidean Division

Defines first of function that allows Coq to normalize. Then only after proves the main required property.

Require Export ZArith_base.
Require Import Zbool.
Require Import Omega.
Require Import ZArithRing.
Require Import Zcomplements.
Require Export Setoid.
Open Local Scope Z_scope.

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

Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q.

Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r.

Syntax

Infix "/" := Zdiv : Z_scope.
Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.


Main division theorem


First a lemma for two positive arguments

Lemma Z_div_mod_POS :
  forall b:Z,
    b > 0 ->
    forall a:positive,
      let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b.

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:

Definition Remainder_alt r b := Zabs r < Zabs b /\ Zsgn r <> - Zsgn b.


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

Hint Unfold Remainder.

Now comes the fully general result about Euclidean division.

Theorem Z_div_mod_full :
  forall a b:Z,
    b <> 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ Remainder r b.

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

Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z),
 {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.

Implicit Arguments Zdiv_eucl_exist.

Uniqueness theorems

Theorem Zdiv_mod_unique :
 forall b q1 q2 r1 r2:Z,
  0 <= r1 < Zabs b -> 0 <= r2 < Zabs b ->
  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.

Theorem Zdiv_mod_unique_2 :
 forall b q1 q2 r1 r2:Z,
  Remainder r1 b -> Remainder r2 b ->
  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.

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

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

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

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

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:

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

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

The previous inequalities are exact iff the modulo is zero.

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

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

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.

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

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

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

A division of respect opposite monotonicity for the divisor

Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
    p / r <= p / q.

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

Relations between usual operations and Zmod and Zdiv


Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.

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

Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.

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.

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

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

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

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

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).

Compatibility


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


Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z :=
  match a with
   | xI a' =>
      let r := Zmod_POS a' b in
      let r' := (2 * r + 1) in
      if Zgt_bool b r' then r' else (r' - b)
   | xO a' =>
      let r := Zmod_POS a' b in
      let r' := (2 * r) in
      if Zgt_bool b r' then r' else (r' - b)
   | xH => if Zge_bool b 2 then 1 else 0
  end.

Definition Zmod' a b :=
  match a with
   | Z0 => 0
   | Zpos a' =>
      match b with
       | Z0 => 0
       | Zpos _ => Zmod_POS a' b
       | Zneg b' =>
          let r := Zmod_POS a' (Zpos b') in
          match r with Z0 => 0 | _ => b + r end
      end
   | Zneg a' =>
      match b with
       | Z0 => 0
       | Zpos _ =>
          let r := Zmod_POS a' b in
          match r with Z0 => 0 | _ => b - r end
       | Zneg b' => - (Zmod_POS a' (Zpos b'))
      end
  end.

Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)).

Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b.

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.


Theorem Zdiv_eucl_extended :
  forall b:Z,
    b <> 0 ->
    forall a:Z,
      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}.

Implicit Arguments Zdiv_eucl_extended.

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).