Error Location and infoview message for induction

Stream: lean4

[Shreyas Srinivas]

When using the lean4 variant of induction or cases, the following things happen which I find odd. Let me illustrate with an #mwe:

import Mathlib.Tactic

@[simp]
def linearListReversalInternal (xs : List α) (acc : List α) : List α :=
  match xs with
  | [] => acc
  | l :: ls => linearListReversalInternal ls (l :: acc)

@[simp]
def linearListReverse (xs : List α) := linearListReversalInternal xs []

@[simp]
def naiveListReverse (xs : List α) :=
  match xs with
  | [] => []
  | (y :: ys) => ys ++ [y]


lemma reversal_identical :
  ∀ l : List α, linearListReverse l = naiveListReverse l := by
  intro l
  induction l with -- Tactic State : No goals

  done


-- error bar here

1. As soon as I type the with, my infoview says "No goals". The case distinctions are visible if the "with" is not inserted
2. The red squiggly line appears well after donewhich is the last line of the proof presumably (I think it is the parser for induction that is reading too far here). In fact I can push the error further down by adding newlines at the end of my file.
3. If I use the case succ n ih style (assuming Nat), and if I have already inserted done. then as I type case ..... , done is treated as the name of one of the hidden variables until I type the => of the case arm.

[Shreyas Srinivas]

Of these problems, the most annoying UX-wise is 1. IIRC, 2 and 3 have been discussed before and I thought they were resolved already.

[Kyle Miller]

induction allows a tactic at the beginning of the with clause, but there's no constraint on the column that that tactic appears in, so it seems done is being used as that tactic. There probably should be a colGt in here.

The error you see is because induction ... with ... expects one or more cases. Maybe the tactic should permit zero cases for parsing purposes?

[Shreyas Srinivas]

the problem is if I don't use with, I can see which cases remain on the infoview and I can start | base_case ...

[Shreyas Srinivas]

This doesn't happen with induction' l with .... The tactic state still shows all the cases.

[Kyle Miller]

Right, so if it permits zero cases, it can parse, and then when the tactic executes it can report all the cases you're missing.

[Shreyas Srinivas]

even if it is not done parsing, why should the tactic state disappear or show "no goals"?

[Kyle Miller]

I find that when there are parsing errors, sometimes tactic execution gives up completely, but it does seem like something is executing here. One tell-tale I think for why induction isn't doing anything is that done should have an error that the cases weren't done.

[Kyle Miller]

So we're looking at the same thing, here's the parser for induction:

syntax inductionAlts := " with" (ppSpace tactic)? withPosition((colGe inductionAlt)+)

syntax (name := induction) "induction " term,+ (" using " ident)?
  (" generalizing" (ppSpace colGt term:max)+)? (inductionAlts)? : tactic

I think it would be more friendly with

syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)*)

[Kyle Miller]

It would also be nice if the tactic would show you the tactic state for missing alternates, rather than just saying the name of the case.

[Shreyas Srinivas]

It would definitely be friendlier, but will it fix the no goals issue?

[Shreyas Srinivas]

I would like to see the remaining goals so that I know which arm I want to work on next and variable names I want to introduce.

[Shreyas Srinivas]

I removed the done. The issue doesn't go away. I still get no goals

[Kyle Miller]

Your item (1) is in an uncertain state right now because, so long as there are parse errors, I feel like you can't really trust what the infoview is showing you. I think you'll still see "no goals", but you'd have a much more informative error message displayed by the induction tactic.

[Shreyas Srinivas]

induction' seems to give no trouble.

[Shreyas Srinivas]

Kyle Miller said:

Your item (1) is in an uncertain state right now because, so long as there are parse errors, I feel like you can't really trust what the infoview is showing you. I think you'll still see "no goals", but you'd have a much more informative error message displayed by the induction tactic.

I kinda get why you say that, but from a UX standpoint I usually need to see the induction cases before choosing the arms. So maybe the zero arm induction needs to be a non-error as you say.

[Kyle Miller]

induction' is a completely different tactic, and its with clause is for just choosing names

[Kyle Miller]

While I think this should still be fixed in some way, do you know about the code action that appears if you don't include with?

[Shreyas Srinivas]

I don't get a code action on the web editor until I type with

[Kyle Miller]

In the live.lean-lang.org playground I get it without the with

image.png

[Shreyas Srinivas]

okay it appears a bit late. But yes I get it now. Both web and vscode.

[Shreyas Srinivas]

Kyle Miller said:

Right, so if it permits zero cases, it can parse, and then when the tactic executes it can report all the cases you're missing.

Could we try this?

[Kyle Miller]

I think so

[Shreyas Srinivas]

should I raise an issue (bug or RFC?)?

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Kyle Miller]

Yeah, I think you could write an issue with an mwe of your example, how it's confusing both with and without done, and that you expect it to report an error about the missing cases.

Here's an mwe I just came up with:

example (n : Nat) : True := by
  induction n with

[Shreyas Srinivas]

making it error free will still leave problems 2 and 3, but I guess that is more convoluted. I would say making done an optional token to mark the end of a by block ought to help. A parser plugin will have to explicitly take the string between by and done or beginning of the next declaration, whichever comes first, and then call the tactic parser on that string. A key difference between this and "bring back begin and end" would be that the existing proofs would still work and done will remain optional. Currently done is a tactic and can be parsed by induction as an inductionAlt and cause errors.

[Shreyas Srinivas]

Mario came up with something similar a few months ago for a Proof ... Qed block, but I suspect implementing an optional done token like this will make the change entirely transparent to existing users.

[Shreyas Srinivas]

Last time I recall showing that a naive implementation doesn't work well for blocks inside a case or a conv, so I am guessing it won't be trivial. done, the tactic as it exists now, can be used at the end of an induction/case arm and have/let declaration.

[Shreyas Srinivas]

Issue : https://github.com/leanprover/lean4/issues/2876

[Shreyas Srinivas]

I have not added the third error since that seems to be a related by separate issue with case

[Shreyas Srinivas]

Update: adding both colGt and zero arm should solve errors 1 and 2

[Mario Carneiro]

induction n with <missing> is still executed using the induction tactic in spite of the parse error

[Mario Carneiro]

and induction always closes all goals unless there are => ?_ arms

[Mario Carneiro]

the code action should still trigger even if you have induction n with <missing>, although possibly it doesn't trigger if you have tactics after the with, I didn't test that

[Shreyas Srinivas]

Yeah, but the code action is not the issue. That works well, provided one knows what the bulb is and clicks it.

[Shreyas Srinivas]

The issue here is about the tactic state and error location.

[Mario Carneiro]

both of those are working as expected

[Mario Carneiro]

because induction n with ... does not produce any subgoals (all goals are closed by the tactic and its embedded pieces)

[Shreyas Srinivas]

Well... from a user experience standpoint it is extremely confusing if after typing induction n with... all I get is "No Goals"

[Mario Carneiro]

you don't just get "no goals", you get a parse error

[Mario Carneiro]

and a lightbulb that will fill in the subgoals

[Shreyas Srinivas]

Where do I get this error?
induction_error_where.png

[Shreyas Srinivas]

somewhere in line 28

[Mario Carneiro]

yes

[Shreyas Srinivas]

a tiny squiggle that I could easily miss.

[Shreyas Srinivas]

Far beyond the expected end of the proof at done

[Mario Carneiro]

it shows up in "all messages" too

[Shreyas Srinivas]

why would I normally turn on "All messages"? I could have hundreds of messages in a file

[Mario Carneiro]

you should not have red errors anywhere

[Shreyas Srinivas]

At the end of a project yes.

[Mario Carneiro]

that's always your first priority to fix

[Mario Carneiro]

no, ever

[Mario Carneiro]

if you have red errors in the file then things can be badly broken and you will not get useful suggestions

[Mario Carneiro]

except for errors on done and by, which have predictable effects similar to sorry

[Mario Carneiro]

and _

[Shreyas Srinivas]

I start a lot of proofs with done before filling in the details.

[Shreyas Srinivas]

So in a file with a few dozen theorems, I am going to have a few dozen errors

[Mario Carneiro]

but parse errors especially make a mess of things

[Shreyas Srinivas]

And my point still stands, that is not the right place to show an error.

[Mario Carneiro]

you should always have no parse errors when you take your hands away from the keyboard

[Mario Carneiro]

that is the right place to show a parse error

[Mario Carneiro]

at least, this one

[Shreyas Srinivas]

Think about this from the point of view of a new user who is not well versed in the parser dark arts

[Mario Carneiro]

I agree that parse errors in general are very poorly surfaced

[Mario Carneiro]

they seem to have been built to be resilient to failure but this doesn't really deliver because it still aborts parsing the rest of the command

[Mario Carneiro]

but they run tactics with missing pieces anyway, and most tactics don't handle this well - pattern matches are assumed to be exhaustive when they aren't, arrays are truncated without warning, weird effects result

[Mario Carneiro]

but it's hard to complain about a parse error showing up at the first place where the remainder cannot be parsed

[Shreyas Srinivas]

I still disagree on the tactic state issue. The basic UX expectation is that if I haven't finished a proof at the cursor point, I should see a tactic state.

[Shreyas Srinivas]

Mario Carneiro said:

but it's hard to complain about a parse error showing up at the first place where the remainder cannot be parsed

This can be fixed by allowing the parser to finish parsing at zero arms

[Mario Carneiro]

What if there is no tactic state because there is a parse error?

[Mario Carneiro]

Not if you made a different parse error

[Mario Carneiro]

I agree about zero arms specifically, I have said as much elsewhere, but this is orthogonal to parse error issues

[Shreyas Srinivas]

Come on. This is a worst case argument. It is perfectly reasonable that induction n with.. is a complete parse so that the induction cases are visible.

[Mario Carneiro]

you should probably be more precise about what you want to see fixed

[Shreyas Srinivas]

I want this fixed: https://github.com/leanprover/lean4/issues/2876

[Mario Carneiro]

because "induction allows zero arms" and "parse errors should show up closer to my cursor position" are completely separate issues

[Shreyas Srinivas]

In this case the root cause of both problems is the same. induction doesn't finish parsing until it sees at least one alternative. Then it can encounter a sorry or a done and try to parse them as an induction argument.

[Shreyas Srinivas]

Allowing zero arms and forcing indentation for inductionAlt makes both these problems go away.

[Shreyas Srinivas]

Besides making induction proof blocks visibly separate from what follows

[Mario Carneiro]

actually there does seem to be a separate issue, compare the parsing of induction n with with induction n with |

[Mario Carneiro]

both are incomplete syntax, but notice that with the cursor on with the goals are still visible in the second case

[Shreyas Srinivas]

I don't get that. I only get a different syntax error unexpected end of input; expected '=>'

[Mario Carneiro]

Yes but look at the goals list

[Shreyas Srinivas]

image.png

[Mario Carneiro]

oh, the done breaks it

[Mario Carneiro]

the cause is this code:

  let hasAlts := altsSyntax.size > 0
  if hasAlts then
    -- default to initial state outside of alts
    -- HACK: because this node has the same span as the original tactic,
    -- we need to take all the info trees we have produced so far and re-nest them
    -- inside this node as well
    let treesSaved ← getResetInfoTrees
    withInfoContext ((modifyInfoState fun s => { s with trees := treesSaved }) *> go) (pure initialInfo)
  else go

It is using altsSyntax.size > 0 to detect whether this is induction x with ... vs induction x but this fails when there are no alts but with was used (and it is a syntax error)

[Shreyas Srinivas]

okay, but isn't the overall issue with the syntax itself which expects an argument?

[Mario Carneiro]

like I said, this is two separate things. Make an issue specifically about induction 0+ instead of talking about parse errors

[Mario Carneiro]

you can have parse errors even with induction 0+, like

induction x with
|
done

[Shreyas Srinivas]

Issue 2876 was a bug report

[Shreyas Srinivas]

So included all the bugs I saw in those two examples

[Mario Carneiro]

and that's not helpful for focusing solutions to the problem

[Mario Carneiro]

make a bug report with a single bug in it

[Mario Carneiro]

then fixes for the bug can close the issue

[Mario Carneiro]

Some more info regarding this issue: In the following example

example (n : Nat) : True := by
  induction n with
  done

There is actually an error being thrown from induction, to wit invalid alternative name '[anonymous]', but apparently errors during tactic evaluation are suppressed in the event of a parse error, so the only error you see is unexpected end of input. Is this deliberate @Sebastian Ullrich ?

[Mario Carneiro]

In this case, because of the error, only half of the info tree data has been set up and so the tactic state ends up missing

[Mario Carneiro]

this error message is visible using set_option trace.Elab.tactic.backtrack true

[Kyle Miller]

Let's understand lean4#2876 to be a user experience issue. It's definitely not a good user experience, and the two issues are intertwined (and not separable unless you're someone like Mario who knows how induction is implemented).

[Kyle Miller]

We can create separate issues that speak to the underlying technical problems if needed.

[Mario Carneiro]

lean4#2885 fixes induction so that induction n with, induction n with | and induction n with done all leave approximately the same info tree results (meaning that with your cursor on with the original goal is still visible rather than no goals)

[Shreyas Srinivas]

I am guessing zero_alt will be necessary for induction to show the cases in the infoview

[Shreyas Srinivas]

I can try to make this PR since it is a small change (a ,+ becomes ,*). It could be my first PR to lean4 proper. I am worried about the consequences of the other change, adding colGt to inductionAlt for proofs

[Shreyas Srinivas]

I'll make the PR after dinner if you agree

[Mario Carneiro]

it won't be as small a change as you are thinking, because of code like the one I linked above. The induction tactic assumes that no alts = induction x and induction x with ... has 1+ alts

[Shreyas Srinivas]

Okay, then it's a better learning experience