Re: [isabelle] arith tactic



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

On Feb 14, 2006, at 11:06 PM, Rafal Kolanski wrote:

Should arith be able to pull this off? It looks like it's missing the ability to reason when "k mod n = k", even given the obvious. I was distracted and made this, it may be of some use to you:

lemma arith_example:
  assumes
   a: "(i::int) < (nb - 1) mod 256"
   "0 <= nb"
   "nb < 256"
   "0 <= i"
   "i < 256"
  shows "i < (i + 1) mod 256"
proof -
  {
    assume c: "nb = 0"
    with a have "(i + 1) mod 256 = i + 1"
      by (subst mod_pos_pos_trivial) auto
    hence ?thesis by simp
  }
  moreover {
    assume c: "nb \<noteq> 0"
    with a have lim1: "nb - 1 \<ge> 0" by simp
    with a have "nb - 1 < 256" by simp
    with lim1 have "(nb - 1) mod 256 = nb - 1"
      by (subst mod_pos_pos_trivial) auto
    with a lim1 have ?thesis
      by (subst mod_pos_pos_trivial) auto
  }
  ultimately show ?thesis by (cases, auto)
qed


Regards,

Rafal Kolanski.


John Matthews wrote:
Hi, I've run into a problem using the arith tactic. I ran arith for over 15 minutes on the following subgoal, without success:
lemma arith_example:
  "[|(i::int) < (nb - 1) mod 256;
    0 <= nb;
    nb < 256;
    0 <= i;
    i < 256|]
   ==> i < (i + 1) mod 256"
apply arith
I'm running the Isabelle_08-Feb-2006 snapshot.
Thanks,
-john






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