Search code examples
coqinduction

proving strong induction in coq from scratch

I am in the middle of proving the equivalence of weak and strong induction.

I have a definition like:

Definition strong_induct (nP : nat->Prop) : Prop :=
  nP 0 /\
  (forall n : nat,
    (forall k : nat, k <= n -> nP k) ->
    nP (S n))
.

And I would like to prove the following, and wrote:

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

However I cannot continue the proof any further. How can I prove the lemma in this situation?

Solution

  • Changing the place of forall in the main lemma makes it much easier to prove. I wrote it as follow:

    Lemma strong_induct_is_correct : forall (nP : nat->Prop),
  strong_induct nP -> (forall n k, k <= n -> nP k).

    (Also note that in the definition of strong_induct you used <= so it's better to use the same relation in the lemma as I did.)

    So I could use the following lemma:

    Lemma leq_implies_le_or_eq: forall m n : nat,
  m <= S n -> m <= n \/ m = S n.

    to prove the main lemma like this:

    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.

    This is much a simpler proof and also you can prove a prettier lemma using the lemma above.

    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.

    Note: Usually after using a destruct or induction tactic once, it is not very helpful to use one of them again. So I think using destruct n' after induction n would not bring you any further.