From fd091d1dfe03b821ac2888921dfe7d13b6096b4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2025 20:35:52 +0100 Subject: [PATCH] feat: pattern normalization in the `grind` tactic (#6538) This PR ensures patterns provided by users are normalized. See new test to understand why this is needed. --- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 10 ++++-- src/Lean/Meta/Tactic/Grind/Internalize.lean | 3 +- src/Lean/Meta/Tactic/Grind/Main.lean | 16 ++-------- src/Lean/Meta/Tactic/Grind/SimpUtil.lean | 32 +++++++++++++++++++ src/Lean/Meta/Tactic/Grind/Util.lean | 7 ++++ tests/lean/run/grind_ematch2.lean | 27 ++++++++++++++++ 6 files changed, 78 insertions(+), 17 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Grind/SimpUtil.lean diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index fd175a908c7b..01be831b1f53 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -37,9 +37,10 @@ def isOffsetPattern? (pat : Expr) : Option (Expr × Nat) := Id.run do let .lit (.natVal k) := k | none return some (pat, k) -def preprocessPattern (pat : Expr) : MetaM Expr := do +def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do let pat ← instantiateMVars pat let pat ← unfoldReducible pat + let pat ← if normalizePattern then normalize pat else pure pat let pat ← detectOffsets pat let pat ← foldProjs pat return pat @@ -424,12 +425,15 @@ def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : /-- Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`, creates an E-matching pattern for it using `addEMatchTheorem n [lhs]` + +If `normalizePattern` is true, it applies the `grind` simplification theorems and simprocs to the +pattern. -/ -def mkEMatchEqTheorem (declName : Name) : MetaM EMatchTheorem := do +def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) : MetaM EMatchTheorem := do let info ← getConstInfo declName let (numParams, patterns) ← forallTelescopeReducing info.type fun xs type => do let_expr Eq _ lhs _ := type | throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}" - let lhs ← preprocessPattern lhs + let lhs ← preprocessPattern lhs normalizePattern return (xs.size, [lhs.abstract xs]) mkEMatchTheorem declName numParams patterns diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 63c2fc81ccae..b0b93b6755e7 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -71,7 +71,8 @@ private partial def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := d if (← get).matchEqNames.contains declName then return () modify fun s => { s with matchEqNames := s.matchEqNames.insert declName } for eqn in (← Match.getEquationsFor declName).eqnNames do - activateTheorem (← mkEMatchEqTheorem eqn) generation + -- We disable pattern normalization to prevent the `match`-expression to be reduced. + activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do if let some (thms, thmMap) := (← get).thmMap.retrieve? fName then diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 8ee85469bdc3..480301d5bb52 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Main.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura prelude import Init.Grind.Lemmas import Lean.Meta.Tactic.Util -import Lean.Meta.Tactic.Simp.Simproc import Lean.Meta.Tactic.Grind.RevertAll import Lean.Meta.Tactic.Grind.PropagatorAttr import Lean.Meta.Tactic.Grind.Proj @@ -15,7 +14,7 @@ import Lean.Meta.Tactic.Grind.Util import Lean.Meta.Tactic.Grind.Inv import Lean.Meta.Tactic.Grind.Intro import Lean.Meta.Tactic.Grind.EMatch -import Lean.Meta.Tactic.Grind.DoNotSimp +import Lean.Meta.Tactic.Grind.SimpUtil namespace Lean.Meta.Grind @@ -35,21 +34,12 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do prop e } -private def getGrindSimprocs : MetaM Simprocs := do - let s ← grindNormSimprocExt.getSimprocs - let s ← addDoNotSimp s - return s - def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) (fallback : Fallback) : MetaM α := do let scState := ShareCommon.State.mk _ let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False) let (trueExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``True) - let thms ← grindNormExt.getTheorems - let simprocs := #[(← getGrindSimprocs), (← Simp.getSEvalSimprocs)] - let simp ← Simp.mkContext - (config := { arith := true }) - (simpTheorems := #[thms]) - (congrTheorems := (← getSimpCongrTheorems)) + let simprocs ← Grind.getSimprocs + let simp ← Grind.getSimpContext x (← mkMethods fallback).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr } private def mkGoal (mvarId : MVarId) : GrindM Goal := do diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean new file mode 100644 index 000000000000..878b0fc59356 --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Meta.Tactic.Simp.Simproc +import Lean.Meta.Tactic.Grind.Simp +import Lean.Meta.Tactic.Grind.DoNotSimp + +namespace Lean.Meta.Grind + +/-- Returns the array of simprocs used by `grind`. -/ +protected def getSimprocs : MetaM (Array Simprocs) := do + let s ← grindNormSimprocExt.getSimprocs + let s ← addDoNotSimp s + return #[s, (← Simp.getSEvalSimprocs)] + +/-- Returns the simplification context used by `grind`. -/ +protected def getSimpContext : MetaM Simp.Context := do + let thms ← grindNormExt.getTheorems + Simp.mkContext + (config := { arith := true }) + (simpTheorems := #[thms]) + (congrTheorems := (← getSimpCongrTheorems)) + +@[export lean_grind_normalize] +def normalizeImp (e : Expr) : MetaM Expr := do + let (r, _) ← Meta.simp e (← Grind.getSimpContext) (← Grind.getSimprocs) + return r.expr + +end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean index 0805b4dd7fb8..4fdb42055d1b 100644 --- a/src/Lean/Meta/Tactic/Grind/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Util.lean @@ -140,4 +140,11 @@ def normalizeLevels (e : Expr) : CoreM Expr := do | _ => return .continue Core.transform e (pre := pre) +/-- +Normalizes the given expression using the `grind` simplification theorems and simprocs. +This function is used for normalzing E-matching patterns. Note that it does not return a proof. +-/ +@[extern "lean_grind_normalize"] -- forward definition +opaque normalize (e : Expr) : MetaM Expr + end Lean.Meta.Grind diff --git a/tests/lean/run/grind_ematch2.lean b/tests/lean/run/grind_ematch2.lean index 613972c80e11..62a4ba2161f1 100644 --- a/tests/lean/run/grind_ematch2.lean +++ b/tests/lean/run/grind_ematch2.lean @@ -66,3 +66,30 @@ info: [grind.ematch.instance] fx: f a (f a a) = a #guard_msgs (info) in example : a = b₁ → c = f b₁ b₂ → f a c ≠ a → a = b₂ → False := by grind + + +namespace pattern_normalization +opaque g : Nat → Nat +@[grind_norm] theorem gthm : g x = x := sorry +opaque f : Nat → Nat → Nat +theorem fthm : f (g x) x = x := sorry +-- The following pattern should be normalized by `grind`. Otherwise, we will not find any instance during E-matching. +/-- +info: [grind.ematch.pattern] fthm: [f #0 #0] +-/ +#guard_msgs (info) in +grind_pattern fthm => f (g x) x + +/-- +info: [grind.assert] f x y = b +[grind.assert] y = x +[grind.assert] ¬b = x +[grind.ematch.instance] fthm: f (g y) y = y +[grind.assert] f y y = y +-/ +#guard_msgs (info) in +set_option trace.grind.assert true in +example : f (g x) y = b → y = x → b = x := by + grind + +end pattern_normalization