Zulip Chat Archive

Stream: new members

Topic: Stupid question: how to swap sides of a hypothesis?


view this post on Zulip Nicholas Dyson (Mar 16 2021 at 17:46):

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?

view this post on Zulip Bryan Gin-ge Chen (Mar 16 2021 at 17:52):

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.)

view this post on Zulip Ruben Van de Velde (Mar 16 2021 at 17:56):

Or rw eq_comm

view this post on Zulip Nicholas Dyson (Mar 16 2021 at 18:04):

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?

view this post on Zulip Bryan Gin-ge Chen (Mar 16 2021 at 18:19):

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.

view this post on Zulip Johan Commelin (Mar 16 2021 at 18:19):

@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.

view this post on Zulip Ruben Van de Velde (Mar 16 2021 at 18:21):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 16 2021 at 18:22):

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++).


Last updated: May 17 2021 at 21:12 UTC