fix: nontermination while generating equation lemmas for match-expr…

…essions (leanprover#6180)

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

closes leanprover#6067

src/Lean/Elab/Tactic/Injection.lean

@@ -40,7 +40,7 @@ private def tryAssumption (mvarId : MVarId) : MetaM (List MVarId) := do
   let ids := stx[1].getArgs.toList.map getNameOfIdent'
   liftMetaTactic fun mvarId => do
     match (← Meta.injections mvarId ids) with
-    | .solved                    => checkUnusedIds `injections mvarId ids; return []
-    | .subgoal mvarId' unusedIds => checkUnusedIds `injections mvarId unusedIds; tryAssumption mvarId'
+    | .solved                      => checkUnusedIds `injections mvarId ids; return []
+    | .subgoal mvarId' unusedIds _ => checkUnusedIds `injections mvarId unusedIds; tryAssumption mvarId'
 
 end Lean.Elab.Tactic

src/Lean/Meta/Match/MatchEqs.lean

@@ -222,16 +222,16 @@ private def contradiction (mvarId : MVarId) : MetaM Bool :=
   Auxiliary tactic that tries to replace as many variables as possible and then apply `contradiction`.
   We use it to discard redundant hypotheses.
 -/
-partial def trySubstVarsAndContradiction (mvarId : MVarId) : MetaM Bool :=
+partial def trySubstVarsAndContradiction (mvarId : MVarId) (forbidden : FVarIdSet := {}) : MetaM Bool :=
   commitWhen do
     let mvarId ← substVars mvarId
-    match (← injections mvarId) with
+    match (← injections mvarId (forbidden := forbidden)) with
     | .solved => return true -- closed goal
-    | .subgoal mvarId' _ =>
+    | .subgoal mvarId' _ forbidden =>
       if mvarId' == mvarId then
         contradiction mvarId
       else
-        trySubstVarsAndContradiction mvarId'
+        trySubstVarsAndContradiction mvarId' forbidden
 
 private def processNextEq : M Bool := do
   let s ← get

src/Lean/Meta/Tactic/Injection.lean

@@ -94,31 +94,48 @@ def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) :
   | .subgoal mvarId numEqs => injectionIntro mvarId numEqs newNames
 
 inductive InjectionsResult where
+  /-- `injections` closed the input goal. -/
   | solved
-  | subgoal (mvarId : MVarId) (remainingNames : List Name)
+  /--
+  `injections` produces a new goal `mvarId`. `remainingNames` contains the user-facing names that have not been used.
+  `forbidden` contains all local declarations to which `injection` has been applied.
+  Recall that some of these declarations may not have been eliminated from the local context due to forward dependencies, and
+  we use `forbidden` to avoid non-termination when using `injections` in a loop.
+  -/
+  | subgoal (mvarId : MVarId) (remainingNames : List Name) (forbidden : FVarIdSet)
 
-partial def injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) : MetaM InjectionsResult :=
+/--
+Applies `injection` to local declarations in `mvarId`. It uses `newNames` to name the new local declarations.
+`maxDepth` is the maximum recursion depth. Only local declarations that are not in `forbidden` are considered.
+Recall that some of local declarations may not have been eliminated from the local context due to forward dependencies, and
+we use `forbidden` to avoid non-termination when using `injections` in a loop.
+-/
+partial def injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) (forbidden : FVarIdSet := {}) : MetaM InjectionsResult :=
   mvarId.withContext do
     let fvarIds := (← getLCtx).getFVarIds
-    go maxDepth fvarIds.toList mvarId newNames
+    go maxDepth fvarIds.toList mvarId newNames forbidden
 where
-  go : Nat → List FVarId → MVarId → List Name → MetaM InjectionsResult
-    | 0,   _,  _,      _        => throwTacticEx `injections mvarId "recursion depth exceeded"
-    | _,   [], mvarId, newNames => return .subgoal mvarId newNames
-    | d+1, fvarId :: fvarIds, mvarId, newNames => do
+  go (depth : Nat) (fvarIds : List FVarId) (mvarId : MVarId) (newNames : List Name) (forbidden : FVarIdSet) : MetaM InjectionsResult := do
+    match depth, fvarIds with
+    | 0,   _                 => throwTacticEx `injections mvarId "recursion depth exceeded"
+    | _,   []                => return .subgoal mvarId newNames forbidden
+    | d+1, fvarId :: fvarIds => do
       let cont := do
-        go (d+1) fvarIds mvarId newNames
-      if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
+        go (d+1) fvarIds mvarId newNames forbidden
+      if forbidden.contains fvarId then
+        cont
+      else if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
         let lhs ← whnf lhs
         let rhs ← whnf rhs
-        if lhs.isRawNatLit && rhs.isRawNatLit then cont
+        if lhs.isRawNatLit && rhs.isRawNatLit then
+          cont
         else
           try
             commitIfNoEx do
               match (← injection mvarId fvarId newNames) with
               | .solved  => return .solved
               | .subgoal mvarId newEqs remainingNames =>
-                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
+                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames (forbidden.insert fvarId)
           catch _ => cont
       else cont
 

tests/lean/run/6067.lean

@@ -0,0 +1,26 @@
+inductive Impl where
+  | inner (l r : Impl)
+  | leaf
+
+namespace Impl
+
+inductive Balanced : Impl → Prop where
+  | leaf : Balanced leaf
+
+@[inline]
+def balanceLErase (r : Impl) (hrb : Balanced r) : Impl :=
+  match r with
+  | leaf => .leaf
+  | l@(inner _ _) =>
+    match l with
+    | leaf => .leaf
+    | r@(inner ll lr) =>
+        if true then
+          match ll, lr with
+          | inner _ _, inner _ _ => .leaf
+          | _, _ => .leaf
+        else .leaf
+
+theorem size_balanceLErase {r : Impl} {hrb} : (balanceLErase r hrb) = .leaf := by
+  simp only [balanceLErase]
+  sorry