even_Sn_not_even_n-在另一个假设中应用1个假设 [英] even_Sn_not_even_n - apply 1 hypothesis in another
问题描述
不幸的是，我再次被卡住了:
Unfortunately I got stuck again:
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.
+ intros H. induction n as [|n' IHn].
- exfalso. apply H. apply ev_0.
- apply evSS_inv'.
这是结果:
1 subgoal (ID 179)
n' : nat
H : ~ even (S n')
IHn : ~ even n' -> even (S n')
============================
even n'
到目前为止，我可以用语言证明这一点:
As far I could prove it in words:
(n'+ 1)甚至不符合H.因此，根据IHn，n'甚至不等于(双重否定)是不正确的:
(n' + 1) is not even according to H. Therefore according to IHn, it is not true that n' is not even (double negation):
IHn : ~ ~ even n'
展开双重否定，我们得出n'是偶数.
Unfolding double negation, we conclude that n' is even.
但是如何用coq编写呢?
But how to write it in coq?
推荐答案
The usual way to strip double negation is to introduce the "excluded middle" axiom, which is defined under the name classic in Coq.Logic.Classical_Prop, and apply the lemma NNPP.
但是，在这种特殊情况下，可以通过显示Prop与布尔函数一致来使用称为 reflection 的技术(您可能还记得本书前面介绍的evenb函数).
However, in this particular case, you can use the technique called reflection by showing that the Prop is consistent with a boolean function (you might remember the evenb function introduced earlier in the book).
(假设您位于IndProp的开头)，您很快将在本章后面看到以下定义:
(Assuming you're at the beginning of IndProp) You'll soon see the following definition later in that chapter:
Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ~ P) : reflect P false.
您可以证明该声明
Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).
，然后使用它在Prop和布尔值(它们包含相同的信息，即n的(非)均匀性)之间移动.这也意味着您可以在不使用classic公理的情况下对该特定属性进行经典推理.
and then use it to move between a Prop and a boolean (which contain the same information i.e. the (non-)evenness of n) at the same time. This also means that you can do classical reasoning on that particular property without using the classic axiom.
我建议完成IndProp中反射"部分下的练习，然后尝试以下练习. (我上传了完整答案此处.)
I suggest to complete the exercises under Reflection section in IndProp, and then try the following exercises. ( I uploaded the full answer here.)
(* Since `evenb` has a nontrivial recursion structure, you need the following lemma: *)
Lemma nat_ind2 :
forall P : nat -> Prop,
P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.
Proof. fix IH 5. intros. destruct n as [| [| ]]; auto.
apply H1. apply IH; auto. Qed.
(* This is covered in an earlier chapter *)
Lemma negb_involutive : forall x : bool, negb (negb x) = x.
Proof. intros []; auto. Qed.
(* This one too. *)
Lemma evenb_S : forall n : nat, evenb (S n) = negb (evenb n).
Proof. induction n.
- auto.
- rewrite IHn. simpl. destruct (evenb n); auto. Qed.
(* Exercises. *)
Lemma evenb_even : forall n : nat, evenb n = true -> even n.
Proof. induction n using nat_ind2.
(* Fill in here *) Admitted.
Lemma evenb_odd : forall n : nat, evenb n = false -> ~ (even n).
Proof. induction n using nat_ind2.
(* Fill in here *) Admitted.
Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).
Proof. (* Fill in here. Hint: You don't need induction. *) Admitted.
Lemma even_iff_evenb : forall n, even n <-> evenb n = true.
Proof. (* Fill in here. Hint: use `reflect_iff` from IndProp. *) Admitted.
Theorem reflect_iff_false : forall P b, reflect P b -> (~ P <-> b = false).
Proof. (* Fill in here. *) Admitted.
Lemma n_even_iff_evenb : forall n, ~ (even n) <-> evenb n = false.
Proof. (* Fill in here. *) Admitted.
Lemma even_Sn_not_even_n : forall n,
even (S n) <-> not (even n).
Proof. (* Fill in here.
Hint: Now you can convert all the (non-)evenness properties to booleans,
and then work with boolean logic! *) Admitted.
这篇关于even_Sn_not_even_n-在另一个假设中应用1个假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
