simp and symmetry

Stream: mathlib4

[Michael Stoll]

simp simplifies x ^ 2 = 0 to x = 0 (in suitable circumstances), but leaves 0 = x ^ 2 alone.
Would it make sense to have a simproc that rewrites 0 = whatever to whatever = 0 before looking for lemmas that can be applied?
This is just a thought I had after noticing the behavior mentioned at the beginning and after listening to Leo talking about simprocs...

[Emilie (Shad Amethyst)]

We could also have a simproc rewriting x ≥ 0 to 0 ≤ x

[Kyle Miller]

I'm not sure you need a simproc here.

@[simp ↓]
theorem zero_eq {α : Type*} [Zero α] (x : α) : 0 = x ↔ x = 0 := by rw [eq_comm]

example (x : ℝ) : 0 = x^2 := by
  simp
  -- ⊢ x = 0

Though perhaps a simproc would be more efficient than this lemma.

[Kevin Buzzard]

It's annoying that I can't easily find out what that down-arrow is doing on mobile (unless docs#simp now works...) (edit : nope)

[Kyle Miller]

It means "apply this simp lemma before simplifying subexpressions." You can use it before lemmas in a list of simp lemmas too.

[Kyle Miller]

The default is @[simp ↑], which means "apply this simp lemma after simplifying subexpressions". You could place ↑ before simp lemmas too, but there's no point since it's the default.

[Kyle Miller]

I'll claim that these are respectively known as "pre-simp lemmas" and "(post-)simp lemmas". (These words don't appear in the lean4 repository though, so this a normative claim rather than a descriptive one.)

[Kyle Miller]

I don't really know how to decide whether it should be a @[simp ↓] lemma or not. It would work fine as just a @[simp] lemma too. Another option is making be high-priority to be sure it triggers before anything else. Pre-simp lemmas effectively have priority infinity compared to post-simp lemmas.