Fix memory in symmetry tactic

[Gustavo2622]

Fixes symmetry not swapping the memory as it was supposed to, adds a distinguishing test.

[fdupress]

Probably deserves discussion with @oskgo . From memory, this was an active choice in soft-coding memories in formulas, to try and avoid some less intuitive behaviours.

[fdupress]

Although clearly, the rebinds show that my memory is flawed, here.

[oskgo]

There's a trade-off here, and it applies to a lot more tactics than just symmetry.

The trade-off is whether we prefer preserving the connection between memory name and procedure or if we prefer keeping the connection between the memory name and "side".

The latter is backwards compatible and much easier to implement, so I went with that one. There would surely be a lot of confusion if &1 suddenly referred to the right memory in existing proofs.

From talking to people it seemed like people were usually thinking about "the left memory" rather than "the memory associated with procedure a". I'd be interested to hear if you feel differently.

Your implementation also has a bug. We should only rebind if we're renaming the memories as we do the swap. You're only moving the memory, not renaming it, so you shouldn't rebind the invariant.

[fdupress]

Closing this, since the patch as provided is incorrect and there is no canonically right way to handle this.

We should make sure to actively discuss which canonically wrong way of handling this we want to make use of instead of defaulting to the backwards compatible one, but this is a much larger discussion. (In particular, it involves acknowledging that using the same notation for side and memory may have been ill-advised in the first place.)