refactor(order/game_add): move game_add to its own file (#15885)

We move `game_add` from the `logic/hydra` file to a new `order/game_add` file, and move it in the `prod` namespace in preparation for a future PR that will add `sym2.game_add`.

src/logic/hydra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
 import data.multiset.basic
+import order.game_add
 import order.well_founded
 
 /-!
@@ -25,8 +26,7 @@ adding back an arbitrary multiset `t` of heads such that all `a' ∈ t` satisfy
 
 To prove this theorem, we follow the proof by Peter LeFanu Lumsdaine at
 https://mathoverflow.net/a/229084/3332, and along the way we introduce the notion of `fibration`
-of relations, and a new operation `game_add` that combines to relations to form a relation on the
-product type, which is used to define addition of games in combinatorial game theory.
+of relations.
 
 TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz)
 hydras, and prove their well-foundedness.
@@ -36,7 +36,7 @@ namespace relation
 
 variables {α β : Type*}
 
-section two_rels
+section fibration
 variables (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)
 
 /-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
@@ -60,50 +60,10 @@ lemma _root_.acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → b ∈ set.r
   (a : α) (ha : acc (inv_image rβ f) a) : acc rβ (f a) :=
 ha.of_fibration f (λ a b h, let ⟨a', he⟩ := dc h in ⟨a', he.substr h, he⟩)
 
-variables (rα rβ)
-
-/-- The "addition of games" relation in combinatorial game theory, on the product type: if
-  `rα a' a` means that `a ⟶ a'` is a valid move in game `α`, and `rβ b' b` means that `b ⟶ b'`
-  is a valid move in game `β`, then `game_add rα rβ` specifies the valid moves in the juxtaposition
-  of `α` and `β`: the player is free to choose one of the games and make a move in it,
-  while leaving the other game unchanged. -/
-inductive game_add : α × β → α × β → Prop
-| fst {a' a b} : rα a' a → game_add (a',b) (a,b)
-| snd {a b' b} : rβ b' b → game_add (a,b') (a,b)
-
-/-- `game_add` is a `subrelation` of `prod.lex`. -/
-lemma game_add_le_lex : game_add rα rβ ≤ prod.lex rα rβ :=
-λ _ _ h, h.rec (λ _ _ b, prod.lex.left b b) (λ a _ _, prod.lex.right a)
-
-/-- `prod.rprod` is a subrelation of the transitive closure of `game_add`. -/
-lemma rprod_le_trans_gen_game_add : prod.rprod rα rβ ≤ trans_gen (game_add rα rβ) :=
-λ _ _ h, h.rec begin
-  intros _ _ _ _ hα hβ,
-  exact trans_gen.tail (trans_gen.single $ game_add.fst hα) (game_add.snd hβ),
-end
-
-variables {rα rβ}
-
-/-- If `a` is accessible under `rα` and `b` is accessible under `rβ`, then `(a, b)` is
-  accessible under `relation.game_add rα rβ`. Notice that `prod.lex_accessible` requires the
-  stronger condition `∀ b, acc rβ b`. -/
-lemma _root_.acc.game_add {a b} (ha : acc rα a) (hb : acc rβ b) : acc (game_add rα rβ) (a, b) :=
-begin
-  induction ha with a ha iha generalizing b,
-  induction hb with b hb ihb,
-  refine acc.intro _ (λ h, _),
-  rintro (⟨_,_,_,ra⟩|⟨_,_,_,rb⟩),
-  exacts [iha _ ra (acc.intro b hb), ihb _ rb],
-end
-
-/-- The sum of two well-founded games is well-founded. -/
-lemma _root_.well_founded.game_add (hα : well_founded rα) (hβ : well_founded rβ) :
-  well_founded (game_add rα rβ) := ⟨λ ⟨a,b⟩, (hα.apply a).game_add (hβ.apply b)⟩
-
-end two_rels
+end fibration
 
 section hydra
-open game_add multiset
+open multiset prod
 
 /-- The relation that specifies valid moves in our hydra game. `cut_expand r s' s`
   means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
@@ -156,10 +116,10 @@ begin
   rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩, dsimp at he ⊢,
   classical, obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he,
   rw [add_assoc, mem_add] at ha, obtain (h|h) := ha,
-  { refine ⟨(s₁.erase a + t, s₂), fst ⟨t, a, hr, _⟩, _⟩,
+  { refine ⟨(s₁.erase a + t, s₂), game_add.fst ⟨t, a, hr, _⟩, _⟩,
     { rw [add_comm, ← add_assoc, singleton_add, cons_erase h] },
     { rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc] } },
-  { refine ⟨(s₁, (s₂ + t).erase a), snd ⟨t, a, hr, _⟩, _⟩,
+  { refine ⟨(s₁, (s₂ + t).erase a), game_add.snd ⟨t, a, hr, _⟩, _⟩,
     { rw [add_comm, singleton_add, cons_erase h] },
     { rw [add_assoc, erase_add_right_pos _ h] } },
 end
@@ -172,7 +132,7 @@ begin
   refine multiset.induction _ _ s,
   { exact λ _, acc.intro 0 $ λ s h, (not_cut_expand_zero s h).elim },
   { intros a s ih hacc, rw ← s.singleton_add a,
-    exact ((hacc a $ s.mem_cons_self a).game_add $ ih $ λ a ha,
+    exact ((hacc a $ s.mem_cons_self a).prod_game_add $ ih $ λ a ha,
       hacc a $ mem_cons_of_mem ha).of_fibration _ (cut_expand_fibration r) },
 end
 

src/order/game_add.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+
+import logic.relation
+import order.basic
+
+/-!
+# Game addition relation
+
+This file defines, given relations `rα : α → α → Prop` and `rβ : β → β → Prop`, a relation
+`prod.game_add` on pairs, such that `game_add rα rβ x y` iff `x` can be reached from `y` by
+decreasing either entry (with respect to `rα` and `rβ`). It is so called since it models the
+subsequency relation on the addition of combinatorial games.
+
+## Main definitions and results
+
+- `prod.game_add`: the game addition relation on ordered pairs.
+- `well_founded.game_add`: formalizes induction on ordered pairs, where exactly one entry decreases
+  at a time.
+
+## Todo
+
+- Add custom `induction` and `fix` lemmas.
+- Define `sym2.game_add`.
+-/
+
+variables {α β : Type*} (rα : α → α → Prop) (rβ : β → β → Prop)
+
+namespace prod
+
+/-- The "addition of games" relation in combinatorial game theory, on the product type: if
+  `rα a' a` means that `a ⟶ a'` is a valid move in game `α`, and `rβ b' b` means that `b ⟶ b'`
+  is a valid move in game `β`, then `game_add rα rβ` specifies the valid moves in the juxtaposition
+  of `α` and `β`: the player is free to choose one of the games and make a move in it,
+  while leaving the other game unchanged. -/
+inductive game_add : α × β → α × β → Prop
+| fst {a' a b} : rα a' a → game_add (a',b) (a,b)
+| snd {a b' b} : rβ b' b → game_add (a,b') (a,b)
+
+/-- `game_add` is a `subrelation` of `prod.lex`. -/
+lemma game_add_le_lex : game_add rα rβ ≤ prod.lex rα rβ :=
+λ _ _ h, h.rec (λ _ _ b, prod.lex.left b b) (λ a _ _, prod.lex.right a)
+
+/-- `prod.rprod` is a subrelation of the transitive closure of `game_add`. -/
+lemma rprod_le_trans_gen_game_add : prod.rprod rα rβ ≤ relation.trans_gen (game_add rα rβ) :=
+λ _ _ h, h.rec begin
+  intros _ _ _ _ hα hβ,
+  exact relation.trans_gen.tail (relation.trans_gen.single $ game_add.fst hα) (game_add.snd hβ),
+end
+
+end prod
+
+variables {rα rβ}
+
+/-- If `a` is accessible under `rα` and `b` is accessible under `rβ`, then `(a, b)` is
+  accessible under `prod.game_add rα rβ`. Notice that `prod.lex_accessible` requires the
+  stronger condition `∀ b, acc rβ b`. -/
+lemma acc.prod_game_add {a b} (ha : acc rα a) (hb : acc rβ b) : acc (prod.game_add rα rβ) (a, b) :=
+begin
+  induction ha with a ha iha generalizing b,
+  induction hb with b hb ihb,
+  refine acc.intro _ (λ h, _),
+  rintro (⟨_,_,_,ra⟩|⟨_,_,_,rb⟩),
+  exacts [iha _ ra (acc.intro b hb), ihb _ rb],
+end
+
+/-- The sum of two well-founded games is well-founded. -/
+lemma well_founded.prod_game_add (hα : well_founded rα) (hβ : well_founded rβ) :
+  well_founded (prod.game_add rα rβ) := ⟨λ ⟨a,b⟩, (hα.apply a).prod_game_add (hβ.apply b)⟩