simp on Sym2 congr_left

Stream: mathlib4

[Jakub Nowak]

simp messes up this Sym2 expression even when explicitly adding Sym2.congr_left to simp lemmas. We should fix that, but I don't know what is the best way to fix it. Anyone cares to look at this?

import Mathlib

variable {α : Type*} {a b c : α}

example (h : s(b, a) = s(c, a)) : sorry := by
  simp [Sym2.congr_left] at h

example (h : s(b, a) = s(c, a)) : sorry := by
  rw [Sym2.congr_left] at h

[Aaron Liu]

simp [-Sym2.eq, Sym2.congr_left] at h

[Jakub Nowak]

Yeah, I know, but I think we should fix it so that simp doesn't messes it up by default.

[Aaron Liu]

I'm don't think docs#Sym2.eq is a good @[simp] lemma

[Aaron Liu]

Or maybe docs#Sym2.rel_iff' is a bad @[simp] lemma

[Aaron Liu]

definitely we shouldn't have both

[Jakub Nowak]

Yeah, these are good lemmas for grind. Not so good for simp.

[Jakub Nowak]

Maybe we should have such four theorems in simp set?

import Mathlib

variable {α : Type*} {a b c d : α}

@[simp]
theorem t1 : b = c ∨ b = a ∧ a = c ↔ b = c := by grind

@[simp]
theorem t2 : b = c ∨ a = c ∧ b = a ↔ b = c := by grind

@[simp]
theorem t3 : a = c ∧ b = a ∨ b = c ↔ b = c := by grind

@[simp]
theorem t4 : b = a ∧ a = c ∨ b = c ↔ b = c := by grind

example (h : s(b, a) = s(c, a)) : sorry := by
  simp at h

example (h : s(a, b) = s(a, c)) : sorry := by
  simp at h

example (h : s(a, b) = s(c, a)) : sorry := by
  simp at h

example (h : s(b, a) = s(a, c)) : sorry := by
  simp at h

[Violeta Hernández]

Aaron Liu said:

Or maybe docs#Sym2.rel_iff' is a bad @[simp] lemma

I vote for this, in general I'd argue most simp lemmas that just unfold definitions are bad simp lemmas (or the definitions thenselves are bad)

[Alfredo Moreira-Rosa]

Yes, and if they are really necessary to a domain, maybe create custom simpsets.

[Jakub Nowak]

I think, that Sym2.eq is pretty bad not only as a simp lemma, but as a lemma too. Sym2.Rel is just an implementation detail of Sym2 and there is close to zero API for Sym2.Rel. If there's a theorem that unfolds Sym2 p = Sym2 q it should unfold directly to p = q ∨ p = q.swap, omitting Sym2.Rel altogether.