From 2337b95676b1369d867be80a2fc0fb525dd00c95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Apr 2025 10:57:56 -0700 Subject: [PATCH] feat: improve case split heuristics in `grind` (#7946) This PR improves the case split heuristics in `grind`. --- src/Lean/Meta/Tactic/Grind/Internalize.lean | 20 ++-- src/Lean/Meta/Tactic/Grind/Lookahead.lean | 38 +------ src/Lean/Meta/Tactic/Grind/MBTC.lean | 62 +++++------ src/Lean/Meta/Tactic/Grind/Split.lean | 74 +++++++++---- src/Lean/Meta/Tactic/Grind/Types.lean | 110 ++++++++++---------- tests/lean/run/grind_bintree.lean | 3 +- 6 files changed, 154 insertions(+), 153 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 9ee4255914..0b8a969467 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -62,10 +62,10 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do match e with | .app .. => if (← getConfig).splitIte && (e.isIte || e.isDIte) then - addSplitCandidate e + addSplitCandidate (.default e) return () if isMorallyIff e then - addSplitCandidate e + addSplitCandidate (.default e) return () if (← getConfig).splitMatch then if (← isMatcherApp e) then @@ -74,7 +74,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do -- and consequently don't need to be split. return () else - addSplitCandidate e + addSplitCandidate (.default e) return () let .const declName _ := e.getAppFn | return () if forbiddenSplitTypes.contains declName then @@ -82,21 +82,21 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do unless (← isInductivePredicate declName) do return () if (← get).split.casesTypes.isSplit declName then - addSplitCandidate e + addSplitCandidate (.default e) else if (← getConfig).splitIndPred then - addSplitCandidate e + addSplitCandidate (.default e) | .fvar .. => let .const declName _ := (← whnfD (← inferType e)).getAppFn | return () if (← get).split.casesTypes.isSplit declName then - addSplitCandidate e + addSplitCandidate (.default e) | .forallE _ d _ _ => if (← getConfig).splitImp then - addSplitCandidate e + addSplitCandidate (.default e) else if Arith.isRelevantPred d then if (← getConfig).lookahead then - addLookaheadCandidate (.imp e) + addLookaheadCandidate (.default e) else - addSplitCandidate e + addSplitCandidate (.default e) | _ => pure () /-- @@ -260,7 +260,7 @@ where -- if (← getConfig).lookahead then -- addLookaheadCandidate (.arg other.app parent i eq) -- else - addSplitCandidate eq + addSplitCandidate (.arg other.app parent i eq) modify fun s => { s with split.argsAt := s.split.argsAt.insert (f, i) ({ arg, type, app := parent } :: others) } return () diff --git a/src/Lean/Meta/Tactic/Grind/Lookahead.lean b/src/Lean/Meta/Tactic/Grind/Lookahead.lean index 8e40ee43c6..e093e2afb8 100644 --- a/src/Lean/Meta/Tactic/Grind/Lookahead.lean +++ b/src/Lean/Meta/Tactic/Grind/Lookahead.lean @@ -12,39 +12,6 @@ import Lean.Meta.Tactic.Grind.EMatch namespace Lean.Meta.Grind -inductive LookaheadStatus where - | resolved - | notReady - | ready - deriving Inhabited, BEq, Repr - -private def checkLookaheadStatus (info : LookaheadInfo) : GoalM LookaheadStatus := do - match info with - | .imp e => - unless (← isEqTrue e) do return .notReady - let .forallE _ d b _ := e | unreachable! - if (← isEqTrue d <||> isEqFalse d) then return .resolved - unless b.hasLooseBVars do - if (← isEqTrue b <||> isEqFalse b) then return .resolved - return .ready - | .arg a b _ eq => - if (← isEqTrue eq <||> isEqFalse eq) then return .resolved - let is := (← get).split.lookaheadArgPos[(a, b)]? |>.getD [] - let mut j := a.getAppNumArgs - let mut it_a := a - let mut it_b := b - repeat - unless it_a.isApp && it_b.isApp do return .ready - j := j - 1 - if j ∉ is then - let arg_a := it_a.appArg! - let arg_b := it_b.appArg! - unless (← isEqv arg_a arg_b) do - return .notReady - it_a := it_a.appFn! - it_b := it_b.appFn! - return .ready - private partial def solve (generation : Nat) (goal : Goal) : GrindM Bool := do cont (← intros generation goal) where @@ -110,10 +77,11 @@ def lookahead : GrindTactic := fun goal => do for info in infos do if (← isInconsistent) then return true - match (← checkLookaheadStatus info) with + match (← checkSplitStatus info) with | .resolved => progress := true + | .ready _ _ true | .notReady => postponed := info :: postponed - | .ready => + | .ready _ _ false => if (← tryLookahead info.getExpr) then progress := true else diff --git a/src/Lean/Meta/Tactic/Grind/MBTC.lean b/src/Lean/Meta/Tactic/Grind/MBTC.lean index cde7fe30d0..9b6d7133fa 100644 --- a/src/Lean/Meta/Tactic/Grind/MBTC.lean +++ b/src/Lean/Meta/Tactic/Grind/MBTC.lean @@ -33,13 +33,20 @@ structure MBTC.Context where -/ eqAssignment : Expr → Expr → GoalM Bool -private abbrev Map := Std.HashMap (Expr × Nat) (List Expr) -private abbrev Candidates := Std.HashSet (Expr × Expr) -private def mkCandidateKey (a b : Expr) : Expr × Expr := - if a.lt b then - (a, b) +private structure ArgInfo where + arg : Expr + app : Expr + +private abbrev Map := Std.HashMap (Expr × Nat) (List ArgInfo) +private abbrev Candidates := Std.HashSet SplitInfo +private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do + let (lhs, rhs) := if a.arg.lt b.arg then + (a.arg, b.arg) else - (b, a) + (b.arg, a.arg) + let eq ← mkEq lhs rhs + let eq ← shareCommon (← canon eq) + return .arg a.app b.app i eq /-- Model-based theory combination. -/ def mbtc (ctx : MBTC.Context) : GoalM Bool := do @@ -58,40 +65,33 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do let some arg ← getRoot? arg | pure () if (← ctx.hasTheoryVar arg) then trace[grind.debug.mbtc] "{arg} @ {f}:{i}" - if let some others := map[(f, i)]? then - unless others.any (isSameExpr arg ·) do - for other in others do - if (← ctx.eqAssignment arg other) then - if (← hasSameType arg other) then - let k := mkCandidateKey arg other - candidates := candidates.insert k - map := map.insert (f, i) (arg :: others) + let argInfo : ArgInfo := { arg, app := e } + if let some otherInfos := map[(f, i)]? then + unless otherInfos.any fun info => isSameExpr arg info.arg do + for otherInfo in otherInfos do + if (← ctx.eqAssignment arg otherInfo.arg) then + if (← hasSameType arg otherInfo.arg) then + candidates := candidates.insert (← mkCandidate argInfo otherInfo i) + map := map.insert (f, i) (argInfo :: otherInfos) else - map := map.insert (f, i) [arg] + map := map.insert (f, i) [argInfo] i := i + 1 if candidates.isEmpty then return false if (← get).split.num > (← getConfig).splits then reportIssue "skipping `mbtc`, maximum number of splits has been reached `(splits := {(← getConfig).splits})`" return false - let result := candidates.toArray.qsort fun (a₁, b₁) (a₂, b₂) => - if isSameExpr a₁ a₂ then - b₁.lt b₂ - else - a₁.lt a₂ - let eqs ← result.filterMapM fun (a, b) => do - let eq ← mkEq a b - trace[grind.mbtc] "{eq}" - let eq ← shareCommon (← canon eq) - if (← isKnownCaseSplit eq) then + let result := candidates.toArray.qsort fun c₁ c₂ => c₁.lt c₂ + let result ← result.filterMapM fun info => do + if (← isKnownCaseSplit info) then return none - else - internalize eq (Nat.max (← getGeneration a) (← getGeneration b)) - return some eq - if eqs.isEmpty then + let .arg a b _ eq := info | return none + internalize eq (Nat.max (← getGeneration a) (← getGeneration b)) + return some info + if result.isEmpty then return false - for eq in eqs do - addSplitCandidate eq + for info in result do + addSplitCandidate info return true def mbtcTac (ctx : MBTC.Context) : GrindTactic := fun goal => do diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean index af8285f318..29ce2fc863 100644 --- a/src/Lean/Meta/Tactic/Grind/Split.lean +++ b/src/Lean/Meta/Tactic/Grind/Split.lean @@ -11,14 +11,14 @@ import Lean.Meta.Tactic.Grind.CasesMatch namespace Lean.Meta.Grind -inductive CaseSplitStatus where +inductive SplitStatus where | resolved | notReady - | ready (numCases : Nat) (isRec := false) + | ready (numCases : Nat) (isRec := false) (tryPostpone := false) deriving Inhabited, BEq, Repr /-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/ -private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do +private def checkIteCondStatus (c : Expr) : GoalM SplitStatus := do if (← isEqTrue c <||> isEqFalse c) then return .resolved else @@ -28,7 +28,7 @@ private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`. That is, `e` is `True`, but neither `a` nor `b` is `True`." -/ -private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do +private def checkDisjunctStatus (e a b : Expr) : GoalM SplitStatus := do if (← isEqTrue e) then if (← isEqTrue a <||> isEqTrue b) then return .resolved @@ -43,7 +43,7 @@ private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`. That is, `e` is `False`, but neither `a` nor `b` is `False`. -/ -private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do +private def checkConjunctStatus (e a b : Expr) : GoalM SplitStatus := do if (← isEqTrue e) then return .resolved else if (← isEqFalse e) then @@ -60,7 +60,7 @@ There are two cases: 1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`. 2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`. -/ -private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do +private def checkIffStatus (e a b : Expr) : GoalM SplitStatus := do if (← isEqTrue e) then if (← (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then return .resolved @@ -83,7 +83,7 @@ private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do else return c'.isApp && isCongruent (← get).enodes c c' -private def checkForallStatus (e : Expr) : GoalM CaseSplitStatus := do +private def checkForallStatus (e : Expr) : GoalM SplitStatus := do if (← isEqTrue e) then let .forallE _ p q _ := e | return .resolved if (← isEqTrue p <||> isEqFalse p) then @@ -97,7 +97,7 @@ private def checkForallStatus (e : Expr) : GoalM CaseSplitStatus := do else return .notReady -private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do +private def checkDefaultSplitStatus (e : Expr) : GoalM SplitStatus := do match_expr e with | Or a b => checkDisjunctStatus e a b | And a b => checkConjunctStatus e a b @@ -133,9 +133,37 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do return .ready info.ctors.length info.isRec return .notReady +def checkSplitInfoArgStatus (a b : Expr) (eq : Expr) : GoalM SplitStatus := do + if (← isEqTrue eq <||> isEqFalse eq) then return .resolved + let is := (← get).split.argPosMap[(a, b)]? |>.getD [] + let mut j := a.getAppNumArgs + let mut it_a := a + let mut it_b := b + repeat + unless it_a.isApp && it_b.isApp do return .ready 2 + j := j - 1 + if j ∉ is then + let arg_a := it_a.appArg! + let arg_b := it_b.appArg! + unless (← isEqv arg_a arg_b) do + trace_goal[grind.split] "may be irrelevant\na: {a}\nb: {b}\neq: {eq}\narg_a: {arg_a}\narg_b: {arg_b}, gen: {← getGeneration eq}" + /- + We tried to return `.notReady` because we would not be able to derive a congruence, but + `grind_ite.lean` breaks when this heuristic is used. TODO: understand better why. + -/ + return .ready 2 (tryPostpone := true) + it_a := it_a.appFn! + it_b := it_b.appFn! + return .ready 2 + +def checkSplitStatus (s : SplitInfo) : GoalM SplitStatus := do + match s with + | .default e => checkDefaultSplitStatus e + | .arg a b _ eq => checkSplitInfoArgStatus a b eq + private inductive SplitCandidate where | none - | some (c : Expr) (numCases : Nat) (isRec : Bool) + | some (c : SplitInfo) (numCases : Nat) (isRec : Bool) (tryPostpone : Bool) /-- Returns the next case-split to be performed. It uses a very simple heuristic. -/ private def selectNextSplit? : GoalM SplitCandidate := do @@ -143,11 +171,11 @@ private def selectNextSplit? : GoalM SplitCandidate := do if (← checkMaxCaseSplit) then return .none go (← get).split.candidates .none [] where - go (cs : List Expr) (c? : SplitCandidate) (cs' : List Expr) : GoalM SplitCandidate := do + go (cs : List SplitInfo) (c? : SplitCandidate) (cs' : List SplitInfo) : GoalM SplitCandidate := do match cs with | [] => modify fun s => { s with split.candidates := cs'.reverse } - if let .some _ numCases isRec := c? then + if let .some _ numCases isRec _ := c? then let numSplits := (← get).split.num -- We only increase the number of splits if there is more than one case or it is recursive. let numSplits := if numCases > 1 || isRec then numSplits + 1 else numSplits @@ -156,24 +184,28 @@ where modify fun s => { s with split.num := numSplits, ematch.num := 0 } return c? | c::cs => - trace_goal[grind.debug.split] "checking: {c}" - match (← checkCaseSplitStatus c) with + trace_goal[grind.debug.split] "checking: {c.getExpr}" + match (← checkSplitStatus c) with | .notReady => go cs c? (c::cs') | .resolved => go cs c? cs' - | .ready numCases isRec => + | .ready numCases isRec tryPostpone => if (← cheapCasesOnly) && numCases > 1 then go cs c? (c::cs') else match c? with - | .none => go cs (.some c numCases isRec) cs' - | .some c' numCases' _ => + | .none => go cs (.some c numCases isRec tryPostpone) cs' + | .some c' numCases' _ tryPostpone' => let isBetter : GoalM Bool := do - if numCases == 1 && !isRec && numCases' > 1 then + if tryPostpone' && !tryPostpone then return true - if (← getGeneration c) < (← getGeneration c') then + else if tryPostpone && !tryPostpone' then + return false + else if numCases == 1 && !isRec && numCases' > 1 then + return true + if (← getGeneration c.getExpr) < (← getGeneration c'.getExpr) then return true return numCases < numCases' if (← isBetter) then - go cs (.some c numCases isRec) (c'::cs') + go cs (.some c numCases isRec tryPostpone) (c'::cs') else go cs c? (c::cs') @@ -195,6 +227,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do else -- model-based theory combination split return mkGrindEM c + | Not e => return mkGrindEM e | _ => if let .forallE _ p _ _ := c then return mkGrindEM p @@ -215,8 +248,9 @@ and returns a new list of goals if successful. -/ def splitNext : GrindTactic := fun goal => do let (goals?, _) ← GoalM.run goal do - let .some c numCases isRec ← selectNextSplit? + let .some c numCases isRec _ ← selectNextSplit? | return none + let c := c.getExpr let gen ← getGeneration c let genNew := if numCases > 1 || isRec then gen+1 else gen markCaseSplitAsResolved c diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 5620329166..056c1650cd 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -484,73 +484,72 @@ structure EMatch.State where matchEqNames : PHashSet Name := {} deriving Inhabited -/-- -Lookahead case-split information. They are cheaper than regular case-splits. -They are created when `Grind.Config.lookahead` is `true`. -The idea is the following: `grind` asserts `¬ p`, if a contradiction is detected -it asserts `p`. --/ -inductive LookaheadInfo where +/-- Case-split information. -/ +inductive SplitInfo where | /-- - Given an implication `e`, use lookahead to check whether the antecedent is - implied to be `True`. The lookahead is marked as resolved if the consequent is already - known to be `True`. + Term `e` may be an inductive predicate, `match`-expression, `if`-expression, implication, etc. -/ - imp (e : Expr) + default (e : Expr) | /-- - Given applications `a` and `b`, use lookahead to check whether the corresponding - `i`-th arguments are equal or not. The lookahead is only performed if all other - arguments are already known to be equal or are also tagged as lookahead. - `eq` is the equality between the two arguments + Given applications `a` and `b`, case-split on whether the corresponding + `i`-th arguments are equal or not. The split is only performed if all other + arguments are already known to be equal or are also tagged as split candidates. -/ arg (a b : Expr) (i : Nat) (eq : Expr) + deriving BEq, Hashable, Inhabited -/-- Returns expression to perform a lookahead case-split. -/ -def LookaheadInfo.getExpr : LookaheadInfo → Expr - | .imp e => e.bindingDomain! +def SplitInfo.getExpr : SplitInfo → Expr + | .default (.forallE _ d _ _) => d + | .default e => e | .arg _ _ _ eq => eq -/-- Argument `arg : type` of an application `app` -/ -structure Arg where +def SplitInfo.lt : SplitInfo → SplitInfo → Bool + | .default e₁, .default e₂ => e₁.lt e₂ + | .arg _ _ _ e₁, .arg _ _ _ e₂ => e₁.lt e₂ + | .default _, .arg .. => true + | .arg .., .default _ => false + +/-- Argument `arg : type` of an application `app` in `SplitInfo`. -/ +structure SplitArg where arg : Expr type : Expr app : Expr /-- Case splitting related fields for the `grind` goal. -/ structure Split.State where - /-- Inductive datatypes marked for case-splitting -/ - casesTypes : CasesTypes := {} - /-- Case-split candidates. -/ - candidates : List Expr := [] /-- Number of splits performed to get to this goal. -/ - num : Nat := 0 + num : Nat := 0 + /-- Inductive datatypes marked for case-splitting -/ + casesTypes : CasesTypes := {} + /-- Case-split candidates. -/ + candidates : List SplitInfo := [] /-- Case-splits that have been inserted at `candidates` at some point. -/ - added : PHashSet ENodeKey := {} + added : Std.HashSet SplitInfo := {} /-- Case-splits that have already been performed, or that do not have to be performed anymore. -/ - resolved : PHashSet ENodeKey := {} + resolved : PHashSet ENodeKey := {} /-- Sequence of cases steps that generated this goal. We only use this information for diagnostics. Remark: `casesTrace.length ≥ numSplits` because we don't increase the counter for `cases` applications that generated only 1 subgoal. -/ - trace : List CaseTrace := [] + trace : List CaseTrace := [] /-- Lookahead "case-splits". -/ - lookaheads : List LookaheadInfo := [] + lookaheads : List SplitInfo := [] /-- - A mapping `(a, b) ↦ is` s.t. for each `LookaheadInfo.arg a b i eq` - in `lookaheads` we have `i ∈ is`. - We use this information to decide whether the lookahead is "ready" + A mapping `(a, b) ↦ is` s.t. for each `SplitInfo.arg a b i eq` + in `candidates` or `lookaheads` we have `i ∈ is`. + We use this information to decide whether the split/lookahead is "ready" to be tried or not. -/ - lookaheadArgPos : Std.HashMap (Expr × Expr) (List Nat) := {} + argPosMap : Std.HashMap (Expr × Expr) (List Nat) := {} /-- Mapping from pairs `(f, i)` to a list of arguments. Each argument occurs as the `i`-th of an `f`-application. - We use this information to add case-splits for + We use this information to add splits/lookaheads for triggering extensionality theorems and model-based theory combination. See `addSplitCandidatesForExt`. -/ - argsAt : PHashMap (Expr × Nat) (List Arg) := {} + argsAt : PHashMap (Expr × Nat) (List SplitArg) := {} deriving Inhabited /-- Clean name generator. -/ @@ -1217,12 +1216,12 @@ def getEqcs : GoalM (List (List Expr)) := return (← get).getEqcs /-- -Returns `true` if `e` has been already added to the case-split list at one point. +Returns `true` if `s` has been already added to the case-split list at one point. Remark: this function returns `true` even if the split has already been resolved and is not in the list anymore. -/ -def isKnownCaseSplit (e : Expr) : GoalM Bool := - return (← get).split.added.contains { expr := e } +def isKnownCaseSplit (s : SplitInfo) : GoalM Bool := + return (← get).split.added.contains s /-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/ def isResolvedCaseSplit (e : Expr) : GoalM Bool := @@ -1238,14 +1237,23 @@ def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do trace_goal[grind.split.resolved] "{e}" modify fun s => { s with split.resolved := s.split.resolved.insert { expr := e } } +private def updateSplitArgPosMap (sinfo : SplitInfo) : GoalM Unit := do + let .arg a b i _ := sinfo | return () + let key := (a, b) + let is := (← get).split.argPosMap[key]? |>.getD [] + modify fun s => { s with + split.argPosMap := s.split.argPosMap.insert key (i :: is) + } + /-- Inserts `e` into the list of case-split candidates if it was not inserted before. -/ -def addSplitCandidate (e : Expr) : GoalM Unit := do - unless (← isKnownCaseSplit e) do - trace_goal[grind.split.candidate] "{e}" +def addSplitCandidate (sinfo : SplitInfo) : GoalM Unit := do + unless (← isKnownCaseSplit sinfo) do + trace_goal[grind.split.candidate] "{sinfo.getExpr}" modify fun s => { s with - split.added := s.split.added.insert { expr := e } - split.candidates := e :: s.split.candidates + split.added := s.split.added.insert sinfo + split.candidates := sinfo :: s.split.candidates } + updateSplitArgPosMap sinfo /-- Returns extensionality theorems for the given type if available. @@ -1269,18 +1277,10 @@ def synthesizeInstanceAndAssign (x type : Expr) : MetaM Bool := do isDefEq x val /-- Add a new lookahead candidate. -/ -def addLookaheadCandidate (info : LookaheadInfo) : GoalM Unit := do - trace_goal[grind.lookahead.add] "{info.getExpr}" - match info with - | .imp .. => - modify fun s => { s with split.lookaheads := info :: s.split.lookaheads } - | .arg a b i _ => - let key := (a, b) - let is := (← get).split.lookaheadArgPos[key]? |>.getD [] - modify fun s => { s with - split.lookaheads := info :: s.split.lookaheads - split.lookaheadArgPos := s.split.lookaheadArgPos.insert key (i :: is) - } +def addLookaheadCandidate (sinfo : SplitInfo) : GoalM Unit := do + trace_goal[grind.lookahead.add] "{sinfo.getExpr}" + modify fun s => { s with split.lookaheads := sinfo :: s.split.lookaheads } + updateSplitArgPosMap sinfo /-- Helper function for executing `x` with a fresh `newFacts` and without modifying diff --git a/tests/lean/run/grind_bintree.lean b/tests/lean/run/grind_bintree.lean index 5630a5f29f..5a68261a2a 100644 --- a/tests/lean/run/grind_bintree.lean +++ b/tests/lean/run/grind_bintree.lean @@ -92,8 +92,7 @@ theorem Tree.forall_insert_of_forall theorem Tree.bst_insert_of_bst {t : Tree β} (h : BST t) (key : Nat) (value : β) : BST (t.insert key value) := by - -- TODO: improve `grind` `funext` support, and minimize the number of splits - induction h <;> grind (splits := 12) [BST.node, BST.leaf, ForallTree.leaf, forall_insert_of_forall] + induction h <;> grind [BST.node, BST.leaf, ForallTree.leaf, forall_insert_of_forall] def BinTree (β : Type u) := { t : Tree β // BST t }