Stupid question: how to swap sides of a hypothesis?

Stream: new members

[Nicholas Dyson]

If my context has a hypothesis

h : a = b

and I want to change it into the hypothesis
h : b = a
what's the recommended way to do that? Naively trying symmetry at h produces the following error:

symmetry tactic failed, target is not a relation application with the expected property.

I can do

have h_tmp : b = a, symmetry, exact h, clear h, rename h_tmp h,

which achieves the desired result, but this seems quite long-winded (especially in real examples where the two sides may be quite complicated rather than just "a" and "b") for such a simple change. Surely there's an easier way to do this?

[Bryan Gin-ge Chen]

I believe symmetry' at h will work. (We need to add a tactic doc for this!)

However, I think I usually just write h.symm wherever I need to put the swapped version of h. (This is short for the term eq.symm h.)

[Ruben Van de Velde]

Or rw eq_comm

[Nicholas Dyson]

Thank you loads, the apostrophe version has worked. Should the error message reflect this more? I think it's somewhat unintuitive that you need slightly different tactics for doing very similar changes on goals and hypotheses. I'm sure I'm not the first person to be confused by this and I won't be the last, so maybe the error should mention the fix in this situation?

[Bryan Gin-ge Chen]

Well, what we really should do is just replace symmetry with symmetry' (see e.g. lean#124), but there's not much appetite for this right now given that Lean 4 is right on the horizon.

[Johan Commelin]

@Nicholas Dyson The problem is (I think) that symmetry is defined in the core repo. For a long time we couldn't change that repo. So mathlib added its own version symmetry'. But once we got used to it, we never updated the version in core after we forked the core repo.

[Ruben Van de Velde]

There's a couple cases like that, where mathlib has improved versions of core tactics. Is it feasible to merge those in lean4?

[Bryan Gin-ge Chen]

I think Lean 4 will make it much easier to override core tactics since they'll all be written in Lean (as opposed to C++).