Stream: Coq users

Topic: ✔ beginners question on induction

Robert Hoedicke (Nov 29 2022 at 11:02):

Thanks again for the detailed answers.

Notification Bot (Nov 29 2022 at 11:02):

Robert Hoedicke has marked this topic as resolved.

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

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