问题描述
我决定证明以下定理：
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的应用之外，这仅是关于各种规则的各种应用
表达式的某些部分可以安全地减少。有没有一种证明方法可以自动推断出这样的细节？
（我也愿意接受其他有关我的证明风格的评论-让我感到困扰的是重复的::int）
解决方法
在对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，这样才能只发生一次。）
该定理的单线证明仍然需要手动实例化相关引理。但是，通常最好将步骤进一步说明。这将使战术能够推断出应如何定理定理，同时为 human 留下更多有用的细节。
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