I'm doing some exercises on Coq and trying to prove the strong induction principle for
Lemma strong_ind (P : nat -> Prop) : (forall m, (forall k : nat, k < m -> P k) -> P m) -> forall n, P n.
I've seen similar question on StackOverflow, but this doesn't really helped me. Currently, I have the following:
Proof. intros. induction n. specialize (H 0) as H0. apply H0. intros. inversion H1. specialize (H (S n)) as HSn. apply HSn. induction k. - intros. apply H. intros. inversion H1. - intros. apply Lt.lt_S_n in H0. apply PeanoNat.Nat.lt_lt_succ_r in H0. apply IHk in H0.
With the next context and goal:
1 goal P : nat -> Prop H : forall m : nat, (forall k : nat, k < m -> P k) -> P m n : nat IHn : P n HSn : (forall k : nat, k < S n -> P k) -> P (S n) k : nat IHk : k < S n -> P k H0 : P k ______________________________________(1/1) P (S k)
I had similar goal before doing
specialize (H (S n)) as HSn. already, since it was the induction step. So it feels like really I haven't gotten really any much progress. I've tried doing this in different ways, but still was stuck.
It feels like I should do twice
induction as I did before (induction by
n, then by
k), but it seems I miss something which this "something" is crucial. I also don't see any other way to get things of form
P (S _) except applying
H every time, but it seems to me that this isn't the way it solves. I also think that I need somehow get
forall k : nat, k < m -> P k into my context, I guess this (or something very similar to that) really solves my problem, but probably I don't know enough tactics to retrieve it.
Can anyone help me with this? Thanks in advance!
Edited: thanks to @Pierre Castéran, I have found the solution. But I'm 100% sure the solution can be optimized and shortened. My solution is the following:
Lemma strong_ind (P : nat -> Prop) : (forall m, (forall k : nat, k < m -> P k) -> P m) -> forall n, P n. Proof. intros H n; enough (H0: forall p, p <= n -> P p). - apply H0, le_n. - induction n. + intros. inversion H0. apply H. intros. inversion H2. + intros. apply H. intros. apply IHn. inversion H0. * rewrite H2 in H1. apply Lt.lt_n_Sm_le in H1. assumption. * specialize (PeanoNat.Nat.lt_le_trans k p n H1 H3). apply PeanoNat.Nat.lt_le_incl. Qed.