Simple proof on interchangeability between strong induction and weak induction

w_ind_s_ind.v

(* Proof on interchangeability between strong induction and weak induction.
   Helped by https://github.com/tchajed/strong-induction. *)

Definition w_ind := forall (P : nat -> Prop), P 0 ->
  (forall n, P n -> P (S n))
  -> forall n, P n.

Definition s_ind := forall (P : nat -> Prop), P 0 ->
  (forall n, 0 < n -> (forall k, k < n -> P k) -> P n)
  -> forall n, P n.

Require Import Arith.

Theorem s_imp_w : s_ind -> w_ind.
Proof.
  unfold w_ind, s_ind. intro s_ind.
  intros P P0 H n.
  apply s_ind. assumption.
  intros n'' Hn'' Pn'.
    apply Nat.lt_exists_pred in Hn''.
    destruct Hn'' as [n' [Heq _]].
    subst n''.
  apply H. apply Pn'. auto.
Qed.

Theorem w_imp_s : w_ind -> s_ind.
Proof.
  unfold w_ind, s_ind. intro w_ind.
  intros P P0 H.
  pose (P' n := forall k, k < n -> P k).
  assert (P' 0) as P'0. { unfold P'. intros. inversion H0. }
  assert (forall n, P' n -> P' (S n)) as HH. {
    unfold P'. intros n IHn k Hk. inversion Hk.
    + destruct n; try exact P0.
      apply H. apply Nat.lt_0_succ.
      intros. apply IHn. exact H0.
    + apply IHn. exact H1.
  }
  intro n.
  pose (w_ind P' P'0 HH) as XX.
  unfold P' in XX.
  apply (w_ind P' P'0 HH (S n) n). auto.
Qed.