From de25524dd6ee85e6a006bc7726cbccbc8ca55e93 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 13 Apr 2025 23:22:04 -0700
Subject: [PATCH] feat: preparation for #7830 (#7955)

This PR adds the tactic implementation for #7830, before changing the
syntax after a stage0 update. It will allow optional RHSs in induction
cases.
---
 src/Lean/Elab/Tactic/Induction.lean | 91 ++++++++++++++++++++---------
 1 file changed, 62 insertions(+), 29 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 58ddfc0ba1..79496cd0da 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -49,36 +49,55 @@ private def altHasExplicitModifier (alt : Syntax) : Bool :=
 private def getAltVars (alt : Syntax) : Array Syntax :=
   let lhs := getFirstAltLhs alt
   lhs[2].getArgs
+private def hasAltRHS (alt : Syntax) : Bool :=
+  if !alt[1].isOfKind nullKind then
+    -- TODO(kmill) Bootstrapping workaround. Delete case in #7830.
+    true
+  else
+    alt[1].getNumArgs > 0
 private def getAltRHS (alt : Syntax) : Syntax :=
-  alt[2]
+  if !alt[1].isOfKind nullKind then
+    -- TODO(kmill) Bootstrapping workaround. Delete case in #7830.
+    alt[2]
+  else
+    alt[1][1]
 private def getAltDArrow (alt : Syntax) : Syntax :=
-  alt[1]
+  if !alt[1].isOfKind nullKind then
+    -- TODO(kmill) Bootstrapping workaround. Delete case in #7830.
+    alt[1]
+  else
+    alt[1][0]
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
 def isHoleRHS (rhs : Syntax) : Bool :=
   rhs.isOfKind ``Parser.Term.syntheticHole || rhs.isOfKind ``Parser.Term.hole
 
-def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : TacticM Unit :=
-  let rhs := getAltRHS alt
-  withCaseRef (getAltDArrow alt) rhs do
-    if isHoleRHS rhs then
-      addInfo
-      mvarId.withContext <| withTacticInfoContext rhs do
-        let mvarDecl ← mvarId.getDecl
-        let val ← elabTermEnsuringType rhs mvarDecl.type
-        mvarId.assign val
-        let gs' ← getMVarsNoDelayed val
-        tagUntaggedGoals mvarDecl.userName `induction gs'.toList
-        setGoals <| (← getGoals) ++ gs'.toList
-    else
-      let goals ← getGoals
-      try
+def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : TacticM Unit := do
+  if !hasAltRHS alt then
+    throwErrorAt alt "(internal error) RHS was not expanded"
+  else
+    let rhs := getAltRHS alt
+    withCaseRef (getAltDArrow alt) rhs do
+      if isHoleRHS rhs then
+        addInfo
+        let goals ← getGoals
         setGoals [mvarId]
-        closeUsingOrAdmit <|
-          withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
-            (addInfo *> evalTactic rhs)
-      finally
-        setGoals goals
+        mvarId.withContext <| withTacticInfoContext (mkNullNode #[getAltLhses alt, rhs]) do
+          let mvarDecl ← mvarId.getDecl
+          let val ← elabTermEnsuringType rhs mvarDecl.type
+          mvarId.assign val
+          let gs' ← getMVarsNoDelayed val
+          tagUntaggedGoals mvarDecl.userName `induction gs'.toList
+          setGoals <| goals ++ gs'.toList
+      else
+        let goals ← getGoals
+        try
+          setGoals [mvarId]
+          closeUsingOrAdmit <|
+            withTacticInfoContext (mkNullNode #[getAltLhses alt, getAltDArrow alt]) <|
+              (addInfo *> evalTactic rhs)
+        finally
+          setGoals goals
 
 /-!
   Helper method for creating an user-defined eliminator/recursor application.
@@ -531,12 +550,26 @@ private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
 private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
   if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
 
-private def isMultiAlt (alt : Syntax) : Bool :=
-  alt[0].getNumArgs > 1
+/--
+Returns true if the `Lean.Parser.Tactic.inductionAlt` either has more than one alternative
+or has no RHS.
+-/
+private def shouldExpandAlt (alt : Syntax) : Bool :=
+  -- TODO(kmill) enable second case in #7830
+  alt[0].getNumArgs > 1 || (false && 1 < alt.getNumArgs && alt[1].getNumArgs == 0)
 
-/-- Return `some #[alt_1, ..., alt_n]` if `alt` has multiple LHSs. -/
-private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
-  if isMultiAlt alt then
+/--
+Returns `some #[alt_1, ..., alt_n]` if `alt` has multiple LHSs or if `alt` has no RHS.
+If there is no RHS, it is filled in with a hole.
+-/
+private def expandAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
+  if shouldExpandAlt alt then
+    let alt :=
+      -- TODO(kmill) enable case in #7830
+      if false && 1 < alt.getNumArgs && alt[1].getNumArgs == 0 then
+        alt.setArg 1 <| mkNullNode #[mkAtomFrom alt "=>", mkHole alt]
+      else
+        alt
     some <| alt[0].getArgs.map fun lhs => alt.setArg 0 (mkNullNode #[lhs])
   else
     none
@@ -553,10 +586,10 @@ Remark: the `RHS` of alternatives with multi LHSs is copied.
 -/
 private def expandInductionAlts? (inductionAlts : Syntax) : Option Syntax := Id.run do
   let alts := getAltsOfInductionAlts inductionAlts
-  if alts.any isMultiAlt then
+  if alts.any shouldExpandAlt then
     let mut altsNew := #[]
     for alt in alts do
-      if let some alt' := expandMultiAlt? alt then
+      if let some alt' := expandAlt? alt then
         altsNew := altsNew ++ alt'
       else
         altsNew := altsNew.push alt