# Re: [isabelle] Congruence rules for modular arithmetic

```Hi John,

```
It would be helpful if you could provide a rough description of the class of terms you want to simplify.
```
```
As for the example (I assumed the variables have type int!) you could simplify it to e.g.
```
uint v0 * uint v1 mod 256 =
(uint (sliceLH 0 0 v1) * uint v0 +
uint (sliceLH 1 1 v1) * (2 * uint v0) +
uint (sliceLH 2 2 v1) * (uint v0 * 4) +
uint (sliceLH 3 3 v1) * (uint v0 * 8)) mod
256

```
automatically using (simp add: zmod_simps H). Here H is a premise saying that (uint_sliceLH n m w) = uint (sliceLH n m w).
```
```
If you only need to gather terms together under mod/div this should not be very difficult, provided that the constants also (not only subterms) are of the form a mod m, for the same modulus. But I doubt your examples are as simple as this.
```
For e.g. (x mod 256 + 8) mod 256 = (x + 8) mod 256

```
one would need more than simple rewriting with zmod_simps (maybe a special simproc or tactic to convert 8 into 8 mod 256 or generally y into y mod m provided we can prove y < m and m >= 0 for the integers).
```
```
Unfortunately the algebra method can not prove the statement above which boils down to
```
EX q1 q2.
uint v0 * uint v1 + 256 * q1 =
uint (sliceLH 0 0 v1) * uint v0 +
uint (sliceLH 1 1 v1) * (2 * uint v0) +
uint (sliceLH 2 2 v1) * (uint v0 * 4) +
uint (sliceLH 3 3 v1) * (uint v0 * 8) +
256 * q2

I guess it does not hold in all rings.

```
Apart from that, the method algebra does not perform simplification, it is only meant for decision. You can however give it extra theorems for definitions or the like to be expanded before the core procedure is called.
```
I hope this helps.

Amine.

John Matthews wrote:
```
```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"
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 (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
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.