从头证明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战术之后，再次使用它们之一并不是很有帮助。因此，我认为在destruct n'之后使用induction n不会给您带来更多好处。