Zulip Chat Archive

Stream: mathlib4

Topic: GroupTheory.GroupAction.ConjAct !4#1871


Johan Commelin (Jan 27 2023 at 06:02):

@Gabriel Ebner Jireh reports that there were some very slow simps in this file. I guess you might be interested in seeing those in action?

Jireh Loreaux (Jan 27 2023 at 06:05):

I sped them up with simp only. Look at the diff to see the original simp. Note that it was necessary also to separate out simp [units_smul_def, other lemmas] into simp only [units_smul_def]; simp [other lemmas], otherwise simp didn't close the goal.

Jireh Loreaux (Jan 27 2023 at 06:07):

I assume that latter has something to do with the order in which simp lemmas are applied being different in Lean 3 versus 4.

Kevin Buzzard (Jan 27 2023 at 08:39):

My understanding of this issue is that there's no way of controlling which order simp applies lemmas but if the order matters then the simp set is not "confluent" and one might want to add or remove lemmas to try and make it confluent. Easier said than done sometimes

Yaël Dillies (Jan 27 2023 at 08:43):

priority precisely lets us control which order simp applies lemmas in. But we haven't decided on the kind of priorities we want to have

Chris Hughes (Jan 27 2023 at 09:49):

I slightly sped it up by deleting the line smul := (. \bub .)


Last updated: Dec 20 2023 at 11:08 UTC