From b02c1c56abf03509339200b0adef56fcdc8b604d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Jun 2024 23:35:09 +0200 Subject: [PATCH] fix: improve `split` discriminant generalization strategy (#4401) This commit also - improves `split` error messages. - adds `trace.split.failure` option. - uses new convention for trace messages. closes #4390 --- src/Lean/Elab/Tactic/Split.lean | 6 +- src/Lean/Meta/Tactic/Split.lean | 115 +++++++++++++++++++++----------- tests/lean/run/4390.lean | 54 +++++++++++++++ 3 files changed, 132 insertions(+), 43 deletions(-) create mode 100644 tests/lean/run/4390.lean diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean index fd27465d4c..0dfc669098 100644 --- a/src/Lean/Elab/Tactic/Split.lean +++ b/src/Lean/Elab/Tactic/Split.lean @@ -21,12 +21,12 @@ open Meta throwErrorAt stx[2] "'split' tactic failed, select a single target to split" if simplifyTarget then liftMetaTactic fun mvarId => do - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" return mvarIds else let fvarId ← getFVarId hyps[0]! liftMetaTactic fun mvarId => do - let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId + let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" return mvarIds | Location.wildcard => liftMetaTactic fun mvarId => do @@ -34,7 +34,7 @@ open Meta for fvarId in fvarIds do if let some mvarIds ← splitLocalDecl? mvarId fvarId then return mvarIds - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" return mvarIds end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 6c625f4bd0..bd20c779ac 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -79,6 +79,17 @@ where else k hs rfls +/-- +Internal exception for discriminant generalization failures due to type errors. +-/ +builtin_initialize discrGenExId : InternalExceptionId ← + registerInternalExceptionId `discrGeneralizationFailure + +def isDiscrGenException (ex : Exception) : Bool := + match ex with + | .internal id => id == discrGenExId + | _ => false + /-- This method makes sure each discriminant is a free variable. Return the tuple `(discrsNew, discrEqs, mvarId)`. `discrsNew` in an array representing the new discriminants, `discrEqs` is an array of auxiliary equality hypotheses @@ -125,7 +136,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N let some matcherApp ← matchMatcherApp? e | return .continue for matcherDiscr in matcherApp.discrs, discr in discrs do unless matcherDiscr == discr do - trace[Meta.Tactic.split] "discr mismatch {matcherDiscr} != {discr}" + trace[split.debug] "discr mismatch {matcherDiscr} != {discr}" return .continue let matcherApp := { matcherApp with discrs := discrVars } foundRef.set true @@ -135,7 +146,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N let altNumParams := matcherApp.altNumParams[i]! let altNew ← lambdaTelescope alt fun xs body => do if xs.size < altNumParams || xs.size < numDiscrEqs then - throwError "'applyMatchSplitter' failed, unexpected `match` alternative" + throwError "internal error in `split` tactic: encountered an unexpected `match` expression alternative\nthis error typically occurs when the `match` expression has been constructed using meta-programming." let body ← mkLambdaFVars xs[altNumParams:] (← mkNewTarget body) let ys := xs[:altNumParams - numDiscrEqs] if numDiscrEqs == 0 then @@ -150,13 +161,13 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N transform (← instantiateMVars e) pre let targetNew ← mkNewTarget (← mvarId.getType) unless (← foundRef.get) do - throwError "'applyMatchSplitter' failed, did not find discriminants" + throwError "internal error in `split` tactic: failed to find match-expression discriminants\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program" let targetNew ← mkForallFVars (discrVars ++ eqs) targetNew unless (← isTypeCorrect targetNew) do - throwError "'applyMatchSplitter' failed, failed to generalize target" + throw <| Exception.internal discrGenExId return (targetNew, rfls) let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew (← mvarId.getTag) - trace[Meta.Tactic.split] "targetNew:\n{mvarNew.mvarId!}" + trace[split.debug] "targetNew:\n{mvarNew.mvarId!}" mvarId.assign (mkAppN (mkAppN mvarNew discrs) rfls) let (discrs', mvarId') ← mvarNew.mvarId!.introNP discrs.size let (discrEqs, mvarId') ← mvarId'.introNP discrs.size @@ -188,7 +199,7 @@ where withLocalDeclD altEqDecl.userName (← mkHEq discrVar pattern) fun altEqNew => do go (i+1) (altEqsNew.push altEqNew) (subst.push (← mkHEqTrans eq altEqNew)) | _, _ => - throwError "'applyMatchSplitter' failed, unexpected discriminant equalities" + throwError "internal error in `split` tactic: encountered unexpected auxiliary equalities created to generalize `match`-expression discriminant\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program" else k altEqsNew subst go 0 #[] #[] @@ -208,21 +219,21 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs : return mvarId def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := do - let some info ← getMatcherInfo? matcherDeclName | throwError "'applyMatchSplitter' failed, '{matcherDeclName}' is not a 'match' auxiliary declaration." + let some info ← getMatcherInfo? matcherDeclName | throwError "internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program" let matchEqns ← Match.getEquationsFor matcherDeclName -- splitterPre does not have the correct universe elimination level, but this is fine, we only use it to compute the `motiveType`, -- and we only care about the `motiveType` arguments, and not the resulting `Sort u`. let splitterPre := mkAppN (mkConst matchEqns.splitterName us.toList) params let motiveType := (← whnfForall (← inferType splitterPre)).bindingDomain! - trace[Meta.Tactic.split] "applyMatchSplitter\n{mvarId}" + trace[split.debug] "applyMatchSplitter\n{mvarId}" let (discrFVarIds, discrEqs, mvarId) ← generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs - trace[Meta.Tactic.split] "after generalizeMatchDiscrs\n{mvarId}" + trace[split.debug] "after generalizeMatchDiscrs\n{mvarId}" let mvarId ← generalizeTargetsEq mvarId motiveType (discrFVarIds.map mkFVar) - mvarId.withContext do trace[Meta.Tactic.split] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}" - trace[Meta.Tactic.split] "after generalize\n{mvarId}" + mvarId.withContext do trace[split.debug] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}" + trace[split.debug] "after generalize\n{mvarId}" let numEqs := discrs.size let (discrFVarIdsNew, mvarId) ← mvarId.introN discrs.size - trace[Meta.Tactic.split] "after introN\n{mvarId}" + trace[split.debug] "after introN\n{mvarId}" let discrsNew := discrFVarIdsNew.map mkFVar let mvarType ← mvarId.getType let elimUniv ← mvarId.withContext <| getLevel mvarType @@ -230,40 +241,43 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le pure <| us.set! uElimPos elimUniv else unless elimUniv.isZero do - throwError "match-splitter can only eliminate into `Prop`" + throwError "`split` tactic failed to split a match-expression: the splitter auxiliary theorem `{matchEqns.splitterName}` can only eliminate into `Prop`" pure us let splitter := mkAppN (mkConst matchEqns.splitterName us.toList) params mvarId.withContext do let motive ← mkLambdaFVars discrsNew mvarType let splitter := mkAppN (mkApp splitter motive) discrsNew check splitter - trace[Meta.Tactic.split] "after check splitter" + trace[split.debug] "after check splitter" let mvarIds ← mvarId.apply splitter unless mvarIds.length == matchEqns.size do - throwError "'applyMatchSplitter' failed, unexpected number of goals created after applying splitter for '{matcherDeclName}'." + throwError "internal error in `split` tactic: unexpected number of goals created after applying splitter auxiliary theorem `{matchEqns.splitterName}` for `{matcherDeclName}`" let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do let numParams := matchEqns.splitterAltNumParams[i]! let (_, mvarId) ← mvarId.introN numParams - trace[Meta.Tactic.split] "before unifyEqs\n{mvarId}" + trace[split.debug] "before unifyEqs\n{mvarId}" match (← Cases.unifyEqs? (numEqs + info.getNumDiscrEqs) mvarId {}) with | none => return (i+1, mvarIds) -- case was solved | some (mvarId, fvarSubst) => - trace[Meta.Tactic.split] "after unifyEqs\n{mvarId}" + trace[split.debug] "after unifyEqs\n{mvarId}" let mvarId ← substDiscrEqs mvarId fvarSubst discrEqs return (i+1, mvarId::mvarIds) return mvarIds.reverse +def mkDiscrGenErrorMsg (e : Expr) : MessageData := + m!"`split` tactic failed to generalize discriminant(s) at{indentExpr e}\nresulting expression was not type correct\npossible solution: generalize discriminant(s) manually before using `split`" + +def throwDiscrGenError (e : Expr) : MetaM α := + throwError (mkDiscrGenErrorMsg e) + def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do - try - let some app ← matchMatcherApp? e | throwError "match application expected" - let matchEqns ← Match.getEquationsFor app.matcherName - let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs - let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do - let mvarId ← simpMatchTargetCore mvarId app.matcherName matchEqns.eqnNames[i]! - return (i+1, mvarId::mvarIds) - return mvarIds.reverse - catch ex => - throwNestedTacticEx `splitMatch ex + let some app ← matchMatcherApp? e | throwError "internal error in `split` tactic: match application expected{indentExpr e}\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program" + let matchEqns ← Match.getEquationsFor app.matcherName + let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs + let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do + let mvarId ← simpMatchTargetCore mvarId app.matcherName matchEqns.eqnNames[i]! + return (i+1, mvarId::mvarIds) + return mvarIds.reverse /-- Return an `if-then-else` or `match-expr` to split. -/ partial def findSplit? (env : Environment) (e : Expr) (splitIte := true) (exceptionSet : ExprSet := {}) : Option Expr := @@ -307,10 +321,14 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L else try splitMatch mvarId e - catch _ => + catch ex => + if isDiscrGenException ex then + trace[split.failure] mkDiscrGenErrorMsg e + else + trace[split.failure] "`split` tactic failed at{indentExpr e}\n{ex.toMessageData}" go (badCases.insert e) else - trace[Meta.Tactic.split] "did not find term to split\n{MessageData.ofGoal mvarId}" + trace[split.debug] "did not find term to split\n{MessageData.ofGoal mvarId}" return none go {} @@ -320,21 +338,38 @@ def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MV if e.isIte || e.isDIte then return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂] else - let mut mvarId := mvarId + let result? ← commitWhenSome? do try + let (fvarIds, mvarId) ← mvarId.revert #[fvarId] + let num := fvarIds.size + let mvarIds ← splitMatch mvarId e + let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.introNP num).2 + return some mvarIds + catch ex => + if isDiscrGenException ex then + return none + else + throw ex + if result?.isSome then + return result? + -- Generalization failed, if `fvarId` is a let-decl or has forward dependencies, we try to `assert` a copy and try again let localDecl ← fvarId.getDecl if (← pure localDecl.isLet <||> exprDependsOn (← mvarId.getType) fvarId <||> fvarId.hasForwardDeps) then - -- If `fvarId` has dependencies or is a let-decl, we create a copy. - mvarId ← mvarId.assert localDecl.userName localDecl.type localDecl.toExpr - else - let (fvarIds, mvarId') ← mvarId.revert #[fvarId] - assert! fvarIds.size == 1 -- fvarId does not have forward dependencies - mvarId := mvarId' - let mvarIds ← splitMatch mvarId e - let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.intro1P).2 - return some mvarIds + try + let mvarId ← mvarId.assert localDecl.userName localDecl.type localDecl.toExpr + let mvarIds ← splitMatch mvarId e + let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.intro1P).2 + return some mvarIds + catch ex => + if isDiscrGenException ex then + throwDiscrGenError e + else + throw ex + throwDiscrGenError e else return none -builtin_initialize registerTraceClass `Meta.Tactic.split +builtin_initialize + registerTraceClass `split.debug + registerTraceClass `split.failure end Lean.Meta diff --git a/tests/lean/run/4390.lean b/tests/lean/run/4390.lean new file mode 100644 index 0000000000..4306f00ae0 --- /dev/null +++ b/tests/lean/run/4390.lean @@ -0,0 +1,54 @@ +def step (state: Nat): Option Nat := + if state = 0 then none else some (state - 1) + +set_option linter.unusedVariables false + +def countdown (state: Nat) := + match h: step state with + | none => [state] + | some newState => state :: countdown newState +termination_by state +decreasing_by sorry + +/-- +error: tactic 'split' failed, consider using `set_option trace.split.failures true` +state : Nat +p : + (match h : step state with + | none => [state] + | some newState => state :: countdown newState) ≠ + [] +⊢ (match h : step state with + | none => [state] + | some newState => state :: countdown newState).head + p = + state +--- +info: [split.failure] `split` tactic failed to generalize discriminant(s) at + match h : step state with + | none => [state] + | some newState => state :: countdown newState + resulting expression was not type correct + possible solution: generalize discriminant(s) manually before using `split` +-/ +#guard_msgs in +example (state: Nat) (p : (match h : step state with + | none => [state] + | some newState => state :: countdown newState) ≠ + []): (match h : step state with + | none => [state] + | some newState => state :: countdown newState).head + p = + state := by + set_option trace.split.failure true in + split + +example (state: Nat) (p : (match h : step state with + | none => [state] + | some newState => state :: countdown newState) ≠ + []): (match h : step state with + | none => [state] + | some newState => state :: countdown newState).head + p = + state := by + split at p <;> simp