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.

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`

.

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?

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`

.

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!

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

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.

(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.)

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

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 `cut`

in [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`

?

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

Kard Zorn has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC