Re: [isabelle] Rounding negative fractions in Isabelle



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


> 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





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