[isabelle] Congruence rules for modular arithmetic · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Congruence rules for modular arithmetic

Email Gateway (Aug 18 2022 at 11:31):

From: John Matthews <matthews@galois.com>
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)

-- "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

Email Gateway (Aug 18 2022 at 11:33):

From: Amine Chaieb <chaieb@in.tum.de>
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:
Test.thy

Email Gateway (Aug 18 2022 at 11:40):

From: John Matthews <matthews@galois.com>
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

Email Gateway (Aug 18 2022 at 11:40):

From: Amine Chaieb <chaieb@in.tum.de>
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:

Email Gateway (Aug 18 2022 at 11:40):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Amine Chaieb wrote:
For integers, the statement above doesn't depend on 8 being equal to 8
mod 256.

In fact it is one of the simplifications in the list rdmods, in
Num_Lemmas.thy in src/HOL/Word.

Incidentally, the stuff I put into Num_Lemmas.thy was stuff I thought
was of more general interest than just to be used within the
machine-word library.

Jeremy Dawson

Last updated: May 03 2024 at 12:27 UTC