从头开始证明 coq 中的强归纳答案

【问题标题】：proving strong induction in coq from scratch从头开始证明 coq 中的强归纳
【发布时间】：2019-12-07 15:28:29
【问题描述】：

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

我有这样的定义：

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

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

【问题讨论】：

您要证明的陈述有问题。 strong_induct nP 始终为真，独立于 nP。所以引理真的说nP n -> forall k, k < n -> nP k 这是不真实的。
我不明白你试图证明的引理与证明弱归纳和强归纳之间的等价性有什么关系。您是否难以证明强归纳意味着弱归纳或相反？

标签： coq induction

【解决方案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' 不会让你更进一步。

【讨论】：