Preuve par induction avec trois cas de base (Isabelle)

Question

Je veux être capable de prouver une déclaration par induction sur n (de type nat). Il s'agit d'un conditionnel dont l'antécédent n'est vrai que pour n> = 2. Un conditionnel dont l'antécédent est faux est toujours vrai. Donc, je voudrais prouver les cas n = 0, n = 1 et n = 2 tous séparément de l'étape inductive principale. Est-il possible de faire une preuve par induction avec trois cas de base comme les suivantes:

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 

En l'état actuel, cela ne semble pas fonctionner. Je pourrais prouver "P (n+2) --> Q" par induction à la place, mais ce ne serait pas une déclaration aussi forte. Je considère un cas divisé en "n=0", "n=1" et "n>=2", et ne prouvant que le dernier cas par induction.

Answer 1

La façon la plus propre est sans doute de prouver une règle d'induction sur mesure pour le type d'induction que vous voulez, comme ceci:

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) 

En théorie, la méthode induction_schema est également très utile pour prouver telles règles d'induction personnalisées , mais dans ce cas, il ne permet pas beaucoup:

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 

Vous pouvez également utiliser less_induct directement et faire une distinction de cas, dans l'étape d'induction pour les cas de base.