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

[Freek Wiedijk <freek@cs.ru.nl>]

Artur:

>in Mizar Mathematical Library division and modulus of
>integers are defined as follows:
>
>definition
>  let i1,i2 be Integer;
>  func i1 div i2 -> Integer equals
>:: INT_1:def 7
>  [\ i1 / i2 /];
>end;
>
>that is 'div' is the floor of frac and then
>
>definition
>  let i1,i2 be Integer;
>  func i1 mod i2 -> Integer equals
>:: INT_1:def 8
>  i1 - (i1 div i2) * i2 if i2 <> 0
>  otherwise 0;
>end;

Just for the record the floor function is defined a little
bit earlier:

definition
  let r be real number;
  func [\ r /] -> Integer means
:: INT_1:def 4
  it <= r & r - 1 < it;
end;

(that is, the way you would expect it.)  Now XCMPLX_1:49
states that for all complex numbers

  a / 0 = 0

This all means that in Mizar

  i mod 0 = 0
  i div 0 = 0

for all integers i.  The second statement is INT_1:75, but I
don't find the first, although in REAL_3 there is the cluster

registration
  let n;
  cluster n div 0 -> zero;
  cluster n mod 0 -> zero;
  cluster 0 div n -> zero;
  cluster 0 mod n -> zero;
end;

Interestingly, in AOFA_I00 (Grzegorz' "Mizar Analysis of
Algorithms: Algorithms over Integers" from 2008), there is
the comment:

:: Remark:
:: Incorrect definition of "mod" in INT_1:  5 mod 0 = 0 i 5 div 0 = 0
:: and  5 <> 0*(5 div 0)+(5 mod 0)

This suggests that 5 mod 0 really should have been 5, right?
(And it makes me wonder: is "i" the Polish word for "and"?)

Freek