Priority for simp theorems

Stream: lean4

[Tomas Skrivan]

It seems that priority can be assigned to theorems marked with simp. Is this documented somewhere? I have an example of a theorems can easily get into an infinite loop unless used carefully. Setting priority solves the problem and I would like to understand how priority for simp works.

Consider this example which uses simp to invert a function. There is a general theorem inverse_of_comp_parm how to invert composition of function with an additional parameter and then there is a specific inverse of addition operation inverse_of_add_1

variable {α β γ δ} [Inhabited α] [Inhabited β]

constant inverse : (α → β) → (β → α)

@[simp 10000]
def inverse_of_comp_parm (f : β → δ → γ) (g : α → β) (d : δ)
      : inverse (λ a => f (g a) d) = (inverse g) ∘ (inverse (λ b => f b d)) := sorry

variable [Add α] [Sub α]

@[simp]
def inverse_of_add_1 (y : α)
    : inverse (λ x => x + y) = (λ x => x - y) := sorry


example (a b : α) : inverse (λ x => (x + a) + b) = (λ x => (x - b) - a) :=
by
  simp

When the theorem inverse_of_comp_parm is just marked with @[simp] then simp in the example gets into an infinite loop.

[Tomas Skrivan]

In ideal world, I do not want to set the priority but I want simp to be smart enough to realize that constantly applying inverse_of_comp_parm is not getting anywhere and stop the infinite loop.

[Tomas Skrivan]

I find the behavior of simp bit odd. Consider this example, a slight modification of the above that gets into an infinite loop:

variable {α β γ δ} [Inhabited α] [Inhabited β]

constant inverse : (α → β) → (β → α)

@[simp 100000]
def inverse_of_comp_parm (f : β → δ → γ) (g : α → β) (d : δ)
      : inverse (λ a => f (g a) d) = (inverse g) ∘ (inverse (λ b => f b d)) := sorry

@[simp]
def inverse_of_id
    : inverse (λ x : α => x) = (λ x => x) := sorry

@[simp]
def comp_id (f : α → β)
    : f ∘ (λ x => x) = f := sorry

variable [Add α] [Sub α]

set_option trace.Meta.Tactic.simp true

example (a b : α) : inverse (λ x => (x + a) + b) = (λ x => (x - b) - a) :=
by
  simp
  -- rw [inverse_of_comp_parm]
  -- rw [inverse_of_comp_parm]
  -- rw [inverse_of_id]
  -- rw [comp_id]
  -- rw [inverse_of_comp_parm]
  -- rw [inverse_of_id]
  -- rw [comp_id]

Looking at the trace log it looks like that simp goes through these rewrites:

1. inverse_of_comp_parm
2. inverse_of_comp_parm
3. inverse_of_id
4. inverse_of_comp_parm
5. inverse_of_comp_parm
6. ....

However I would expect these rewrites to be:

1. inverse_of_comp_parm
2. inverse_of_comp_parm
3. inverse_of_id
4. comp_id
5. inverse_of_comp_parm
6. inverse_of_id
7. ...

With the expected order or rewrites the goal after the step 1. and 4. are identical and a loop can be detected.

[Gabriel Ebner]

This comes up every once in a while: https://leanprover.zulipchat.com/#narrow/search/simplifier.20priority

[Gabriel Ebner]

Priorities don't work the way you think they do. The priority of a simp lemma only affects the choice of simp lemmas for the same subterm. If you have a term f (g a) d and simp lemmas g a = ... and g x = ..., then you can use priorities to specify which one of them to use.

[Gabriel Ebner]

But if you have a lemma f (g a) d = ... then this will always be applied after the lemmas for g a because simp first processes the subterms, no matter the priorities.

[Tomas Skrivan]

Thanks! Now the behavior makes sense. It looks like that I have to ditch the inverse_of_comp_parm and rewrite inverse_of_add_1 to the form

@[simp]
def inverse_of_add_1 (y : β) (f : α → β)
    : inverse (λ x => (f x) + y) = (inverse f) ∘ (λ x => x - y) := sorry