Library Coq.Numbers.Integer.Abstract.ZDivTrunc


Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.

Euclidean Division for integers (Trunc convention)

We use here the convention known as Trunc, or Round-Toward-Zero, where a/b is the integer with the largest absolute value to be between zero and the exact fraction. It can be summarized by:
a = bq+r /\ 0 <= |r| < |b| /\ Sign(r) = Sign(a)
This is the convention of Ocaml and many other systems (C, ASM, ...). This convention is named "T" in the following paper:
R. Boute, "The Euclidean definition of the functions div and mod", ACM Transactions on Programming Languages and Systems, Vol. 14, No.2, pp. 127-144, April 1992.
See files ZDivFloor and ZDivEucl for others conventions.

Module Type ZQuotProp
 (Import A : ZAxiomsSig')
 (Import B : ZMulOrderProp A)
 (Import C : ZSgnAbsProp A B).

We benefit from what already exists for NZ

 Module Import Private_Div.
 Module Quot2Div <: NZDiv A.
  Definition div := quot.
  Definition modulo := A.rem.
  Definition div_wd := quot_wd.
  Definition mod_wd := rem_wd.
  Definition div_mod := quot_rem.
  Definition mod_bound_pos := rem_bound_pos.
 End Quot2Div.
 Module NZQuot := Nop <+ NZDivProp A Quot2Div B.
 End Private_Div.

Ltac pos_or_neg a :=
 let LT := fresh "LT" in
 let LE := fresh "LE" in
 destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT].

Another formulation of the main equation

Lemma rem_eq :
 forall a b, b~=0 -> a rem b == a - b*(a÷b).

A few sign rules (simple ones)

Lemma rem_opp_opp : forall a b, b ~= 0 -> (-a) rem (-b) == - (a rem b).

Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b).

Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b).

Lemma quot_opp_opp : forall a b, b ~= 0 -> (-a)÷(-b) == a÷b.

Uniqueness theorems

Theorem quot_rem_unique : forall b q1 q2 r1 r2 : t,
  (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) ->
  b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.

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

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

A division by itself returns 1

Lemma quot_same : forall a, a~=0 -> a÷a == 1.

Lemma rem_same : forall a, a~=0 -> a rem a == 0.

A division of a small number by a bigger one yields zero.

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

Same situation, in term of remulo:

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

Basic values of divisions and modulo.


Lemma quot_0_l: forall a, a~=0 -> 0÷a == 0.

Lemma rem_0_l: forall a, a~=0 -> 0 rem a == 0.

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

Lemma rem_1_r: forall a, a rem 1 == 0.

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

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

Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a.

Lemma rem_mul : forall a b, b~=0 -> (a*b) rem b == 0.

Theorem quot_unique_exact a b q: b~=0 -> a == b*q -> q == a÷b.

The sign of a rem b is the one of a (when it's not null)

Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b.

Lemma rem_nonpos : forall a b, b~=0 -> a <= 0 -> a rem b <= 0.

Lemma rem_sign_mul : forall a b, b~=0 -> 0 <= (a rem b) * a.

Lemma rem_sign_nz : forall a b, b~=0 -> a rem b ~= 0 ->
 sgn (a rem b) == sgn a.

Lemma rem_sign : forall a b, a~=0 -> b~=0 -> sgn (a rem b) ~= -sgn a.

Operations and absolute value

Lemma rem_abs_l : forall a b, b ~= 0 -> (abs a) rem b == abs (a rem b).

Lemma rem_abs_r : forall a b, b ~= 0 -> a rem (abs b) == a rem b.

Lemma rem_abs : forall a b, b ~= 0 -> (abs a) rem (abs b) == abs (a rem b).

Lemma quot_abs_l : forall a b, b ~= 0 -> (abs a)÷b == (sgn a)*(a÷b).

Lemma quot_abs_r : forall a b, b ~= 0 -> a÷(abs b) == (sgn b)*(a÷b).

Lemma quot_abs : forall a b, b ~= 0 -> (abs a)÷(abs b) == abs (a÷b).

We have a general bound for absolute values

Lemma rem_bound_abs :
 forall a b, b~=0 -> abs (a rem b) < abs b.

Order results about rem and quot

A modulo cannot grow beyond its starting point.

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

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

Lemma quot_str_pos : forall a b, 0<b<=a -> 0 < a÷b.

Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b).

Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b).

As soon as the divisor is strictly greater than 1, the division is strictly decreasing.

Lemma quot_lt : forall a b, 0<a -> 1<b -> a÷b < a.

le is compatible with a positive division.

Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c.

With this choice of division, rounding of quot is always done toward zero:

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

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

For positive numbers, considering S (a÷b) leads to an upper bound for a

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

Similar results with negative numbers

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

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

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

Inequality mul_quot_le is exact iff the modulo is zero.

Lemma quot_exact : forall a b, b~=0 -> (a == b*(a÷b) <-> a rem b == 0).

Some additional inequalities about quot.

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

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

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

A division respects opposite monotonicity for the divisor

Lemma quot_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p÷r <= p÷q.

Relations between usual operations and rem and quot

Unlike with other division conventions, some results here aren't always valid, and need to be restricted. For instance (a+b*c) rem c <> a rem c for a=9,b=-5,c=2

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

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

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

Cancellations.

Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
 (a*c)÷(b*c) == a÷b.

Lemma quot_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
 (c*a)÷(c*b) == a÷b.

Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 ->
  (a*c) rem (b*c) == (a rem b) * c.

Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 ->
  (c*a) rem (c*b) == c * (a rem b).

Operations modulo.

Theorem rem_rem: forall a n, n~=0 ->
 (a rem n) rem n == a rem n.

Lemma mul_rem_idemp_l : forall a b n, n~=0 ->
 ((a rem n)*b) rem n == (a*b) rem n.

Lemma mul_rem_idemp_r : forall a b n, n~=0 ->
 (a*(b rem n)) rem n == (a*b) rem n.

Theorem mul_rem: forall a b n, n~=0 ->
 (a * b) rem n == ((a rem n) * (b rem n)) rem n.

addition and modulo
Generally speaking, unlike with other conventions, 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.

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

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

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

Conversely, the following results need less restrictions here.

Lemma quot_quot : forall a b c, b~=0 -> c~=0 ->
 (a÷b)÷c == a÷(b*c).

Lemma mod_mul_r : forall a b c, b~=0 -> c~=0 ->
 a rem (b*c) == a rem b + b*((a÷b) rem c).

Lemma rem_quot: forall a b, b~=0 ->
 a rem b ÷ b == 0.

A last inequality:

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

End ZQuotProp.