[mizar] Integer division

[Robert Boyer <boyer@cs.utexas.edu>]

Hey, why discriminate against rounding towards positive
infinity (Lisp:ceiling) or to the nearest integer
(lisp:round).  And then, how to round 1/2?  Round to
odd?  Round to even?  I vote for adding 'round to
nearest prime' :)

Before you finally settle these important things, may I
suggest you also consult with Vel Kahan, the Turing
award winner who is largely responsible for the IEEE
floating point standard.  He has very serious and
considered views on such matters.  And Knuth, too.  It
would be so nice if we had an agreed upon formal
version of that IEEE standard.

In his book 'A Theory of Sets', A. P. Morse really
likes to make function calls on strange args, e.g.,
x/0, default to some default values rather than being
undefined or 'giving an error', whatever that may mean.
Morse's default approach certainly simplifies lemmas
and proofs, both for humans and machines.  Nqthm does a
lot of such defaulting in definitions and theorems.
'Social' obstacles, however, exist. If you default
where much of the world says 'undefined', others may
think your results queer, or never remember what your
defaults are, or get sloppy and use x^0=1 and 0^x=0 to
give rise to a contradiction, as in some in computer
algebra systems.  I remain unsure whether keeping the
undefined undefined is wisest.  Though Lewis Carol may
believe that words mean what he makes them mean, one
can go to jail for screaming 'Fire' in a theater even
if you make 'Fire' mean 'Popcorn'.

Bob