Stream: Coq users

Topic: induction on n


view this post on Zulip zohaze (Oct 26 2021 at 00:11):

I have natural number n as input argument in a function. Have pattern matching on it , It may be 0 or S n'. When I perform induction I get 0 & S n. S n is some greater number of n. But it should be S n'( any number not necessary greater).Why this happen?

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 00:56):

S n is not a bigger number than the original n, because it uses an unrelated n.

view this post on Zulip Paolo Giarrusso (Oct 26 2021 at 00:59):

the tactic "induction n" removes the original n from the context, and introduces an unrelated n.


Last updated: Jan 29 2023 at 01:02 UTC