induction, case, rcases

Stream: mathlib4

[Yury G. Kudryashov]

@Gabriel Ebner @Mario Carneiro , what do you think about making case _ after induction support rcases syntax? Or it's hard to change because rcases is in std, not in core?

[Gabriel Ebner]

To be honest, I really dislike the proliferation of rcases syntax in mathlib4. rcases was absolutely amazing in Lean 3, because we didn't have anything else and because it was a strict superset of the built-in pattern matching syntax. In Lean 4, the rcases syntax conflicts heavily with and doesn't support half of the built-in syntax.

[Gabriel Ebner]

import Std.Tactic.Ext

example (p q : Nat × Nat → Nat) : p = q := by
  ext (x, y) -- syntax error (uses rcases)

example (p q : Nat × Nat → Nat) : p = q := by
  funext (x, y) -- works (uses normal pattern-matching syntax)

[Gabriel Ebner]

In an ideal world, the built-in pattern matching would support nested or-patterns and we wouldn't have a separate rcases. (Although I believe this would be a tad less powerful than the current rcases, because it doesn't work as amazingly with rfl.)

[Yury G. Kudryashov]

Can I use these built-in features in https://github.com/leanprover-community/mathlib4/blob/port/Order.Filter.Basic/Mathlib/Order/Filter/Basic.lean#L371 ?

[Gabriel Ebner]

To get back to your original question, we could add an rcase tactic that accepts rcases patterns. The built-in case tactic doesn't support patterns. (Neither does induction x with | ctor .. =>.)

[Kevin Buzzard]

rintro (h1 | h2) beats lean 4 lambda, right?

[Mario Carneiro]

Yeah, I'm not holding my breath for a grand unification of rcases patterns and regular lean patterns. Lean patterns are literally just term which ties our hands on a bunch of things. I'm more hopeful that we can make rcases patterns subsume term patterns, but you would have to be really careful to avoid ambiguities since there are so many things that could be legal in a term expression (including notations defined after rcases and its pattern grammar is defined)