Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 01 2021 at 10:54):

But I was hoping for a syntactic solution, sorta?

view this post on Zulip Ignat Insarov (Oct 01 2021 at 10:54):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ignat Insarov (Oct 01 2021 at 12:47):

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

view this post on Zulip 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:

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?

view this post on Zulip Ignat Insarov (Oct 01 2021 at 13:02):


view this post on Zulip 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

view this post on Zulip 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 applying the subgoal, in the second case after using the symmetry of /\.

view this post on Zulip Meven Lennon-Bertrand (Oct 01 2021 at 13:16):

Haha, nice collision

view this post on Zulip Andrés Goens (Oct 01 2021 at 13:16):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ignat Insarov (Oct 01 2021 at 13:28):

Not literally.

view this post on Zulip 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.

view this post on Zulip Meven Lennon-Bertrand (Oct 01 2021 at 13:31):

Ah, fair enough

view this post on Zulip 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: Mar 29 2024 at 09:02 UTC