Difference in simp lemma priorities?

Stream: mathlib4

[Heather Macbeth]

Here's another simp example behaving differently between Lean 3 and Lean 4. My guess is that it's a different choice of priorities, with Lean 3 prioritizing the lemmas given by the user in simp [...] over generic @[simp] lemmas, and Lean 4 not doing this. Can anyone confirm this?

If that diagnosis is correct, it seems like it's something we will hit over and over again in the port.

class Bot (α : Type) where bot : α
class Inv (α : Type) where inv : α → α

notation "⊥" => Bot.bot
postfix:max "⁻¹" => Inv.inv

variable {α : Type} [Bot α] [Inv α]

@[simp] theorem inv_eq_bot {a : α} : a⁻¹ = ⊥ ↔ a = ⊥ := sorry

theorem inv_ne_bot {a : α} (h : a ≠ ⊥) : a⁻¹ ≠ ⊥ := sorry

example (a : α) (ha : a ≠ ⊥) : a⁻¹ = ⊥ ↔ false := by simp [inv_ne_bot ha]
-- fails in Lean 4, works in Lean 3

[Kevin Buzzard]

Hmm. In both Lean 3 and Lean 4 this code (appropriately decapitalised in Lean 3)

-- Lean 4
@[simp] theorem foo : Nat = Bool := sorry

example (h : Nat = Int) : Nat = Fin 37 := by simp
  -- unsolved goals
  -- ⊢ Bool = Fin 37

take you to Bool = Fin 37, so in both cases the generic simp lemma wins.

[Mario Carneiro]

The order in which simp applies lemmas with the same priority has always been "random", and it has indeed changed between lean 3 and lean 4 as a side effect of the discrimination tree indexing. This will unfortunately break some proofs, because while we try to keep the simp set confluent it isn't always the case, especially if you add your own lemmas to the global simp set. In theory it is possible to have a linter detect when a proof would not have gone through if the lemmas were applied in a different order, but I don't know how hard we should be on such proofs if they happen to work

[Mario Carneiro]

the workaround, when you want to use a non-confluent simp, is to use multiple simp calls with a subset of the lemmas, or use simp_rw

[Heather Macbeth]

A variant workaround: I identified the bad_lemma which was taking priority in Lean 4 and removed it from the simp set with simp [...., -bad_lemma].

[Kevin Buzzard]

But was the bad lemma making simp non-confluent? Is there a way of instead adding a new lemma to make simp confluent again?

[Mario Carneiro]

that depends

[Mario Carneiro]

in your example (did you mean to use simp [h] there?) it's clearly non-confluent

[Mario Carneiro]

In heather's example, you can add ha to the simp set to make it to the end

[Mario Carneiro]

And yes, Heather's example is non-confluent. This is basically always the case if removing a lemma causes simp to succeed where it didn't before

[Heather Macbeth]

Since the upshot of this discussion is "expected behaviour, wontfix" I have added a mention of non-confluent simps to the porting wiki.