Zulip Chat Archive
Stream: PR reviews
Topic: game_add_swap
Violeta Hernández (Jul 13 2022 at 14:29):
@Junyan Xu Regarding my game_add_swap
PR and the existing cut_expand
relation
Violeta Hernández (Jul 13 2022 at 14:31):
Should we maybe add the condition a ∈ s
to the cut_expand
relation and prove cut_expand_iff
in the other direction?
Violeta Hernández (Jul 13 2022 at 14:31):
I'd imagine that the less we need to carry around irreflexivity conditions, the better
Violeta Hernández (Jul 13 2022 at 14:32):
Also, I take it that your suggestion is to define game_add_swap r (a, b) (c, d)
as cut_expand r {a, b} {c, d}
?
Violeta Hernández (Jul 13 2022 at 14:33):
I'd be completely in favor, as long as we still proved game_add_swap r (a, b) (c, d) ↔ game_add r r (a, b) (c, d) ∨ game_add r r (a, b) (d, c)
: this is a much easier condition to verify
Junyan Xu (Jul 13 2022 at 15:21):
Oh somehow I only saw your first message when I left my latest comment at #15286. I think what you suggest here are all very reasonable!
Last updated: Dec 20 2023 at 11:08 UTC