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

[semorrison]

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 aa845de, Release)

[semorrison]

I'll briefly summarise here Mario's response to this in a meeting today, and then close later if there's no further discussion.

This use case probably counts as mis-use of the simplifier, because it is using side conditions to control flow. One should imagine an alternate version of the simplifier, which instead of checking side conditions as they arose, collected them all and only checked them at the end. This version would loop in this example without the perm check. Probably one doesn't want to have to think about this difference in the specification of the simplifier's behavior.

Mario suggested as a possible alternative, relevant for the application I had in mind, a way of specifying a custom term order to the simplifier (i.e. to use at https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L73), as an alternative to the side conditions.

I still think it would be nice to have a hook to disable this term order check entirely, for people who want to play with fire, but I appreciate the reason to be hesitant. :-)

A separate issue that came up in this conversation was that this example relies on the simplifier using decidability to discharge side conditions, which is potentially extremely expensive, and will probably be turned off as the default behaviour in future.

[digama0]

I still think it would be nice to have a hook to disable this term order check entirely, for people who want to play with fire, but I appreciate the reason to be hesitant. :-)

By the way, if the term order was a user function, then you could supply fun _ _ => true as the term order if you like to play with fire...

[semorrison]

I had a quick look at this possibility. Unfortunately one couldn't add a termOrder : Expr → Expr → MetaM Bool field to Simp.Config without a lot of rearranging, because that is defined in src/Init/Meta.lean, before MetaM is available.

[digama0]

Not Simp.Config, Simp.Methods