From c811617e71a1fa980830af00dfc92e49b53f5dc8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2024 07:56:17 -0800 Subject: [PATCH] fix: internalize nested ground patterns when activating ematch theorems This PR internalize nested ground patterns when activating ematch theorems in the (WIP) `grind` tactic. --- src/Lean/Meta/Tactic/Grind.lean | 1 + src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 11 +++--- src/Lean/Meta/Tactic/Grind/Internalize.lean | 20 +++++++++-- tests/lean/run/grind_pattern2.lean | 34 +++++++++++++++++++ 4 files changed, 60 insertions(+), 6 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index fb945ab507d4..91c6bf637869 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -37,5 +37,6 @@ builtin_initialize registerTraceClass `grind.congr builtin_initialize registerTraceClass `grind.proof builtin_initialize registerTraceClass `grind.proof.detail builtin_initialize registerTraceClass `grind.pattern +builtin_initialize registerTraceClass `grind.internalize end Lean diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 968293d2cd5f..907883cb86c2 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -67,22 +67,25 @@ private def isForbidden (declName : Name) := forbiddenDeclNames.contains declNam private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]") -private def mkGroundPattern (e : Expr) : Expr := +def mkGroundPattern (e : Expr) : Expr := mkAnnotation `grind.ground_pat e -private def groundPattern? (e : Expr) : Option Expr := +def groundPattern? (e : Expr) : Option Expr := annotation? `grind.ground_pat e private def isGroundPattern (e : Expr) : Bool := groundPattern? e |>.isSome +def isPatternDontCare (e : Expr) : Bool := + e == dontCare + private def isAtomicPattern (e : Expr) : Bool := - e.isBVar || e == dontCare || isGroundPattern e + e.isBVar || isPatternDontCare e || isGroundPattern e partial def ppPattern (pattern : Expr) : MessageData := Id.run do if let some e := groundPattern? pattern then return m!"`[{e}]" - else if pattern == dontCare then + else if isPatternDontCare pattern then return m!"?" else match pattern with | .bvar idx => return m!"#{idx}" diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 42a48cc7f364..99c35a8b92ee 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -7,6 +7,7 @@ prelude import Init.Grind.Util import Lean.Meta.LitValues import Lean.Meta.Tactic.Grind.Types +import Lean.Meta.Tactic.Grind.Util namespace Lean.Meta.Grind @@ -37,7 +38,19 @@ private def updateAppMap (e : Expr) : GoalM Unit := do s.appMap.insert key [e] } -private def activateTheoremPatterns (fName : Name) : GoalM Unit := do +mutual +/-- Internalizes the nested ground terms in the given pattern. -/ +private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do + if pattern.isBVar || isPatternDontCare pattern then + return pattern + else if let some e := groundPattern? pattern then + let e ← shareCommon (← canon (← normalizeLevels (← unfoldReducible e))) + internalize e generation + return mkGroundPattern e + else pattern.withApp fun f args => do + return mkAppN f (← args.mapM (internalizePattern · generation)) + +private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : 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 @@ -47,6 +60,7 @@ private def activateTheoremPatterns (fName : Name) : GoalM Unit := do match symbols with | [] => trace[grind.pattern] "activated `{thm.origin.key}`" + let thm := { thm with patterns := (← thm.patterns.mapM (internalizePattern · generation)) } modify fun s => { s with newThms := s.newThms.push thm } | _ => trace[grind.pattern] "reinsert `{thm.origin.key}`" @@ -54,6 +68,7 @@ private def activateTheoremPatterns (fName : Name) : GoalM Unit := do partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do if (← alreadyInternalized e) then return () + trace[grind.internalize] "{e}" match e with | .bvar .. => unreachable! | .sort .. => return () @@ -79,7 +94,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do registerParent e c else if let .const fName _ := f then - activateTheoremPatterns fName + activateTheoremPatterns fName generation else internalize f generation registerParent e f @@ -91,5 +106,6 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do addCongrTable e updateAppMap e propagateUp e +end end Lean.Meta.Grind diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean index 4b091799de3f..f8e696a136ee 100644 --- a/tests/lean/run/grind_pattern2.lean +++ b/tests/lean/run/grind_pattern2.lean @@ -37,3 +37,37 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by fail_if_success grind sorry + +def a := 10 +def b := 20 +def foo (x : List Nat) (y : List Nat) := x ++ y ++ x + +theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl + +/-- +info: [grind.pattern] fooThm: [foo #0 `[[a, b]]] +-/ +#guard_msgs in +grind_pattern fooThm => foo x [a, b] + + +/-- +warning: declaration uses 'sorry' +--- +info: [grind.internalize] foo x y +[grind.pattern] activated `fooThm` +[grind.internalize] [a, b] +[grind.internalize] Nat +[grind.internalize] a +[grind.internalize] [b] +[grind.internalize] b +[grind.internalize] [] +[grind.internalize] x +[grind.internalize] y +[grind.internalize] z +-/ +#guard_msgs in +set_option trace.grind.internalize true in +example : foo x y = z → False := by + fail_if_success grind + sorry