1
$\begingroup$

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:

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.
$\endgroup$
1
  • $\begingroup$ In my experience, it's easier to prove (forall m, (forall k : nat, k < m -> P k) -> P m) -> (forall m k, k < m -> P k) where the outer k < m acts as some kind of accumulator. I have a proof like that with fancy types. $\endgroup$
    – gallais
    Jun 13 at 18:10

1 Answer 1

3
$\begingroup$

A classic solution is to define a stronger property, which you prove by induction.

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.
    (* ... *)
Qed.
$\endgroup$
1
  • $\begingroup$ Thank you! Via this, I've solved the puzzle. The only thing is that perhaps my solution is not optimal and maybe it might be shorten. $\endgroup$ Jun 13 at 17:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.