4

偶数の性質を証明するための帰納仮説を書こうとしています。以下を定式化し、証明した。

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.

それが証明されているという事実にもかかわらず、それを使用しようとすると、エラー メッセージが表示されます。

誘導仮説の問題点、またはそれを適用する方法を教えてください。

ありがとう、

マイヤー

4

2 に答える 2

2

induction使用される帰納法の原則は固定された形式であると私は信じています

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

混乱しているように見えるあなたのind_hyp_on_evens試合のみ。P (plus n n)induction

たとえば、適切な目標がある場合は、通常forall n, is_even (n+n)行う手順を手動で実行し、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戦術としてこれらのステップをまとめることは機能するはずです。

于 2012-09-17T23:53:11.360 に答える
0

偶数を記述する帰納的述語を書くことを検討できます (コードはテストされていません)。

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

Coq は誘導原理を自動的に生成します。even nn の「均一性」について帰納法を実行するには、それが成り立つことを証明する必要があります。

于 2012-05-22T04:54:58.303 に答える