From 3f0acbbb483d54e844260c960e80af86b48bbf46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Jan 2026 12:33:43 -0800 Subject: [PATCH] fix: use `isClass?` instead of binder annotation to identify instance parameters (#12172) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes how we determine whether a function parameter is an instance. Previously, we relied on binder annotations (e.g., `[Ring A]` vs `{_ : Ring A}`) to make this determination. This is unreliable because users legitimately use `{..}` binders for class types when the instance is already available from context. For example: ```lean structure OrdSet (α : Type) [Hashable α] [BEq α] where ... def OrdSet.insert {_ : Hashable α} {_ : BEq α} (s : OrdSet α) (a : α) : OrdSet α := ... ``` Here, `Hashable` and `BEq` are classes, but the `{..}` binder is intentional, the instances come from `OrdSet`'s parameters, so type class resolution is unnecessary. The fix checks the parameter's *type* using `isClass?` rather than its syntax, and caches this information in `FunInfo`. This affects several subsystems: - **Discrimination trees**: instance parameters should not be indexed even if marked with `{..}` - **Congruence lemma generation**: instances require special treatment - **`grind` canonicalizer**: must ensure canonical instances **Potential regressions**: automation may now behave differently in cases where it previously misidentified instance parameters. For example, a rewrite rule in `simp` that was not firing due to incorrect indexing may now fire. --------- Co-authored-by: Kim Morrison Co-authored-by: Claude --- src/Lean/Elab/Structure.lean | 8 +- src/Lean/Meta/ACLt.lean | 4 +- src/Lean/Meta/Basic.lean | 2 + src/Lean/Meta/CongrTheorems.lean | 4 +- src/Lean/Meta/DiscrTree/Main.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 10 +- src/Lean/Meta/FunInfo.lean | 52 ++++++--- src/Lean/Meta/LazyDiscrTree.lean | 2 +- src/Lean/Meta/Tactic/Grind/Anchor.lean | 4 +- src/Lean/Meta/Tactic/Grind/Canon.lean | 2 +- src/Lean/Meta/Tactic/Simp/Types.lean | 6 +- tests/lean/run/12172_regression.lean | 63 +++++++++++ tests/lean/run/grind_ematch_gen_pattern.lean | 4 +- tests/lean/run/grind_finish_trace.lean | 59 +++++----- .../grind_indexmap_getElem_indices_lt.lean | 4 +- tests/lean/run/grind_indexmap_trace.lean | 106 +++++++++--------- tests/lean/run/grind_interactive.lean | 20 ++-- tests/lean/run/grind_option.lean | 4 +- tests/lean/run/grind_order_issue.lean | 8 +- tests/lean/run/grind_reducible.lean | 6 +- tests/lean/run/grind_trace.lean | 12 +- tests/lean/run/grind_try_trace.lean | 4 +- tests/lean/run/sym_simp_4.lean | 2 +- 23 files changed, 240 insertions(+), 148 deletions(-) create mode 100644 tests/lean/run/12172_regression.lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 1593bf52dd..907f6962e0 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1272,9 +1272,6 @@ private def addProjections (params : Array Expr) (r : ElabHeaderResult) (fieldIn for fieldInfo in fieldInfos do if fieldInfo.kind.isSubobject then addDeclarationRangesFromSyntax fieldInfo.declName r.view.ref fieldInfo.ref - for decl in projDecls do - -- projections may generate equation theorems - enableRealizationsForConst decl.projName private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do let fields ← infos.filterMapM fun info => do @@ -1563,6 +1560,11 @@ def elabStructureCommand : InductiveElabDescr where checkResolutionOrder view.declName return { finalize := do + -- Enable realizations for projections here (after @[class] attribute is applied) + -- so that the realization context has class information available. + for fieldInfo in fieldInfos do + if fieldInfo.kind.isInCtor then + enableRealizationsForConst fieldInfo.declName if view.isClass then addParentInstances parentInfos } diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean index cb79c49614..ebb739560d 100644 --- a/src/Lean/Meta/ACLt.lean +++ b/src/Lean/Meta/ACLt.lean @@ -117,7 +117,7 @@ where let infos ← getParamsInfo aFn aArgs.size for i in *...infos.size do -- We ignore instance implicit arguments during comparison - if !infos[i]!.isInstImplicit then + if !infos[i]!.isInstance then if (← lt aArgs[i]! bArgs[i]!) then return true else if (← lt bArgs[i]! aArgs[i]!) then @@ -155,7 +155,7 @@ where let infos ← getParamsInfo f args.size for i in *...infos.size do -- We ignore instance implicit arguments during comparison - if !infos[i]!.isInstImplicit then + if !infos[i]!.isInstance then if !(← lt args[i]! b) then return false for h : i in infos.size...args.size do diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 05d6720d38..59a0b558ea 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -241,6 +241,8 @@ structure ParamInfo where This information affects the generation of congruence theorems. -/ isDecInst : Bool := false + /-- `isInstance` is true if the parameter type is a class instance. -/ + isInstance : Bool := false /-- `higherOrderOutParam` is true if this parameter is a higher-order output parameter of local instance. diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 6b6627302f..2b0f7de86c 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -197,7 +197,7 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) : result := result.push .fixed else if info.paramInfo[i].isProp then result := result.push .cast - else if info.paramInfo[i].isInstImplicit then + else if info.paramInfo[i].isInstance then if let some mask := mask? then if h2 : i < mask.size then if mask[i] then @@ -226,7 +226,7 @@ def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) := result := result.push .eq else if info.paramInfo[i].isProp then result := result.push .cast - else if info.paramInfo[i].isInstImplicit then + else if info.paramInfo[i].isInstance then if shouldUseSubsingletonInst info result i then result := result.push .subsingletonInst else diff --git a/src/Lean/Meta/DiscrTree/Main.lean b/src/Lean/Meta/DiscrTree/Main.lean index f84d7db52b..bdfbcdff9d 100644 --- a/src/Lean/Meta/DiscrTree/Main.lean +++ b/src/Lean/Meta/DiscrTree/Main.lean @@ -104,7 +104,7 @@ private def tmpStar := mkMVar tmpMVarId private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do if h : i < infos.size then let info := infos[i] - if info.isInstImplicit then + if info.isInstance then return true else if info.isImplicit || info.isStrictImplicit then return !(← isType a) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index ce236f2a6e..27a97984b2 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -300,7 +300,13 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let a₁ := args₁[i]! let a₂ := args₂[i]! let info := finfo.paramInfo[i]! - if info.isInstImplicit then + /- + **Note**: We use `binderInfo.isInstImplicit` (the `[..]` annotation) rather than + `info.isInstance` (whether the type is a class). Type class synthesis should only + be triggered for parameters explicitly marked for instance resolution, not merely + for parameters whose types happen to be class types. + -/ + if info.binderInfo.isInstImplicit then discard <| trySynthPending a₁ discard <| trySynthPending a₂ unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do @@ -309,7 +315,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let a₁ := args₁[i]! let a₂ := args₂[i]! let info := finfo.paramInfo[i]! - if info.isInstImplicit then + if info.isInstance then unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false else diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index 80a984a390..4388c0b1d6 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -85,26 +85,50 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := let dependsOnHigherOrderOutParam := !higherOrderOutParams.isEmpty && Option.isSome (decl.type.find? fun e => e.isFVar && higherOrderOutParams.contains e.fvarId!) + let className? ← isClass? decl.type + /- + **Note**: We use `isClass? decl.type` instead of relying solely on binder annotations + (`[...]`) because users sometimes use implicit binders for class types when the instance + is already available from context. For example: + ``` + structure OrdSet (α : Type) [Hashable α] [BEq α] where ... + def OrdSet.insert {_ : Hashable α} {_ : BEq α} (s : OrdSet α) (a : α) : OrdSet α := ... + ``` + Here, `Hashable` and `BEq` are classes, but implicit binders are used because the + instances come from `OrdSet`'s parameters. + + However, we also require the binder to be non-explicit because structures extending + classes use explicit binders for their constructor parameters: + ``` + structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α + -- Constructor type: + -- MyGroupTopology.mk (toMyTopology : MyTopology α) (toIsContinuousMul : IsContinuousMul α) : ... + ``` + These explicit parameters should not be treated as instances for automation purposes. + + -/ + let isInstance := className?.isSome && !decl.binderInfo.isExplicit paramInfo := updateHasFwdDeps paramInfo backDeps paramInfo := paramInfo.push { - backDeps, dependsOnHigherOrderOutParam + backDeps, dependsOnHigherOrderOutParam, isInstance binderInfo := decl.binderInfo isProp := (← isProp decl.type) isDecInst := (← forallTelescopeReducing decl.type fun _ type => return type.isAppOf ``Decidable) } - if decl.binderInfo == .instImplicit then - /- Collect higher order output parameters of this class -/ - if let some className ← isClass? decl.type then - if let some outParamPositions := getOutParamPositions? (← getEnv) className then - unless outParamPositions.isEmpty do - let args := decl.type.getAppArgs - for h2 : i in *...args.size do - if outParamPositions.contains i then - let arg := args[i] - if let some idx := fvars.idxOf? arg then - if (← whnf (← inferType arg)).isForall then - paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true } - higherOrderOutParams := higherOrderOutParams.insert arg.fvarId! + if isInstance then + /- Collect higher order output parameters of this class IF `isInstance` is `true` -/ + let some className := className? | unreachable! + /- Collect higher order output parameters of this class IF `isInstance` is `true` -/ + if let some outParamPositions := getOutParamPositions? (← getEnv) className then + unless outParamPositions.isEmpty do + let args := decl.type.getAppArgs + for h2 : i in *...args.size do + if outParamPositions.contains i then + let arg := args[i] + if let some idx := fvars.idxOf? arg then + if (← whnf (← inferType arg)).isForall then + paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true } + higherOrderOutParams := higherOrderOutParams.insert arg.fvarId! let resultDeps := collectDeps fvars type paramInfo := updateHasFwdDeps paramInfo resultDeps return { resultDeps, paramInfo } diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 97003fcec8..c5c6c1cc6b 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -78,7 +78,7 @@ def tmpStar := mkMVar tmpMVarId def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool := do if h : i < infos.size then let info := infos[i] - if info.isInstImplicit then + if info.isInstance then return true else if info.isImplicit || info.isStrictImplicit then return !(← isType a) diff --git a/src/Lean/Meta/Tactic/Grind/Anchor.lean b/src/Lean/Meta/Tactic/Grind/Anchor.lean index ad1b836d1c..984fb90d79 100644 --- a/src/Lean/Meta/Tactic/Grind/Anchor.lean +++ b/src/Lean/Meta/Tactic/Grind/Anchor.lean @@ -74,9 +74,9 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do let arg := args[i] if h : i < pinfos.size then let info := pinfos[i] - -- **Note**: we ignore implicit instances we computing stable hash codes + -- **Note**: we ignore instances we computing stable hash codes -- TODO: evaluate whether we should ignore regular implicit arguments too. - unless info.isInstImplicit do + unless info.isImplicit do r := mix r (← getAnchor arg) else r := mix r (← getAnchor arg) diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 416a88b15e..a4fb5f6926 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -174,7 +174,7 @@ See comments at `ShouldCanonResult`. private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do if h : i < pinfos.size then let pinfo := pinfos[i] - if pinfo.isInstImplicit then + if pinfo.isInstance then return .canonInst else if pinfo.isProp then return .visit diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index c8f7ce971b..ffe70a8b02 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -627,7 +627,7 @@ def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do if h : i < infos.size then trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}" let info := infos[i] - if cfg.ground && info.isInstImplicit then + if cfg.ground && info.isInstance then -- We don't visit instance implicit arguments when we are reducing ground terms. -- Motivation: many instance implicit arguments are ground, and it does not make sense -- to reduce them if the parent term is not ground. @@ -713,7 +713,7 @@ def simpAppUsingCongr (e : Expr) : SimpM Result := do if h : i < infos.size then let info := infos[i] trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {a} hasFwdDeps: {info.hasFwdDeps}" - if cfg.ground && info.isInstImplicit then + if cfg.ground && info.isInstance then -- We don't visit instance implicit arguments when we are reducing ground terms. -- Motivation: many instance implicit arguments are ground, and it does not make sense -- to reduce them if the parent term is not ground. @@ -788,7 +788,7 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do let mut i := 0 -- index at args for arg in args, kind in cgrThm.argKinds do if h : config.ground ∧ i < infos.size then - if (infos[i]'h.2).isInstImplicit then + if (infos[i]'h.2).isInstance then -- Do not visit instance implicit arguments when `ground := true` -- See comment at `congrArgs` argsNew := argsNew.push arg diff --git a/tests/lean/run/12172_regression.lean b/tests/lean/run/12172_regression.lean new file mode 100644 index 0000000000..34bf7c69ed --- /dev/null +++ b/tests/lean/run/12172_regression.lean @@ -0,0 +1,63 @@ +/- +Regression test for https://github.com/leanprover/lean4/pull/12172 + +The pattern: +1. A class `MeasurableSpace` is used as both a class and explicit argument (via @) +2. `Measure.trim` takes a Prop proof `hm : m ≤ m0` and returns `@Measure α m` +3. A typeclass `SigmaFinite` depends on `μ.trim hm` +4. A function `myFun` has `hm` explicit and `[SigmaFinite (μ.trim hm)]` as instance +5. A section variable makes `hm` implicit +6. A lemma `myFun_eq` takes an explicit proof argument before the final arg + +When calling `simp only [myFun_eq μ hs]`: +- Before #12172: `hm` is inferred, instance is found, works +- After #12172: Instance synthesis happens before `hm` is inferred, fails with + "failed to synthesize instance SigmaFinite (μ.trim ?m.XX)" + +Workaround: `simp only [myFun_eq (hm := hm) μ hs]` + +This pattern is used in Mathlib's MeasureTheory.Function.ConditionalExpectation.CondexpL1 +-/ + +set_option autoImplicit false +set_option linter.unusedVariables false + +universe u + +class MeasurableSpace (α : Type u) where + dummy : Unit := () + +instance {α : Type u} : LE (MeasurableSpace α) where + le _ _ := True + +structure Measure (α : Type u) [MeasurableSpace α] where + val : Nat + +def Measure.trim {α : Type u} {m m0 : MeasurableSpace α} + (μ : @Measure α m0) (_hm : m ≤ m0) : @Measure α m := + @Measure.mk α m μ.val + +class SigmaFinite {α : Type u} {m0 : MeasurableSpace α} (_μ : @Measure α m0) : Prop where + sigma_finite : True + +def myFun {α : Type u} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : @Measure α m0) + [SigmaFinite (μ.trim hm)] (n : Nat) : Nat := n + +section +variable {α : Type u} {m m0 : MeasurableSpace α} +variable (μ : @Measure α m0) +variable {hm : m ≤ m0} [SigmaFinite (μ.trim hm)] {s : Nat} + +theorem myFun_eq (hs : s > 0) (n : Nat) : myFun hm μ n = n := rfl + +-- This should work (worked before #12172) +theorem test_implicit_hm (hs : s > 0) (x y : Nat) : + myFun hm μ (x + y) = myFun hm μ x + myFun hm μ y := by + simp only [myFun_eq μ hs] + +-- Workaround with explicit hm also works +theorem test_explicit_hm (hs : s > 0) (x y : Nat) : + myFun hm μ (x + y) = myFun hm μ x + myFun hm μ y := by + simp only [myFun_eq (hm := hm) μ hs] + +end diff --git a/tests/lean/run/grind_ematch_gen_pattern.lean b/tests/lean/run/grind_ematch_gen_pattern.lean index adee8830c4..03b902bdfd 100644 --- a/tests/lean/run/grind_ematch_gen_pattern.lean +++ b/tests/lean/run/grind_ematch_gen_pattern.lean @@ -10,13 +10,13 @@ example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = som /-- info: Try these: - [apply] grind only [= gen Option.pbind_some', f, #ebef] + [apply] grind only [= gen Option.pbind_some', f, #81d1] [apply] grind only [= gen Option.pbind_some', f] [apply] grind => instantiate only [= gen Option.pbind_some'] instantiate only [f] mbtc - cases #ebef + cases #81d1 -/ #guard_msgs (info) in example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean index b8d3fdaf87..7356d0ecf4 100644 --- a/tests/lean/run/grind_finish_trace.lean +++ b/tests/lean/run/grind_finish_trace.lean @@ -2,8 +2,8 @@ open Lean Grind /-- info: Try these: - [apply] cases #c4b6 <;> cases #4c68 <;> ring - [apply] finish only [#c4b6, #4c68] + [apply] cases #e4c4 <;> cases #3e9f <;> ring + [apply] finish only [#e4c4, #3e9f] -/ #guard_msgs in example {α : Type} [CommRing α] (a b c d e : α) : @@ -17,10 +17,10 @@ example {α : Type} [CommRing α] (a b c d e : α) : /-- info: Try these: [apply] ⏎ - cases #b0f4 - · cases #50fc - · cases #50fc <;> lia - [apply] finish only [#b0f4, #50fc] + cases #6c8c + · cases #4228 + · cases #4228 <;> lia + [apply] finish only [#6c8c, #4228] -/ #guard_msgs in example (p : Nat → Prop) (x y z w : Int) : @@ -69,8 +69,8 @@ example (p : Nat → Prop) (x y z w : Int) : /-- info: Try these: - [apply] cases #5c4b <;> cases #896f <;> ac - [apply] finish only [#5c4b, #896f] + [apply] cases #5d93 <;> cases #11de <;> ac + [apply] finish only [#5d93, #11de] -/ #guard_msgs in example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d e : α) : @@ -105,11 +105,11 @@ set_option warn.sorry false /-- info: Try this: [apply] ⏎ - cases #c4b6 - · cases #8c9f + cases #e4c4 + · cases #7fb4 · ring · sorry - · cases #8c9f + · cases #7fb4 · ring · sorry -/ @@ -124,7 +124,7 @@ example {α : Type} [CommRing α] (a b c d e : α) : info: Try this: [apply] ⏎ instantiate only [= Nat.min_def] - cases #7640 + cases #d485 · sorry · lia -/ @@ -137,8 +137,8 @@ example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j info: Try these: [apply] ⏎ instantiate only [= getMsbD_setWidth'] - cases #aa9d - [apply] finish only [= getMsbD_setWidth', #aa9d] + cases #1f39 + [apply] finish only [= getMsbD_setWidth', #1f39] -/ #guard_msgs in open BitVec in @@ -151,13 +151,13 @@ example (ge : m ≥ n) (x : BitVec n) (i : Nat) : getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by grind => instantiate only [= getMsbD_setWidth'] - cases #aa9d + cases #c2c1 /-- info: Try these: - [apply] cases #9942 <;> - instantiate only [= BitVec.getElem_and] <;> instantiate only [= BitVec.getElem_or] <;> cases #cfbc - [apply] finish only [= BitVec.getElem_and, = BitVec.getElem_or, #9942, #cfbc] + [apply] cases #52a6 <;> + instantiate only [= BitVec.getElem_and] <;> instantiate only [= BitVec.getElem_or] <;> cases #de0f + [apply] finish only [= BitVec.getElem_and, = BitVec.getElem_or, #52a6, #de0f] -/ #guard_msgs in example (x y : BitVec 64) : (x ||| y) &&& x = x := by @@ -186,8 +186,8 @@ example (a : Array (BitVec 64)) (i : Nat) (v : BitVec 64) info: Try these: [apply] ⏎ mbtc - cases #a6c8 - [apply] finish only [#a6c8] + cases #aceb + [apply] finish only [#aceb] -/ #guard_msgs in example (f : Nat → Nat) (x : Nat) @@ -198,8 +198,8 @@ example (f : Nat → Nat) (x : Nat) info: Try these: [apply] ⏎ mbtc - cases #beb4 - [apply] finish only [#beb4] + cases #cb64 + [apply] finish only [#cb64] -/ #guard_msgs in example (f : Int → Int → Int) (x y : Int) @@ -220,7 +220,7 @@ example (f : Int → Int) (x y : Int) : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by grind => mbtc - cases #23ad <;> mbtc <;> cases #beb4 <;> mbtc <;> cases #beed + cases #ae37 <;> mbtc <;> cases #cb64 <;> mbtc <;> cases #de9d example (f : Int → Int) (x y : Int) : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by @@ -238,9 +238,9 @@ example (f g : Int → Int) (x y z w : Int) set_option trace.grind.split true in grind => mbtc - cases #23ad + cases #ae37 mbtc - cases #beb4 + cases #cb64 /-- trace: [grind.split] w = 0, generation: 0 @@ -269,7 +269,7 @@ example (f g : Int → Int) (x y z w : Int) g w ≠ z → f x = y := by fail_if_success grind [#23ad] -- not possible to solve using this set of anchors. set_option trace.grind.split true in - grind only [#23ad, #beb4] -- Only these two splits were performed. + grind only [#ae37, #cb64] -- Only these two splits were performed. /-- trace: [grind.split] x = 0, generation: 0 @@ -282,7 +282,8 @@ example (f g : Int → Int) (x y z w : Int) f 0 = y → f 1 = y → g w ≠ z → f x = y := by set_option trace.grind.split true in - grind => finish only [#23ad, #beb4] -- Only these two splits were performed. + grind => + finish only [#ae37, #cb64] /-- trace: [grind.ematch.instance] h: f (f a) = f a @@ -314,7 +315,7 @@ example (f g : Int → Int) (_ : g (g b) = b) : f (f (f a)) = f a := by set_option trace.grind.ematch.instance true in - grind only [#99cb] + grind only [#7a0d] /-- trace: [grind.ematch.instance] x✝²: f (f a) = f a @@ -329,4 +330,4 @@ example (f g : Int → Int) (_ : g (g b) = b) : f (f (f a)) = f a := by set_option trace.grind.ematch.instance true in - grind => finish only [#99cb] + grind => finish only [#7a0d] diff --git a/tests/lean/run/grind_indexmap_getElem_indices_lt.lean b/tests/lean/run/grind_indexmap_getElem_indices_lt.lean index bc1cc9cb67..a886c23ea6 100644 --- a/tests/lean/run/grind_indexmap_getElem_indices_lt.lean +++ b/tests/lean/run/grind_indexmap_getElem_indices_lt.lean @@ -110,7 +110,7 @@ example {h : a ∈ m} : m.indices[a] < m.size := by have : m.indices[a]? = some m.indices[a] := by grind have := m.WF m.indices[a] grind => - instantiate only [#41bd] + instantiate only [#bc4b] instantiate only [= getElem?_neg] instantiate only [= size_keys] @@ -119,7 +119,7 @@ example {h : a ∈ m} : m.indices[a] < m.size := by have : m.indices[a]? = some m.indices[a] := by grind have := m.WF m.indices[a] grind => - instantiate only [#41bd] + instantiate only [#bc4b] -- Display asserted facts show_asserted -- Display asserted facts with `generation > 0` diff --git a/tests/lean/run/grind_indexmap_trace.lean b/tests/lean/run/grind_indexmap_trace.lean index 008ab4f426..d1d33a2438 100644 --- a/tests/lean/run/grind_indexmap_trace.lean +++ b/tests/lean/run/grind_indexmap_trace.lean @@ -149,22 +149,22 @@ info: Try these: [apply] ⏎ instantiate only [= mem_indices_of_mem, insert] instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos] - cases #4ed2 - · cases #ffdf + cases #bd4f + · cases #54dd · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] - · cases #10d8 - · cases #2688 + · cases #2eb4 + · cases #cc2e · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] - · cases #ffdf + · cases #54dd · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos, - = HashMap.contains_insert, #4ed2, #ffdf, #10d8, #2688] + = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e] -/ #guard_msgs in example (m : IndexMap α β) (a a' : α) (b : β) : @@ -176,22 +176,22 @@ info: Try these: [apply] ⏎ instantiate only [= mem_indices_of_mem, insert] instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos] - cases #4ed2 - · cases #ffdf + cases #bd4f + · cases #54dd · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] - · cases #10d8 - · cases #2688 + · cases #2eb4 + · cases #cc2e · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] - · cases #ffdf + · cases #54dd · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos, - = HashMap.contains_insert, #4ed2, #ffdf, #10d8, #2688] + = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e] -/ #guard_msgs in example (m : IndexMap α β) (a a' : α) (b : β) : @@ -203,40 +203,33 @@ example (m : IndexMap α β) (a a' : α) (b : β) : grind => instantiate only [= mem_indices_of_mem, insert] instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos] - cases #4ed2 - · cases #ffdf + cases #bd4f + · cases #54dd · instantiate only · instantiate only instantiate only [= HashMap.contains_insert] - · cases #10d8 - · cases #2688 <;> finish only [= HashMap.contains_insert] - · cases #ffdf <;> finish only [= HashMap.contains_insert] + · cases #2eb4 + · cases #cc2e <;> finish only [= HashMap.contains_insert] + · cases #54dd <;> finish only [= HashMap.contains_insert] example (m : IndexMap α β) (a a' : α) (b : β) : a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by grind => instantiate only [= mem_indices_of_mem, insert] instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos] - cases #4ed2 - next => - cases #ffdf - next => instantiate only - next => - instantiate only + cases #bd4f + · cases #54dd + · instantiate only + · instantiate only instantiate only [= HashMap.contains_insert] - next => - cases #95a0 - next => - cases #2688 - next => instantiate only - next => - instantiate only + · cases #2eb4 + · cases #cc2e + · instantiate only + · instantiate only instantiate only [= HashMap.contains_insert] - next => - cases #ffdf - next => instantiate only - next => - instantiate only + · cases #54dd + · instantiate only + · instantiate only instantiate only [= HashMap.contains_insert] /-- @@ -247,9 +240,9 @@ info: Try these: instantiate only [=_ WF] instantiate only [= getElem?_neg, = getElem?_pos, = WF] instantiate only [= getElem?_neg, = getElem?_pos, = size_keys] - cases #f590 + cases #dbaf · instantiate only [size] - cases #ffdf + cases #54dd · instantiate only instantiate only [= Array.getElem_set] · instantiate only @@ -257,14 +250,14 @@ info: Try these: · instantiate only [= mem_indices_of_mem, = getElem_def, size] instantiate only [usr getElem_indices_lt, =_ WF] instantiate only [= getElem?_pos] - cases #ffdf + cases #54dd · instantiate only [WF'] instantiate only [= Array.getElem_set] · instantiate only instantiate only [= HashMap.getElem?_insert, = Array.getElem_push] [apply] finish only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push, - usr getElem_indices_lt, WF', #f590, #ffdf] + usr getElem_indices_lt, WF', #dbaf, #54dd] -/ #guard_msgs in example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : @@ -276,8 +269,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : grind => instantiate only [= mem_indices_of_mem, insert, = getElem_def] instantiate only [= getElem?_neg, = getElem?_pos] - cases #f590 - · cases #ffdf + cases #dbaf + · cases #54dd · instantiate only instantiate only [= Array.getElem_set] · instantiate only @@ -286,7 +279,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : · instantiate only [= mem_indices_of_mem, = getElem_def] instantiate only [usr getElem_indices_lt] instantiate only [size] - cases #ffdf + cases #54dd · instantiate only [usr getElem_indices_lt, =_ WF] instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set, = Array.getElem_set] @@ -298,7 +291,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : info: Try these: [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push, - usr getElem_indices_lt, WF', #f590, #ffdf] + usr getElem_indices_lt, WF', #dbaf, #54dd] [apply] grind only [= mem_indices_of_mem, insert, = getElem_def, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, = WF, = size_keys, size, = Array.getElem_set, = HashMap.getElem?_insert, = Array.getElem_push, usr getElem_indices_lt, WF'] @@ -308,9 +301,9 @@ info: Try these: instantiate only [=_ WF] instantiate only [= getElem?_neg, = getElem?_pos, = WF] instantiate only [= getElem?_neg, = getElem?_pos, = size_keys] - cases #f590 + cases #dbaf · instantiate only [size] - cases #ffdf + cases #54dd · instantiate only instantiate only [= Array.getElem_set] · instantiate only @@ -318,7 +311,7 @@ info: Try these: · instantiate only [= mem_indices_of_mem, = getElem_def, size] instantiate only [usr getElem_indices_lt, =_ WF] instantiate only [= getElem?_pos] - cases #ffdf + cases #54dd · instantiate only [WF'] instantiate only [= Array.getElem_set] · instantiate only @@ -334,8 +327,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : grind => instantiate only [= mem_indices_of_mem, insert, = getElem_def] instantiate only [= getElem?_neg, = getElem?_pos] - cases #f590 - · cases #ffdf + cases #dbaf + · cases #54dd · instantiate only instantiate only [= Array.getElem_set] · instantiate only @@ -344,7 +337,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : · instantiate only [= mem_indices_of_mem, = getElem_def] instantiate only [usr getElem_indices_lt] instantiate only [size] - cases #ffdf + cases #54dd · instantiate only [usr getElem_indices_lt, =_ WF] instantiate only [= mem_indices_of_mem, = getElem?_pos, = Array.size_set, = Array.getElem_set] @@ -356,7 +349,8 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by grind only [= mem_indices_of_mem, insert, = getElem_def, = getElem?_neg, = getElem?_pos, = Array.getElem_set, size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push, - usr getElem_indices_lt, =_ WF, = Array.size_set, WF', #f590, #ffdf] + usr getElem_indices_lt, usr Array.eq_empty_of_size_eq_zero, =_ WF, = Array.size_set, WF', #dbaf, + #54dd] /-- info: Try these: @@ -366,12 +360,12 @@ info: Try these: instantiate only [=_ WF] instantiate only [= getElem?_neg] instantiate only [= size_keys] - cases #1bba + cases #ffde · instantiate only [findIdx] · instantiate only instantiate only [= HashMap.getElem?_insert] [apply] finish only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, - = size_keys, = HashMap.getElem?_insert, #1bba] + = size_keys, = HashMap.getElem?_insert, #ffde] -/ #guard_msgs in example (m : IndexMap α β) (a : α) (b : β) : @@ -382,7 +376,7 @@ example (m : IndexMap α β) (a : α) (b : β) : info: Try these: [apply] grind [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, - = size_keys, = HashMap.getElem?_insert, #1bba] + = size_keys, = HashMap.getElem?_insert, #ffde] [apply] grind only [findIdx, insert, = mem_indices_of_mem, usr getElem?_pos, = getElem?_neg, = getElem?_pos, =_ WF, = size_keys, = HashMap.getElem?_insert] [apply] grind => @@ -391,7 +385,7 @@ info: Try these: instantiate only [=_ WF] instantiate only [= getElem?_neg] instantiate only [= size_keys] - cases #1bba + cases #ffde · instantiate only [findIdx] · instantiate only instantiate only [= HashMap.getElem?_insert] @@ -410,7 +404,7 @@ example (m : IndexMap α β) (a : α) (b : β) : grind => instantiate only [findIdx, insert, = mem_indices_of_mem] instantiate only [= getElem?_neg, = getElem?_pos] - cases #1bba + cases #acc3 · instantiate only [findIdx] · finish only [= HashMap.mem_insert, = HashMap.getElem_insert] @@ -419,7 +413,7 @@ example (m : IndexMap α β) (a : α) (b : β) : grind => instantiate only [findIdx, insert, = mem_indices_of_mem] instantiate only [= getElem?_neg, = getElem?_pos] - cases #1bba <;> + cases #acc3 <;> finish only [findIdx, = HashMap.mem_insert, = HashMap.getElem_insert] end IndexMap diff --git a/tests/lean/run/grind_interactive.lean b/tests/lean/run/grind_interactive.lean index ef6d92b235..e6baf33bc8 100644 --- a/tests/lean/run/grind_interactive.lean +++ b/tests/lean/run/grind_interactive.lean @@ -217,11 +217,11 @@ def h (as : List Nat) := /-- trace: [splits] Case split candidates - [split] #829a := match bs with + [split] #8289 := match bs with | [] => 1 | [head] => 2 | head :: head_1 :: tail => 3 - [split] #dce6 := match as with + [split] #bf4f := match as with | [] => 1 | [head] => 2 | head :: head_1 :: tail => 3 @@ -237,7 +237,7 @@ example : h bs = 1 → h as ≠ 0 := by grind [h.eq_def] => instantiate show_cases - cases #dce6 + cases #bf4f instantiate focus instantiate instantiate @@ -263,7 +263,7 @@ example : h bs = 1 → h as ≠ 0 := by example : h bs = 1 → h as ≠ 0 := by grind [h.eq_def] => instantiate | as - cases #dce6 + cases #bf4f all_goals instantiate /-- @@ -309,12 +309,12 @@ example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p example : h bs = 1 → h as ≠ 0 := by grind [h.eq_def] => instantiate - cases #dce6 <;> instantiate + cases #bf4f <;> instantiate example : h bs = 1 → h as ≠ 1 := by grind [h.eq_def] => instantiate - cases #dce6 + cases #8289 any_goals instantiate sorry @@ -330,7 +330,7 @@ h✝ : as = [] example : h bs = 1 → h as ≠ 0 := by grind -verbose [h.eq_def] => instantiate - cases #dce6 + cases #bf4f next => skip all_goals sorry @@ -343,7 +343,7 @@ def g (as : List Nat) := example : g bs = 1 → g as ≠ 0 := by grind [g.eq_def] => instantiate - cases #dce6 + cases #bf4f next => instantiate next => finish tactic => @@ -542,7 +542,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by show_cases rename_i y w _ -- Must reset cached anchors show_cases - cases #e2a6 + cases #dded all_goals sorry example : (a : Point Nat) → p a → x ≠ y → False := by @@ -553,7 +553,7 @@ example : (a : Point Nat) → p a → x ≠ y → False := by show_cases next y w _ => show_cases - cases #e2a6 + cases #dded all_goals sorry example : (a : Point Nat) → p a → x ≠ y → False := by diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean index c61fd01701..07b0ebbc89 100644 --- a/tests/lean/run/grind_option.lean +++ b/tests/lean/run/grind_option.lean @@ -38,11 +38,11 @@ example : Option.guard (· ≤ 7) 3 = some 3 := by grind? /-- info: Try these: - [apply] grind only [= Option.mem_bind_iff, #99bb] + [apply] grind only [= Option.mem_bind_iff, #8b09] [apply] grind only [= Option.mem_bind_iff] [apply] grind => instantiate only [= Option.mem_bind_iff] - instantiate only [#99bb] + instantiate only [#8b09] -/ #guard_msgs in example {x : β} {o : Option α} {f : α → Option β} (h : a ∈ o) (h' : x ∈ f a) : x ∈ o.bind f := by grind? diff --git a/tests/lean/run/grind_order_issue.lean b/tests/lean/run/grind_order_issue.lean index 41ebe74f78..2b9fd3734b 100644 --- a/tests/lean/run/grind_order_issue.lean +++ b/tests/lean/run/grind_order_issue.lean @@ -101,9 +101,9 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by grind -ring -linarith -lia => instantiate only [= getElem_def, insert] - cases #f590 + cases #dbaf next => - cases #ffdf + cases #54dd next => sorry next => instantiate only @@ -116,9 +116,9 @@ example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) : (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by grind -ring -linarith -lia => instantiate only [= getElem_def, insert] - cases #f590 + cases #dbaf next => - cases #ffdf + cases #54dd next => sorry next => instantiate only diff --git a/tests/lean/run/grind_reducible.lean b/tests/lean/run/grind_reducible.lean index b8a9b88dc7..cfb7bd815c 100644 --- a/tests/lean/run/grind_reducible.lean +++ b/tests/lean/run/grind_reducible.lean @@ -47,13 +47,13 @@ example : example : (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by - grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun] + grind -reducible => cases #d592 <;> instantiate only [Equiv.congr_fun] /-- info: Try these: - [apply] grind -reducible only [Equiv.congr_fun, #5103] + [apply] grind -reducible only [Equiv.congr_fun, #d592] [apply] grind -reducible only [Equiv.congr_fun] - [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun] + [apply] grind -reducible => cases #d592 <;> instantiate only [Equiv.congr_fun] -/ #guard_msgs in example : diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean index 276182ee80..289e7a0dbd 100644 --- a/tests/lean/run/grind_trace.lean +++ b/tests/lean/run/grind_trace.lean @@ -42,20 +42,20 @@ attribute [grind ext] List.ext_getElem? info: Try these: [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none, = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some, - = Option.map_none, #12fe, #986e, #0323] + = Option.map_none, #648a, #bb68, #a564] [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none, = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some, = Option.map_none] [apply] grind => - cases #12fe + cases #648a instantiate only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none, = List.getElem?_eq_getElem] instantiate only [= List.getElem?_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem, = List.length_replicate] instantiate only [= List.length_replicate] - cases #986e + cases #bb68 · instantiate only [= List.getElem?_eq_some_iff] - cases #0323 + cases #a564 · instantiate only [= Option.map_some] · instantiate only [= Option.map_none] · instantiate only [= Option.map_some] @@ -66,11 +66,11 @@ theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := /-- info: Try these: - [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self, #e8ab] + [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self, #1ecf] [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self] [apply] grind => instantiate only [= List.getLast?_eq_some_iff] - cases #e8ab <;> instantiate only [← List.mem_concat_self] + cases #1ecf <;> instantiate only [← List.mem_concat_self] -/ #guard_msgs (info) in theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean index 074b3596b4..83e55f8e23 100644 --- a/tests/lean/run/grind_try_trace.lean +++ b/tests/lean/run/grind_try_trace.lean @@ -61,12 +61,12 @@ example : f (f 0) > 0 := by /-- info: Try these: [apply] grind [= f.eq_def] - [apply] grind only [= f.eq_def, #bb96] + [apply] grind only [= f.eq_def, #6818] [apply] grind only [= f.eq_def] [apply] grind => instantiate only [= f.eq_def] instantiate only - cases #bb96 <;> instantiate only + cases #6818 <;> instantiate only -/ #guard_msgs (info) in example : f x > 0 := by diff --git a/tests/lean/run/sym_simp_4.lean b/tests/lean/run/sym_simp_4.lean index ebacf90cf9..c81448e03d 100644 --- a/tests/lean/run/sym_simp_4.lean +++ b/tests/lean/run/sym_simp_4.lean @@ -52,7 +52,7 @@ example (α β : Type) (p q : Prop) : q → β → p → α → True := by sym_simp [] /-- -trace: α✝ : Sort ?u.1893 +trace: α✝ : Sort ?u.1921 x : α✝ α : Type p : Prop