Re: [isabelle] Modular arithmetic theory?



Amine Chaieb writes:
 
> The problem with arith in the original problem
 
>   lemma "(n mod 4294967296 + m mod 4294967296) mod 4294967296 = (m + n) mod 4294967296"
>   by arith

[...]
 
> Thanks Michael for the discussion, i now enhanced the preparation
> step and can prove the theorem above in 0.020 seconds.

Excellent!

> A propos the split rule with the "4" universal quantifiers: If k is
> a numeral in m mod k (which is neceesary for our implementation of
> presburger, we don't consider uniform presburger arithmetic), and
> you add computation rules for numerals then at least one of the two
> quantifier blocks will vanish and most two remain at the end.

Right.  As you long as you simplify the numeral early rather than
late, you will avoid any sort of exponential blow-up.
 
> > Even with so-called "delta-elimination" enabled, I can't get
> > comparable performance out of Cooper's algorithm, which is a shame.
 
> I don't see why this is specific to cooper and not Omega test.
 
I think this may have to do with using nats rather than ints.  (Or I'm
just being stupid.)  What performance do you get when you do this
proof on the nats?

Michael.






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