isabelle - 证明关于 case 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击中它.