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?
I know there is a tactic symmetry
and various commutativity rewrite rules, but I am not sure how to apply them effectively.
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?
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.
But I was hoping for a syntactic solution, sorta?
Surely there is no need to be so grandiose as to invoke Category Theory.
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.
There is a wlog
(for "without loss of generality") tactic in ssreflect that can be used for these kind of cases
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
Nice article, I can actually understand what it is talking about and it feels good!
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?
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
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 /\
.
Haha, nice collision
@Meven Lennon-Bertrand beat me to the same suggestion :)
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.
… 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.
This is literally what is written in the two paragraphs just above the tactic syntax when introducing it, isn’t it?
Not literally.
They never say that H → G is G with the extra hypothesis. Not in a way I could understand.
Ah, fair enough
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