coq – 偶数的归纳假设

2019年8月3日 172次阅读

我试图写一个感应假设专门用于证明偶数的性质.我制定并证明了以下内容：

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.

尽管已经证实了这一点,但任何使用它的尝试都会产生错误信息：“错误：不是正确数量的归纳参数.”

有人可以告诉我归纳假设的问题是什么,或者,如何应用它？

谢谢,

迈耶

最佳答案 我认为归纳假设任何将要使用的归纳原理都具有

固定形式

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

你的ind_hyp_on_evens只匹配P(加n n),这似乎混淆了归纳.

如果你有一个合适的目标,比如forall n,is_even(n n),你可以手动完成
感应通常会做的步骤,并扩展它以处理特殊形式.

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策略应该可行.

点赞