我正在证明弱感应和强感应的等效性。
我有一个类似的定义：
Definition strong_induct (nP : nat->Prop) : Prop :=
nP 0 /\
(forall n : nat,
(forall k : nat, k <= n -> nP k) ->
nP (S n))
.
我想证明以下内容，并写道：
Lemma n_le_m__Sn_le_Sm : forall n m,
n <= m -> S n <= S m
.
Lemma strong_induct_nP__nP_n__nP_k : forall (nP : nat->Prop)(n : nat),
strong_induct nP -> nP n ->
(forall k, k < n -> nP k)
.
Proof.
intros nP n [Hl Hr].
induction n as [|n' IHn].
- intros H k H'. inversion H'.
- intros H k H'.
inversion H'.
+ destruct n' as [|n''] eqn : En'.
* apply Hl.
* apply Hr.
unfold lt in IHn.
assert(H'' : nP (S n'') -> forall k : nat, k <= n'' -> nP k). {
intros Hx kx Hxx.
apply n_le_m__Sn_le_Sm in Hxx.
apply IHn.
- apply Hx.
- apply Hxx.
}
但是，我无法再继续证明。在这种情况下如何证明引理？
更改forall主引理中的位置使证明变得容易得多。我写如下：
Lemma strong_induct_is_correct : forall (nP : nat->Prop),
strong_induct nP -> (forall n k, k <= n -> nP k).
（还请注意，在strong_induct您使用的定义中，<=因此最好在引理中使用与我相同的关系。）
所以我可以使用以下引理：
Lemma leq_implies_le_or_eq: forall m n : nat,
m <= S n -> m <= n \/ m = S n.
证明这样的主要引理：
Proof.
intros nP [Hl Hr] n.
induction n as [|n' IHn].
- intros k Hk. inversion Hk. apply Hl.
- intros k Hk. apply leq_implies_le_or_eq in Hk.
destruct Hk as [Hkle | Hkeq].
+ apply IHn. apply Hkle.
+ rewrite Hkeq. apply Hr in IHn. apply IHn.
Qed.
这是一个更简单的证明，您也可以使用上述引理证明更漂亮的引理。
Lemma strong_induct_is_correct_prettier : forall (nP : nat->Prop),
strong_induct nP -> (forall n, nP n).
Proof.
intros nP H n.
apply (strong_induct_is_correct nP H n n).
auto.
Qed.
注意：通常在一次使用adestruct或inductiontactic后，再次使用它们之一并不是很有帮助。因此，我认为使用destruct n'afterinduction n不会给您带来更多好处。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句