## Stream: Coq users

### Topic: Is there any way to give an argument to symmetry?

#### Ignat Insarov (Oct 01 2021 at 10:12):

For example, the relation `λx y, x = y` is the identity relation on the left and on the right with respect to the composition `λ xRy yRz, λ x z, ∃ y, xRy x y ∧ yRz y z`. The proof is very nearly the same. Is there any way to make one proof work for both?

#### Ignat Insarov (Oct 01 2021 at 10:22):

I know there is a tactic `symmetry` and various commutativity rewrite rules, but I am not sure how to apply them effectively.

#### Ignat Insarov (Oct 01 2021 at 10:33):

Concretely, I have these goals:

``````2 subgoals (ID 39)

X : Type
Y : Type
xRy : binary_relation
============================
∀ (x : X) (x0 : Y), (∃ y : Y, xRy x y ∧ y = x0) ↔ xRy x x0

subgoal 2 (ID 40) is:
∀ (x : X) (x0 : Y), (∃ y : X, x = y ∧ xRy y x0) ↔ xRy x x0
``````

They are the same up to the symmetry of `∧` and names of variables. What can I do to solve both goals at once?

#### Ignat Insarov (Oct 01 2021 at 10:53):

I suppose I could make an argument that the left identity is the right identity in the opposite category and the category of types and relations is the opposite category of itself.

#### Ignat Insarov (Oct 01 2021 at 10:54):

But I was hoping for a syntactic solution, sorta?

#### Ignat Insarov (Oct 01 2021 at 10:54):

Surely there is no need to be so grandiose as to invoke Category Theory.

#### Gaëtan Gilbert (Oct 01 2021 at 11:05):

this doesn't seem to be about the symmetry tactic
when in prose we say "by symmetry the previous argument applies", formally this means the 2 goals can be factored in some way, and in coq you need to do that factoring upfront. you can do that in a highly abstract way with category theory, or make a custom definition. however this is rarely practical compared to just copying the tactics.

#### Meven Lennon-Bertrand (Oct 01 2021 at 12:02):

There is a `wlog`(for "without loss of generality") tactic in ssreflect that can be used for these kind of cases

#### Andrés Goens (Oct 01 2021 at 12:24):

There's an interesting paper also about this subject. Perhaps not very directly of practical use (since it is based on HOL), but maybe still interesting to take a look: https://www.cl.cam.ac.uk/~jrh13/papers/wlog.pdf

#### Ignat Insarov (Oct 01 2021 at 12:47):

Nice article, I can actually understand what it is talking about and it feels good!

#### Ignat Insarov (Oct 01 2021 at 13:02):

The idea of wielding a total order to pick a canonical representative from an orbit of an element in a set subject to actions by a group is not new to me. In terms familiar to me, the article seems to be saying this:

• With i variables, there is the symmetric group Sᵢ that describes how they can be rearranged, and there is a total order that allows one to choose a canonical rearrangement. A theorem is then proven for the canonical rearrangement, and then it is proven that the proposition is invariant under the actions of the group.

• With geometric shapes in a space, there is a general linear or affine group that allows us to say the same. An arbitrary ordering on the elements of the basis induces a lexicographic ordering on the vectors.

• In a discrete space, there is a hyperoctahedral group, and the ordering is constructed similarly to the previous.

However, I cannot see how their results would generalize to my case. I wish to take a goal, prove that it is provable, and then translate this proof of provability to other goals. But there is no symmetry group nor ordering for propositions in first order logic, or is there?

What we have is, I suppose, a groupoid — a category where each arrow has an inverse. The objects are expressions in first order logic, and the arrows are the usual theorems of commutativity, associativity and so on. If we can reliably find an orbit of an expression under the actions of this groupoid, and pick the least element, then we could talk about applying the _«without loss of generality»_ pattern.

Makes sense?

#### Meven Lennon-Bertrand (Oct 01 2021 at 13:15):

I guess in your case this is more about factoring out an interesting proof step. What I would do would be to use `assert` your first goal before the split (or even state as separate lemma), so that in the first branch you can call just this, and in the second you can massage the goal/extra asserted hypothesis to apply it again

#### Andrés Goens (Oct 01 2021 at 13:15):

Remember that in the end we're just using tactics as convenient ways of constructing the underlying proof objects. So, I'm not sure you'd necessarily need to mechanize that group. You could argue that you do have this group action in the meta-theory and you could technically leverage that to write a tactic that solves goals of these kinds of ways.

I'm not aware that such a tactic exists, but I'm also not particularly knowledgeable in what tactics exist.

In your case what I would do is prove the first subgoal in an `assert (Hsubgoal : forall (x : X) ...)` to get it into the environment and use that to prove both, by `apply`ing the subgoal, in the second case after using the symmetry of `/\`.

#### Meven Lennon-Bertrand (Oct 01 2021 at 13:16):

Haha, nice collision

#### Andrés Goens (Oct 01 2021 at 13:16):

@Meven Lennon-Bertrand beat me to the same suggestion :)

#### Meven Lennon-Bertrand (Oct 01 2021 at 13:19):

As for the « without loss » pattern, the most general situation (and the one that the `wlog`/`without loss` tactic provides support for) is that you want to prove `G`, and to do it you prove separately `H -> G` (this is `G` with the extra hypothesis) and `(H -> G) -> G` (this is showing that you hypothesis was indeed without loss of generality). The second one can in some cases be completely automatized using symmetries (this is what Harrison’s paper suggests), but even when it cannot, you can still use this pattern.

#### Ignat Insarov (Oct 01 2021 at 13:24):

… you want to prove G, and to do it you prove separately H -> G (this is G with the extra hypothesis) …

I wish you write this into the reference. Now it all makes sense.

#### Meven Lennon-Bertrand (Oct 01 2021 at 13:26):

This is literally what is written in the two paragraphs just above the tactic syntax when introducing it, isn’t it?

Not literally.

#### Ignat Insarov (Oct 01 2021 at 13:30):

They never say that H → G is G with the extra hypothesis. Not in a way I could understand.

Ah, fair enough

#### Ignat Insarov (Oct 01 2021 at 15:08):

Maybe `autorewrite` can help with the groupoid thing? That is to say, maybe one can ask `autorewrite` to normalize all goals?

Last updated: Jan 27 2023 at 02:04 UTC