Stream: Beginner Questions

Topic: Doing induction on two variables


view this post on Zulip Gergely Buday (Jan 27 2021 at 11:21):

Suppose you have a goal of the form P(a) + P(b) = P(a+b) or something similar.

Sometimes (induction a) auto ...

sometimes (induction a b) auto ...

even other times (induction a arbitrary: b) auto ... works

Is there a rule, not necessarily formal, that tells us which one should I use?

view this post on Zulip Gergely Buday (Jan 27 2021 at 11:22):

... and sometimes (induction a rule: function.induct ) is needed


Last updated: Sep 25 2021 at 09:17 UTC