Email Gateway (Aug 22 2022 at 11:31): Email Gateway (Aug 22 2022 at 11:31):From: Zhe Hou <zhe.hou@hotmail.com>
Hi,
I found that Isabelle doesn’t round negative fractions in the way I expected. For example, I expect
(18406909::int) div (- 2240)
to be -8217, but Isabelle says it’s -8218. I tried it in a few other languages such as Ocaml, C++. They all reported -8217. In SML, the rounding mode IEEEReal.TO_NEGINF results in -8218.
However, Isabelle says
is -8217.
As a result, I can prove the following in Isabelle (2015 version):
lemma "(18406909::int) div (- 2240) ≠ - ((18406909::int) div (2240))"
by auto
I think this is unusual. If anyone could point me to an alternative way to do division in Isabelle, I’d be very grateful.
Thank you.
Zhe
Email Gateway (Aug 22 2022 at 11:39):From: Larry Paulson <lp15@cam.ac.uk>
Dear Zhe, thanks for your query.
I don’t have a book with me at the moment to cite, but my understanding is that mathematicians normally define the sign of the remainder to match that of the divisor. Thus 1 div 2 = 0 with remainder 1, but 1 div ~2 = -1 with remainder -1. (And -1 * -2 + -1 = 2-1 = 1.)
The sources I could find online didn’t seem to define division in the case of a negative divisor. However, note that -1 div 2 = -1 and -1 mod 2 = 1. When the divisor is positive, a negative remainder is definitely wrong.
Standard ML was designed to follow this classical definition. Isabelle’s number theory libraries do the same. However, computer hardware designers (either because they didn’t know better, or to keep circuits as simple as possible) adopted the same sign rules for division as for multiplication. Languages such as C and OCaml give you what the hardware gives you. For example, OCaml gives -1 / 2 = 0 and -1 mod 2 = -1. These answers are simply wrong.
Larry Paulson
Email Gateway (Aug 22 2022 at 11:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Zhe,
I don’t have a book with me at the moment to cite, but my
understanding is that mathematicians normally define the sign of the
remainder to match that of the divisor. Thus 1 div 2 = 0 with remainder
1, but 1 div ~2 = -1 with remainder -1. (And -1 * -2 + -1 = 2-1 = 1.)
that is easily made plausible: the units of a ring (in case of int, +1
and -1) form a field. In this segment you expect the conventional rules
of field division to hold:
+1 div +1 = +1
-1 div +1 = -1
+1 div -1 = -1
-1 div -1 = -1
And also
a div b = (sgn a * abs a) div (sgn b * abs b) = (sgn a div sgn b) *
(abs a div abs b)
where »abs a div abs b« is already explained and »sgn a * abs a« follows
the rules above.
The sign rules for mod follow naturally using the obviously desirable facts:
b <> 0 ==> a * b div b = a
a div b * b + a mod b = a
As far as I understand at the moment, this generalizes to each euclidean
ring.
So, the sign rules are computationally confusing at first sight, but
make perfect sense from an algebraic point of view.
Hope this helps,
Florian
The sources I could find online didn’t seem to define division in the case of a negative divisor. However, note that -1 div 2 = -1 and -1 mod 2 = 1. When the divisor is positive, a negative remainder is definitely wrong.
Standard ML was designed to follow this classical definition. Isabelle’s number theory libraries do the same. However, computer hardware designers (either because they didn’t know better, or to keep circuits as simple as possible) adopted the same sign rules for division as for multiplication. Languages such as C and OCaml give you what the hardware gives you. For example, OCaml gives -1 / 2 = 0 and -1 mod 2 = -1. These answers are simply wrong.
Larry Paulson
On 1 Oct 2015, at 04:09, Zhe Hou <zhe.hou@hotmail.com> wrote:
Hi,
I found that Isabelle doesn’t round negative fractions in the way I expected. For example, I expect
(18406909::int) div (- 2240)
to be -8217, but Isabelle says it’s -8218. I tried it in a few other languages such as Ocaml, C++. They all reported -8217. In SML, the rounding mode IEEEReal.TO_NEGINF results in -8218.
However, Isabelle says
- ((18406909::int) div 2240)
is -8217.
As a result, I can prove the following in Isabelle (2015 version):
lemma "(18406909::int) div (- 2240) ≠ - ((18406909::int) div (2240))"
by autoI think this is unusual. If anyone could point me to an alternative way to do division in Isabelle, I’d be very grateful.
Thank you.
Zhe
Email Gateway (Aug 22 2022 at 11:46):From: Lars Noschinski <noschinl@in.tum.de>
On 01.10.2015 17:19, Florian Haftmann wrote:
that is easily made plausible: the units of a ring (in case of int, +1
and -1) form a field. In this segment you expect the conventional rules
of field division to hold:
[...]
-1 div -1 = -1
I guess you meant "-1 div -1 = +1"?
Email Gateway (Aug 22 2022 at 11:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Zhe,
Larry and Florian already wrote about why division on integers in Isabelle is defined the
way it is. If you want a different behaviour for division, you must define your own
division operator. Fortunately, you can achieve this probably quite easily by doing a few
case distinctions on the sign of the operands. In my AFP entry JinjaThreads, I have done
something similar for division and modulo on fixed-size integers ('a word), because the
division operation in HOL-Word did not match the sign rules of Java. Have a look at the
theory JinjaThreads/Common/BinOp.thy (search for word_sdiv); maybe this gives you some
inspiration.
Best,
Andreas
Last updated: Apr 26 2024 at 16:20 UTC