Re: [mizar] Integer division and modulus/remainder in Mizar

[trybulec <trybulec@math.uwb.edu.pl>]

Hi John,

Artur and Freek explained the situation. Maybe it is worth to look how 
it works with negative integers.

(-7) div 3 = -3, (-7) mod 3 = 2
so  -7 = ((-7) div 3)*3 + (-7) mod 3

for negative j,  i mod j is negative
7 div (-3) = -3, 7 mod (-3) =  -2
(-7) div (-3) = 2, (-7)  mod (-3) = -1

so for non zero j we have
    i = (i div j)*j + i mod j.

and always   0 <= abs(i mod j) <= abs j
(the second equality only for j=0).

We plan to generalize it to real numbers. Actually, it is long overdue. 
Your message prompted us to do it in the next revision.
I believe, Euclid did it for positive reals (for intervals), so back to 
Euclid. The same goes for gcd and lcm.

Regards,
Andrzej


John Harrison wrote:

> I'm curious how Mizar defines division and modulus of integers where
> one or both arguments are negative.
>
> This is a well-known area where programming languages disagree or are
> undefined, so I'm doing a little survey of some of the world's leading
> theorem provers to see if there is a consensus there.
>
> John.
>
>