偶数の帰納仮説

Question

のの恒等仮説を具体的に証明しようとしています。私は、次のように定式化し、証明した：

Theorem ind_hyp_on_evens: 
forall (p : nat -> Prop), 
(p 0 -> (forall n, p n -> p (S (S n))) -> 
forall n, p (n + n)). 
Proof. 
intros p P0 P1. 
intro n. 
assert(p (n + n) /\ p (S (S (n + n)))). 
induction n as [| n']. 
split. unfold plus. assumption. 
unfold plus. 
apply (P1 0). 
assumption. 
destruct IHn' as [A B]. 
split. 
rewrite <- plus_Snm_nSm. 
rewrite -> ? plus_Sn_m. 
assumption. 
rewrite <- plus_Snm_nSm. 
rewrite -> ? plus_Sn_m. 
apply (P1 (S (S (n' + n')))). 
assumption. 
destruct H as [H1 H2]. 
assumption. Qed. 

それが証明したという事実、それはエラーメッセージになり、使用するいかなる試みにもかかわらず：「エラー：未誘導引数の正しい数」

誘発仮説の問題点や、それを適用する方法を教えてもらえますか？あなたも、数字（コードテストされていない）について説明し、誘導述語を書いて検討することもでき

おかげで、

メイヤー

Answer 1

は：

Inductive even : nat -> Prop := 
| evenO : even O 
| evenSSn : forall n, even n -> even (S (S n)) 
. 

コックが自動的に誘導原理を生成します。 nの "均一性"を誘導する前に、even nが成り立つことを証明しなければなりません。私は信じていinduction

Answer 2

が使用されます任意の誘導原理はinductionを混同し

forall ... (P : SomeType -> Type) ..., (* or ->Set or ->Prop *) 
    ... -> 
    forall (v : SomeType), P v 

あなたind_hyp_on_evens試合だけP (plus n n)思わ 定形を持っていることを前提としています。

forall n, is_even (n+n)のような適切な目標を持っている場合は、inductionが手動で行うことができます。inductionは、特別なフォームを処理するために手動で行うことができます。

intro n0;       (* temp. var *) 
pattern (n0 + n0);     (* restructure as (fun x => (is_even x)) (n0+n0) *) 
refine (ind_hyp_on_evens _ _ _ n0); (* apply ind. scheme *) 
clear n0; [| intros n IHn ].   (* clear temp., do one 'intros' per branch *) 

それはしかし、動作するはずごとのスキームLtac戦術としてこれらの手順を荷造り、任意の誘導スキームのための一般的なヘルパー戦術としてそれを荷造りすることが可能です場合、私は知りません。