Should `getElem_mem` be `@[simp]`?

Stream: lean4

[Daniel Weber]

Why is getElem_mem not a simp lemma? This seems like something we should want simp to solve, and it doesn't look like it will hurt performance significantly

[Kim Morrison]

I've gone back and forth on this one. It does mess up confluence of the simp set a bit, but that is a minor concern given how nice it is not to have to close such a goal by hand.

Similarly head_mem and getLast_mem.

[Kim Morrison]

I would be happy to have further opinions on this one.

[Joachim Breitner]

Probably fine to keep it [simp]. Maybe non-confluence is less bad for “closing” simp lemmas like these, where at least if it doesn't fire the rewriting won’t go in a completely different direction, but just gets stuck.

[Kim Morrison]

lean#5520

[Notification Bot]

33 messages were moved from this topic to #lean4 > "Closing simp lemmas" by Kyle Miller.