feat(logic/hydra): induction on an unordered pair

[vihdzp]

We define the relation game_add_swap r a b = game_add r r a b ∨ game_add r r a.swap b and prove its well-foundedness. This formalizes induction on an unordered pair, where either entry decreases.

To facilitate using these relations, we also add custom induction/recursion lemmas for game_add and game_add_swap.

---

[alreadydone]

I don't think we need to duplicate the fix, fix_eq and induction lemmas for every well-founded relation. Did you see such pattern elsewhere in mathlib?

I'm now a bit regretful that I didn't include the condition a ∈ s in cut_expand; if I did so then you should be able to use the map α × α → multiset α, show that game_add_swap is contained in the inv_image of cut_expand, then prove game_add_swap_aux (aside: shouldn't it be called acc.game_add_swap?) using acc_of_singleton and acc.cut_expand (which shouldn't need the is_irrefl hypothesis if cut_expand required a ∈ s).

[vihdzp]

The reason I'm specializing fix and fix_eq specifically for these two relations is so that they can be comfortably be used as lemmas on two variables, rather than lemmas on a single pair.

Also, every well founded relation is irreflexive, so maybe what you're saying can still be done? I would still like to have the fix and fix_eq theorems close to their current form if we did this: it's easier to prove a relation between four elements than it is to prove a relation between two multisets.

[vihdzp]

Regarding game_add_swap_aux: this is just the conjunction of two applications of acc.game_add_swap, so I don't think it deserves any role beyond being an auxiliary result.

[alreadydone]

Regarding game_add_swap_aux: this is just the conjunction of two applications of acc.game_add_swap, so I don't think it deserves any role beyond being an auxiliary result.

OK, I missed that game_add_swap_aux is a conjunction,and acc.game_add_swap already exists and is what I expect.

The reason I'm specializing fix and fix_eq specifically for these two relations is so that they can be comfortably be used as lemmas on two variables, rather than lemmas on a single pair.

OK, I missed that they take C : α → α → Sort* instead of the uncurried form.

Also, every well founded relation is irreflexive, so maybe what you're saying can still be done? I would still like to have the fix and fix_eq theorems close to their current form if we did this: it's easier to prove a relation between four elements than it is to prove a relation between two multisets.

You can prove well_founded.game_add_swap this way but not acc.game_add_swap, and I think we should have the acc result for completeness. The form of the fix and fix_eq theorems looks good.

[vihdzp]

I just learned about sym2, and I think it will be better to implement this new relation in terms of it.

[vihdzp]

I'll redo this in terms of sym2 in a future PR.

[alreadydone]

I just came up with another proof of well-foundedness of game_add_swap using relation.fibration, as shown in this branch. It's only slightly shorter though.

I'm not sure sym2 makes things any easier; is your idea to define game_add_swap as the inv_image of the relation.map of game_add under the quotient map? That seems too convoluted.