fix: nontermination when generating the match-expression splitter the…

…orem (#6146)

This PR fixes a non-termination bug that occurred when generating the
match-expression splitter theorem. The bug was triggered when the proof
automation for the splitter theorem repeatedly applied `injection` to
the same local declaration, as it could not be removed due to forward
dependencies. See issue #6065 for an example that reproduces this issue.

closes #6065

src/Lean/Meta/Match/MatchEqs.lean

@@ -375,7 +375,8 @@ private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr →
 inductive InjectionAnyResult where
   | solved
   | failed
-  | subgoal (mvarId : MVarId)
+  /-- `fvarId` refers to the local declaration selected for the application of the `injection` tactic. -/
+  | subgoal (fvarId : FVarId) (mvarId : MVarId)
 
 private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some (_, lhs, rhs) ← matchEq? type then
@@ -385,21 +386,28 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
+/--
+Try applying `injection` to a local declaration that is not in `forbidden`.
+
+We use `forbidden` because the `injection` tactic might fail to clear the variable if there are forward dependencies.
+See `proveSubgoalLoop` for additional details.
+-/
+private def injectionAny (mvarId : MVarId) (forbidden : FVarIdSet := {}) : MetaM InjectionAnyResult := do
   mvarId.withContext do
     for localDecl in (← getLCtx) do
-      if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
-        unless (← isDefEq lhs rhs) do
-          let lhs ← whnf lhs
-          let rhs ← whnf rhs
-          unless lhs.isRawNatLit && rhs.isRawNatLit do
-            try
-              match (← injection mvarId localDecl.fvarId) with
-              | InjectionResult.solved  => return InjectionAnyResult.solved
-              | InjectionResult.subgoal mvarId .. => return InjectionAnyResult.subgoal mvarId
-            catch ex =>
-              trace[Meta.Match.matchEqs] "injectionAnyFailed at {localDecl.userName}, error\n{ex.toMessageData}"
-              pure ()
+      unless forbidden.contains localDecl.fvarId do
+        if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
+          unless (← isDefEq lhs rhs) do
+            let lhs ← whnf lhs
+            let rhs ← whnf rhs
+            unless lhs.isRawNatLit && rhs.isRawNatLit do
+              try
+                match (← injection mvarId localDecl.fvarId) with
+                | InjectionResult.solved  => return InjectionAnyResult.solved
+                | InjectionResult.subgoal mvarId .. => return InjectionAnyResult.subgoal localDecl.fvarId mvarId
+              catch ex =>
+                trace[Meta.Match.matchEqs] "injectionAnyFailed at {localDecl.userName}, error\n{ex.toMessageData}"
+                pure ()
     return InjectionAnyResult.failed
 
 
@@ -601,27 +609,32 @@ where
         let eNew := mkAppN eNew mvars
         return TransformStep.done eNew
 
-  proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
+  /-
+  `forbidden` tracks variables that we have already applied `injection`.
+  Recall that the `injection` tactic may not be able to eliminate them when
+  they have forward dependencies.
+  -/
+  proveSubgoalLoop (mvarId : MVarId) (forbidden : FVarIdSet) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
     if (← mvarId.contradictionQuick) then
       return ()
-    match (← injectionAny mvarId) with
-    | InjectionAnyResult.solved => return ()
-    | InjectionAnyResult.failed =>
+    match (← injectionAny mvarId forbidden) with
+    | .solved => return ()
+    | .failed =>
       let mvarId' ← substVars mvarId
       if mvarId' == mvarId then
         if (← mvarId.contradictionCore {}) then
           return ()
         throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}"
       else
-        proveSubgoalLoop mvarId'
-    | InjectionAnyResult.subgoal mvarId => proveSubgoalLoop mvarId
+        proveSubgoalLoop mvarId' forbidden
+    | .subgoal fvarId mvarId => proveSubgoalLoop mvarId (forbidden.insert fvarId)
 
   proveSubgoal (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← mvarId.getDecl).kind}, {← mvarId.isAssigned}\n{MessageData.ofGoal mvarId}"
     let (_, mvarId) ← mvarId.intros
     let mvarId ← mvarId.tryClearMany (alts.map (·.fvarId!))
-    proveSubgoalLoop mvarId
+    proveSubgoalLoop mvarId {}
 
 /--
   Create new alternatives (aka minor premises) by replacing `discrs` with `patterns` at `alts`.
@@ -646,7 +659,7 @@ where
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
-  trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
+  withTraceNode `Meta.Match.matchEqs (fun _ => return m!"mkEquationsFor '{matchDeclName}'") do
   withConfig (fun c => { c with etaStruct := .none }) do
   /-
   Remark: user have requested the `split` tactic to be available for writing code.

tests/lean/run/6065.lean

@@ -0,0 +1,25 @@
+def foo (r : Nat) : Nat :=
+  match r with
+  | Nat.zero => 0
+  | l@(Nat.succ _) =>
+    match l with
+    | 0 => 0
+    | Nat.succ ll =>
+      match ll with
+      | Nat.succ _ => 0
+      | _ => 0
+
+example {r : Nat} : foo r = 0 := by
+  simp only [foo.eq_def]
+  guard_target =ₛ
+    (match r with
+        | Nat.zero => 0
+        | l@h:(Nat.succ n) =>
+          match l, h with
+          | 0, h => 0
+          | Nat.succ ll, h =>
+            match ll, h with
+            | Nat.succ n_1, h => 0
+            | x, h => 0) =
+        0
+  sorry