证明关于案例的简单定理 mod 10

Question

我想证明以下引理：

lemma mod10_cases:
  "P 0 ⟹ P 1 ⟹ P 2 ⟹ P 3 ⟹ P 4 ⟹ P 5 ⟹ P 6 ⟹ P 7 ⟹ P 8 ⟹ P 9 ⟹ P (n mod 10)"

但我发现它非常棘手。引理感觉很简单；它只是说为了证明属性 P 对每个以 10 为模的数字成立，我只需要检查它是否对 0、1、2、3、4、5、6、7 成立、8 和 9。

（更广泛的图片：我想用我的引理来证明 foo(n mod 10) 形式的定理，我打算先说 apply (cases rule: mod10_cases)。）

Answer 1

我常用的技巧是先显示n mod 10 ∈ {..<10}（simp简单证明）然后展开{..<10}到{0, 1, 2, 3, 4, 5, 6, 7, 8, 9}，这可以通过喂食来完成简化器的正确规则：

lemma mod10_induct [case_names 0 1 2 3 4 5 6 7 8 9]:
  fixes n :: nat
  assumes "P 0" "P 1" "P 2" "P 3" "P 4" "P 5" "P 6" "P 7" "P 8" "P 9"
  shows   "P (n mod 10)"
proof -
  have "n mod 10 ∈ {..<10}"
    by simp
  also have "{..<10} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9 :: nat}"
    by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
  finally show ?thesis using assms
    by fastforce
qed

请注意，您编写定理的方式具有归纳规则的形式，而不是案例拆分规则。案例拆分规则看起来更像这样：

lemma mod10_cases [case_names 0 1 2 3 4 5 6 7 8 9]:
  fixes n :: nat
  obtains "n mod 10 = 0" | "n mod 10 = 1" | "n mod 10 = 2" | "n mod 10 = 3" | "n mod 10 = 4" | 
          "n mod 10 = 5" | "n mod 10 = 6" | "n mod 10 = 7" | "n mod 10 = 8" | "n mod 10 = 9"
proof -
  have "n mod 10 ∈ {..<10}"
    by simp
  also have "{..<10} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9 :: nat}"
    by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
  finally show ?thesis using that
    by fast
qed

如果这里的 obtains 让你感到困惑，你从这里得到的最终定理如下所示：

theorem mod10_cases:
 (?n mod 10 = 0 ⟹ ?thesis) ⟹
 (?n mod 10 = 1 ⟹ ?thesis) ⟹
 (?n mod 10 = 2 ⟹ ?thesis) ⟹
 (?n mod 10 = 3 ⟹ ?thesis) ⟹
 (?n mod 10 = 4 ⟹ ?thesis) ⟹
 (?n mod 10 = 5 ⟹ ?thesis) ⟹
 (?n mod 10 = 6 ⟹ ?thesis) ⟹
 (?n mod 10 = 7 ⟹ ?thesis) ⟹
 (?n mod 10 = 8 ⟹ ?thesis) ⟹
 (?n mod 10 = 9 ⟹ ?thesis) ⟹ ?thesis

然后您可以像这样使用您的规则：

lemma "P (n mod 10 :: nat)"
  apply (induction n rule: mod10_induct)
  oops

lemma "P (n mod 10 :: nat)"
  apply (cases n rule: mod10_cases)
  oops

然而，在大多数情况下，我不会像你开始时那样为此推导出一个单独的规则——我只是在我需要的地方展开 {..<10}，因为它只需要大约 4 行，然后将 n mod 10 ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} 作为我的实际目标并用 auto.

实现

证明关于案例的简单定理 mod 10

Proving simple theorem about cases mod 10

isabelle

modular-arithmetic