# Re: [isabelle] Modular arithmetic theory?

```Amine Chaieb writes:

> Every mod or div results into 4 universal quantifiers (nested into
> the formula).

Surely the elimination only produces two quantifiers.  The relevant
theorem is

P (n mod c) = EX q r. n = q * c + r /\ r < c /\ P r

In HOL4, my normalisation of the goal

``(n MOD 10 + m MOD 10) MOD 10 = (n + m) MOD 10``

gives (in 0.05s)

?k.
0 <= k /\
?r.
0 <= r /\ (& n + & m = k * 10 + r) /\ r < 10 /\
?k.
0 <= k /\
?r'.
0 <= r' /\ (& n = k * 10 + r') /\ r' < 10 /\
?k.
0 <= k /\
?r''.
0 <= r'' /\
?k'.
0 <= k' /\
?r'''.
0 <= r''' /\ (r' + r'' = k' * 10 + r''') /\
r''' < 10 /\ (& m = k * 10 + r'') /\ r'' < 10 /\
(r''' = r)

This is a natural number goal, so all of the existential variables
have picked up 0 <= constraints.  Things go horribly after this step,
though the first three variables can be eliminated very cheaply
because of the equality constraints.

If you use integer modulus, you get a more complicated body because
you allow for negative arguments, but you don't have the 0 <=
constraints.

Michael.

```

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