심지어 붙는 보조 정리가 붙어 있습니다

Question

this lecture에서 "연습 문제로 남았습니다"라는 보조 정리에 붙어 있습니다. 그것은 다음과 같이 진행됩니다 even가 유도 조건은 다음과 같이

Lemma even_double : forall n, even n -> exists k, n = 2 * k. 
Proof. 
    intros n H. 
    induction H. 
    ... 

을 정의하는 경우 :

Inductive even : nat -> Prop := 
| even0 : even 0 
| evenS : forall p:nat, even p -> even (S (S p). 

도움말, 제발? 나는 항상 (S (S p) = 2 또는 그와 비슷한 것으로 끝납니다.

편집

일부 보조 정리 내가 (완료되지 증거)를 사용 전술 :

destruct IHeven 
exists (S x) 
rewrite mult_succ_l 
apply eq_S 
apply plus_n_Sm 

Answer 1

당신의 유도 단계를 수행 한 후, 당신은 두 가지 목표를 가져야한다.

첫 번째 사례 (even0의 기본 사례)는 쉽게 증명해야합니다. 실존 적 증인은 0으로 골라야하며, 그 후에 목표는 반사적으로 유지되어야합니다. (같은 evenS에 대한)

두 번째 경우가 보일 것이다

p : nat 
H : even p 
IHeven : exists k : nat, p = 2 * k 
============================ 
exists k : nat, S (S p) = 2 * k 

IHeven 숫자가 존재한다는 것을 말한다 p = 2 * k1 그러한 (의이 k1 이름을 보자).

목표는 S (S p) = 2 * k2을 증명할 수있는 숫자 (예 : k2)를 제시하는 것입니다.

수학을 수행하면 (S k1)이 가장 적합한 후보임을 알 수 있습니다.

그래서 다음과 같은 전술을 사용할 수 있습니다 진행합니다 :

• destruct 증인 k1 및 증거 p = 2 * k1 것을 분리 IHeven를 폭파 할 수 있습니다.
• exists은 (S k1)을 실존 적 증인으로 표시합니다.
• 그런 다음 평등성이 있음을 증명할 수있는 작업이 있습니다.