search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.78k stars 323 forks source link

Make `rcases` use the `induction`/`cases` framework #3901

Open kmill opened 3 weeks ago

kmill commented 3 weeks ago

Currently rcases uses Lean.MVarId.cases, but the cases tactic uses its own system of applying casesOn.

The rcases tactic should use the same system as cases.

Note that #3747 introduced a hack into Lean.MVarId.cases via the useNatCasesAuxOn argument for the "beautiful Nat induction" project. This should be removed, since this has a general solution via @[induction_eliminator] and @[cases_eliminator] in induction/cases. (The Lean.MVarId.cases is a low-level function that should not use user-defined eliminators.)

nomeata commented 3 weeks ago

The Lean.MVarId.cases is a low-level function that should not use user-defined eliminators.)

Maybe worth renaming. It's confusing if Lean.MVarId.foo and tactic foo are mostly unrelated.