Induction Parse Error on zero cases : Misleading infoview and wrong error location

[Shreyas4991]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The issue is twofold:

1. As soon as I type the with in induction <Var> with, the infoview says "No goals". The case distinctions that are visible if the "with" is not inserted disappear.
2. The parsing error for induction (unexpected end of input; expected '|') indicated by a red squiggly line appears well after a done at the end of the file. Adding more empty lines to the file pushes the error further down.

This is unhelpful because:

1. There are goals for each induction arm that are being hidden.
2. Showing the goals is essential so that users can choose the next arm and give names to the required hypothesis, especially when the induction gets complicated.
3. The error location can be well beyond the end of the proof block.

Context

Zulipchat discussion

Steps to Reproduce

Open the following examples in the web editor or your text editor and observe observe tactic state and error location as denoted by the comments:

Example 1:

example (n : Nat) : True := by
  induction n with -- Tactic State : "No Goals"


-- Error line here

Here the error message appears at the last line of the file.

Example 2:

example (n : Nat) : True := by
  induction n with -- Tactic State : "No Goals"

  done -- No error here even though there are unresolved goals


-- Error line here : 

The addition of done at the end has no effect. done is not recognised as a point at which induction should stop parsing partially because it appears in the same column as the alternatives of induction would.

Example 3:

example (n : Nat) : True := by
  induction n -- No with inserted yet. Tactic State : induction alternatives shown as expected

  done -- Error because there are unsolved goals 


-- Error line here: unexpected end of input; expected '|'

In this example we see that before adding with the goals for the induction alternatives are visible in the tactic state. There is rightly an error mark on done because there are unresolved goals. This should be the behaviour even after with is added.

Expected behavior: [Clear and concise description of what you expect to happen]

1. After typing induction <var> with the goals of the induction alternatives remain visible in the tactic state. This allows users to see what goals exist and what hypothesis they need to add names for.
2. If the induction tactic is incomplete and the proof goals are not resolved, the corresponding error is shown at the line of the done tactic.

Actual behavior: Explained in ###Steps to Reproduce.

Versions

1. Lean (version 4.3.0-rc1, commit baa4b68a7192, Release)
2. The one in live lean as of 14 Nov 2023 19:53 (UTC+1:00).

Proposed Solution

@kmill proposes the following solutions:

1. Add colGt to the syntax of each induction alternative. This ensures that done and other tactic lines are not spuriously parsed as an arm of induction. This is most probably the cause of induction's parser reading past the done in example 2.
2. Allow zero alternatives in the syntax of induction. This allows a parse upto with to happen without error and report the tactic state.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.