feat: multiple grind propagators per declaration

This PR allows users to declare additional `grind` constraint propagators for
declarations that already include propagators in core.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -53,18 +53,18 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
   return {
     fallback
     propagateUp := fun e => do
-     propagateForallPropUp e
-     propagateReflCmp e
-     let .const declName _ := e.getAppFn | return ()
-     propagateProjEq e
-     if let some prop := builtinPropagators.up[declName]? then
-       prop e
+      propagateForallPropUp e
+      propagateReflCmp e
+      let .const declName _ := e.getAppFn | return ()
+      propagateProjEq e
+      if let some props := builtinPropagators.up[declName]? then
+       props.forM fun prop => prop e
     propagateDown := fun e => do
-     propagateForallPropDown e
-     propagateLawfulEqCmp e
-     let .const declName _ := e.getAppFn | return ()
-     if let some prop := builtinPropagators.down[declName]? then
-       prop e
+      propagateForallPropDown e
+      propagateLawfulEqCmp e
+      let .const declName _ := e.getAppFn | return ()
+      if let some props := builtinPropagators.down[declName]? then
+       props.forM fun prop => prop e
   }
 
 -- A `simp` discharger that does not use assumptions.

src/Lean/Meta/Tactic/Grind/PropagatorAttr.lean

@@ -11,10 +11,16 @@ import Init.Grind
 public section
 namespace Lean.Meta.Grind
 
+abbrev PropagatorMap := Std.HashMap Name (List Propagator)
+
+def PropagatorMap.insert (m : PropagatorMap) (declName : Name) (p : Propagator) : PropagatorMap :=
+  let ps := m[declName]? |>.getD []
+  Std.HashMap.insert m declName (p :: ps)
+
 /-- Builtin propagators. -/
 structure BuiltinPropagators where
-  up   : Std.HashMap Name Propagator := {}
-  down : Std.HashMap Name Propagator := {}
+  up   : PropagatorMap := {}
+  down : PropagatorMap := {}
   deriving Inhabited
 
 builtin_initialize builtinPropagatorsRef : IO.Ref BuiltinPropagators ← IO.mkRef {}
@@ -23,12 +29,8 @@ private def registerBuiltinPropagatorCore (declName : Name) (up : Bool) (proc :
   unless (← initializing) do
     throw (IO.userError s!"invalid builtin `grind` propagator declaration, it can only be registered during initialization")
   if up then
-    if (← builtinPropagatorsRef.get).up.contains declName then
-      throw (IO.userError s!"invalid builtin `grind` upward propagator `{declName}`, it has already been declared")
     builtinPropagatorsRef.modify fun { up, down } => { up := up.insert declName proc, down }
   else
-    if (← builtinPropagatorsRef.get).down.contains declName then
-      throw (IO.userError s!"invalid builtin `grind` downward propagator `{declName}`, it has already been declared")
     builtinPropagatorsRef.modify fun { up, down } => { up, down := down.insert declName proc }
 
 def registerBuiltinUpwardPropagator (declName : Name) (proc : Propagator) : IO Unit :=