존재하는 보조정리에도 붙어 있음

Question

나는 "연습으로 남겨진" 보조정리에 갇혔습니다. 이번 강의.다음과 같이 진행됩니다.

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

어디 even 는 다음과 같이 정의된 귀납적 술어입니다.

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 숫자가 있다고 합니다(이름을 지정해 보겠습니다). k1) 그런 식으로 p = 2 * k1.

당신의 목표는 숫자를 보여주는 것입니다(예: k2) 증명할 수 있도록 S (S p) = 2 * k2.

계산해보면 알겠지만 (S k1) 완벽한 후보자가 될 것입니다.

따라서 계속 진행하려면 다음 전술을 사용할 수 있습니다.

• destruct 파괴하다 IHeven 증인을 분리하기 위해 k1 그리고 그 증거는 p = 2 * k1.
• exists 전시하다 (S k1) 당신의 목표에 대한 실존적인 증인으로서.
• 그런 다음 일부는 평등이 유지된다는 것을 증명하기 위해 노력합니다.