Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: John Matthews <matthews@galois.com>
Hi Rafal, thanks for the lemma. My understanding is that the arith
tactic is able to handle the mod operator, provided that its second
argument is a constant. In fact, after I sent off my original email,
I was able to get arith to prove the lemma, with a bit of manual
guidance:
lemma arith_example:
"[|(i::int) < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < (i + 1) mod 256"
apply (subst mod_pos_pos_trivial, auto)
by arith
In that proof script, this is the subgoal given to arith to solve:
"[|i < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < 255"
The arith tactic still needed to have understood the mod operator to
have solved this subgoal.
The bigger issue is that we'll be encountering many, many subgoals
like this in our projects here, most of which involve reasoning about
machine arithmetic. So we're relying on arith to discharge them
automatically and efficiently.
All the best,
-john
Email Gateway (Aug 17 2022 at 13:46):From: nipkow@in.tum.de
My understanding is that the arith tactic is able to handle the mod
operator, provided that its second argument is a constant.
In principle, yes. In your case the resulting Presburger goal killed the
decision procedure. We are working on it but it may take a little while.
There is no doubt that this is an important class of formulae.
Tobias
Email Gateway (Aug 17 2022 at 13:46):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
John,
The reasoning about mod in arith about mod and div is poor and enhancing
it is on the TODO list.
I recently wrote a more effitient implementation of the same QE algorithm,
which is able to solve your problem whithin 3 minutes,
running in ML (without proofs) which is just a pitty.
Presburger arithmetic is just too general to deal with mod and div in a
practically acceptable manner. The decision problem in Presburger
arithmetic is doubly exponential in space with respect to the largest
constant occuring in the formula (255).
Could you give me a "description" of this formula class?
Amine.
Last updated: May 03 2024 at 01:09 UTC