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