From 1f3919f08a3c18b796cc1674652fdc081e6188ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2024 00:43:06 -0800 Subject: [PATCH 1/3] chore: add assertion A global theorem should not have free variables in `symbols`. --- src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean index 82833aad3671..4b605d38bef5 100644 --- a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean +++ b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean @@ -288,6 +288,7 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) let us := info.levelParams.map mkLevelParam let proof := mkConst declName us let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns + assert! symbols.all fun s => s matches .const _ trace[grind.pattern] "{declName}: {patterns.map ppPattern}" if let .missing pos ← checkCoverage proof numParams bvarFound then let pats : MessageData := m!"{patterns.map ppPattern}" From c6c49383ce149c07864b8306c54b8274b5f5bfd3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2024 01:23:36 -0800 Subject: [PATCH 2/3] feat: ematch theorem activation --- src/Lean/Meta/Tactic/Grind/Internalize.lean | 19 ++++++++- src/Lean/Meta/Tactic/Grind/Run.lean | 3 +- .../Meta/Tactic/Grind/TheoremPatterns.lean | 30 ++++++++++---- src/Lean/Meta/Tactic/Grind/Types.lean | 10 +++++ tests/lean/run/grind_pattern2.lean | 39 +++++++++++++++++++ 5 files changed, 92 insertions(+), 9 deletions(-) create mode 100644 tests/lean/run/grind_pattern2.lean diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 32d1de928af2..eb3d30e2b32b 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -37,6 +37,21 @@ private def updateAppMap (e : Expr) : GoalM Unit := do s.appMap.insert key [e] } +private def activateTheoremPatterns (fName : Name) : GoalM Unit := do + if let some thms := (← get).thmMap.find? fName then + modify fun s => { s with thmMap := s.thmMap.erase fName } + let appMap := (← get).appMap + for thm in thms do + let symbols := thm.symbols.filter fun sym => !appMap.contains sym + let thm := { thm with symbols } + match symbols with + | [] => + trace[grind.pattern] "activated `{thm.origin.key}`" + modify fun s => { s with newThms := s.newThms.push thm } + | _ => + trace[grind.pattern] "reinsert `{thm.origin.key}`" + modify fun s => { s with thmMap := s.thmMap.insertTheorem thm } + partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do if (← alreadyInternalized e) then return () match e with @@ -63,7 +78,9 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do internalize c generation registerParent e c else - unless f.isConst do + if let .const fName _ := f then + activateTheoremPatterns fName + else internalize f generation registerParent e f for h : i in [: args.size] do diff --git a/src/Lean/Meta/Tactic/Grind/Run.lean b/src/Lean/Meta/Tactic/Grind/Run.lean index f2b534b4557e..9395b9d64d1f 100644 --- a/src/Lean/Meta/Tactic/Grind/Run.lean +++ b/src/Lean/Meta/Tactic/Grind/Run.lean @@ -46,7 +46,8 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do def mkGoal (mvarId : MVarId) : GrindM Goal := do let trueExpr ← getTrueExpr let falseExpr ← getFalseExpr - GoalM.run' { mvarId } do + let thmMap ← getTheoremPatterns + GoalM.run' { mvarId, thmMap } do mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0) mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0) diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean index 4b605d38bef5..5e20188461f2 100644 --- a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean +++ b/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean @@ -25,6 +25,14 @@ inductive Origin where | other deriving Inhabited, Repr +/-- A unique identifier corresponding to the origin. -/ +def Origin.key : Origin → Name + | .decl declName => declName + | .fvar fvarId => fvarId.name + | .stx id _ => id + | .other => `other + +-- TODO: find better name structure TheoremPattern where proof : Expr numParams : Nat @@ -34,16 +42,21 @@ structure TheoremPattern where origin : Origin deriving Inhabited -abbrev TheoremPatterns := SMap Name (List TheoremPattern) +-- TODO: find better name +abbrev TheoremPatterns := PHashMap Name (List TheoremPattern) + +def TheoremPatterns.insertTheorem (s : TheoremPatterns) (thm : TheoremPattern) : TheoremPatterns := Id.run do + let .const declName :: syms := thm.symbols + | unreachable! + let thm := { thm with symbols := syms } + if let some thms := s.find? declName then + return s.insert declName (thm::thms) + else + return s.insert declName [thm] builtin_initialize theoremPatternsExt : SimpleScopedEnvExtension TheoremPattern TheoremPatterns ← registerSimpleScopedEnvExtension { - addEntry := fun s t => Id.run do - let .const declName :: _ := t.symbols | unreachable! - if let some ts := s.find? declName then - s.insert declName (t::ts) - else - s.insert declName [t] + addEntry := TheoremPatterns.insertTheorem initial := .empty } @@ -298,4 +311,7 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) origin := .decl declName } +def getTheoremPatterns : CoreM TheoremPatterns := + return theoremPatternsExt.getState (← getEnv) + end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index edc96c5db537..0374264e91c5 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Simp.Types import Lean.Meta.Tactic.Util import Lean.Meta.Tactic.Grind.Canon import Lean.Meta.Tactic.Grind.Attr +import Lean.Meta.Tactic.Grind.TheoremPatterns namespace Lean.Meta.Grind @@ -273,6 +274,15 @@ structure Goal where gmt : Nat := 0 /-- Next unique index for creating ENodes -/ nextIdx : Nat := 0 + /-- Active theorems that we have performed ematching at least once. -/ + thms : PArray TheoremPattern := {} + /-- Active theorems that we have not performed any round of ematching yet. -/ + newThms : PArray TheoremPattern := {} + /-- + Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. + Local theorem provided by users are added directly into `newThms`. + -/ + thmMap : TheoremPatterns deriving Inhabited def Goal.admit (goal : Goal) : MetaM Unit := diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean new file mode 100644 index 000000000000..4b091799de3f --- /dev/null +++ b/tests/lean/run/grind_pattern2.lean @@ -0,0 +1,39 @@ +def Set (α : Type) := α → Bool + +def insertElem [DecidableEq α] (s : Set α) (a : α) : Set α := + fun x => a = x || s x + +def contains (s : Set α) (a : α) : Bool := + s a + +theorem contains_insert [DecidableEq α] (s : Set α) (a : α) : contains (insertElem s a) a := by + simp [contains, insertElem] + +grind_pattern contains_insert => contains (insertElem s a) a + +-- TheoremPattern activation test + +set_option trace.grind.pattern true + +/-- +warning: declaration uses 'sorry' +--- +info: [grind.pattern] activated `contains_insert` +-/ +#guard_msgs in +example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : + s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by + fail_if_success grind + sorry + +/-- +warning: declaration uses 'sorry' +--- +info: [grind.pattern] reinsert `contains_insert` +[grind.pattern] activated `contains_insert` +-/ +#guard_msgs in +example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : + ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by + fail_if_success grind + sorry From d2df7e1dd9293efe62a7b5c158b6820ecbe545b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2024 01:39:39 -0800 Subject: [PATCH 3/3] refactor: rename `TheoremPattern` to `EMatchTheorem` --- src/Lean/Elab/Tactic/Grind.lean | 2 +- src/Lean/Meta/Tactic/Grind.lean | 2 +- ...heoremPatterns.lean => EMatchTheorem.lean} | 26 +++++++++---------- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/Tactic/Grind/Run.lean | 2 +- src/Lean/Meta/Tactic/Grind/Types.lean | 8 +++--- 6 files changed, 21 insertions(+), 21 deletions(-) rename src/Lean/Meta/Tactic/Grind/{TheoremPatterns.lean => EMatchTheorem.lean} (93%) diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 2ceef07fc832..293e06197eed 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -26,7 +26,7 @@ def elabGrindPattern : CommandElab := fun stx => do let pattern ← instantiateMVars (← elabTerm term none) let pattern ← Grind.unfoldReducible pattern return pattern.abstract xs - Grind.addTheoremPattern declName xs.size patterns.toList + Grind.addEMatchTheorem declName xs.size patterns.toList | _ => throwUnsupportedSyntax def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 4013ab8d4b37..fb945ab507d4 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -21,7 +21,7 @@ import Lean.Meta.Tactic.Grind.PP import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Ctor import Lean.Meta.Tactic.Grind.Parser -import Lean.Meta.Tactic.Grind.TheoremPatterns +import Lean.Meta.Tactic.Grind.EMatchTheorem namespace Lean diff --git a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean similarity index 93% rename from src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean rename to src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 5e20188461f2..968293d2cd5f 100644 --- a/src/Lean/Meta/Tactic/Grind/TheoremPatterns.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -32,8 +32,8 @@ def Origin.key : Origin → Name | .stx id _ => id | .other => `other --- TODO: find better name -structure TheoremPattern where +/-- A theorem for heuristic instantiation based on E-matching. -/ +structure EMatchTheorem where proof : Expr numParams : Nat patterns : List Expr @@ -42,21 +42,21 @@ structure TheoremPattern where origin : Origin deriving Inhabited --- TODO: find better name -abbrev TheoremPatterns := PHashMap Name (List TheoremPattern) +/-- The key is a symbol from `EMatchTheorem.symbols`. -/ +abbrev EMatchTheorems := PHashMap Name (List EMatchTheorem) -def TheoremPatterns.insertTheorem (s : TheoremPatterns) (thm : TheoremPattern) : TheoremPatterns := Id.run do +def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems := Id.run do let .const declName :: syms := thm.symbols | unreachable! let thm := { thm with symbols := syms } if let some thms := s.find? declName then - return s.insert declName (thm::thms) + return PersistentHashMap.insert s declName (thm::thms) else - return s.insert declName [thm] + return PersistentHashMap.insert s declName [thm] -builtin_initialize theoremPatternsExt : SimpleScopedEnvExtension TheoremPattern TheoremPatterns ← +private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTheorem EMatchTheorems ← registerSimpleScopedEnvExtension { - addEntry := TheoremPatterns.insertTheorem + addEntry := EMatchTheorems.insert initial := .empty } @@ -295,7 +295,7 @@ private def ppParamsAt (proof : Expr) (numParms : Nat) (paramPos : List Nat) : M msg := msg ++ m!"{x} : {← inferType x}" addMessageContextFull msg -def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do +def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do let .thmInfo info ← getConstInfo declName | throwError "`{declName}` is not a theorem, you cannot assign patterns to non-theorems for the `grind` tactic" let us := info.levelParams.map mkLevelParam @@ -306,12 +306,12 @@ def addTheoremPattern (declName : Name) (numParams : Nat) (patterns : List Expr) if let .missing pos ← checkCoverage proof numParams bvarFound then let pats : MessageData := m!"{patterns.map ppPattern}" throwError "invalid pattern(s) for `{declName}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}" - theoremPatternsExt.add { + ematchTheoremsExt.add { proof, patterns, numParams, symbols origin := .decl declName } -def getTheoremPatterns : CoreM TheoremPatterns := - return theoremPatternsExt.getState (← getEnv) +def getEMatchTheorems : CoreM EMatchTheorems := + return ematchTheoremsExt.getState (← getEnv) end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index eb3d30e2b32b..42a48cc7f364 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -50,7 +50,7 @@ private def activateTheoremPatterns (fName : Name) : GoalM Unit := do modify fun s => { s with newThms := s.newThms.push thm } | _ => trace[grind.pattern] "reinsert `{thm.origin.key}`" - modify fun s => { s with thmMap := s.thmMap.insertTheorem thm } + modify fun s => { s with thmMap := s.thmMap.insert thm } partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do if (← alreadyInternalized e) then return () diff --git a/src/Lean/Meta/Tactic/Grind/Run.lean b/src/Lean/Meta/Tactic/Grind/Run.lean index 9395b9d64d1f..e36c3437d813 100644 --- a/src/Lean/Meta/Tactic/Grind/Run.lean +++ b/src/Lean/Meta/Tactic/Grind/Run.lean @@ -46,7 +46,7 @@ def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α := do def mkGoal (mvarId : MVarId) : GrindM Goal := do let trueExpr ← getTrueExpr let falseExpr ← getFalseExpr - let thmMap ← getTheoremPatterns + let thmMap ← getEMatchTheorems GoalM.run' { mvarId, thmMap } do mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0) mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 0374264e91c5..0342646871a3 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -13,7 +13,7 @@ import Lean.Meta.Tactic.Simp.Types import Lean.Meta.Tactic.Util import Lean.Meta.Tactic.Grind.Canon import Lean.Meta.Tactic.Grind.Attr -import Lean.Meta.Tactic.Grind.TheoremPatterns +import Lean.Meta.Tactic.Grind.EMatchTheorem namespace Lean.Meta.Grind @@ -275,14 +275,14 @@ structure Goal where /-- Next unique index for creating ENodes -/ nextIdx : Nat := 0 /-- Active theorems that we have performed ematching at least once. -/ - thms : PArray TheoremPattern := {} + thms : PArray EMatchTheorem := {} /-- Active theorems that we have not performed any round of ematching yet. -/ - newThms : PArray TheoremPattern := {} + newThms : PArray EMatchTheorem := {} /-- Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into `newThms`. -/ - thmMap : TheoremPatterns + thmMap : EMatchTheorems deriving Inhabited def Goal.admit (goal : Goal) : MetaM Unit :=