三个基本案例的归纳证明 (Isabelle)

Question

我希望能够通过对 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"，并且仅通过归纳法证明最后一个案例。

Answer 1

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

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，然后在基本案例的归纳步骤中进行案例区分。

三个基本案例的归纳证明 (Isabelle)

Proof by induction with three base cases (Isabelle)

induction

isabelle

isar