rcases and `@[cases_eliminator]`

Stream: mathlib4

[Yury G. Kudryashov]

Recently, @Eric Wieser marked docs#WithBot.recBotCoe as @[cases_eliminator], so cases and cases' use it instead of the one coming from Option. @Mario Carneiro , how hard would it be to make rcases use it too?

[Kyle Miller]

rcases uses a meta tactic for cases (Lean.MVarId.cases) rather than the the system induction/cases uses. This latter system is not packaged up in any nice way yet. I had looked into getting the meta tactic to use cases_eliminator, but (1) it seemed like a big project and (2) it would interfere with a lot of code that assumes that .cases does the "proper" cases using the actual eliminator.

[Kyle Miller]

Right now, there is a hack in place for specifically Nat so that rcases puts things in terms of 0 and n + 1.

[Eric Wieser]

I think the argument goes that rcases should behave like match, for which custom eliminators aren't relevant?

[Yury G. Kudryashov]

So, if we want to use custom eliminators, then we have to use cases, not rcases, at least in the near future?

[Kyle Miller]

Yeah, there was FRO support for "beautiful Nat induction", and we managed to get @[cases_eliminator] only because that was the easiest and cleanest way to implement it for Nat.

[Eric Wieser]

For which type do you want to do this Yury?

[Yury G. Kudryashov]

WithTop, WithBot

[Yury G. Kudryashov]

I'm just cleaning up remaining uses of none_eq_bot/none_eq_top/some_eq_coe

[Eric Wieser]

Are the rcases calls replaceable with cases'?

[Yury G. Kudryashov]

So far, yes.