induction ... generalizing ... and case tactics

[Kha]

induction e generalizing ids first reverts ids and then reintroduces them in each new subgoal. case n ids focuses on the induction/cases subgoal corresponding to the constructor n and optionally renames identifiers introduced by it using ids. This is nice not just for documentation, but also for avoiding having to name parameters of eliminated cases, and for reordering cases so that simple ones can be solved with a single final tactic.
See in action at Kha/semantics-lean@23965f9#diff-2372531b49c81b52df5a4e3090283065L118

[gebner]

I really like the case syntax. If I understand it correctly, the case tactic traverses the so-far constructed proof left-to-right and picks the first metavariable that is 1) the correct minor premise of the correct recursor-like function and 2) contained in the goal list. After that the local constants are renamed to the provided names using tactic.rename.

I feel that the left-to-right traversal of the proof will result in unintuitive behavior if you reorder the goals (for example using tactic.swap).

[Kha]

I feel that the left-to-right traversal of the proof will result in unintuitive behavior if you reorder the goals (for example using tactic.swap).

That should only happen if you're using case in a nested case goal that you didn't separate with case or { }, which sounds like a bad idea to do in general. But we could also guard against this by flagging an error if we find multiple applicable subgoals.

[gebner]

That should only happen if you're using case in a nested case goal that you didn't separate with case or { }, which sounds like a bad idea to do in general.

I agree, it's unlikely to happen in practice.

But we could also guard against this by flagging an error if we find multiple applicable subgoals.

Then we could no longer do double induction, right?

induction n,
case zero {
 induction m,
 case zero { exact sorry },
 case succ m {
  -- now we should have two subgoals that for the nat.succ constructor
 }
}

[johoelzl]

I also like the case syntax. But the implementation feels a little bit hackish. Would it be possible to add meta-data to meta-variables? Maybe adding a special local constant containing the name.

Then case walks through the goals and selects the first one with the right name. Then cases and induction need to setup the names. But this could be extended: apply could give names based on the binder information.

constructor could also provide names. Then with exactn (i.e. exact at name n) we could construct type class instances, and the remaining cases can be solved by automation.

[Kha]

now we should have two subgoals that for the nat.succ constructor

No, the outer nat.succ subgoal isn't visible from inside case zero's focus tactic (i.e., it isn't returned by get_goals).

[Kha]

I also like the case syntax. But the implementation feels a little bit hackish.

Sure, it's not pretty, but it should be quite robust. Having to implement a metadata management system and teach it to all interested tactics sounds much more involved. And we could even incorporate all your examples into the current approach without having to touch those tactics at all - with the minor caveat that it would match an argument goal of the given name in any application created from any tactic :) . Still, it should do the right thing in realistic scenarios like directly after apply or constructor. But it should probably be a separate tactic from case.

[Kha]

By the way, a colleague just reminded me that in Isabelle you can also select goals by type using show. For parameters, I think I would prefer that over selecting by name, but of course we can also implement both.

[leodemoura]

By the way, a colleague just reminded me that in Isabelle you can also select goals by type using show. For parameters, I think I would prefer that over selecting by name, but of course we can also implement both.

This is useful. show is a keyword in Lean, but we can add special support for this at tactic_notation.cpp.

[Kha]

It would probably be preferable if we could add new tactic "keyword arguments" without changing the global token table. For identifier-like keywords, we could do that with a scanner decorator (both before and after implementing lookahead).

[leodemoura]

Did you try to use the lean command precedence?

[Kha]

You mean I should do

precedence `generalizing` : 0

instead of changing token_table.cpp? That's definitely better, right, but it would still be even better if it was a keyword just in that tactic instead of globally.

[leodemoura]

You mean I should do precedence generalizing : 0 instead of changing token_table.cpp?

Yes.

it would still be even better if it was a keyword just in that tactic instead of globally.

I think this may produce ambiguity. Example: suppose the user has declarations named generalizing