game_add_swap

Stream: PR reviews

[Violeta Hernández]

@Junyan Xu Regarding my game_add_swap PR and the existing cut_expand relation

[Violeta Hernández]

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]

I'd imagine that the less we need to carry around irreflexivity conditions, the better

[Violeta Hernández]

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]

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]

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!