From 4c0765fc071b1b6bf6fd46ce4f67f4fda9690b4e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 21 Dec 2025 18:59:52 +0100 Subject: [PATCH] fix: grind using congr equation of private imported matcher (#11756) This PR fixes an issue where `grind` fails when trying to unfold a definition by pattern matching imported by `import all` (or from a non-`module`). Fixes #11715 --------- Co-authored-by: Sebastian Ullrich --- src/Lean/Meta/Match/MatchEqs.lean | 54 ++++++++++++------------ tests/lean/run/issue11211.lean | 2 +- tests/pkg/module/Module/Basic.lean | 10 +++++ tests/pkg/module/Module/ImportedAll.lean | 8 +++- 4 files changed, 46 insertions(+), 28 deletions(-) diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 9c7b17fd12..5a1a9f4b12 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -245,17 +245,6 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no let result := { eqnNames, splitterName, splitterMatchInfo } registerMatchEqns matchDeclName result -/- We generate the equations and splitter on demand, and do not save them on .olean files. -/ -builtin_initialize matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name)) ← - -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`. - -- The resulting state can still be accessed on the generated declarations using `.asyncEnv`; - -- see below - registerEnvExtension (pure {}) (asyncMode := .local) - -def registerMatchCongrEqns (matchDeclName : Name) (eqnNames : Array Name) : CoreM Unit := do - modifyEnv fun env => matchCongrEqnsExt.modifyState env fun map => - map.insert matchDeclName eqnNames - /-- Generate the congruence equations for the given match auxiliary declaration. The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants), @@ -269,11 +258,14 @@ not always needed, so for now we live with the code duplication. -/ @[export lean_get_congr_match_equations_for] def genMatchCongrEqnsImpl (matchDeclName : Name) : MetaM (Array Name) := do - let baseName := mkPrivateName (← getEnv) matchDeclName - let firstEqnName := .str baseName congrEqn1ThmSuffix - realizeConst matchDeclName firstEqnName (go baseName) - return matchCongrEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := firstEqnName) (← getEnv) |>.find! matchDeclName -where go baseName := withConfig (fun c => { c with etaStruct := .none }) do + let firstEqnName := matchDeclName.str congrEqn1ThmSuffix + realizeConst matchDeclName firstEqnName go + let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function" + let mut thmNames := #[] + for i in *...matchInfo.numAlts do + thmNames := thmNames.push <|(matchDeclName.str congrEqnThmSuffixBase).appendIndexAfter (i+1) + return thmNames +where go := withConfig (fun c => { c with etaStruct := .none }) do withConfig (fun c => { c with etaStruct := .none }) do let constInfo ← getConstInfo matchDeclName let us := constInfo.levelParams.map mkLevelParam @@ -290,7 +282,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do let mut idx := 1 for i in *...alts.size do let altInfo := matchInfo.altInfos[i]! - let thmName := (Name.str baseName congrEqnThmSuffixBase).appendIndexAfter idx + let thmName := (Name.str matchDeclName congrEqnThmSuffixBase).appendIndexAfter idx eqnNames := eqnNames.push thmName let notAlt ← do let alt := alts[i]! @@ -333,26 +325,36 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do return notAlt notAlts := notAlts.push notAlt idx := idx + 1 - registerMatchCongrEqns matchDeclName eqnNames builtin_initialize registerTraceClass `Meta.Match.matchEqs -private def isMatchEqName? (env : Environment) (n : Name) : Option (Name × Bool) := do +private def isMatchEqName? (env : Environment) (n : Name) : Option Name := do let .str p s := n | failure - guard <| isEqnReservedNameSuffix s || s == "splitter" || isCongrEqnReservedNameSuffix s + guard <| isEqnReservedNameSuffix s || s == "splitter" let p ← privateToUserName? p guard <| isMatcherCore env p - return (p, isCongrEqnReservedNameSuffix s) + return p builtin_initialize registerReservedNamePredicate (isMatchEqName? · · |>.isSome) builtin_initialize registerReservedNameAction fun name => do - let some (p, isGenEq) := isMatchEqName? (← getEnv) name | + let some p := isMatchEqName? (← getEnv) name | return false - if isGenEq then - let _ ← MetaM.run' <| genMatchCongrEqnsImpl p - else - let _ ← MetaM.run' <| getEquationsFor p + let _ ← MetaM.run' <| getEquationsForImpl p + return true + +private def isMatchCongrEqName? (env : Environment) (n : Name) : Option Name := do + let .str p s := n | failure + guard <| isCongrEqnReservedNameSuffix s + guard <| isMatcherCore env p + return p + +builtin_initialize registerReservedNamePredicate (isMatchCongrEqName? · · |>.isSome) + +builtin_initialize registerReservedNameAction fun name => do + let some p := isMatchCongrEqName? (← getEnv) name | + return false + let _ ← MetaM.run' <| genMatchCongrEqnsImpl p return true end Lean.Meta.Match diff --git a/tests/lean/run/issue11211.lean b/tests/lean/run/issue11211.lean index 885bbf4c19..6ede36b781 100644 --- a/tests/lean/run/issue11211.lean +++ b/tests/lean/run/issue11211.lean @@ -28,7 +28,7 @@ info: private def f.match_1.splitter.{u_1} : (motive : List Nat → Sort u_1) /-- -info: private theorem f.match_1.congr_eq_1.{u_1} : ∀ (motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : Unit → motive []) +info: theorem f.match_1.congr_eq_1.{u_1} : ∀ (motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : Unit → motive []) (h_2 : (x : List Nat) → motive x), xs = [] → (match xs with diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 856edfdcf4..75738d0557 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -544,3 +544,13 @@ Eq.refl five -/ #guard_msgs in #print instA._proof_1 + +/-- Setup for #11715. -/ + +public structure OpOperand2 where + nextUse : Option Nat + +public def func (ctx : Nat) (operand : OpOperand2) : Nat := + match operand.nextUse with + | none => ctx + | some nextPtr => ctx diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index 8de160d484..6bc963e9ed 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -2,7 +2,7 @@ module public import Module.Basic import all Module.Basic -import Lean.CoreM +import Lean /-! `import all` should import private information, privately. -/ @@ -160,3 +160,9 @@ error: Invalid `⟨...⟩` notation: Constructor for `StructWithPrivateField` is #guard_msgs in #with_exporting #check (⟨1⟩ : StructWithPrivateField) + +/-! #11715: `grind` should not fail to apply private matcher from imported module. -/ + +attribute [local grind] func in +theorem stmt1 : func ctx op = ctx := by + grind