From fc4305ab15d7137f6bda64a557dc2ca9c6fc460f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2024 18:20:33 +0100 Subject: [PATCH] fix: nontermination when generating the match-expression splitter theorem (#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 | 57 +++++++++++++++++++------------ tests/lean/run/6065.lean | 25 ++++++++++++++ 2 files changed, 60 insertions(+), 22 deletions(-) create mode 100644 tests/lean/run/6065.lean diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 728c09462be3..813870443752 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/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. diff --git a/tests/lean/run/6065.lean b/tests/lean/run/6065.lean new file mode 100644 index 000000000000..0325e8fdc7f8 --- /dev/null +++ b/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