1

n (nat 型) の帰納法によってステートメントを証明できるようにしたいと考えています。これは、前件が n >= 2 の場合にのみ真である条件で構成されます。前件が偽である条件は、常に真です。そこで、n=0、n=1、n=2 の場合を主な誘導ステップとは別に証明したいと思います。次のような3つの基本ケースで帰納法による証明を行うことは可能ですか?

  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 に答える