✔ Proving strong ind <-> ind. · Coq users

I'm trying to prove that strong induction is equivalent to induction, but I am having some trouble. First of all, I've used the tactic induction to prove strongInd -> Ind, but at least it worked.
On the other hand, I cannot prove Ind -> strongInd even using induction tactic.

Guillaume Melquiond (Feb 27 2022 at 06:16):

First, you did not prove STRONG_TO_IND, you just proved plain IND. The goal of this homework (I suppose it is one) is to find, given P, how to instantiate Q in STRONG so that it becomes equivalent to IND P. Using induction defeats the point; use only apply. And conversely, to prove IND_TO_STRONG, you need to find how to instantiate P in IND so that it becomes equivalent to STRONG.

Vinícius Melo (Feb 27 2022 at 15:13):

You are right, I've even said I've used induction because I was having some trouble otherwise.
Any hints?

Guillaume Melquiond (Feb 28 2022 at 12:01):

You should not do just apply H. Indeed, Coq will automatically infer the proposition on which to perform the induction. And in the case IND -> STRONG, it will infer a proposition way too weak for the proof to succeed. Instead, you should provide the proposition yourself, by writing something akin to apply (H (fun n => ...)) with ... that is not just Q n.

Vinícius Melo (Feb 28 2022 at 12:29):

Vinícius Melo (Apr 07 2022 at 17:56):

Ana de Almeida Borges (Apr 07 2022 at 18:51):

The trick is to change your desired goal to something for which the assumption of STRONG will be useful. So here:

  ind : forall P : nat -> Prop,
        P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
  Q : nat -> Prop
  prog : forall n : nat, (forall m : nat, m < n -> Q m) -> Q n
  n : nat
  ============================
  Q n

instead of proving Q n directly, we can prove some other statement by induction on n that implies Q n. (I am just restating what Guillaume already said in other words.)

As for coming up with the statement, well, we are trying to prove strong induction. So, using the n = 3 example, strong induction tells us that in order to prove Q 3 we must first prove Q 0 and Q 1 and Q 2 . With regular induction we have Q 0 as assumption, but how to prove Q 1 and Q 2? Well, the same way we prove Q 3, of course! This is why "strong" induction is actually not strong at all: it has way too many assumptions! So the idea is to prove Q 0 /\ Q 1 /\ Q2 /\ Q 3 instead of only Q 3. The former clearly implies the latter and it is something you can feed to the assumptions of STRONG to obtain Q 3 at the end. If this is clear, try to generalize it to an arbitrary n. If you still struggle, let us know which part is problematic.

Ana de Almeida Borges (Apr 07 2022 at 18:55):

(Also: confirm you understand how the idea I described works on paper before you try to formalize it. You will avoid struggling with understanding the math and Coq at the same time, which makes both processes much simpler.)

Vinícius Melo (Apr 27 2022 at 21:16):

@Ana de Almeida Borges Boa noite, Ana! I believe I understand what you described. However, I still cannot implement it on coq. I always end up in a loop where I can prove the base case 0, then (S 0) and S(S 0) etc, but cannot generalize it. I'm still not sure how to instantiate Q.

Hw: Hweak
Q: nat -> Prop
Hstrong: forall n : nat, (forall m : nat, m < n -> Q m) -> Q n
n, m: nat
Hm: m < S n
k: nat
Hk: k < m
-------------------------------------
Q k

This is as far as I could get. I don't know how to generate the induction hypothesis IHn without using the built-in induction tactic.

Ana de Almeida Borges (Apr 28 2022 at 14:56):

Lemma IND_TO_STRONG: IND -> STRONG.
Proof.
  unfold IND, STRONG.
  intros ind Q prog n.
  cut (forall m, m <= n -> Q m). (* [1] *)
  - admit.
  - generalize dependent n.
    apply (ind (fun n => forall m, m <= n -> Q m)). (* [2] *)
    + admit.
    + admit.
Admitted.

Note how I'm proving forall m, m <= n -> Q m instead of Q n via the cutin [1]. Then in [2] I apply the induction principle to a specific statement. This is the point where usually one would use the induction tactic.

I don't quite understand why in [2] apply ind doesn't work. The ssreflect version, apply: ind, can figure it out, but the regular apply needs a little help, possibly because it gets confused with forall n vs fun n?

Vinícius Melo (Apr 28 2022 at 15:10):

@Ana de Almeida Borges Thanks! I'm gonna try again now. Just for clarification, this is the code relative to my last answer:

Lemma IND_TO_STRONG:
IND -> STRONG.
Proof.
unfold STRONG.
intros Hweak Q Hstrong n. apply Hweak.
  - apply Hstrong. lia.
  - intros m Hm. apply Hstrong.  intros k Hk.   (* I guess this is the point where I'm supposed to use the induction hypothesis *)
Admitted.

Stream: Coq users

Topic: ✔ Proving strong ind <-> ind.

Vinícius Melo (Feb 27 2022 at 05:02):