disable rejection of `perm` simp lemmas, or override `perm` field for a simp lemma

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The simplifier identifies some simp lemmas as permutation lemmas (if the lhs and rhs differ only by a permutation of variables), and then rejects some rewrites by these lemmas.

This has undesirable effects, in particular when using simp lemmas with side conditions that independently prevent looping. It would be helpful to either be able to disable the check that rejects rewrites by perm lemmas, or on a per-lemma basis to override the perm field.

(This is a feature request, not a bug report.)

Steps to Reproduce

class AddCommMonoid (α : Type _) extends Add α where
  add_assoc : ∀ a b c : α, a + b + c = a + (b + c) 
  add_comm : ∀ a b : α, a + b = b + a

open AddCommMonoid

variable [AddCommMonoid α]

theorem comm (f : Nat → Nat → α) (_h : i < j) : f a j + f b i = f b i + f a j :=
  add_comm _ _

theorem comm_assoc (f : Nat → Nat → α) (h : i < j) : 
    f a j + (f b i + x) = f b i + (f a j + x) := by
  rw [← add_assoc, comm _ h, add_assoc]
  
set_option trace.Meta.Tactic.simp.rewrite true

example (f : Nat → Nat → α) : f a 5 + f b 3 + f c 0 = f c 0 + f b 3 + f a 5 := by
  simp only [comm, comm_assoc, add_assoc] -- succeeds

example (f : Nat → Nat → α) : f a 5 + f b 3 + f 37 0 = f 37 0 + f b 3 + f a 5 := by
  simp only [comm, comm_assoc, add_assoc] -- fails

Note here the two examples are identical, except that I have replaced c with 37 in the second example.
The intention here is that simp only [comm, comm_assoc, add_assoc] should sort a sum of f a i terms according to the value of i.

Expected behavior:

Both examples to succeed. I'd be happy if I needed to add some annotation that tells simp that comm should not be considered a perm lemma (because of the side condition), or to specify a configuration object for simp that disables the perm check.

Actual behavior:

The first example succeeds, tracing:

[Meta.Tactic.simp.rewrite] @comm:1000:perm, f a 5 + f b 3 ==> f b 3 + f a 5 
[Meta.Tactic.simp.rewrite] @AddCommMonoid.add_assoc:1000, f b 3 + f a 5 + f c 0 ==> f b 3 + (f a 5 + f c 0) 
[Meta.Tactic.simp.rewrite] @comm:1000:perm, f a 5 + f c 0 ==> f c 0 + f a 5 
[Meta.Tactic.simp.rewrite] @comm_assoc:1000:perm, f b 3 + (f c 0 + f a 5) ==> f c 0 + (f b 3 + f a 5) 
[Meta.Tactic.simp.rewrite] @AddCommMonoid.add_assoc:1000, f c 0 + f b 3 + f a 5 ==> f c 0 + (f b 3 + f a 5) 
[Meta.Tactic.simp.rewrite] @eq_self:1000, f c 0 + (f b 3 + f a 5) = f c 0 + (f b 3 + f a 5) ==> True 

The second example fails with unsolved goals, tracing:

[Meta.Tactic.simp.rewrite] @comm:1000:perm, f a 5 + f b 3 ==> f b 3 + f a 5 
[Meta.Tactic.simp.rewrite] @AddCommMonoid.add_assoc:1000, f b 3 + f a 5 + f 37 0 ==> f b 3 + (f a 5 + f 37 0) 
[Meta.Tactic.simp.rewrite] @comm:1000:perm, perm rejected f a 5 + f 37 0 ==> f 37 0 + f a 5 
[Meta.Tactic.simp.rewrite] @AddCommMonoid.add_assoc:1000, f 37 0 + f b 3 + f a 5 ==> f 37 0 + (f b 3 + f a 5) 

Versions

Lean (version 4.0.0-nightly-2022-10-12, commit aa845dee98e3, Release)

Start with src/Lean/Meta/Tactic/Simp/SimpTheorems.lean, where simp lemmas are identified as permutation lemmas, and src/Lean/Meta/Tactic/Simp/Rewrite.lean, where some rewrites are rejected. Reproduce the two examples from the issue and investigate a configuration or per-lemma override that allows the side-conditioned rewrite; done means both examples succeed without unintended looping.