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