Library Coq.Numbers.Integer.Abstract.ZDivFloor
Euclidean Division for integers (Floor convention)
We use here the convention known as Floor, or Round-Toward-Bottom,
where
a/b is the closest integer below the exact fraction.
It can be summarized by:
a = bq+r /\ 0 <= |r| < |b| /\ Sign(r) = Sign(b)
This is the convention followed historically by
Zdiv in Coq, and
corresponds to convention "F" 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
ZDivTrunc and
ZDivEucl for others conventions.
We benefit from what already exists for NZ
Another formulation of the main equation
Uniqueness theorems
Sign rules
With the current conventions, the other sign rules are rather complex.
The sign of a mod b is the one of b
A division by itself returns 1
A division of a small number by a bigger one yields zero.
Same situation, in term of modulo:
Basic values of divisions and modulo.
Order results about mod and div
A modulo cannot grow beyond its starting point.
As soon as the divisor is strictly greater than 1,
the division is strictly decreasing.
le is compatible with a positive division.
In this convention, div performs Rounding-Toward-Bottom.
Since we cannot speak of rational values here, we express this
fact by multiplying back by b, and this leads to separates
statements according to the sign of b.
First, a/b is below the exact fraction ...
... and moreover it is the larger such integer, since S(a/b)
is strictly above the exact fraction.
NB: The four previous properties could be used as
specifications for div.
Inequality mul_div_le is exact iff the modulo is zero.
Some additionnal inequalities about div.
A division respects opposite monotonicity for the divisor
Relations between usual operations and mod and div
Cancellations.
Operations modulo.
With the current convention, the following result isn't always
true for negative divisors. For instance
3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) .
A last inequality:
mod is related to divisibility