Stream: Coq users

Topic: ✔ Proving strong ind <-> ind.


view this post on Zulip Vinícius Melo (Feb 27 2022 at 05:02):

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.

view this post on Zulip 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.

view this post on Zulip Vinícius Melo (Feb 27 2022 at 15:13):

Guillaume Melquiond said:

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.

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

view this post on Zulip 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.

view this post on Zulip Vinícius Melo (Feb 28 2022 at 12:29):

Guillaume Melquiond said:

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.

Thanks!

view this post on Zulip Vinícius Melo (Apr 07 2022 at 17:56):

This is still unsolved. Can anyone give me another hint?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Apr 28 2022 at 14:56):

Ok, here is a skeleton for the proof:

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?

view this post on Zulip 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.

Edit: It worked!!!!! Thanks a lot.

view this post on Zulip Notification Bot (Apr 28 2022 at 16:03):

Kard Zorn has marked this topic as resolved.


Last updated: Jun 25 2024 at 15:02 UTC