Re: [isabelle] Modular arithmetic theory?

Am Freitag, den 18.11.2005, Amine Chaieb wrote:
> > -An attempt to decide a challenge problem
> >
> >    "(x div y) * y + (x mod y) = x"
> >
> >  (div, mod, + * all 2's complement operations,
> >   such a property is required for the integers
> >   in the Java Language Specification)
> >
> >  with an up-to-date wordlevel-BDD package
> >  was only feasible for a bit-length of 5 (!).
> why don't you use mod_div_equality (on nat) or zdiv_zmod_equality (on 
> int)?

Seems that you not quite understood the problem, sorry. As I said,
The div and mods, * and + are the 2's complement operations, so

"(x::JavaInt) + y == 
        Int_to_JavaInt (Rep_JavaInt x + Rep_JavaInt y)"


  Int_to_JavaInt :: "int => JavaInt" 
        "Int_to_JavaInt (x::int) ==
              Abs_JavaInt(( ( x + (-MinInt_int)) mod 
                            (2 * (-MinInt_int))) 
            + MinInt_int )"

* and div and mod analogously. For div and mod the question is
slightly obscured by the treatment of the signs. But: In the essence,
around each operator, there is a "mod (2 * (-MinInt_int))".
(you might ignore Abs_JavaInt and Rep_JavaInt as identities
 introduced by a type definition. Still, if you unfold the
theorem above, you get a quite nasty expression with 4 "adjusting
modulos", which are costly by theory.
for the full theory document).

Therefore, we prove div_mod *on JavaInt* (i.e. on a standard 2's 
complement arithmetic for 32 Bit with a specific definition of
the signs for div and mod), not on nat or int. The proof of
the challenge problem used indeed  zdiv_zmod_equality, but was
still highly nontrivial. Nevertheless it is interesting 
*in itself* because it is required by the Java Language Specification.

We started to get interested in the problem of deciding such
problems automatically, since one of our referees claimed that
this type of problems can be solved automatically, a claim,
that we found completely unfounded.

> Any way, presburger solves the problem above in 0.02 seconds.

Well, this theorem *is not* presburger arithmetic. I assume
therefore, that your presburger arithmetic tactic makes a simplification
step prior to further operations, and that zdiv_zmod_equality
is simply in the rewriter set. Since zdiv_zmod_equality has
been proven interactivly in the library, this is *not*
an automatic proof in this theorem.

Hope that helps,


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