Reversed simp priority

Stream: lean4

[Gabriel Ebner]

In Lean 3, simp lemmas with a high priority were preferred over lemmas with low priority. In Lean 4, this seems to be reversed now. Was this intentional?

constant n : Nat
@[simp] axiom prio_1000 : n = 1000
@[simp 10] axiom prio_10 : n = 10
example : n = 10 := by simp -- succeeds now?!

[Kevin Buzzard]

does anything change if you switch the order of the axioms?

[Gabriel Ebner]

Lean 4 seems to be insensitive to the order of the simp lemmas (because they're no longer stored in a list, but in a discrimination tree now).

[Kevin Buzzard]

Can you also prove n = 1000 with simp?

[Gabriel Ebner]

If I change the priority from 10 to 9000, yes. (The two axioms are of course contradictory, but that's not the point here.)

[Sebastian Ullrich]

I think it's safe to say that's a bug - https://github.com/leanprover/lean4/blob/d6d47c8ce425572a8b973e80f2713ec3c1ce6d07/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L120

[Gabriel Ebner]

Okay, I'll submit a PR then.