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

[John Harrison <John.Harrison@cl.cam.ac.uk>]

Freek writes:

| So John apparently prefers to have
| 
|	0 <= i mod j < abs j
|   
| for negative j, although he didn't explain why.

I was convinced by a discussion with Rob Arthan, and by reading:

  Raymond Boute:
  "The Euclidean definition of the functions div and mod".
  ACM TOPLAS vol. 14 (1992), pp127-144

that this definition fits more nicely with the "abstract algebra"
viewpoint. For example, you can think of "i mod j" as a canonical
representative of i's equivalence class modulo the ideal <j>. If you
think of it in this ideal-centric way, then since <j> = <-j>, the
representative should be independent of the sign.

Andrzej writes:

| I would like it. Actually, I was certain that it is the case in Mizar. 
| Well, Mizar has a different opinion. But I would like
| to have
|      i = (i div j)*j + i mod j,
| too. We can't probably have both?

Well, you can have it if you're prepared to make the definition
"mod-dominant" in the terminology of Boute's paper, i.e. define mod
first and then div to make that equation hold. Boute distinguishes
three main possibilities, all of which satisfy that law for nonzero
divisor. (Like Freek, I support i div 0 = 0 and i mod 0 = i so it
holds even for zero divisors, and I've recently changed HOL Light's
definitions accordingly.) Then the choices are determined by the
following:

  T-definition: i div j = trunc(i / j), i.e. rounded towards zero
  F-definition: i div j = floor(i / j), i.e. rounded towards -infinity
  E-definition: 0 <= i mod j < |j|

The little survey of a few leading theorem provers that I conducted
(my message to this forum was part of it) came up with the following
results:

  ACL2: following Common LISP, provides different choices, floor/mod
        giving the F-definition and truncate/rem the T-definition.

  Coq: F-definition

  HOL Light: E-definition

  HOL4: F-definition, at least according to my reading of
        integerScript.sml, where the definition is a bit involved.

  Isabelle/HOL: F-definition, which section 8.4.3 of the Tutorial
                says is "mathematical practice".

  Mizar: F-definition

  ProofPower: E-definition

  PVS: Not defined for negative divisors in the PVS prelude. A
       supplementary NASA library uses the T-definition ("Ada style").

The HOL Light entry is cheating, really, since I chose it after
starting my survey and starting to think about the topic.

Note that common programming languages either tend to use the
T-definition or to leave it to the underlying hardware, which also
tends to use the T-definition. There is quite a nice Wikipedia page
with a survey:

  http://en.wikipedia.org/wiki/Modulo_operation 

John.