Stream: Beginner Questions

Topic: Changing variable not being inducted on


view this post on Zulip Ryan Shao (Mar 15 2023 at 19:27):

Hello,

I have a multiple-argument definition fun that takes in three arguments: l, f, and x. I'm proving it's equivalent to some result by inducting on l. As part of the inductive step, I invoke (fun l f (x + 1)), which I thought should be fine as I'm inducting on l and not x but this doesn't seem to work. Could I get some advice?

view this post on Zulip Mathias Fleury (Mar 15 2023 at 19:30):

Usually you should use fun.induct instead of the induction principle from l

view this post on Zulip Mathias Fleury (Mar 15 2023 at 19:31):

The other solution is induction l arbitrary: x


Last updated: Feb 27 2024 at 08:17 UTC