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

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

Hi Freek:

Freek Wiedijk wrote:

> 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
>
>  
Yes, you right 'i' is Polish for 'and'. The same in Russian.

I do not agree with Grzegorz' opinion. We do dirty tricks with the 
division by 0, the only objective is to make the formalization easier.  
More general theorems (without assumption that a number is non zero) are 
easier to use. _Technically_ more general because on the substantial 
level it is nothing. A proof of such a theorem quite often needs to be 
done per cases, and we want
the case zero to be simple. So the i mod 0 = 0 helps (and even more if 
we use registration).

Artur pointed out  (we discussed the Grzegorz' complain yesterday) that
      i mo 0 = j mod 0
also helps to simplify the proof.

Regards,
Andrzej