Zulip Chat Archive

Stream: general

Topic: Using `submonoid.closure_induction` with the induction tacti

Eric Wieser (Nov 10 2020 at 09:19):

I'm currently using refine submonoid.closure_induction r.prop (λ x hx, _) _ (λ x y hx hy, _) (where r : ↥some_submonoid), but I was hoping I could use something like induction r using submonoid.closure_induction. Unfortunately, using r gives

invalid user defined recursor, type of the major premise 'x' must be for the form (I ...), where I is a constant

while using r.prop gives

generalize tactic failed, failed to find expression in the target

Is there something odd with the signature of docs#submonoid.closure_induction which prevents the induction tactic understanding it?

Kevin Buzzard (Nov 10 2020 at 11:44):

I always just apply these induction functions -- I didn't even know the induction tactic could use custom functions!

Eric Wieser (Nov 10 2020 at 11:52):

Using the induction tactic has the nice bonus of naming your goals

Last updated: Dec 20 2023 at 11:08 UTC