Re: [isabelle] arith tactic
Hi Amine, thanks for looking into this.
The formulas we are using arith for are those generated from unsigned
32-bit machine word arithmetic. Here's the setup:
We are reasoning about some security-critical system code written in
C, which uses unsigned machine word arithmetic. To accurately model
the code in Isabelle/HOL, we've defined a predicate subtype "mword"
containing just those integers that fall within [0 .. 2^32 - 1], and
overloaded the arithmetic operators on mword to return their results
mod 2^32. The mword (op <) operator is defined in terms of the
corresponding (op <) on ints.
At the moment we reason about machine integer subgoals simply by
unfolding the definitions of the operators. For example, here's the
machine integer subgoal I was working with a few days back:
"(x :: mword) < y - 1 ==> x + 1 > x"
I unwound the definitions of (op <), (op +), and (op -) for machine
words, and simplified it using auto, extended with some split rules
specially designed for this type. The subgoal that remained is what I
sent to the Isabelle mailing list (although I changed all occurrences
of 2^32 to 2^8, just to make sure the large constant wasn't an issue):
[| i < (nb - 1) mod 256; 0 <= nb; nb < 256; 0 <= i; i < 256 |]
==> i < (i + 1) mod 256
Just today I noticed that I can also solve this subgoal by case-
splitting on whether nb - 1 >= 0, and then just use auto. On the
other hand, case-splitting on whether i + 1 >= 0 doesn't help. But
perhaps I could write a special case-splitting heuristic on all
expressions guarded by the mod operator as a tactic. I'm a bit
nervous about the possible exponential blowup, but it sounds like I'm
already hitting that or worse with Cooper's algorithm in arith.
On the other hand, it's also really useful that arith can return
counterexamples to some invalid Presburger subgoals. Here is a
variant of the above machine integer problem that looks harder, but
actually can be handled using just auto with split rules:
"(x :: mword) < y ==> x + 1 > x"
by (auto simp add: mword_ops_defs
I then wrote a seemingly equivalent subgoal:
"(x :: mword) <= y - 1 ==> x + 1 > x"
apply (auto simp add: mword_ops_defs
Unfolding the definitions and case splitting generates the following
1. !!nb. [|0 <= nb; nb < 256|]
==> (nb - 1) mod 256 < ((nb - 1) mod 256 + 1) mod 256
2. !!nb i.
[|0 <= nb; nb < 256; 0 <= i; i < 256; i < (nb - 1) mod 256|]
==> i < (i + 1) mod 256
I then tried my case-splitting heuristic on the first subgoal,
apply (case_tac "nb - 1 >= 0", auto)
which Isabelle simplified to False!
In other words, this "equivalent" lemma is invalid. The arith tactic
doesn't appear to terminate on this first subgoal either. But if it
had, it would presumably have given me a counterexample assignment to
the free variable nb. However, with my current auto plus case-
splitting approach I have to figure out by hand what is wrong.
Amine Chaieb wrote:
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).
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.
Could you give me a "description" of this formula class?
This archive was generated by a fusion of
Pipermail (Mailman edition) and