Stream: Coq users

Topic: ✔ beginners question on induction


view this post on Zulip Robert Hoedicke (Nov 29 2022 at 11:02):

Thanks again for the detailed answers.

view this post on Zulip Notification Bot (Nov 29 2022 at 11:02):

Robert Hoedicke has marked this topic as resolved.

view this post on Zulip Robert Hoedicke (Nov 29 2022 at 13:23):

Paolo Giarrusso said:

I would assume that if the induction hypothesis holds for an arbitrary n, it also holds for (S n).

Maybe that's clear by now, but that is never something you can assume: when proving ∀ n, P n by induction for some specific P, you must prove P (S n) assuming only P n, and the only way to do that is by using the properties of your specific P.

You found me out. This is really quite embarrassing. I am glad that the answers to my stupid question yielded much deeper insights (at least for me).

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 13:32):

Oh dear, I never meant embarrassment, only to clarify (if necessary) :-|


Last updated: Feb 09 2023 at 00:03 UTC