1

我希望能够通过对 n（nat 类型）的归纳来证明一个陈述。它由一个前提条件组成，其前提条件仅在 n >= 2 时为真。前提条件为假的条件始终为真。所以我想证明 n=0、n=1 和 n=2 的情况都与主要归纳步骤分开。是否可以通过以下三个基本案例进行归纳证明：

  lemma "P (n::nat) --> Q"
  proof (induct n)
    case 0
    show ?case sorry
  next
    case 1
    show ?case sorry
  next 
    case 2
    show ?case sorry
  next
    case (Suc n)
    show ?case sorry
  qed

就目前而言，这似乎不起作用。我可以"P (n+2) --> Q"通过归纳来证明，但这不会是一个强有力的陈述。我正在考虑将一个案例拆分为"n=0","n=1"和"n>=2", 并仅通过归纳证明最后一个案例。

4

1 回答 1

3

最简洁的方法可能是为您想要的那种归纳证明自定义归纳规则，如下所示：

lemma nat_0_1_2_induct [case_names 0 1 2 step]:
  assumes "P 0" "P 1" "P 2" "⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)"
  shows   "P n"
proof (induction n rule: less_induct)
  case (less n)
  show ?case using assms(4)[OF _ less.IH[of "n - 1"]]
    by (cases "n ≤ 2") (insert assms(1-3), auto simp: eval_nat_numeral le_Suc_eq)
qed

lemma "P (n::nat) ⟶ Q"
proof (induction n rule: nat_0_1_2_induct)

理论上，该induction_schema方法对于证明此类自定义归纳规则也非常有用，但在这种情况下，它并没有太大帮助：

lemma nat_0_1_2_induct [case_names 0 1 2 step]:
  "P 0 ⟹ P 1 ⟹ P 2 ⟹ (⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)) ⟹ P n"
proof (induction_schema, goal_cases complete wf terminate)
  case (complete P n)
  thus ?case by (cases n) force+
next
  show "wf (Wellfounded.measure id)" by (rule wf_measure)
qed simp_all

您也可以less_induct直接使用，然后在基本案例的归纳步骤中进行案例区分。

于 2016-12-29T22:27:21.117 回答