Re: [isabelle] Congruence rules for modular arithmetic



Hi Amine,

Thanks for looking into this. The examples I gave were simple, but in my application the terms I'm trying to simplify are much larger. Here is a very small instance:

uint v0 mod 256 * (uint v1 mod 256) mod 256 =
    (((uint_sliceLH 0 0 v1 mod 256 *
         (uint v0 mod 256) mod 256 +
       uint_sliceLH 1 1 v1 mod 256 *
         (2 * (uint v0 mod 256) mod 256) mod 256) mod 256 +
       uint_sliceLH 2 2 v1 mod 256 *
         (uint v0 mod 256 * 4 mod 256) mod 256) mod 256 +
       uint_sliceLH 3 3 v1 mod 256 *
         (uint v0 mod 256 * 8 mod 256) mod 256) mod 256

where (uint_sliceLH n m w) = uint (sliceLH n m w).

Also, I need Isabelle to simplify the term itself, as I don't know beforehand what the term should simplify to. This is why I need to use congruence rules, rather than decision procedures like presburger. Can the algebra method perform simplification, especially when given extra definitions such as uint_sliceLH?

Thanks,
-john

On Mar 17, 2008, at 9:56 AM, Amine Chaieb wrote:
Hi John,

Sorry for the late answer (I have actually just noticed the mail).

The two lemmas can be proved automatically by presburger.

But you still might want to prove them once for all for arbitrary n, not just 2. the method algebra actually proves such problems, but unfortunately it is not yet set up properly.

Attached is a theory that shows how to use it. The auxiliary lemmas are actually proved in libraries (Prime numbers and Pocklington). We should maybe move them to HOL and set up algebra properly to prove such simple theorems.

Best Regards,
Amine.

John Matthews wrote:
Hi,
I'm trying to use congruence rules to simplify modular arithmetic expressions. For example, I'd like to automatically prove the following:
 lemma test1: "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
 lemma test2: "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
To do this, I made a special definition
 definition
   cong_zmod :: "int => int => int" where
  "cong_zmod p x == x mod p"
and then the following congruence rules (among others):
 lemma zmod_cong:
   assumes "p = p'"
       and "cong_zmod p' x = cong_zmod p' x'"
   shows "x mod p = x' mod p'"
 lemma cong_zmod_mod[simp]:
   "p dvd q ==> cong_zmod p (x mod q) = cong_zmod p x"
 lemma cong_zmod_plus[cong]:
   assumes A1: "p = p'"
       and A2: "cong_zmod p' x = cong_zmod p' x'"
       and A3: "cong_zmod p' y = cong_zmod p' y'"
       and A4: "x' + y' = z"
   shows "cong_zmod p (x + y) = cong_zmod p' z"
 lemma cong_zmod_mult[cong]:
   assumes A1: "cong_zmod p x = cong_zmod p x'"
       and A2: "cong_zmod p y = cong_zmod p y'"
       and A3: "x' * y' = z"
   shows "cong_zmod p (x * y) = cong_zmod p z"
With these congruence rules, I can get Isabelle to prove the first lemma:
 lemma test1: "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
 by (simp cong: zmod_cong)
but not the second:
 lemma test2: "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
 by (simp cong: zmod_cong)
 [Isabelle's response:  *** Terminal proof method failed
                        *** At command "by".]
Since Isabelle only stores one congruence rule for any given function symbol, the congruence rule cong_zmod_mult clobbers cong_zmod_plus. Is there any way to fix this so Isabelle can have multiple congruence rules for a function symbol, when the left-hand-sides are distinct? The alternative of coding this up as a simproc wouldn't interact well with other modular arithmetic simplification rules that users may want to add later on.
I'm appending the complete theory below.
Thanks,
-john
------------------------------------
theory "zmod_cong_plus_example"
imports "~~/src/HOL/Word/WordGenLib"
begin
definition
 cong_zmod :: "int \<Rightarrow> int \<Rightarrow> int" where
"cong_zmod p x \<equiv> x mod p"
lemma zmod_cong:
 assumes "p = p'"
     and "cong_zmod p' x = cong_zmod p' x'"
 shows "x mod p = x' mod p'"
by (cut_tac prems, simp add: cong_zmod_def)
lemma cong_zmod_mod[simp]:
 "p dvd q \<Longrightarrow> cong_zmod p (x mod q) = cong_zmod p x"
by (simp add: cong_zmod_def zmod_zmod_cancel)
lemma cong_zmod_plus[cong]:
 assumes A1: "p = p'"
     and A2: "cong_zmod p' x = cong_zmod p' x'"
     and A3: "cong_zmod p' y = cong_zmod p' y'"
     and A4: "x' + y' = z"
 shows "cong_zmod p (x + y) = cong_zmod p' z"
apply (cut_tac prems)
by (simp add: cong_zmod_def cong: mod_plus_cong)
-- "REVISIT: Submit to WordGenLib.thy"
lemma mod_mult_cong:
 assumes A1: "b = b'"
     and A2: "(x::int) mod b' = x' mod b'"
     and A3: "(y\<Colon>int) mod b' = y' mod b'"
     and A4: "x' * y' = z'"
 shows "(x * y) mod b = z' mod b'"
apply (simp add: A1)
apply (subst pull_mods(2)[symmetric])
by (simp add: A2 A3 A4 pull_mods(2))
lemma cong_zmod_mult[cong]:
 assumes A1: "cong_zmod p x = cong_zmod p x'"
     and A2: "cong_zmod p y = cong_zmod p y'"
     and A3: "x' * y' = z"
 shows "cong_zmod p (x * y) = cong_zmod p z"
apply (cut_tac prems)
by (simp add: cong_zmod_def cong: mod_mult_cong)
lemma test1:
 "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
apply (simp cong: zmod_cong)
done
lemma test2:
 "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
apply (simp cong: zmod_cong)
done
end
theory test
imports Main
begin

lemma test1: "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
 by presburger

lemma test2: "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
 by presburger

lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
proof
 assume H: "x mod n = y mod n"
 hence "x mod n - y mod n = 0" by simp
 hence "(x mod n - y mod n) mod n = 0" by simp
 hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
 thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
next
 assume H: "n dvd x - y"
 then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
 hence "x = n*k + y" by simp
 hence "x mod n = (n*k + y) mod n" by simp
 thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
qed

lemma int_mod_lemma: assumes xyn: "(x::int) mod n = y mod n" and xy:"y \<le> x"
 shows "\<exists>q. x = y + n * q"
proof-
 from xy have th: "x - y = (x - y)" by presburger
 from xyn have "n dvd x - y"
   by (simp only: zmod_eq_dvd_iff[symmetric])
then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
qed

lemma int_mod: "(x::int) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
 (is "?lhs = ?rhs")
proof
 assume H: "x mod n = y mod n"
 {assume xy: "x \<le> y"
   from H have th: "y mod n = x mod n" by simp
   from int_mod_lemma[OF th xy] have ?rhs
apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
 moreover
 {assume xy: "y \<le> x"
   from int_mod_lemma[OF H xy] have ?rhs
apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
 ultimately  show ?rhs using linear[of x y] by blast
next
assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
 hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
 thus  ?lhs by (simp add: zmod_zadd_right_eq)
qed

lemma test3: "((x::int) * y mod n) mod n = (x * y) mod n"
 unfolding zmod_simps mod_mod_trivial
 unfolding int_mod
 apply algebra
 done

lemma test4: "((x::int) + y mod n) mod n = (x + y) mod n"
 unfolding zmod_simps mod_mod_trivial
 unfolding int_mod
 apply algebra
 done

end






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