chore: remove [grind_norm] attribute (#6692)

This PR removes the `[grind_norm]` attribute. The normalization theorems
used by `grind` are now fixed and cannot be modified by users. We use
normalization theorems to ensure the built-in procedures receive term
wish expected "shapes". We use it for types that have built-in support
in grind. Users could misuse this feature as a simplification rule. For
example, consider the following example:

```lean
def replicate : (n : Nat) → (a : α) → List α
  | 0,   _ => []
  | n+1, a => a :: replicate n a

-- I want `grind` to instantiate the equations theorems for me.
attribute [grind] replicate

-- I want it to use the equation theorems as simplication rules too.
attribute [grind_norm] replicate

/--
info: [grind.assert] n = 0
[grind.assert] ¬replicate n xs = []
[grind.ematch.instance] replicate.eq_1: replicate 0 xs = []
[grind.assert] True
-/
set_option trace.grind.ematch.instance true in
set_option trace.grind.assert true in
example (xs : List α) : n = 0 → replicate n xs = [] := by
  grind -- fails :(
```

In this example, `grind` starts by asserting the two propositions as
expected: `n = 0`, and `¬replicate n xs = []`. The normalizer cannot
reduce `replicate n xs` as expected.
Then, the E-matching module finds the instance `replicate 0 xs = []` for
the equation theorem `replicate.eq_1` also as expected. But, then the
normalizer kicks in and reduces the new instance to `True`. By removing
`[grind_norm]` we elimninate this kind of misuse. Users that want to
preprocess a formula before invoking `grind` should use `simp` instead.

src/Init/Grind/Norm.lean

@@ -12,116 +12,105 @@ import Init.ByCases
 namespace Lean.Grind
 /-!
 Normalization theorems for the `grind` tactic.
-
-We are also going to use simproc's in the future.
 -/
 
--- Not
-attribute [grind_norm] Classical.not_not
-
--- Ne
-attribute [grind_norm] ne_eq
-
--- Iff
-@[grind_norm] theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
+theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
--- Eq
-attribute [grind_norm] eq_self heq_eq_eq
-
--- Prop equality
-@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
-@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
-@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
+theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
+theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
+theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
--- True
-attribute [grind_norm] not_true
-
--- False
-attribute [grind_norm] not_false_eq_true
-
 -- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
 theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
-@[grind_norm] theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
-@[grind_norm] theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
-@[grind_norm] theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
-@[grind_norm] theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
-@[grind_norm] theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
+theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
+theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
+theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
+theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
+theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
 
--- And
-@[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
+theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
   by_cases p <;> by_cases q <;> simp [*]
-attribute [grind_norm] and_true true_and and_false false_and and_assoc
 
--- Or
-attribute [grind_norm↓] not_or
-attribute [grind_norm] or_true true_or or_false false_or or_assoc
-
--- ite
-attribute [grind_norm] ite_true ite_false
-@[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
+theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
   by_cases p <;> simp [*]
 
-@[grind_norm] theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
+theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
   by_cases p <;> simp
 
-@[grind_norm] theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
+theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
   by_cases p <;> simp
 
--- Forall
-@[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
-attribute [grind_norm] forall_and
+theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
 
--- Exists
-@[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
-attribute [grind_norm] exists_const exists_or exists_prop exists_and_left exists_and_right
+theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
 
--- Bool cond
-@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
+theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
   cases c <;> simp [*]
 
--- Bool or
-attribute [grind_norm]
-  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
-
--- Bool and
-attribute [grind_norm]
-  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
-
--- Bool not
-attribute [grind_norm]
-  Bool.not_not
-
--- beq
-attribute [grind_norm] beq_iff_eq
-
--- bne
-attribute [grind_norm] bne_iff_ne
-
--- Bool not eq true/false
-attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
-
--- decide
-attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
-
--- Nat LE
-attribute [grind_norm] Nat.le_zero_eq
-
--- Nat/Int LT
-@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
+theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
   simp [Nat.lt, LT.lt]
 
-@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
+theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
   simp [Int.lt, LT.lt]
 
--- GT GE
-attribute [grind_norm] GT.gt GE.ge
+theorem ge_eq [LE α] (a b : α) : (a ≥ b) = (b ≤ a) := rfl
+theorem gt_eq [LT α] (a b : α) : (a > b) = (b < a) := rfl
 
--- Succ
-attribute [grind_norm] Nat.succ_eq_add_one
+init_grind_norm
+  /- Pre theorems -/
+  not_and not_or not_ite not_forall not_exists
+  |
+  /- Post theorems -/
+  Classical.not_not
+  ne_eq iff_eq eq_self heq_eq_eq
+  -- Prop equality
+  eq_true_eq eq_false_eq not_eq_prop
+  -- True
+  not_true
+  -- False
+  not_false_eq_true
+  -- Implication
+  true_imp_eq false_imp_eq imp_true_eq imp_false_eq imp_self_eq
+  -- And
+  and_true true_and and_false false_and and_assoc
+  -- Or
+  or_true true_or or_false false_or or_assoc
+  -- ite
+  ite_true ite_false ite_true_false ite_false_true
+  -- Forall
+  forall_and
+  -- Exists
+  exists_const exists_or exists_prop exists_and_left exists_and_right
+  -- Bool cond
+  cond_eq_ite
+  -- Bool or
+  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
+  -- Bool and
+  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
+  -- Bool not
+  Bool.not_not
+  -- beq
+  beq_iff_eq
+  -- bne
+  bne_iff_ne
+  -- Bool not eq true/false
+  Bool.not_eq_true Bool.not_eq_false
+  -- decide
+  decide_eq_true_eq decide_not not_decide_eq_true
+  -- Nat LE
+  Nat.le_zero_eq
+  -- Nat/Int LT
+  Nat.lt_eq
+  -- Nat.succ
+  Nat.succ_eq_add_one
+  -- Int
+  Int.lt_eq
+  -- GT GE
+  ge_eq gt_eq
 
 end Lean.Grind

src/Init/Tactics.lean

@@ -1648,17 +1648,6 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
-/--
-Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
--/
-syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
-
-/--
-Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
--/
-syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
-
-
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
 

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

@@ -10,12 +10,6 @@ import Lean.Meta.Tactic.Simp.Simproc
 namespace Lean.Meta.Grind
 open Simp
 
-builtin_initialize grindNormExt : SimpExtension ←
-  registerSimpAttr `grind_norm "simplification/normalization theorems for `grind`"
-
-builtin_initialize grindNormSimprocExt : SimprocExtension ←
-  registerSimprocAttr `grind_norm_proc "simplification/normalization procedured for `grind`" none
-
 builtin_initialize grindCasesExt : SimpleScopedEnvExtension Name NameSet ←
   registerSimpleScopedEnvExtension {
     initial        := {}

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

@@ -24,8 +24,6 @@ def registerNormTheorems (preDeclNames : Array Name) (postDeclNames : Array Name
 
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
-  let s ← grindNormSimprocExt.getSimprocs
-  let s ← addDoNotSimp s
   let e ← Simp.getSEvalSimprocs
   /-
   We don't want to apply `List.reduceReplicate` as a normalization operation in
@@ -41,11 +39,12 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   We don't want it to be simplified to `[] = []`.
   -/
   let e := e.erase ``List.reduceReplicate
-  return #[s, e]
+  let e ← addDoNotSimp e
+  return #[e]
 
 /-- Returns the simplification context used by `grind`. -/
 protected def getSimpContext : MetaM Simp.Context := do
-  let thms ← grindNormExt.getTheorems
+  let thms ← normExt.getTheorems
   Simp.mkContext
     (config := { arith := true })
     (simpTheorems := #[thms])

tests/lean/run/grind_ematch2.lean

@@ -63,30 +63,3 @@ 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