chore: remove [grind_norm] attribute

[leodemoura]

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:

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.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7ee938290b898efa0adbd36ae7e3f9bd4c243595 --onto d4070d4bfbeb821b1614455e74198f5a11f557d5. (2025-01-19 02:16:00)