模算术中的有效推理答案

【问题标题】：Efficient reasoning in modular arithmetic模算术中的有效推理
【发布时间】：2021-01-16 22:42:51
【问题描述】：

我决定证明以下定理：

theory Scratch
  imports Main
begin

lemma "(3::int)^k mod 4 = 1 ⟷ even k"
proof (cases "even k")
  case True
    then obtain l where "2*l = k" by auto
    then show ?thesis
      using power_mult [of "(3::int)" 2 l]
      and power_mod [of "(9::int)" 4 l] by auto
next
  case False
    then obtain l where "2*l + 1 = k" using odd_two_times_div_two_succ by blast
    then have "(3::int)^k mod 4 = 3"
      using power_mult [of "(3::int)" 2 l ]
      and mod_mult_right_eq [of "(3::int)" "9^l" 4]
      and power_mod [of "(9::int)" 4 l]
      by auto
    then show ?thesis using `odd k` by auto
qed

end

Isabelle 接受了证明，但在我看来，关于如何执行 mod 4 的计算有太多琐碎的细节：

    then have "(3::int)^k mod 4 = 3"
      using power_mult [of "(3::int)" 2 l ]
      and mod_mult_right_eq [of "(3::int)" "9^l" 4]
      and power_mod [of "(9::int)" 4 l]
      by auto

除了power_mult的应用，这只是各种规则的应用部分表达式可以安全地减少。有没有一种证明方法可以自动推断出这样的细节？

（对于我的证明风格，我也对任何其他 cmets 持开放态度 - 困扰我的一件事是重复的 ::int）

【问题讨论】：

对于那个精确的证明，lemma "(3::int)^k mod 4 = 1 ⟷ even k" apply (cases ‹even k›) apply (auto elim!: oddE simp: power_mult simp flip: mod_mult_right_eq[of 3 ‹9^_›] power_mod[of 9]) done 确实有效。但是您通常不想像那样压缩您的证明。而且我没有找到一种方法来折磨 simp 在没有实例化的情况下进行简化。 Simprocs 会很有用……

标签： isabelle modular-arithmetic

【解决方案1】：

经过对 IRC 的一些讨论和后续实验，我了解到以下内容：

首先，a mod c = b mod c 有点冗长。 HOL-Number_Theory.Cong 定义了符号[a = b] (mod c)，使用起来更舒服。

theory Scratch
  imports
    Main
    "HOL-Number_Theory.Cong" (* or "HOL-Number_Theory.Number_Theory",
                                but that requires some more computation *)
begin

（请注意，这将使 Isabelle 编译理论，这可能需要一些时间。您可能希望运行 isabelle jedit -l HOL-Number_Theory，这样只会发生一次。）

定理的单行证明仍需要手动实例化相关引理。但是，通常最好再详细说明这些步骤。这将允许策略推断应该如何实例化定理，同时为人类留下更多有用的细节。

proof (cases "even k")
  case True
  then obtain l where "2*l = k" by auto
  then have "[3^k = (3^2)^l] (mod 4)" (is "cong _ ... _")
    by (auto simp add: power_mult)
  also have "[... = (1::int)^l] (mod 4)" (is "cong _ ... _")
    by (intro cong_pow) (simp add: cong_def)
  also have "[... = 1] (mod 4)" by auto
  finally have "[3^k = 1::int] (mod 4)".
  thus ?thesis using `even k` by blast
next
  case False
  then obtain l where "2*l + 1 = k"
    using oddE by blast
  then have "[3^k = 3^(2*l+1)] (mod 4)" (is "cong _ ... _") by auto
  also have "[... = (3^2)^l * 3] (mod 4)" (is "cong _ ... _")
    by (metis power_mult power_add power_one_right cong_def)
  also have "[... = (1::int)^l * 3] (mod 4)" (is "cong _ ... _")
    by (intro cong_mult cong_pow) (auto simp add: cong_def)
  also have "[... = 3] (mod 4)" by auto
  finally have "[3^k ≠ 1::int] (mod 4)" by (auto simp add: cong_def)
  then show ?thesis using `odd k` by blast
qed

这是一个非常标准的计算证明，我们使用... 来引用上一个命令的 RHS。默认情况下，它引用顶级函数应用程序的最后一个参数。在这种情况下，这就是模数，所以我们用(is "cong _ ... _") 覆盖它。

还要注意，我们可以通过重用minus_one_power_iff来避免大部分工作：

lemma "[3^k = 1::int] (mod 4) ⟷ even k"
proof -
  have "[3^k = (-1::int)^k] (mod 4)"
    by (intro cong_pow) (auto simp: cong_def)
  thus ?thesis
    by (auto simp: cong_def minus_one_power_iff)
qed

【讨论】：