symm with Ne

Stream: mathlib4

[Ruben Van de Velde]

This seems not to work in lean4:

example (a b : ℕ) (h : a ≠ b) : b ≠ a := by
  symm
  exact h

with error

symmetry lemmas only apply to binary relations, not
  b = a → False

It feels like it should work...

[Kyle Miller]

The implementation of symm uses docs4#Lean.MVarId.getType', which uses whnf on the goal type. The definition docs4#Ne is marked reducible, so in the end symm is seeing b = a → False.

I wonder if there are any cases where you really want to unfold definitions, or whether there should be a withReducible in front of getType'.

[Alexander Bentkamp]

Or maybe symm could be extended to handle also negations of symmetric binary relations?

[Kyle Miller]

Perhaps, but that's not a complete solution here since symm would cause b ≠ a to become a = b → False.