Is cases' deprecated?

Stream: mathlib4

[Kevin Buzzard]

I looked in the style guide but I didn't see any mention of whether cases' is still an OK tactic to use. I just saw an instance of it in #12156:

theorem zero_of_hom_zero {x : Γ₀} (hx : IsRankOne.hom v x = 0) : x = 0 := by
  have hx0 : 0 ≤ x := zero_le'
  cases' le_iff_lt_or_eq.mp hx0 with h_lt h_eq
  · have hs := IsRankOne.strictMono v h_lt
    rw [_root_.map_zero, hx] at hs
    exact absurd hs not_lt_zero'
  · exact h_eq.symm

and here both hypotheses need to be named, so if you do cases then must you end up with a longer proof and/or longer lines? I was reluctant to suggest that the author change it to cases when I couldn't make it more compact as well.

[Ruben Van de Velde]

I would personally not use cases', but I don't think there's yet a consensus. cases would take one more line. If you want compact, try .symm <| hx0.eq_or_lt.resolve_left ...

[Kim Morrison]

It isn't deprecated, perhaps mostly out of hope that one day we will have a tool for automatic replacement. I think it would be reasonable to have a rule against new uses, in any case.

[Kyle Miller]

An intermediate style that I like to use if I don't want to figure out the names of the constructors is

theorem zero_of_hom_zero {x : Γ₀} (hx : IsRankOne.hom v x = 0) : x = 0 := by
  have hx0 : 0 ≤ x := zero_le'
  cases le_iff_lt_or_eq.mp hx0
  next h_lt =>
    have hs := IsRankOne.strictMono v h_lt
    rw [_root_.map_zero, hx] at hs
    exact absurd hs not_lt_zero'
  next h_eq =>
    exact h_eq.symm

That said, I don't think we need a rule against cases'. It's fair to suggest alternatives however.

[Kevin Buzzard]

That suggestion is even two lines longer than the cases' variant

[Kim Morrison]

The "return" key on most keyboards is pretty durable, Kevin. :-)

[Kim Morrison]

(That is, number of lines is not something we should be optimising for. It's structurally the same proof, so the only relevant questions are maintainability / readability.)

[Mario Carneiro]

rcases is often a much smaller diff from cases', and it's available in core

[Mario Carneiro]

I think we can deprecate cases' in favor of rcases, obtain, cases. I think there are no cases where cases' is actually better than all three of those alternatives

[Ruben Van de Velde]

Now if only cases supported rcases patterns :)

[Kevin Buzzard]

I'm visiting Johan today and we had a discussion about this during which he revealed that he didn't use rcases because it wasn't an English word and so it made the code look more confusing. He convinced me that obtain is best.

[Yaël Dillies]

I deeply agree with Johan on this

[Mario Carneiro]

I also agree, I prefer obtain over rcases, not just because of the non-word but also because the argument order is more sensible. There are some cases where you might prefer rcases argument order, e.g. if it's a really big or complex match, but in those cases you are probably better off using cases or match with their more heavyweight (but better documenting) syntax

[Mario Carneiro]

(in case you weren't aware, obtain and rcases are basically the same tactic, they just have slightly different syntax to the same backend)

[Richard Osborn]

Things would be simpler if intro and have were invisibly upgraded to their more powerful variants in mathlib (rintro & obtain). I'm guessing mathlib doesn't want to diverge from standard lean? I know have can be used in term mode, so perhaps it would be confusing if its behavior was different between the two modes.

[Mario Carneiro]

it's not quite as simple as that, intro and have have also leveled up in lean 4 and the grammar is incomparable with rcases patterns

[Mario Carneiro]

for example you can write have (a, b) := c but that's not legal obtain syntax

[Ruben Van de Velde]

I'd say the optimal solution would be that core lean adopts a syntax for have, cases, intro and suffices that supports all use cases that are currently supported in the r* variants

[Jireh Loreaux]

I have also switched from rcases to obtain in all situations for readability purposes.

[Mario Carneiro]

Ruben Van de Velde said:

I'd say the optimal solution would be that core lean adopts a syntax for have, cases, intro and suffices that supports all use cases that are currently supported in the r* variants

The issue here is that have, let, and match get their flexibility by allowing a term for the pattern, which is powerful but also limiting because it means you have less ability to have specialized syntax (like the - rcases pattern for clearing assumptions) without polluting the term category for everything else

[Richard Osborn]

Mario Carneiro said:

it's not quite as simple as that, intro and have have also leveled up in lean 4 and the grammar is incomparable with rcases patterns

Is there a path to making obtain a strict superset of have?

[Johan Commelin]

How many use cases are there in practice for non-trivial term patterns (that aren't simple variants of rcases patterns)? Because if there aren't too many, it might be an idea to put them behind some flag or switch.

[Mario Carneiro]

I use have/let ⟨a, b⟩ := c all the time

[Mario Carneiro]

(I use those keywords basically in free variation, since it doesn't matter, they both act like have when doing destructuring)

[Mario Carneiro]

an example of a nontrivial pattern which isn't covered by rcases is let a :: l := l', which you will be surprised to know is actually legal sometimes

[Mario Carneiro]

example {f : α → β} (l : List α) (h : (l.map f).length = 4) : True := by
  let a :: l := l
  trivial

[Jireh Loreaux]

What is going on there that Lean knows this is legal?

[Mario Carneiro]

it desugars to a match expression with (generalizing := true), and so in the missing match arm lean tries to prove the context is inconsistent via injection

[Jireh Loreaux]

:astonished: that's some black magic.

[Mario Carneiro]

Conversely, a case where lean's pattern matching is less powerful than rcases's is fun rfl vs rintro rfl, because the former will not generalize variables not participating in the match. This one is specifically problematic for unification of the two syntaxes because they are both using the same syntax

[Mario Carneiro]

example : a = 4 → a + a = 8 := by
  refine fun | rfl => ?_
  -- ⊢ a + a = 8

example : a = 4 → a + a = 8 := by
  rintro rfl
  -- ⊢ 4 + 4 = 8

[Richard Osborn]

Could we change the rcases syntax? I know some people have wanted rcases to support ← and → for rewriting.
i.e. obtain → : some_prop := by proof instead of rw [show some_prop by proof].

[Mario Carneiro]

that syntax makes no sense at all to me

[Mario Carneiro]

what is being rewritten and where?

[Jireh Loreaux]

I think the idea is that some_prop is an equality or iff, and you are immediately rewriting with it in the goal.

[Jireh Loreaux]

Rocq has something similar to this, and it came up at LftCM

[Mario Carneiro]

yes, rintro patterns are very similar to (a small subset of) intro patterns in ssreflect

[Mario Carneiro]

I do get worried about the readability aspect of these extensions though

[Mario Carneiro]

from a technical standpoint there is no obstruction to doing this

[Mario Carneiro]

it an example of how not using term gives us more flexibility to do these things

[Richard Osborn]

example (h : a = 4) : a + a = 8 := by
  -- assume h is a long proof
  -- obtain → : a = 4 := h
  rewrite [show a = 4 by exact h]
  -- ⊢ 4 + 4 = 8

[Richard Osborn]

I agree that readability could be a concern, but rfl in rcases doesn't seem to impact readability negatively, so I can't imagine ← and → to be worse.

[Mario Carneiro]

rfl is actually a pattern though

[Mario Carneiro]

which is to say, it makes sense as a term that we are matching against

[Jireh Loreaux]

The thing that struck me about the ssreflect syntax was the tight integration. It seemed to me that many of the specialized features in one tactic were available in other tactics with the same syntax. However, if only one specialized feature is available in one tactic and a different one in another, then it gets hard to remember.

[Mario Carneiro]

well rcases patterns are used by several tactics, so it's not that crazy

[Mario Carneiro]

but indeed it sucks that we have three four separate pattern languages:

1. have, let, match, intro, fun: uses terms as patterns
2. obtain, rcases, rintro, ext, rcongr/ congr!, convert: uses rcases patterns
3. cases, induction: uses binder names as patterns
4. match_expr, let_expr: uses constants

[Jireh Loreaux]

Sure, I'm not necessarily saying it's bad, but I think this kind of tight integration is what we should be striving for. So, medium-term, it would be great if we could, for example, unify have and obtain (possibly with a term flag) and obliterate rcases. Obviously this is a bit tricky, but I believe it's a good goal. Joachim Breitner mentioned a while ago that the fewer the tactics the better, and I have come to agree with that.

[Mario Carneiro]

No, I mean that the so called "tight integration" is in fact provided by the fact that there are many tactics that use the same pattern language as rcases, so if you learn rcases patterns you can use them in all of those cases

[Mario Carneiro]

the trouble is that 1 and 2 are incompatible approaches and both have significant uptake in lean

[Mario Carneiro]

4 looks like a slightly lazy tactic implementation so I'm not too worried about it, but 3 also has its strengths and weaknesses over the others so I'm not sure what we can do

[Mario Carneiro]

I worry though that if we just directly overload e.g. have and obtain it will become more confusing, not less, because sometimes you will be getting 1 and other times 2 and there isn't a clear indication of which is which

[Johan Commelin]

Is there any symbol that terms can't start with, that could be used as a sigil to indicate that what follows is an rcases pattern?

[Kim Morrison]

How about as a start we see if we can largely remove uses of rcases in favour of obtain, since it seems everyone likes that direction?

[Mario Carneiro]

I think both of these (cases' -> rcases, rcases -> obtain) should wait until we have the global refactor tool, as this is a perfect use case for it

[Yaël Dillies]

Johan Commelin said:

Is there any symbol that terms can't start with, that could be used as a sigil to indicate that what follows is an rcases pattern?

$?

[Yaël Dillies]

Ah sorry that would rather be to show rhat something isn't a rcases pattern

[Johan Commelin]

Ooh, that might also work.

[Sebastian Ullrich]

Funnily enough, $ is the one character basically anything in Lean can start with, because of syntax quotations. At least when followed by an ident or open paren.

[Johan Commelin]

But an rcases pattern can not start with it. So the strategy could be "if the argument starts with $ then strip it off and treat the remainder as a term pattern like have does; otherwise, treat the argument as rcases pattern"

[Mario Carneiro]

no, rcases patterns can start with $

[Mario Carneiro]

sebastian is right, $ is a uniquely bad option because $ can be the start of an antiquotation in any syntax category

[Mario Carneiro]

note, this is valid lean syntax

example := `(by rcases x with $pat)

[Frédéric Dupuis]

I'm not sure I like using obtain instead of rcases in all situations. When there's an actual case split going on, rcases sounds more natural I think.

[Ruben Van de Velde]

Maybe € instead of $, then

[Jon Eugster]

I think this is very well worth thinking about there is already a topic about this: Zulip topic (I posted to the wrong topic, maybe they should be merged anyways?)

Some summary from that topic:

Kim Morrison said:

[cases'] isn't deprecated, perhaps mostly out of hope that one day we will have a tool for automatic replacement. I think it would be reasonable to have a rule against new uses, in any case.

Mario Carneiro said:

I think we can deprecate cases' in favor of rcases, obtain, cases. I think there are no cases where cases' is actually better than all three of those alternatives

Many people (including Yael, Johan, Jireh, Ruben - and I'd include myself too) express there opinion about obtain being better than rcases

Kim Morrison said:

How about as a start we see if we can largely remove uses of rcases in favour of obtain, since it seems everyone likes that direction?

Kim Morrison said:

[...] number of lines is not something we should be optimising for. It [an example provided] is structurally the same proof, so the only relevant questions are maintainability / readability.

From that topic the conclusion seems to be that cases' and rcases would ideally not be used in favour of rcases obtain (! I cannot type), but maybe that could be discussed here again.

@Jeremy Tan maybe you could make a poll here whether that's indeed what we want and also how rigorous we should address this.

[Jeremy Tan]

/poll Should cases' and rcases be deprecated in favour of obtain and cases?
Yes
cases' only
No

[Ruben Van de Velde]

I'm in favour of deprecating for new code, less excited about going around changing existing code

[Jon Eugster]

I was thinking of slightly more refined options, but I guess this is a valid response for the prompt I've given :sweat_smile:

[Kevin Buzzard]

Frédéric Dupuis said:

I'm not sure I like using obtain instead of rcases in all situations. When there's an actual case split going on, rcases sounds more natural I think.

I was neutral on this question until recently, when I heard Johan argue that obtain might be preferred to rcases on the basis that obtain is an actual word basically being used to mean something which it means in regular English, whereas rcases is not a word and something which we've just become used to as a community. I don't think I've used rcases ever since. But I still don't really have a strong opinion about what to make the community do, I just currently have a personal preference.

[Shreyas Srinivas]

Deprecated in what sense? Will old proofs break after lake update or will mathlib PRs be required to avoid using cases'?

[Jeremy Tan]

Shreyas Srinivas said:

Deprecated in what sense? Will old proofs break after lake update or will mathlib PRs be required to avoid using cases'?

I envision cases' being first deprecated like normal declarations are, and then finally removed from mathlib

[Shreyas Srinivas]

Why break proofs outside mathlib, when you can just lint out its uses inside mathlib?

[Shreyas Srinivas]

To be specific, I'd say, let the tactic remain, but lint out its uses inside mathlib. This way downstream users don't get bothered needlessly.

[Violeta Hernández]

I'm all for removing redundancy, and the argument about rcases being a meaningless word is pretty compelling too. But unless there's a nontrivial maintenance cost I think it should only be linted within Mathlib, at least for the near future.

[Eric Wieser]

There's also the question here of whether obtain actually needs to exist at all in the presence of have pattern matching - should core expand its pattern-matching dialect to absorb "obtain/rcases" patterns?

[Ruben Van de Velde]

I think that would be great, though I understood that there's some incompatible overlap between the sunglasses syntaxes

[Joseph Myers]

It seems quite a few things have an "only be linted within Mathlib" conclusion. Is there a simple way for a non-mathlib project to put something in lakefile.toml to opt into all such lints, present and future, without needing to hardcode a list (for projects that aim to put their code into mathlib or the mathlib archive, so want all mathlib-only lints applied now rather than only discovering issues later at the point of PRing to mathlib)?

[Jeremy Tan]

All right, #16526 constitutes the first automated replacement of cases' in mathlib

[Jeremy Tan]

There are about 1800 uses right now and this PR removes about 450 of them

[Shreyas Srinivas]

I don't see any consensus reached yet. Why the urgency for the PR?

[Jeremy Tan]

There is a consensus, as shown by the poll, that cases' must go

[Shreyas Srinivas]

There is no consensus on the form the deprecation should take

[Shreyas Srinivas]

Because that was not asked in the poll

[Shreyas Srinivas]

Of course I think the votes so far indicate that the uses of cases' within mathlib should be removed

[Eric Wieser]

Jeremy Tan said:

There is a consensus, as shown by the poll

Usually it's best to leave polls for (at least) a few days before declaring consensus.

[Shreyas Srinivas]

Also, consensus implies that everyone agrees. There are a few different opinions that are being discussed

[Jon Eugster]

@Joseph Myers I think there should be a set_option linter.style.all true (or something thelike) which enables all mathlib-only style linters. It might not exist yet, but it would certainly be useful to have, and I'll make a PR eventually if nobody else does it first. (but that's a different topic)

[Jon Eugster]

derprecating/removing the tactic itself is a bad idea, as people mentioned, because of the usage in downstream projects. And we do have tactics in mathlib which are essentially not used in code but they are still exist for people's convenience. The modified have is such an example. Most primed tactics would probably fit well on this list too.

[Jon Eugster]

For a starter, Jeremy's #16526 does seem like a strict improvement; I would have chosen obtain h | h := ..... instead, but again that's currently only a "preferred style"

[Robert Maxton]

I really wish I had noticed when this thread was active, because I would have argued quite militantly for leaving cases' alone!

cases' is useful when

• you have a custom recursor you want to use (this automatically excludes everything based on rcases, which is nearly everything outside of core)
• the custom recursor only has a single case
• you want to name the resulting parameters

In this scenario, there is still no satisfactory replacement for cases'; the closest is

cases x using recOn_foo with | bar x y =>

which is a) incredibly ugly and b) requires you to remember and include the specific name of the constructor, which is otherwise zero-data.

[Robert Maxton]

In general, I'm not sure why we should go out of our way to be deprecating/discouraging tactics like this at all, rather than just letting people use what they find comfortable; the question of maintainability is one that should be resolved by ensuring that similar tactics are in fact just different front-ends to the same internal machinery, rather than insisting that we have exactly one set of external interfaces that necessarily does not cover all uses. Having primed tactics is something I considered a strength of Mathlib.

[Patrick Massot]

I think it is very much worth the trouble to reduce the number of tactics used in Mathlib. They create a big barrier to entry for very little added value. There is a lot of nearly duplicated tactics for historical reasons.

[Michael Rothgang]

Note that nobody is preventing anyone from using cases' in projects depending on mathlib. But having a more uniform style (and formatting, etc) is very much worth it.

Disallowing basically synonymous tactics, if they are not used, feels worth the uniformity benefits to me.

[Michael Rothgang]

That said: if there I'd a way to make cases/obtain/rcases look nice in the setting you describe, I believe many people would be happy to see that.

[Michael Rothgang]

Do you have some idea how often this occurs in mathlib?

[Kevin Cheung]

I have been using rcases a lot. How might using obtain in place of rcases look like? Any example will be greatly appreciated.

[Yaël Dillies]

rcases proof with patt becomes obtain patt := proof

[Ruben Van de Velde]

Robert Maxton said:

I really wish I had noticed when this thread was active, because I would have argued quite militantly for leaving cases' alone!

cases' is useful when

• you have a custom recursor you want to use (this automatically excludes everything based on rcases, which is nearly everything outside of core)
• the custom recursor only has a single case
• you want to name the resulting parameters

In this scenario, there is still no satisfactory replacement for cases'; the closest is

cases x using recOn_foo with | bar x y =>

which is a) incredibly ugly and b) requires you to remember and include the specific name of the constructor, which is otherwise zero-data.

Minor point: I think this works, so you don't need to remember the constructor name:

cases x using recOn_foo with | _ x y =>

[Kyle Miller]

For a one-line version, I'd recommend cases x using recOn_foo with | _ x y => ?_. That makes it be a single tactic rather than have any nesting.

I think in core we're moving to allow cases x using recOn_foo with | _ x y to make it a little easier to type.

[Robert Maxton]

Patrick Massot said:

I think it is very much worth the trouble to reduce the number of tactics used in Mathlib. They create a big barrier to entry for very little added value. There is a lot of nearly duplicated tactics for historical reasons.

Do they, though? I think this is mostly an artifact of the lack of good (esp. good "canonical") documentation for tactics. To my knowledge the only way of getting any sort of systematic coverage of what tactics are available is through Haruhisa's trick, which yes, results in a big barrier to entry that scales with the number of tactics. But if we had, in any of our three major documentation sources, a guide to the most common/"center path" tactics that work most of the time in each field, then having variants IMO ceases to be a barrier to entry; new users should follow the documentation and use the rarely-changing shortlist of common tactics to get started, and treat the variants as "advanced usage."

... Actually, do the various textbooks take PRs? Because I might just contribute an appendix somewhere myself.

[Robert Maxton]

Michael Rothgang said:

That said: if there I'd a way to make cases/obtain/rcases look nice in the setting you describe, I believe many people would be happy to see that.

rcases etc would work great, aesthetically speaking; the problem is that for reasons I admittedly don't really understand, the rcases machinery (and therefore everything derived from it) can't hook into the same elab_as_elim, cases_eliminator setup that the core cases does, so it's just not applicable. If we could write

rcases X using casesOn_foo with ⟨x, y, ...⟩

I'd have no further objections; my objection is to deprecating cases' without a satisfactory replacement. (The "dangling single case" doesn't count, especially with the extra unnamed metavariable.)

[Kyle Miller]

It's not that it can't hook in, it's just that it hasn't, mostly because the framework for cases/induction hasn't been made into an API yet.

There's a hack in place right now so that rcases etc. use the custom eliminator for Nat, which is why everything is in terms of 0 and n + 1 instead of Nat.zero and Nat.succ n.

[Robert Maxton]

Mm. Could you go into detail somewhere? I'd be willing to put my time toward fixing that, if there isn't a major theoretical obstacle.

[Kyle Miller]

I don't think this is something the FRO would want from an external contributor, sorry, but I think that it's possible that we could see progress here. The biggest challenge will be the time to fix mathlib, since I have to imagine that a lot of mathlib would break...

The core of this is that the rcases family uses Lean.MVarId.cases, which is really meant for low-level casing. I tried making it use the cases_eliminator, but it breaks Lean internals catastrophically (e.g. the processing of match expressions, and generating equation lemmas). We need to expose a version of the cases tactic frontend that isn't so tied to the cases tactic.

(By the way, elab_as_elim is not relevant. That's a way to get the app elaborator to elaborate the arguments using the expected type in a different way.)

[Robert Maxton]

Kyle Miller said:

I don't think this is something the FRO would want from an external contributor, sorry, but I think that it's possible that we could see progress here. The biggest challenge will be the time to fix mathlib, since I have to imagine that a lot of mathlib would break...

Mm. Unfortunate, but I'll keep watching, I guess. Let me know if there's anything I can do to help.

The core of this is that the rcases family uses Lean.MVarId.cases, which is really meant for low-level casing. I tried making it use the cases_eliminator, but it breaks Lean internals catastrophically (e.g. the processing of match expressions, and generating equation lemmas). We need to expose a version of the cases tactic frontend that isn't so tied to the cases tactic.

How does cases itself do it, then?

[Kyle Miller]

It's mostly in this file, and here's the entry point: https://github.com/leanprover/lean4/blob/29303b37b8f8b7f2f92057cf07b1800d374c7487/src/Lean/Elab/Tactic/Induction.lean#L932