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 n在能够对 n 的“均匀性”进行归纳之前，您必须证明这一点成立。

于 2012-05-22T04:54:58.303 回答