From 6ebb738bd8da2953e828d5be5b47578d4e29e3d9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 18 Nov 2025 10:46:40 +0100 Subject: [PATCH] refactor: extract functionality from Match.MatchEqs This PR extracts two modules from `Match.MatchEqs`, in preparation of #11220 and to use the module system to draw clear boundaries between concerns here. --- src/Lean/Elab/PreDefinition/WF/Unfold.lean | 1 + src/Lean/Meta/Match/MatchEqs.lean | 247 +-------------------- src/Lean/Meta/Match/SimpH.lean | 158 +++++++++++++ src/Lean/Meta/Match/SolveOverlap.lean | 109 +++++++++ 4 files changed, 273 insertions(+), 242 deletions(-) create mode 100644 src/Lean/Meta/Match/SimpH.lean create mode 100644 src/Lean/Meta/Match/SolveOverlap.lean diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean index 89bb48863603..8a82212342fc 100644 --- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean +++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean @@ -92,6 +92,7 @@ matcherArgPusher params motive {α} {β} (f : ∀ (x : α), β x) rel alt1 .. x1 def mkMatchArgPusher (matcherName : Name) (matcherInfo : MatcherInfo) : MetaM Name := do let name := (mkPrivateName (← getEnv) matcherName) ++ `_arg_pusher realizeConst matcherName name do + prependError m!"Cannot create match arg pusher for {matcherName}" do let matcherVal ← getConstVal matcherName forallBoundedTelescope matcherVal.type (some (matcherInfo.numParams + 1)) fun xs _ => do let params := xs[*...matcherInfo.numParams] diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 7e743badce00..85d6d76805d9 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -11,40 +11,13 @@ public import Lean.Meta.Match.MatchEqsExt public import Lean.Meta.Tactic.Refl public import Lean.Meta.Tactic.Delta import Lean.Meta.Tactic.SplitIf +import Lean.Meta.Match.SimpH +import Lean.Meta.Match.SolveOverlap public section namespace Lean.Meta -/-- -A custom, approximated, and quick `contradiction` tactic. -It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where -`p`s are structurally equal. The procedure is not quadratic like `contradiction`. - -We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`. -We will eventually have to write more efficient proof automation for this module. -The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics -such as `contradiction`. --/ -private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do - mvarId.withContext do - let mut posMap : Std.HashMap Expr FVarId := {} - let mut negMap : Std.HashMap Expr FVarId := {} - for localDecl in (← getLCtx) do - unless localDecl.isImplementationDetail do - if let some p ← matchNot? localDecl.type then - if let some pFVarId := posMap[p]? then - mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr) - return true - negMap := negMap.insert p localDecl.fvarId - if (← isProp localDecl.type) then - if let some nFVarId := negMap[localDecl.type]? then - mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr (mkFVar nFVarId)) - return true - posMap := posMap.insert localDecl.type localDecl.fvarId - pure () - return false - /-- Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`, apply `cases xMajor`. -/ @@ -215,152 +188,6 @@ where else return e -namespace SimpH - -/-- - State for the equational theorem hypothesis simplifier. - - Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases. - We have one hypothesis for each previous case. - - Each hypothesis is of the form `forall xs, eqs → False` - - We use tactics to minimize code duplication. --/ -structure State where - mvarId : MVarId -- Goal representing the hypothesis - xs : List FVarId -- Pattern variables for a previous case - eqs : List FVarId -- Equations to be processed - eqsNew : List FVarId := [] -- Simplified (already processed) equations - -abbrev M := StateRefT State MetaM - -/-- - Apply the given substitution to `fvarIds`. - This is an auxiliary method for `substRHS`. --/ -private def applySubst (s : FVarSubst) (fvarIds : List FVarId) : List FVarId := - fvarIds.filterMap fun fvarId => match s.apply (mkFVar fvarId) with - | Expr.fvar fvarId .. => some fvarId - | _ => none - -/-- - Given an equation of the form `lhs = rhs` where `rhs` is variable in `xs`, - replace it everywhere with `lhs`. --/ -private def substRHS (eq : FVarId) (rhs : FVarId) : M Unit := do - assert! (← get).xs.contains rhs - let (subst, mvarId) ← substCore (← get).mvarId eq (symm := true) - modify fun s => { s with - mvarId, - xs := applySubst subst (s.xs.erase rhs) - eqs := applySubst subst s.eqs - eqsNew := applySubst subst s.eqsNew - } - -private def isDone : M Bool := - return (← get).eqs.isEmpty - -/-- Customized `contradiction` tactic for `simpH?` -/ -private def contradiction (mvarId : MVarId) : MetaM Bool := - mvarId.contradictionCore { genDiseq := false, emptyType := false } - -/-- - 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) (forbidden : FVarIdSet := {}) : MetaM Bool := - commitWhen do - let mvarId ← substVars mvarId - match (← injections mvarId (forbidden := forbidden)) with - | .solved => return true -- closed goal - | .subgoal mvarId' _ forbidden => - if mvarId' == mvarId then - contradiction mvarId - else - trySubstVarsAndContradiction mvarId' forbidden - -private def processNextEq : M Bool := do - let s ← get - s.mvarId.withContext do - if let eq :: eqs := s.eqs then - modify fun s => { s with eqs } - let eqType ← inferType (mkFVar eq) - -- See `substRHS`. Recall that if `rhs` is a variable then if must be in `s.xs` - if let some (_, lhs, rhs) ← matchEq? eqType then - -- Common case: Different constructors - match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with - | some lhsCtor, some rhsCtor => - if lhsCtor.name != rhsCtor.name then - return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality - | _,_ => pure () - if (← isDefEq lhs rhs) then - return true - if rhs.isFVar && s.xs.contains rhs.fvarId! then - substRHS eq rhs.fvarId! - return true - if let some (α, lhs, β, rhs) ← matchHEq? eqType then - -- Try to convert `HEq` into `Eq` - if (← isDefEq α β) then - let (eqNew, mvarId) ← heqToEq s.mvarId eq (tryToClear := true) - modify fun s => { s with mvarId, eqs := eqNew :: s.eqs } - return true - -- If it is not possible, we try to show the hypothesis is redundant by substituting even variables that are not at `s.xs`, and then use contradiction. - else - match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with - | some lhsCtor, some rhsCtor => - if lhsCtor.name != rhsCtor.name then - return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality - else if (← trySubstVarsAndContradiction s.mvarId) then - return false - | _, _ => - if (← trySubstVarsAndContradiction s.mvarId) then - return false - try - -- Try to simplify equation using `injection` tactic. - match (← injection s.mvarId eq) with - | InjectionResult.solved => return false - | InjectionResult.subgoal mvarId eqNews .. => - modify fun s => { s with mvarId, eqs := eqNews.toList ++ s.eqs } - catch _ => - modify fun s => { s with eqsNew := eq :: s.eqsNew } - return true - -partial def go : M Bool := do - if (← isDone) then - return true - else if (← processNextEq) then - go - else - return false - -end SimpH - -/-- - Auxiliary method for simplifying equational theorem hypotheses. - - Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases. - We have one hypothesis for each previous case. --/ -private partial def simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr) := withDefault do - let numVars ← forallTelescope h fun ys _ => pure (ys.size - numEqs) - let mvarId := (← mkFreshExprSyntheticOpaqueMVar h).mvarId! - let (xs, mvarId) ← mvarId.introN numVars - let (eqs, mvarId) ← mvarId.introN numEqs - let (r, s) ← SimpH.go |>.run { mvarId, xs := xs.toList, eqs := eqs.toList } - if r then - s.mvarId.withContext do - let eqs := s.eqsNew.reverse.toArray.map mkFVar - let mut r ← mkForallFVars eqs (mkConst ``False) - /- We only include variables in `xs` if there is a dependency. -/ - for x in s.xs.reverse do - if (← dependsOn r x) then - r ← mkForallFVars #[mkFVar x] r - trace[Meta.Match.matchEqs] "simplified hypothesis{indentExpr r}" - check r - return some r - else - return none private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := mvarId.withContext do for localDecl in (← getLCtx) do @@ -443,45 +270,6 @@ private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr → f xs go 0 #[] -inductive InjectionAnyResult where - | solved - | failed - /-- `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 - return some (lhs, rhs) - else if let some (α, lhs, β, rhs) ← matchHEq? type then - if (← isDefEq α β) then - return some (lhs, rhs) - return none - -/-- -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 - 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 - - private abbrev ConvertM := ReaderT (FVarIdMap (Expr × Nat × Array Bool)) $ StateRefT (Array MVarId) MetaM /-- @@ -498,7 +286,8 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al let (proof, mvarIds) ← convertTemplate template |>.run map |>.run #[] trace[Meta.Match.matchEqs] "splitter proof: {proof}" for mvarId in mvarIds do - proveSubgoal mvarId + let mvarId ← mvarId.tryClearMany (alts.map (·.fvarId!)) + solveOverlap mvarId instantiateMVars proof where mkMap : FVarIdMap (Expr × Nat × Array Bool) := Id.run do @@ -680,32 +469,6 @@ where let eNew := mkAppN eNew mvars return TransformStep.done eNew - /- - `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 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' 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 {} /-- Create new alternatives (aka minor premises) by replacing `discrs` with `patterns` at `alts`. @@ -896,7 +659,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do let mut hs := #[] for notAlt in notAlts do let h ← instantiateForall notAlt patterns - if let some h ← Match.simpH? h patterns.size then + if let some h ← simpH? h patterns.size then hs := hs.push h trace[Meta.Match.matchEqs] "hs: {hs}" let mut notAlt := mkConst ``False diff --git a/src/Lean/Meta/Match/SimpH.lean b/src/Lean/Meta/Match/SimpH.lean new file mode 100644 index 000000000000..1b0d6ad06942 --- /dev/null +++ b/src/Lean/Meta/Match/SimpH.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ + +module +prelude +public import Lean.Meta.Basic +import Lean.Meta.Tactic.Contradiction + +namespace Lean.Meta.Match.SimpH + +/-- + State for the equational theorem hypothesis simplifier. + + Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases. + We have one hypothesis for each previous case. + + Each hypothesis is of the form `forall xs, eqs → False` + + We use tactics to minimize code duplication. +-/ +structure State where + mvarId : MVarId -- Goal representing the hypothesis + xs : List FVarId -- Pattern variables for a previous case + eqs : List FVarId -- Equations to be processed + eqsNew : List FVarId := [] -- Simplified (already processed) equations + +abbrev M := StateRefT State MetaM + +/-- + Apply the given substitution to `fvarIds`. + This is an auxiliary method for `substRHS`. +-/ +def applySubst (s : FVarSubst) (fvarIds : List FVarId) : List FVarId := + fvarIds.filterMap fun fvarId => match s.apply (mkFVar fvarId) with + | Expr.fvar fvarId .. => some fvarId + | _ => none + +/-- + Given an equation of the form `lhs = rhs` where `rhs` is variable in `xs`, + replace it everywhere with `lhs`. +-/ +def substRHS (eq : FVarId) (rhs : FVarId) : M Unit := do + assert! (← get).xs.contains rhs + let (subst, mvarId) ← substCore (← get).mvarId eq (symm := true) + modify fun s => { s with + mvarId, + xs := applySubst subst (s.xs.erase rhs) + eqs := applySubst subst s.eqs + eqsNew := applySubst subst s.eqsNew + } + +def isDone : M Bool := + return (← get).eqs.isEmpty + +/-- Customized `contradiction` tactic for `simpH?` -/ +def contradiction (mvarId : MVarId) : MetaM Bool := + mvarId.contradictionCore { genDiseq := false, emptyType := false } + +/-- + 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) (forbidden : FVarIdSet := {}) : MetaM Bool := + commitWhen do + let mvarId ← substVars mvarId + match (← injections mvarId (forbidden := forbidden)) with + | .solved => return true -- closed goal + | .subgoal mvarId' _ forbidden => + if mvarId' == mvarId then + contradiction mvarId + else + trySubstVarsAndContradiction mvarId' forbidden + +def processNextEq : M Bool := do + let s ← get + s.mvarId.withContext do + if let eq :: eqs := s.eqs then + modify fun s => { s with eqs } + let eqType ← inferType (mkFVar eq) + -- See `substRHS`. Recall that if `rhs` is a variable then if must be in `s.xs` + if let some (_, lhs, rhs) ← matchEq? eqType then + -- Common case: Different constructors + match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with + | some lhsCtor, some rhsCtor => + if lhsCtor.name != rhsCtor.name then + return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality + | _,_ => pure () + if (← isDefEq lhs rhs) then + return true + if rhs.isFVar && s.xs.contains rhs.fvarId! then + substRHS eq rhs.fvarId! + return true + if let some (α, lhs, β, rhs) ← matchHEq? eqType then + -- Try to convert `HEq` into `Eq` + if (← isDefEq α β) then + let (eqNew, mvarId) ← heqToEq s.mvarId eq (tryToClear := true) + modify fun s => { s with mvarId, eqs := eqNew :: s.eqs } + return true + -- If it is not possible, we try to show the hypothesis is redundant by substituting even variables that are not at `s.xs`, and then use contradiction. + else + match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with + | some lhsCtor, some rhsCtor => + if lhsCtor.name != rhsCtor.name then + return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality + else if (← trySubstVarsAndContradiction s.mvarId) then + return false + | _, _ => + if (← trySubstVarsAndContradiction s.mvarId) then + return false + try + -- Try to simplify equation using `injection` tactic. + match (← injection s.mvarId eq) with + | InjectionResult.solved => return false + | InjectionResult.subgoal mvarId eqNews .. => + modify fun s => { s with mvarId, eqs := eqNews.toList ++ s.eqs } + catch _ => + modify fun s => { s with eqsNew := eq :: s.eqsNew } + return true + +partial def go : M Bool := do + if (← isDone) then + return true + else if (← processNextEq) then + go + else + return false + +end SimpH + + +/-- + Auxiliary method for simplifying equational theorem hypotheses. + + Recall that each equation contains additional hypotheses to ensure the associated case was not taken by previous cases. + We have one hypothesis for each previous case. +-/ +public partial def simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr) := withDefault do + let numVars ← forallTelescope h fun ys _ => pure (ys.size - numEqs) + let mvarId := (← mkFreshExprSyntheticOpaqueMVar h).mvarId! + let (xs, mvarId) ← mvarId.introN numVars + let (eqs, mvarId) ← mvarId.introN numEqs + let (r, s) ← SimpH.go |>.run { mvarId, xs := xs.toList, eqs := eqs.toList } + if r then + s.mvarId.withContext do + let eqs := s.eqsNew.reverse.toArray.map mkFVar + let mut r ← mkForallFVars eqs (mkConst ``False) + /- We only include variables in `xs` if there is a dependency. -/ + for x in s.xs.reverse do + if (← dependsOn r x) then + r ← mkForallFVars #[mkFVar x] r + trace[Meta.Match.matchEqs] "simplified hypothesis{indentExpr r}" + check r + return some r + else + return none diff --git a/src/Lean/Meta/Match/SolveOverlap.lean b/src/Lean/Meta/Match/SolveOverlap.lean new file mode 100644 index 000000000000..26f716a9da53 --- /dev/null +++ b/src/Lean/Meta/Match/SolveOverlap.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module + +prelude +public import Lean.Meta.Basic +import Lean.Meta.Tactic.Contradiction + +namespace Lean.Meta.Match + +/-- +A custom, approximated, and quick `contradiction` tactic. +It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where +`p`s are structurally equal. The procedure is not quadratic like `contradiction`. + +We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`. +We will eventually have to write more efficient proof automation for this module. +The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics +such as `contradiction`. +-/ +private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do + mvarId.withContext do + let mut posMap : Std.HashMap Expr FVarId := {} + let mut negMap : Std.HashMap Expr FVarId := {} + for localDecl in (← getLCtx) do + unless localDecl.isImplementationDetail do + if let some p ← matchNot? localDecl.type then + if let some pFVarId := posMap[p]? then + mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr) + return true + negMap := negMap.insert p localDecl.fvarId + if (← isProp localDecl.type) then + if let some nFVarId := negMap[localDecl.type]? then + mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr (mkFVar nFVarId)) + return true + posMap := posMap.insert localDecl.type localDecl.fvarId + pure () + return false + +inductive InjectionAnyResult where + | solved + | failed + /-- `fvarId` refers to the local declaration selected for the application of the `injection` tactic. -/ + | subgoal (fvarId : FVarId) (mvarId : MVarId) + +def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr)) := do + if let some (_, lhs, rhs) ← matchEq? type then + return some (lhs, rhs) + else if let some (α, lhs, β, rhs) ← matchHEq? type then + if (← isDefEq α β) then + return some (lhs, rhs) + return none + +/-- +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. +-/ +def injectionAny (mvarId : MVarId) (forbidden : FVarIdSet := {}) : MetaM InjectionAnyResult := do + mvarId.withContext do + for localDecl in (← getLCtx) do + 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 + + +/-- +Solves the overlap assumptions expected by the alternative of a splitter +-/ +public partial def solveOverlap (mvarId : MVarId) : MetaM Unit := do + trace[Meta.Match.matchEqs] "solveOverlap {mkMVar mvarId}, {repr (← mvarId.getDecl).kind}\n{indentD mvarId}" + let (_, mvarId) ← mvarId.intros + loop mvarId {} +where + /- + `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. + -/ + loop (mvarId : MVarId) (forbidden : FVarIdSet) : MetaM Unit := do + trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}" + if (← mvarId.contradictionQuick) then + return () + match (← injectionAny mvarId forbidden) with + | .solved => return () + | .failed => + let mvarId' ← substVars mvarId + if mvarId' == mvarId then + if (← mvarId.contradictionCore {}) then + return () + throwError "failed to solve overlap assumption, unsolved subgoal{indentD mvarId}" + else + loop mvarId' forbidden + | .subgoal fvarId mvarId => loop mvarId (forbidden.insert fvarId)