Symm can't look past \not for \neq

Stream: mathlib4

[Shreyas Srinivas]

Consider the following example. I understand why the error is thrown in the second example, but it can get annoying in the middle of a large proof. Is it possible to make symm look past unary prop operators negations? :

import Mathlib.Tactic

-- a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

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

example (h : ¬ a = b) : ¬ b = a := by
  symm -- error
  exact h

[Emilie (Shad Amethyst)]

I really, really wish ≠ was a notation, like \notin; I guess it would worsen your issue, though

[Shreyas Srinivas]

Symm seems to be expecting a binary relation at the top of the expression tree. It sees a unary relation when it encounters the negation and stops. I guess an exception could be made for negation since it is so basic and there are multiple ways to express it.

[Damiano Testa]

Would adding this work for you?

macro_rules | `(tactic| symm) => `(tactic| refine ne_comm.mp ?_)

[Shreyas Srinivas]

I am not at my machine, but would it also work with multiple negations?

[Damiano Testa]

If you have a double negation, then I would expect that you should first deal with cancelling negations and then symmetrize, if you wanted.

[Damiano Testa]

In any case, this fails:

macro_rules | `(tactic| symm) => `(tactic| refine ne_comm.mp ?_)

example (h : a ≠ b) : ¬ b ≠ a := by
  symm -- error

[Shreyas Srinivas]

I guess I am basically asking how I can transparently deal with inequalities (\neq) without thinking too hard about what form they are written in. Further symm works on the neq form while simp often reduces the neq form to \neg <equality> form whic his useful in some cases but stops symm from working

[Damiano Testa]

simp should cancel repeated negations, so I would expect the outcome of simp to have at most one negation. With that, the macro above should work, no?

[Damiano Testa]

I think that it is reasonable to expect a tactic to work assuming that the goal in in simp-normal form.

[Damiano Testa]

(Note that I am not saying that the macro above is fool-proof: I only tested it in the examples that you provided! But some variation might be what you are looking for.)

[Timo Carlin-Burns]

Is (· ≠ ·) special here? It seems it would be a valid feature request for symm for it to rw ¬ r a b ↔ ¬ r b a

[Kevin Buzzard]

My guess is that it is different, because it's Ne, not Not (eq ...).

[Timo Carlin-Burns]

Sure, I should've said (¬ · = ·). symm already applies to (· ≠ ·)

[Kevin Buzzard]

Right. I was answering the question "is it special here?" It is -- it has a name. The docstring for docs#Lean.MVarId.applySymm says that symm works on binary relations for which the corresponding symm lemma exists and is tagged with @[symm], and Ne is a binary relation, and Ne.symm is tagged with @[symm] in Mathlib.Init.Logic, but \not Eq doesn't fit into this framework. I guess one could ask for it to work on \not r goals if r.symm is tagged with @[symm] -- might be a nice metaprogramming exercise!

[Thomas Murrills]

Ah, I have a stale branch from waay back causing symm and trans to match the whole target to handle just this (mentioned in mathlib4>trans/symm changes, and possibly elsewhere)—but then it conflicted with a different refactor (#mathlib4 > Reordering arguments of Set.EqOn) a couple months later, so I didn't pursue merging it. But it worked! (I think the relevant branches are rfl-symm-trans-reducibility and rfl-symm-trans-enhance, but they're likely horribly out of date.)

Point is, it can be done...and matching the whole target after whnfR is one way to do it :)

[Thomas Murrills]

Matching the whole target is also good for more general relations, as it sets the stage for relations in which the arguments are buried in some expression or otherwise not literally the last two arguments, e.g. HEq. These aren't frequent, but symm and trans could handle them pretty painlessly with this modification + storing some extra data on "where" the arguments are in the expression (if necessary).

[Timo Carlin-Burns]

Sorry, what does "matching the whole target" mean exactly? That it looks for a @[symm] lemma with a conclusion which unifies with the target?

[Thomas Murrills]

Basically, yes: the way it works currently is that we destruct the target into rel a b, then match rel in the DiscrTree. If the target is not of this form, we fail. Instead, we could just match against the whole target, and then we'd have the chance to match against things like Not (Eq a b).

[Thomas Murrills]

(Btw, in checking that this was still the case, I realized symm is currently in std, so perhaps this topic should move streams :eyes:)