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.