짝수에 대한 유도 가설

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)) 
. 

COQ 자동으로 유도 원리를 생성합니다. 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 단계를 수동으로 수행하여 특수 양식을 처리 할 수 ​​있습니다.

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 전술이 단계를 꾸리고, 어떤 유도 방식에 대한 일반적인 도우미 전술이를 포장 할 수 있는지 모르겠어요.