我试图证明以下引理:
Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).
Lemma even_Sn_not_even_n : forall n,
even (S n) <-> not (even n).
Proof.
intros n. split.
+ intros H. unfold not. intros H1. induction H1 as [|n' E' IHn].
- inversion H.
- inversion_clear H. apply IHn in H0. apply H0.
+ unfold not. intros H. induction n as [|n' E' IHn].
-
Qed.
以下是我最终得到的内容:
1 subgoal (ID 173)
H : even 0 -> False
============================
even 1
我希望coq能够将"even 0"计算为true,"even 1"计算为false。我尝试了"simpl"、"apply ev_0 in H.",但它们都出错了。该怎么办?