从零开始证明 coq 的强归纳法

Question

我正在证明弱归纳法和强归纳法的等价性。

我的定义如下：

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.
        }

但是我无法继续证明了。在这种情况下如何证明引理？

Answer 1

改变主引理中 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.

注意：通常在使用一次destruct或induction战术后，再次使用其中一个并没有太大帮助。所以我认为在 induction n 之后使用 destruct n' 不会给你带来任何进一步的好处。

从零开始证明 coq 的强归纳法

proving strong induction in coq from scratch

coq

induction