fix: some goal state issues (#5677)

This PR resolves the following issues related to goal state display:
1. In a new line after a `case` tactic with a completed proof, the state
of the proof in the `case` would be displayed, not the proof state after
the `case`
1. In the range of `next =>` / `case' ... =>`, the state of the proof in
the corresponding case would not be displayed, whereas this is true for
`case`
1. In the `suffices ... by` tactic, the tactic state of the `by` block
was not displayed after the `by` and before the first tactic

The incorrect goal state after `case` was caused by `evalCase` adding a
`TacticInfo` with the full block proof state for the full range of the
`case` block that the goal state selection has no means of
distinguishing from the `TacticInfo` with the same range that contains
the state after the whole `case` block. Narrowing the range of this
`TacticInfo` to `case ... =>` fixed this issue.

The lack of a case proof state on `next =>` was caused by the `case`
syntax that `next` expands to receiving noncanonical synthetic
`SourceInfo`, which is usually ignored by the language server. Adding a
token antiquotation for `next` fixed this issue.

The lack of a case proof state on `case' ... =>` was caused by
`evalCase'` not adding a `TacticInfo` with the full block state to the
range of `case' ... =>`. Adding this `TacticInfo` fixed this issue.

The tactic state of the block not being displayed after the `by` was
caused by the macro expansion of `suffices` to `have` not transferring
the trailing whitespace of the `by`. Ensuring that this trailing
whitespace information is transferred fixed this issue.

Fixes #2881.

src/Init/Tactics.lean

@@ -268,9 +268,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+macro nextTk:"next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
   -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
+  withRef arrowTk `(tactic| case%$nextTk _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic

src/Lean/Elab/BuiltinNotation.lean

@@ -135,13 +135,21 @@ open Meta
   | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
-  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
-  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
-  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
-  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
-  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
-  | _                                                                 => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)   => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)   => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)   => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type $b:byTactic'; $body) =>
+    -- Pass on `SourceInfo` of `b` to `have`. This is necessary to display the goal state in the
+    -- trailing whitespace of `by` and sound since `byTactic` and `byTactic'` are identical.
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk $x : $type := $body; $b:byTactic)
+  | `(suffices%$tk _%$x          : $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk _%$x : $type := $body; $b:byTactic)
+  | `(suffices%$tk $hy:hygieneInfo $type $b:byTactic'; $body) =>
+    let b := ⟨b.raw.setKind `Lean.Parser.Term.byTactic⟩
+    `(have%$tk $hy:hygieneInfo : $type := $body; $b:byTactic)
+  | _ => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -520,28 +520,28 @@ where
 
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
-  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     -- disable incrementality if body is run multiple times
     Term.withoutTacticIncrementality (tag.size > 1) do
       for tag in tag, hs in hs do
         let (g, gs) ← getCaseGoals tag
         let g ← renameInaccessibles g hs
         setGoals [g]
         g.setTag Name.anonymous
-        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
+        withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <|
           Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
         setGoals gs
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic «case'»] def evalCase' : Tactic
-  | `(tactic| case' $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
+  | `(tactic| case'%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq) => do
     let mut acc := #[]
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       let mvarTag ← g.getTag
       setGoals [g]
-      withCaseRef arr tac (evalTactic tac)
+      withCaseRef arr tac <| withTacticInfoContext (mkNullNode #[caseTk, arr]) <| evalTactic tac
       let gs' ← getUnsolvedGoals
       if let [g'] := gs' then
         g'.setTag mvarTag

src/Lean/Elab/Tactic/Induction.lean

@@ -27,8 +27,10 @@ open Meta
   syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
   ```
 -/
+private def getAltLhses (alt : Syntax) : Syntax :=
+  alt[0]
 private def getFirstAltLhs (alt : Syntax) : Syntax :=
-  alt[0][0]
+  (getAltLhses alt)[0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
 private def getAltName (alt : Syntax) : Name :=
   let lhs := getFirstAltLhs alt
@@ -70,7 +72,9 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
       let goals ← getGoals
       try
         setGoals [mvarId]
-        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
+        closeUsingOrAdmit <|
+          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
+            (addInfo *> evalTactic rhs)
       finally
         setGoals goals
 

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 194, column := 42 }, charUtf16 := 42, endPos := { line := 200, column := 31 },
+      { pos := { line := 202, column := 42 }, charUtf16 := 42, endPos := { line := 208, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 },
+      { pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },
         endCharUtf16 := 58 } }

tests/lean/interactive/2881.lean

@@ -0,0 +1,49 @@
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  case' zero => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n
+  next => sorry
+     -- `succ` goal
+--^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry -- `zero` goal
+ --^ $/lean/plainGoal
+
+example (n : Nat) : True := by
+  induction n with
+  | zero => sorry
+    -- General goal
+--^ $/lean/plainGoal
+
+example : True := by
+  suffices True by
+      -- Goal assuming `True`
+  --^ $/lean/plainGoal
+    sorry

tests/lean/interactive/2881.lean.expected.out

@@ -0,0 +1,31 @@
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 2, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 8, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 13, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 19, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 24, "character": 3}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 30, "character": 2}}
+{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
+ "goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 35, "character": 3}}
+{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 41, "character": 2}}
+{"rendered": "```lean\nn : Nat\n⊢ True\n```", "goals": ["n : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file:///2881.lean"},
+ "position": {"line": 46, "character": 4}}
+{"rendered": "```lean\nthis : True\n⊢ True\n```",
+ "goals": ["this : True\n⊢ True"]}