Fixing rcases for nightly

Stream: mathlib4

[Henrik Böving]

I tried to update mathlib4 to todays nightly over here: https://github.com/leanprover-community/mathlib4/pull/261/files so I can make use of the new csimp attr doc-gen4 (the doc-gen4 master branch CI also deploys the mathlib4 docs so it would break if mathlib4 isnt nightly compatible...).

There is a single thing still missing which is that right now here: https://github.com/leanprover-community/mathlib4/blob/87ed85b650faf850847f5416821e80f3066f302e/Mathlib/Tactic/RCases.lean#L521 ty is already an Option Syntax since Lean now implicity calls .getOptional onto the optional argument. And I'm basically not exactly sure on what to do with it now. Does someone know? Maybe @Mario Carneiro since you are the author of it?

[Mario Carneiro]

The first parameter is just the span for error messages. So something like this should do:

elab (name := rintro) tk:"rintro" pats:(ppSpace colGt rintroPat)+ ty:(" : " term)? : tactic => do
  let ty? := ty.map (Syntax.getOp · 1)
  withMainContext do
    replaceMainGoal (← RCases.rintro (ty.getD tk) pats ty? (← getMainGoal))

[Henrik Böving]

Ah that did the trick yes...unfortunately now all the other tactics start blowing up as well xD, I'll see how far I get^^

[Henrik Böving]

Hmm, the new errors go beyond my rather limited experience in meta world, I think it would be better if $someone else who knows what they are doing takes over there since I don't wanna break anything. (I pushed what I have to the PR)

[Mario Carneiro]

I fixed up the PR. One thing to keep in mind regarding the new behavior of ? in elab args: getOptional? is a lossy operation when used on a parser that produces multiple syntax nodes. So it will almost always have to be disabled in such cases, by using an extra set of parentheses. For example, the rintro code above is incorrect, it should be

elab (name := rintro) "rintro" pats:(ppSpace colGt rintroPat)+ ty:((" : " term)?) : tactic => do
  let ty? := ty.map (Syntax.getOp · 1)
  withMainContext do
    replaceMainGoal (← RCases.rintro ty pats ty? (← getMainGoal))

which is the same as before except that it uses ty:((" : " term)?) instead of ty:(" : " term)?. Using the latter will silently always return none.

[Mario Carneiro]

@Sebastian Ullrich This is arguably a bug in getOptional?. I would suggest that it returns the syntax unchanged wrapped in some if the node has more than one child. (I know that you think multi-arg optional nodes should not exist, but I would really like things like (" : " term)? to Just Work and not need additional wrappers because this is a common case.)

[Sebastian Ullrich]

@Mario Carneiro That would "fix" this use case, yes. But I think $[...]? splices would still misbehave. I'm starting to believe that there is no way around tracking parser "arity" (number of produced nodes) in ParserDescr; I tried before for Parser and gave up because some coercions didn't quite work out, but for ParserDescr we have full control over the translation from stx. Then we could automatically insert the group around " : " term.

[Sebastian Ullrich]

And I wouldn't really be satisfied with ty:(" : " term)? either, as it can further be analyzed only by indexing, not via syntax patterns. It would also be problematic for a type-safe representation of syntax. I assume (" : " ty:term)? would be strictly more helpful, but that's not quite trivial to implement...