Re: [isabelle] Rounding negative fractions in Isabelle



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 at 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 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
> 
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.