simp experts: priority for commutatitve case?

Stream: mathlib4

[Siddhartha Gadgil]

I was fixing a few issues in mathlib4#1331 for Algebra.Star.Basic and while one could be fixed, I do not know if the fix will have the correct behaviour or I have gamed the linter. Could some simp expert please take a look.

The issue is that there is a field star_mul : ∀ r s : R, star (r * s) = star s * star r and a theorem in the commutative case which avoids the skew:

theorem star_mul' [CommSemigroup R] [StarSemigroup R] (x y : R) : star (x * y) = star x * star y := ...

Both are marked simp. The linter complained that the left-hand side of star_mul' simplifies to star y * star x, which is because of the above field. I fixed this by moving the attribute statement to after the theorem.

[Scott Morrison]

Looks good to me. Happily star_mul' still has higher priority, apparently.

[Kevin Buzzard]

My understanding is that the order in which simp tries things is completely nondeterministic and might change if we add some other lemma elsewhere?

[Mario Carneiro]

no, it's not that nondeterministic. It's a well defined order, it's just a little hard to think about since it involves the structure of the term and the order of declarations

[Mario Carneiro]

it should be relatively stable to new simp lemma additions

[Reid Barton]

If you want a specific simp lemma to have higher priority then why not give it higher priority though?

[Eric Wieser]

By giving it a priority explicitly, you're saying "make this higher priority than every lemma in every other file"

[Yaël Dillies]

... except that this only matters for other lemmas whose LHS has head star, right?

[Eric Wieser]

Sure, but chance are that if there are lemmas like that in docstream files, those want to be higher priority than any of the lemmas in star.basic

[Yaël Dillies]

If our simp set is confluent (which is wishful thinking, I know), this won't matter.

[Reid Barton]

Other lemmas that match star (r * s)?

[Reid Barton]

How many could there be?

[Yaël Dillies]

By simp_nf, none. But the point is that possibly another simplification could happen instead.

[Yaël Dillies]

For example, star (1 * a) ↦ star 1 * star a ↦ 1 * star a ↦ star a vs star (1 * a) ↦ star a. Increasing the priority of star_mul will make simp always take the first path (which is fine IMHO).

[Eric Wieser]

My comment is more of a general one that if we start putting explicit priorities on everything we end up with a 20 GOTO 10-style mess

[Eric Wieser]

I'd prefer it if we could just write assert_simp_priority old_lemma < new_lemma or something to confirm relative priorities are what we intend, and keep our existing heuristic-based priority

[Reid Barton]

I agree that priorities aren't a great way to express what we mean, but relying on undocumented simp behavior to get the order we want (which is only described on zulip) seems worse

[Eric Wieser]

Is priority documented anywhere but on zulip?

[Reid Barton]

Is that a serious question?

[Eric Wieser]

Partially, yes; I'm curious whether simp knows anything about priority, or if it just acts as an override on "order of declarations" when asking "give me all the declarations with this attribute"