The plan to remove cases'

Stream: mathlib4

[Jeremy Tan]

Here is my strategy to remove the cases' tactic from mathlib, a continuation of the discussion here.

I apply the following diff to mathlib:

diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 34ad80c027..944d54b992 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -164,6 +164,8 @@ elab (name := cases') "cases' " tgts:(Parser.Tactic.casesTarget,+) usingArg:(("
       g.assign result.elimApp
       let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
          (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
+      let body ← inferType (targets.get! 0)
+      logWarningAt tgts m!"{body.getAppFn.setPPExplicit true} {subgoals.toList.length}"
       setGoals <| subgoals.toList ++ gs

 end Mathlib.Tactic

Then I am running lake build -q > cases-targets (quiet option) now. This will produce a file mostly containing lines like

warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:209:46: @Exists 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:387:13: @Set.Nonempty 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:430:32: Sum 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:533:47: Sum 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:533:47: Sum 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:533:47: Sum 0
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:533:47: Sum 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:630:13: Prod α γ 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:640:13: Prod γ α 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:656:11: Prod 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:668:13: Prod 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:672:13: Prod 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:685:13: Prod 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:1245:6: @Exists 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:1412:9: Or 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:1513:4: Or 2
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:1783:9: @Membership.mem 1
warning: ././././Mathlib/SetTheory/Ordinal/Arithmetic.lean:1832:9: @Exists 1

where every cases' invocation is tagged with the head of the expression and the number of subgoals generated. Then I can look for specific combinations like Prod 2 or And 1 and replace them automatically via Python with an appropriate rcases or obtain, as the docstring of cases' itself encourages

[Jeremy Tan]

Note that #16451 handles some of the Or 2 instances in that file, which were found in a more primitive way

[Jeremy Tan]

How does this plan sound?

[Jeremy Tan]

cases-targets
here is the resulting targets file

[Jeremy Tan]

Here is the replacement script:

#!/usr/bin/env python3
import re
target_re = re.compile(r"warning: \./\./\./\./(.*?):(\d+):(\d+): ([^ ]+?) .*(\d)\n")
cases_re = re.compile(r"cases' (.*?) with (.*?)(?=\n|;| <;>)")
keys = {}
with open("cases-targets", 'r') as f:
    for l in f:
        if (m := target_re.fullmatch(l)):
            filename, line_n, col_n, head, n_subgoals = m.groups()
            if filename not in keys:
                keys[filename] = {}
            if line_n not in keys[filename]:
                keys[filename][line_n] = {}
            keys[filename][line_n].update({col_n: (head, n_subgoals)})
        elif not l.startswith('⚠'):
            raise ValueError

for (filename, d) in keys.items():
    with open(filename, 'r') as f:
        lines = f.readlines()
    for (line_n, t) in d.items():
        i = int(line_n) - 1
        line = lines[i]
        replacements = []
        for (col_n, (head, n_subgoals)) in t.items():
            if (m := cases_re.match(line, int(col_n) - 7)):
                body, nvars = m.groups()
                nvars = nvars.split()
                nstr = None
                if head == "Or" and int(n_subgoals) == 2:
                    nstr = f"rcases {body} with {' | '.join(nvars)}"
                if nstr != None:
                    replacements.append(m.span() + (nstr,))
        for (start, end, rep) in sorted(replacements, reverse=True):
            line = line[:start] + rep + line[end:]
        lines[i] = line
    with open(filename, 'w') as f:
        f.write("".join(lines))

[Jeremy Tan]

And branch#or2 contains the results

[Yaël Dillies]

I sincerely hope you are not going to replace all proofs of the form

cases' side_condition
· short_proof_in_easy_case
long_unindented_proof

by

cases side_condition
case pos =>
  short_proof_in_easy_case
case neg =>
  long_indented_proof

[Yaël Dillies]

This would be particularly damageable for proofs with two, three, ... side conditions, as then the entirety of the main proof would be indented three or four times, even though are supposed to be, well, auxiliary

[Jeremy Tan]

As of now all replacements in branch#or2 (save for one manual long line linter fix) are really one-line replacements

[Jeremy Tan]

In fact the Python script above can only do one-line-to-one-line replacements

[Yaël Dillies]

Okay, that's reassuring. But reading the diff, I find it to be a clear negative. Why use rcases when cases' does the job?

[Jeremy Tan]

cases', like refine', is a Lean 3-ism

[Yaël Dillies]

You have declared this. I have never seen a consensus on the matter.

[Yaël Dillies]

You must know that I am of the opinion rcases should be obliterated in favour of obtain. Certainly it wouldn't look as bad if you replaced cases' by obtain.

[Yaël Dillies]

But generally I would hope that you can find a better use of your time than doing mass replacements without mass support from the community.

[Jeremy Tan]

Nevertheless some of the other replacements I plan to do will involve obtain

[Yaël Dillies]

... as in? Deleting uses of it? Adding uses of it?

[Jeremy Tan]

And 1, @Exists 1 and the like (producing only one subgoal) are going to be replaced by obtain

[Yaël Dillies]

Yaël Dillies said:

You must know that I am of the opinion rcases should be obliterated in favour of obtain. Certainly it wouldn't look as bad if you replaced cases' by obtain.

@David Ang, the point of this message is not to push for a consensus, but to show there is no consensus. I don't think we should be changing statu quo style towards non-consensus approved style, regardless of the styles in question.

[Jeremy Tan]

@Yaël Dillies the docstring of cases' explicitly discourages its own use:

/-!
# Backward compatible implementation of lean 3 `cases` tactic

...

Prefer `cases` or `rcases` when possible, because these tactics promote structured proofs.
-/

[Jeremy Tan]

(to cases and rcases as the list of suggested replacements obtain is obviously added)

[Yaël Dillies]

This seems to be very recent: #15751 @Michael Rothgang, why mark cases' as deprecated? As explained above, cases can't provide proofs structured according to "unindented proof is the main proof".

[Michael Rothgang]

For induction', I copied that from the tactic docstring to the main module docstring --- and changed cases' by analogy. To me, the wording is not absolute (and does not imply performing mass-replacements), but I am very happy to remove or tweak it (or do review such a PR).

[Michael Rothgang]

Actually, wait: that PR only added to the tactic docstring what was already written in the module docstring: I did not invent that wording, I only made it more prominent.

[Michael Rothgang]

(The rest of my message still applies.)

[Jeremy Tan]

How I see it is that obtain should be used to deconstruct a hypothesis without alternatives (no new goals are generated), cases/rcases otherwise (new goals are generated, i.e. hypothesis specifies alternatives).

[Johan Commelin]

Well... obtain has been used loads of times when there are alternatives, and I think that use case is totally fine and should remain supported.

[Jeremy Tan]

Of course these are merely ideals I am putting forth

[Yakov Pechersky]

Regarding rcases vs obtain, something we had in mathlib3 that I miss is rcases?, for which it's not clear to me how the same would work for some obtain?. The reason being is that code actions so far have modified a line to the right of the expressions in question (exact?%, structure hole) and that is what rcases? does as well. obtain? would need to modify the line to the left of the assignment walrus

[Jon Eugster]

What exactly did rcases? do?

[Yakov Pechersky]

It inspected the type of expression being deconstructed and inserted a pattern that dealt with all the conjunctions and disjunctions

[Damiano Testa]

If I remember correctly, it deconstructed more than conjunctions and disjunctions: I think that it also recursed, for instance, in Nat.succ with a limit of 4 iterations.

[Johan Commelin]

The case (no pun intended) of cases' was discussed amongst maintainers. Our conclusion: it's fine to create PRs that change cases' to cases or obtain etc. But we are not banning cases' in new contributions.

[Kim Morrison]

(And where obtain works, that is preferred, because it results in more readable proofs.)

[Jeremy Tan]

Reviving #16526…

[Rémy Degenne]

I deleted the "depriming" label. Those PRs are marked "tech debt" already, and don't need another super specific label.

[Jeremy Tan]

#16526 is once again ready for review

[Ruben Van de Velde]

Speaking of making sure everyone is one the same line for refactors like this, #21359 replaces induction by induction'

[Kevin Buzzard]

For reasons, I played through NNG today and one thing I noticed was that we still use cases there for lean 4 cases'. I'm not sure the lean4game infrastructure can support |, at least not without a lot of thought. Will we completely lose the ability to write a one-liner which turns one Or hypothesis into two named hypotheses if cases' goes?

[Daniel Weber]

Are you talking about the | in rcases and obtain? Why would that be a problem?

[Jeremy Tan]

It is coming https://github.com/leanprover-community/mathlib4/compare/master...deprime-cases-automated

[Eric Wieser]

I think Kevin is talking about

case some_or with
| inl _ => _
| inr _ => _

[Ruben Van de Velde]

You can always import cases' into nng

[Kevin Buzzard]

@Daniel Weber did you ever try NNG? Usually users type in one command in one line and expect to be done. I'm not sure that cases fits into that paradigm in lean 4 (it did in lean 3)

[Jeremy Tan]

cases-uses

[Jeremy Tan]

#21939 is now ready

[Violeta Hernández]

Out of curiosity, do we have any motivation for doing this besides "tactic duplication is bad"?

[Jeremy Tan]

Violeta Hernández said:

Out of curiosity, do we have any motivation for doing this besides "tactic duplication is bad"?

Higher readability of the replacement tactics

[Kyle Miller]

cases' has also always been the Lean 3 compatibility tactic. The docstring for cases' says to use cases.

[Jeremy Tan]

New version:
cases-uses

[Jeremy Tan]

#21976

[Jeremy Tan]

For some reason the cases' in Data.Seq.Seq operating on a Seq cannot be replaced by rcases or obtain; it has to be replaced by cases in full. Is there a better way?

  cases' s with b s'
  · injection e
  · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
    rw [h_eq] at e
    apply h1 _ _ (Or.inr (IH e))

has to become

  cases s with
  | nil => injection e
  | cons b s' =>
    have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
    rw [h_eq] at e
    apply h1 _ _ (Or.inr (IH e))

[Aaron Liu]

Is this bad?

[Jeremy Tan]

Not if you can come up with a better solution

[Aaron Liu]

Do you like refine s.recOn ?_ fun b s' => ?_ any better?

[Jeremy Tan]

see what others have to say about that

[Jeremy Tan]

There's a somewhat similar problem with WithTop/WithBot

[Jeremy Tan]

But I now should have in branch#option2 a compiling mathlib without any cases' in the main body, Archive or Counterexamples

[Yury G. Kudryashov]

AFAIR, rcases doesn't use custom eliminators.

[Yury G. Kudryashov]

IMHO, verbose cases is OK here. I definitely prefer it to s.recOn.

[Jeremy Tan]

Well, two PRs are awaiting your review

[Jeremy Tan]

Now one (#21976)

[Jeremy Tan]

After #22075 is merged the instances below should be the only cases' remaining:

ℹ [2367/6275] Replayed Mathlib.Data.Seq.Seq
info: ././././Mathlib/Data/Seq/Seq.lean:257:9: Seq [b, s'] 2
info: ././././Mathlib/Data/Seq/Seq.lean:339:13: Seq [x, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:339:35: Seq [x', s'] 2
info: ././././Mathlib/Data/Seq/Seq.lean:339:35: Seq [x', s'] 2
info: ././././Mathlib/Data/Seq/Seq.lean:569:9: Seq [x, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:718:9: Seq [x, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:731:15: Seq [_, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:732:17: Seq [_, t] 2
info: ././././Mathlib/Data/Seq/Seq.lean:733:19: Seq [_, u] 2
info: ././././Mathlib/Data/Seq/Seq.lean:772:13: Seq [_, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:773:15: Seq [_, t] 2
info: ././././Mathlib/Data/Seq/Seq.lean:829:13: Seq [x, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:833:13: Seq [x, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:846:15: Seq [_, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:847:17: Seq [s, S] 2
info: ././././Mathlib/Data/Seq/Seq.lean:848:19: Seq [s, T] 2
info: ././././Mathlib/Data/Seq/Seq.lean:909:9: Seq [c, t₁] 2
info: ././././Mathlib/Data/Seq/Seq.lean:1017:15: Seq [_, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:1018:17: Seq [x, S] 2
info: ././././Mathlib/Data/Seq/Seq.lean:1039:15: Seq [_, s] 2
info: ././././Mathlib/Data/Seq/Seq.lean:1040:17: Seq [S, SS] 2
info: ././././Mathlib/Data/Seq/Seq.lean:1043:19: Seq [x, s] 2

ℹ [4985/6275] Replayed Mathlib.Data.Ordmap.Ordset
info: ././././Mathlib/Data/Ordmap/Ordset.lean:315:9: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:316:11: Ordnode [ls, ll, lx, lr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:317:11: Ordnode [lls, lll, llx, llr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:317:46: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:317:46: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:320:11: Ordnode [ls, ll, lx, lr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:323:11: Ordnode [lls, lll, llx, llr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:323:46: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:323:46: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:580:9: Ordnode [ls, ll, lx, lr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:581:11: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:584:13: Ordnode [rls, rll, rlx, rlr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:584:48: Ordnode [rrs, rrl, rrx, rrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:584:48: Ordnode [rrs, rrl, rrx, rrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:609:11: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:611:13: Ordnode [lls, lll, llx, llr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:611:48: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:611:48: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:642:17: Ordnode [rls, rll, rlx, rlr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:645:17: Ordnode [rrs, rrl, rrx, rrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:653:17: Ordnode [lls, lll, llx, llr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:656:17: Ordnode [lrs, lrl, lrx, lrr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:667:9: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:669:11: Ordnode [ls, ll, lx, lr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:1007:9: Ordnode [s, ml, z, mr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:1071:9: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:1238:9: Ordnode [ls, ll, lx, lr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:1239:9: Ordnode [rs, rl, rx, rr] 2
info: ././././Mathlib/Data/Ordmap/Ordset.lean:1301:6: And [v, e] 1
ℹ [5020/6275] Replayed Mathlib.Data.Seq.WSeq
info: ././././Mathlib/Data/Seq/WSeq.lean:447:15: fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct [h, h] 2
info: ././././Mathlib/Data/Seq/WSeq.lean:507:9: Option (α × WSeq α) [a] 2
info: ././././Mathlib/Data/Seq/WSeq.lean:507:29: Option (α × WSeq α) [c] 2
info: ././././Mathlib/Data/Seq/WSeq.lean:507:29: Option (α × WSeq α) [c] 2
ℹ [5021/6275] Replayed Mathlib.Data.Seq.Parallel
info: ././././Mathlib/Data/Seq/Parallel.lean:175:15: Option (Computation α) [c] 2
info: ././././Mathlib/Data/Seq/Parallel.lean:198:13: Sum [a, ls] 2
info: ././././Mathlib/Data/Seq/Parallel.lean:236:13: Option [c] 2
ℹ [5091/6275] Replayed Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
info: ././././Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean:45:9: @Exists [s, hs] 1
ℹ [5092/6275] Replayed Mathlib.FieldTheory.IsAlgClosed.Classification
info: ././././Mathlib/FieldTheory/IsAlgClosed/Classification.lean:157:9: @Exists [s, hs] 1
info: ././././Mathlib/FieldTheory/IsAlgClosed/Classification.lean:159:9: @Exists [t, ht] 1
info: ././././Mathlib/FieldTheory/IsAlgClosed/Classification.lean:176:9: @Exists [s, hs] 1
info: ././././Mathlib/FieldTheory/IsAlgClosed/Classification.lean:178:9: @Exists [t, ht] 1
ℹ [5095/6275] Replayed Mathlib.ModelTheory.Syntax
info: ././././Mathlib/ModelTheory/Syntax.lean:201:15: Functions [f, f] 2
ℹ [5096/6275] Replayed Mathlib.ModelTheory.Semantics
info: ././././Mathlib/ModelTheory/Semantics.lean:170:13: Functions [_, f] 2
info: ././././Mathlib/ModelTheory/Semantics.lean:448:9: L[[α]].Relations n [R, R] 2
ℹ [5104/6275] Replayed Mathlib.ModelTheory.Substructures
info: ././././Mathlib/ModelTheory/Substructures.lean:709:11: Functions [f, f] 2
ℹ [5119/6275] Replayed Mathlib.FieldTheory.SeparableDegree
info: ././././Mathlib/FieldTheory/SeparableDegree.lean:476:9: Nat [_, _, hprime, _] 2
ℹ [5129/6275] Replayed Mathlib.FieldTheory.Cardinality
info: ././././Mathlib/FieldTheory/Cardinality.lean:70:9: PSum [h, h] 2
ℹ [5170/6275] Replayed Mathlib.Geometry.Euclidean.Circumcenter
info: ././././Mathlib/Geometry/Euclidean/Circumcenter.lean:503:11: PointsWithCircumcenterIndex n [i] 2
ℹ [5176/6275] Replayed Mathlib.Geometry.Euclidean.MongePoint
info: ././././Mathlib/Geometry/Euclidean/MongePoint.lean:168:9: PointsWithCircumcenterIndex (n + 2) [i] 2
ℹ [5249/6275] Replayed Mathlib.GroupTheory.GroupAction.Blocks
info: ././././Mathlib/GroupTheory/GroupAction/Blocks.lean:124:9: @IsTrivialBlock [hB, hB] 2
info: ././././Mathlib/GroupTheory/GroupAction/Blocks.lean:133:9: @IsTrivialBlock [hB, hB] 2
ℹ [5253/6275] Replayed Mathlib.GroupTheory.GroupAction.Primitive
info: ././././Mathlib/GroupTheory/GroupAction/Primitive.lean:143:11: @IsTrivialBlock [H, H] 2
ℹ [5264/6275] Replayed Mathlib.GroupTheory.Perm.Cycle.Concrete
info: ././././Mathlib/GroupTheory/Perm/Cycle/Concrete.lean:140:9: List α [hd, tl] 2
ℹ [5606/6275] Replayed Mathlib.RingTheory.DedekindDomain.Factorization
info: ././././Mathlib/RingTheory/DedekindDomain/Factorization.lean:435:9: Int [n] 2
ℹ [5826/6275] Replayed Mathlib.RingTheory.LaurentSeries
info: ././././Mathlib/RingTheory/LaurentSeries.lean:590:11: Int [s, s] 2
ℹ [5909/6275] Replayed Mathlib.SetTheory.Game.PGame
info: ././././Mathlib/SetTheory/Game/PGame.lean:1865:13: LeftMoves [i, i] 2
info: ././././Mathlib/SetTheory/Game/PGame.lean:1897:58: (mk xl xr xL xR + mk zl zr zL zR).LeftMoves [i, i] 2
info: ././././Mathlib/SetTheory/Game/PGame.lean:1897:58: (mk yl yr yL yR + mk zl zr zL zR).RightMoves [i, i] 2
ℹ [5910/6275] Replayed Mathlib.SetTheory.Game.Basic
info: ././././Mathlib/SetTheory/Game/Basic.lean:928:9: Bool [a, _, a, _, a, _, a] 5
ℹ [6242/6275] Replayed Archive.Wiedijk100Theorems.CubingACube
info: ././././Archive/Wiedijk100Theorems/CubingACube.lean:344:9: @OnBoundary [bi, bi] 2
ℹ [6254/6275] Replayed Counterexamples.CanonicallyOrderedCommSemiringTwoMul
info: ././././Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean:56:11: @LE.le [ab, ab] 2
info: ././././Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean:58:13: @LE.le [ba, ba] 2

[Jeremy Tan]

And #22079 should remove these last stragglers

[Jeremy Tan]

At last, #21832 adds the cases' linter

[Jeremy Tan]

@Damiano Testa I am completely clueless as to how using `....cases solves the import problem

[Jeremy Tan]

Not like this, certainly

/-- `getCases' t` returns all usages of the `cases'` tactic in the input syntax `t`. -/
partial
def getCases' : Syntax → Array Syntax
  | stx@(.node _ kind args) =>
    let rargs := (args.map getCases').flatten
    if kind == `....cases then rargs.push stx else rargs
  | _ => default

[Damiano Testa]

I left a comment: simply remove one backtick and then let the test file make sure that you are using the correct SyntaxNodeKind.

[Jeremy Tan]

what's the difference between one backtick and two?

[Damiano Testa]

Two backticks give an error if it can't find a declaration with that name. It should be preferred, but is not a deal-breaker.

[Jeremy Tan]

OK, I think the main problems with the PR have been sorted out

[Jovan Gerbscheid]

Recently I added Rat.divCasesOn as the default cases lemma for Rat, so that you can unfold a Rat in the natural way. I intended it to be used with cases'. Is the following now the preferred form?

example (r : ℚ) (P : ℚ → Prop) : P r := by
  cases r with
  | h p q nonzero coprime =>
    sorry

[Jeremy Tan]

@Jovan Gerbscheid I have no preference between cases, rcases or obtain. Use whatever floats your boat, but not cases'

[Jovan Gerbscheid]

The issue is that rcases and obtain don't work with custom eliminators. So it leaves only cases. But having to write the name of the case h is a bit awkward.

[Jeremy Tan]

example (r : ℚ) (P : ℚ → Prop) : P r := by
  obtain ⟨p, q, nonzero, coprime⟩ := r
  sorry

[Aaron Liu]

Jovan Gerbscheid said:

The issue is that rcases and obtain don't work with custom eliminators. So it leaves only cases. But having to write the name of the case h is a bit awkward.

So rename the case! h isn't really descriptive anyways.

[Jovan Gerbscheid]

What is a good name for a single case? I feel like there isn't much to describe when there is only one case.

[Aaron Liu]

mk, mkDiv, div, and castDiv are all infinitely better than h.

[Jovan Gerbscheid]

Sounds good, renaming it to div: #22528

[Eric Wieser]

I think | _ p q nonzero coprime is legal too if you really don't want to write the case name

[Eric Wieser]

But explicitly writing div sounds better

[Kyle Miller]

I've been wondering if there should be special syntax for one-constructor case. The current version invites an unnecessary indentation.

Some people use the style

example (r : ℚ) (P : ℚ → Prop) : P r := by
  cases r with | _ p q nonzero coprime =>
  sorry

but that's not guaranteed to work in the future; it might be affected by the proposal to accept empty tactic blocks.

I guess it could be as simple as letting the => be optional if there's one case. I'm not sure about this, but it was the first reasonable syntax I could think of.

example (r : ℚ) (P : ℚ → Prop) : P r := by
  cases r with | _ p q nonzero coprime
  sorry

[Kyle Miller]

It's worth mentioning that this is currently valid:

example (r : ℚ) (P : ℚ → Prop) : P r := by
  cases r with | _ p q nonzero coprime => ?_
  sorry

A missing => could be interpreted as => ?_, when there is just one case.

[Jeremy Tan]

On another note: #22533 removes some induction' and imports of Mathlib.Tactic.Cases

[Jeremy Tan]

@Damiano Testa I had to update #21832 because one new PR introduced four cases'. Can we merge that already to prevent rotting?

[Robert Maxton]

Kyle Miller said:

I've been wondering if there should be special syntax for one-constructor case. The current version invites an unnecessary indentation.

I absolutely would like this. I'm currently dreading the removal of cases', because it's really nice to have the rcases-like "just let me name the variables of a one-case cases" feature on types that have custom cases_eliminators.

Relatedly, the argument against having to write out the case name is the same as the argument for having implicit binders and for not naming unused variables: for a one-case eliminator the name contains zero information, so it shouldn't be referenced.

[Jeremy Tan]

Can't you use obtain for that? It doesn't require naming the case

[Robert Maxton]

obtain goes through rcases, I believe, which means it doesn't use custom recursors