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 plainIND
. The goal of this homework (I suppose it is one) is to find, givenP
, how to instantiateQ
inSTRONG
so that it becomes equivalent toIND P
. Usinginduction
defeats the point; use onlyapply
. And conversely, to proveIND_TO_STRONG
, you need to find how to instantiateP
inIND
so that it becomes equivalent toSTRONG
.
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 caseIND -> 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 toapply (H (fun n => ...))
with...
that is not justQ 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