## Stream: Coq users

### Topic: ✔ Proving strong ind <-> ind.

#### 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.

#### 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):

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?

#### 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):

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!

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

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

#### 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):

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). (*  *)
- generalize dependent n.
apply (ind (fun n => forall m, m <= n -> Q m)). (*  *)
``````

Note how I'm proving `forall m, m <= n -> Q m` instead of `Q n` via the `cut`in . Then in  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 `` `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 *)