From a157abbbc9913a4fef5c5e7de6a7b733c4651660 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Aug 2025 14:12:57 -0700 Subject: [PATCH] fix: E-matching patterns containing ground universe polymorphic patterns in `grind` (#9857) This PR ensures `grind` can E-match patterns containing universe polymorphic ground sub-patterns. For example, given ``` set_option pp.universes true in attribute [grind?] Id.run_pure ``` the pattern ``` Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)] ``` contains two nested universe polymorphic ground patterns - `Id.{u_1}` - `Applicative.toPure.{u_1, u_1}` This kind of pattern is not common, but it occurs in core. --- src/Lean/Meta/Tactic/Grind/EMatch.lean | 47 ++++++++++++------- src/Lean/Meta/Tactic/Grind/Internalize.lean | 21 +++++++-- .../run/grind_univ_poly_ground_pattern.lean | 3 ++ 3 files changed, 50 insertions(+), 21 deletions(-) create mode 100644 tests/lean/run/grind_univ_poly_ground_pattern.lean diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index 696c07cb3e..7e19f6fa7b 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -131,6 +131,33 @@ protected def _root_.Lean.Meta.Grind.GenPatternInfo.assign? (genInfo : GenPatter let c ← assignDelayedEqProof? c genInfo.hIdx return c +private def matchGroundPattern (pArg eArg : Expr) : GoalM Bool := do + /- + 1) Remark: + We need to use `withReducibleAndInstances` because ground patterns are often instances. + Here is an example + ``` + instance : Max Nat where + max := Nat.max -- Redefined the instance + + example (a : Nat) : max a a = a := by + grind + ``` + Possible future improvements: + - When `diagnostics` is true, try with `withDefault` and report issue if it succeeds. + - (minor) Only use `withReducibleAndInstances` if the argument is an implicit instance. + Potential issue: some user write `{_ : Class α}` when the instance can be inferred from + explicit arguments. + 2) Remark: + If `pArg` contains universe metavariables, we use `withoutModifyingMCtx` to ensure the metavariables + are not assigned. These universe metavariables are created at `internalizePattern` for universe polymorphic + ground patterns. They are not common, but they occur in practice. + -/ + if pArg.hasLevelMVar then + withoutModifyingMCtx <| withReducibleAndInstances <| isDefEq pArg eArg + else + isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg) + /-- Matches a pattern argument. See `matchArgs?`. -/ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM Choice := do if isPatternDontCare pArg then @@ -138,23 +165,7 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C else if pArg.isBVar then assign? c pArg.bvarIdx! eArg else if let some pArg := groundPattern? pArg then - /- - We need to use `withReducibleAndInstances` because ground patterns are often instances. - Here is an example - ``` - instance : Max Nat where - max := Nat.max -- Redefined the instance - - example (a : Nat) : max a a = a := by - grind - ``` - Possible future improvements: - - When `diagnostics` is true, try with `withDefault` and report issue if it succeeds. - - (minor) Only use `withReducibleAndInstances` if the argument is an implicit instance. - Potential issue: some user write `{_ : Class α}` when the instance can be inferred from - explicit arguments. - -/ - guard (← isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg)) + guard (← matchGroundPattern pArg eArg) return c else if let some (pArg, k) := isOffsetPattern? pArg then assert! Option.isNone <| isOffsetPattern? pArg @@ -165,7 +176,7 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C let c ← assign? c pArg.bvarIdx! eArg genInfo.assign? c eArg else if let some pArg := groundPattern? pArg then - guard (← isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg)) + guard (← matchGroundPattern pArg eArg) genInfo.assign? c eArg else if let some (pArg, k) := isOffsetPattern? pArg then return { c with cnstrs := .offset (some genInfo) pArg k eArg :: c.cnstrs } diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 3d51d79f5c..4dcc2f4bd5 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -12,6 +12,7 @@ public import Lean.Meta.LitValues public import Lean.Meta.Match.MatcherInfo public import Lean.Meta.Match.MatchEqsExt public import Lean.Meta.Match.MatchEqs +public import Lean.Util.CollectLevelParams public import Lean.Meta.Tactic.Grind.Types public import Lean.Meta.Tactic.Grind.Util public import Lean.Meta.Tactic.Grind.Canon @@ -151,7 +152,7 @@ private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit := mkENodeCore e (ctor := false) (interpreted := false) (generation := generation) /-- Internalizes the nested ground terms in the given pattern. -/ -private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do +private partial def internalizePattern (pattern : Expr) (generation : Nat) (origin : Origin) : GoalM Expr := do -- Recall that it is important to ensure patterns are maximally shared since -- we assume that in functions such as `getAppsOf` in `EMatch.lean` go (← shareCommon pattern) @@ -161,7 +162,21 @@ where return pattern else if let some e := groundPattern? pattern then let e ← preprocessLight e - internalize e generation none + let e ← if e.hasLevelParam && origin matches .decl _ then + /- + If `e` has universe parameters and it is **not** local. That is, + it contains the universe parameters of some global theorem. + Then, we convert `e`'s universe parameters into universe meta-variables. + Remark: it is pointless to internalize the result because it contains these helper meta-variables. + Remark: universe polymorphic ground patterns are not common, but they do occur in the + core library. + -/ + let ps := collectLevelParams {} e |>.params + let us ← ps.mapM fun _ => mkFreshLevelMVar + pure <| e.instantiateLevelParamsArray ps us + else + internalize e generation none + pure e return mkGroundPattern e else pattern.withApp fun f args => do return mkAppN f (← args.mapM go) @@ -203,7 +218,7 @@ def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do -- Recall that we use the proof as part of the key for a set of instances found so far. -- We don't want to use structural equality when comparing keys. let proof ← shareCommon thm.proof - let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) } + let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation thm.origin)) } trace_goal[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}" modify fun s => { s with ematch.newThms := s.ematch.newThms.push thm } diff --git a/tests/lean/run/grind_univ_poly_ground_pattern.lean b/tests/lean/run/grind_univ_poly_ground_pattern.lean new file mode 100644 index 0000000000..cddb01239b --- /dev/null +++ b/tests/lean/run/grind_univ_poly_ground_pattern.lean @@ -0,0 +1,3 @@ +/-! Test for E-matching patterns containing nested universe polymorphic ground patterns. -/ +example : Id.run (pure true) = true := by + grind only [Id.run_pure]