*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Congruence rules for modular arithmetic*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Sun, 06 Apr 2008 13:07:01 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5198AD0B-C1A2-4D74-8ED0-6E4DFA2F154B@galois.com>*References*: <B4AE463E-E0ED-433D-945E-46D1735591BD@galois.com> <47DEA2B0.9000306@in.tum.de> <5198AD0B-C1A2-4D74-8ED0-6E4DFA2F154B@galois.com>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Hi John,

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

For e.g. (x mod 256 + 8) mod 256 = (x + 8) mod 256

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.

I hope this helps. Amine. John Matthews wrote:

Hi Amine,Thanks for looking into this. The examples I gave were simple, but in myapplication the terms I'm trying to simplify are much larger. Here is avery 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 knowbeforehand what the term should simplify to. This is why I need to usecongruence rules, rather than decision procedures like presburger. Canthe algebra method perform simplification, especially when given extradefinitions 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, butunfortunately it is not yet set up properly.Attached is a theory that shows how to use it. The auxiliary lemmasare actually proved in libraries (Prime numbers and Pocklington). Weshould maybe move them to HOL and set up algebra properly to provesuch simple theorems.Best Regards, Amine. John Matthews wrote:Hi,I'm trying to use congruence rules to simplify modular arithmeticexpressions. 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 firstlemma: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 functionsymbol, the congruence rule cong_zmod_mult clobbers cong_zmod_plus.Is there any way to fix this so Isabelle can have multiple congruencerules for a function symbol, when the left-hand-sides are distinct?The alternative of coding this up as a simproc wouldn't interact wellwith other modular arithmetic simplification rules that users maywant 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 endtheory 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 presburgerlemma 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) qedlemma 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 arithqedlemma 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 ?rhsapply clarify apply (rule_tac x="q" in exI) by (rule exI[wherex="0"], simp)}moreover {assume xy: "y \<le> x" from int_mod_lemma[OF H xy] have ?rhsapply 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 nextassume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" byblasthence "(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

**Follow-Ups**:**Re: [isabelle] Congruence rules for modular arithmetic***From:*Jeremy Dawson

**References**:**Re: [isabelle] Congruence rules for modular arithmetic***From:*John Matthews

- Previous by Date: Re: [isabelle] Congruence rules for modular arithmetic
- Next by Date: Re: [isabelle] Program verification
- Previous by Thread: Re: [isabelle] Congruence rules for modular arithmetic
- Next by Thread: Re: [isabelle] Congruence rules for modular arithmetic
- Cl-isabelle-users April 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list