Re: [isabelle] Congruence rules for modular arithmetic



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.