refactor(set_theory/game/*): Delete winner.lean (#14271)

The file `winner.lean` currently consists of one-line definitions and theorems, including aliases for basic inequalities. This PR removes the file, inlines all previous definitions and theorems, and golfs various proofs in the process.



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/set_theory/game/impartial.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fox Thomson
 -/
-import set_theory.game.winner
+
+import set_theory.game.basic
 import tactic.nth_rewrite.default
 
 /-!
@@ -19,10 +20,11 @@ universe u
 
 namespace pgame
 
-local infix ` ≈ ` := equiv
 local infix ` ⧏ `:50 := lf
+local infix ` ≈ ` := equiv
+local infix ` ∥ `:50 := fuzzy
 
-/-- The definition for a impartial game, defined using Conway induction -/
+/-- The definition for a impartial game, defined using Conway induction. -/
 def impartial_aux : pgame → Prop
 | G := G ≈ -G ∧ (∀ i, impartial_aux (G.move_left i)) ∧ ∀ j, impartial_aux (G.move_right j)
 using_well_founded { dec_tac := pgame_wf_tac }
@@ -51,6 +53,9 @@ by { rw impartial_def, simpa using impartial.impartial_zero }
 
 lemma neg_equiv_self (G : pgame) [h : G.impartial] : G ≈ -G := (impartial_def.1 h).1
 
+@[simp] lemma mk_neg_equiv_self (G : pgame) [h : G.impartial] : -⟦G⟧ = ⟦G⟧ :=
+quot.sound (neg_equiv_self G).symm
+
 instance move_left_impartial {G : pgame} [h : G.impartial] (i : G.left_moves) :
   (G.move_left i).impartial :=
 (impartial_def.1 h).2.1 i
@@ -105,116 +110,94 @@ begin
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma nonpos (G : pgame) [G.impartial] : ¬ 0 < G :=
+variables (G : pgame) [impartial G]
+
+lemma nonpos : ¬ 0 < G :=
 λ h, begin
   have h' := neg_lt_neg_iff.2 h,
   rw [pgame.neg_zero, lt_congr_left (neg_equiv_self G).symm] at h',
   exact (h.trans h').false
 end
 
-lemma nonneg (G : pgame) [G.impartial] : ¬ G < 0 :=
+lemma nonneg : ¬ G < 0 :=
 λ h, begin
   have h' := neg_lt_neg_iff.2 h,
   rw [pgame.neg_zero, lt_congr_right (neg_equiv_self G).symm] at h',
   exact (h.trans h').false
 end
 
-lemma winner_cases (G : pgame) [G.impartial] : G.first_loses ∨ G.first_wins :=
+/-- In an impartial game, either the first player always wins, or the second player always wins. -/
+lemma equiv_or_fuzzy_zero : G ≈ 0 ∨ G ∥ 0 :=
 begin
-  rcases G.winner_cases with h | h | h | h,
+  rcases lt_or_equiv_or_gt_or_fuzzy G 0 with h | h | h | h,
   { exact ((nonneg G) h).elim },
   { exact or.inl h },
   { exact ((nonpos G) h).elim },
   { exact or.inr h }
 end
 
-lemma not_first_wins (G : pgame) [G.impartial] : ¬G.first_wins ↔ G.first_loses :=
-begin
-  cases winner_cases G; -- `finish using [not_first_loses_of_first_wins]` can close these goals
-  simp [not_first_loses_of_first_wins, not_first_wins_of_first_loses, h]
-end
+@[simp] lemma not_equiv_zero_iff : ¬ G ≈ 0 ↔ G ∥ 0 :=
+⟨(equiv_or_fuzzy_zero G).resolve_left, fuzzy.not_equiv⟩
 
-lemma not_first_loses (G : pgame) [G.impartial] : ¬G.first_loses ↔ G.first_wins :=
-iff.symm $ iff_not_comm.1 $ iff.symm $ not_first_wins G
+@[simp] lemma not_fuzzy_zero_iff : ¬ G ∥ 0 ↔ G ≈ 0 :=
+⟨(equiv_or_fuzzy_zero G).resolve_right, equiv.not_fuzzy⟩
 
-lemma add_self (G : pgame) [G.impartial] : (G + G).first_loses :=
-first_loses_is_zero.2 $ (add_congr_left (neg_equiv_self G)).trans (add_left_neg_equiv G)
+lemma add_self : G + G ≈ 0 :=
+(add_congr_left (neg_equiv_self G)).trans (add_left_neg_equiv G)
 
-lemma equiv_iff_sum_first_loses (G H : pgame) [G.impartial] [H.impartial] :
-  G ≈ H ↔ (G + H).first_loses :=
-begin
-  split,
-  { intro heq,
-    exact first_loses_of_equiv (add_congr_right heq) (add_self G) },
-  { intro hGHp,
-    split,
-    { rw le_iff_sub_nonneg,
-      exact hGHp.2.trans
-        (add_comm_le.trans $ le_of_le_of_equiv le_rfl $ add_congr_right (neg_equiv_self G)) },
-    { rw le_iff_sub_nonneg,
-      exact hGHp.2.trans
-        (le_of_le_of_equiv le_rfl $ add_congr_right (neg_equiv_self H)) } }
-end
+@[simp] lemma mk_add_self : ⟦G⟧ + ⟦G⟧ = 0 := quot.sound (add_self G)
+
+/-- This lemma doesn't require `H` to be impartial. -/
+lemma equiv_iff_add_equiv_zero (H : pgame) : H ≈ G ↔ H + G ≈ 0 :=
+by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_right_cancel_iff _ _ (-⟦G⟧)], simpa }
+
+/-- This lemma doesn't require `H` to be impartial. -/
+lemma equiv_iff_add_equiv_zero' (H : pgame) : G ≈ H ↔ G + H ≈ 0 :=
+by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_left_cancel_iff _ _ (-⟦G⟧), eq_comm], simpa }
 
 lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G :=
 by rw [←zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
 
 lemma lf_zero_iff {G : pgame} [G.impartial] : G ⧏ 0 ↔ 0 ⧏ G :=
 by rw [←zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]
 
-lemma first_loses_symm (G : pgame) [G.impartial] : G.first_loses ↔ G ≤ 0 :=
-⟨and.left, λ h, ⟨h, le_zero_iff.1 h⟩⟩
-
-lemma first_wins_symm (G : pgame) [G.impartial] : G.first_wins ↔ G ⧏ 0 :=
-⟨and.left, λ h, ⟨h, lf_zero_iff.1 h⟩⟩
+lemma equiv_zero_iff_le: G ≈ 0 ↔ G ≤ 0 := ⟨and.left, λ h, ⟨h, le_zero_iff.1 h⟩⟩
+lemma fuzzy_zero_iff_lf : G ∥ 0 ↔ G ⧏ 0 := ⟨and.left, λ h, ⟨h, lf_zero_iff.1 h⟩⟩
+lemma equiv_zero_iff_ge : G ≈ 0 ↔ 0 ≤ G := ⟨and.right, λ h, ⟨le_zero_iff.2 h, h⟩⟩
+lemma fuzzy_zero_iff_gf : G ∥ 0 ↔ 0 ⧏ G := ⟨and.right, λ h, ⟨lf_zero_iff.2 h, h⟩⟩
 
-lemma first_loses_symm' (G : pgame) [G.impartial] : G.first_loses ↔ 0 ≤ G :=
-⟨and.right, λ h, ⟨le_zero_iff.2 h, h⟩⟩
-
-lemma first_wins_symm' (G : pgame) [G.impartial] : G.first_wins ↔ 0 ⧏ G :=
-⟨and.right, λ h, ⟨lf_zero_iff.2 h, h⟩⟩
-
-lemma no_good_left_moves_iff_first_loses (G : pgame) [G.impartial] :
-  (∀ (i : G.left_moves), (G.move_left i).first_wins) ↔ G.first_loses :=
+lemma forall_left_moves_fuzzy_iff_equiv_zero : (∀ i, G.move_left i ∥ 0) ↔ G ≈ 0 :=
 begin
   refine ⟨λ hb, _, λ hp i, _⟩,
-  { rw [first_loses_symm G, le_iff_forall_lf],
-    exact ⟨λ i, (hb i).1, is_empty_elim⟩ },
-  { rw first_wins_symm,
-    exact (le_iff_forall_lf.1 $ (first_loses_symm G).1 hp).1 i }
+  { rw [equiv_zero_iff_le G, le_zero_lf],
+    exact λ i, (hb i).1 },
+  { rw fuzzy_zero_iff_lf,
+    exact move_left_lf_of_le i hp.1 }
 end
 
-lemma no_good_right_moves_iff_first_loses (G : pgame) [G.impartial] :
-  (∀ (j : G.right_moves), (G.move_right j).first_wins) ↔ G.first_loses :=
+lemma forall_right_moves_fuzzy_iff_equiv_zero : (∀ j, G.move_right j ∥ 0) ↔ G ≈ 0 :=
 begin
-  rw [first_loses_of_equiv_iff (neg_equiv_self G), ←no_good_left_moves_iff_first_loses],
-  refine ⟨λ h i, _, λ h i, _⟩,
-  { rw [move_left_neg',
-      ←first_wins_of_equiv_iff (neg_equiv_self (G.move_right (to_left_moves_neg.symm i)))],
-    apply h },
-  { rw [move_right_neg_symm',
-      ←first_wins_of_equiv_iff (neg_equiv_self ((-G).move_left (to_left_moves_neg i)))],
-    apply h }
+  refine ⟨λ hb, _, λ hp i, _⟩,
+  { rw [equiv_zero_iff_ge G, zero_le_lf],
+    exact λ i, (hb i).2 },
+  { rw fuzzy_zero_iff_gf,
+    exact lf_move_right_of_le i hp.2 }
 end
 
-lemma good_left_move_iff_first_wins (G : pgame) [G.impartial] :
-  (∃ (i : G.left_moves), (G.move_left i).first_loses) ↔ G.first_wins :=
+lemma exists_left_move_equiv_iff_fuzzy_zero : (∃ i, G.move_left i ≈ 0) ↔ G ∥ 0 :=
 begin
-  refine ⟨λ ⟨i, hi⟩, (first_wins_symm' G).2 (lf_of_exists_le $ or.inl ⟨i, hi.2⟩), λ hn, _⟩,
-  rw [first_wins_symm' G, lf_iff_exists_le] at hn,
-  rcases hn with ⟨i, hi⟩ | ⟨j, _⟩,
-  { exact ⟨i, (first_loses_symm' _).2 hi⟩ },
-  { exact pempty.elim j }
+  refine ⟨λ ⟨i, hi⟩, (fuzzy_zero_iff_gf G).2 (lf_of_le_move_left hi.2), λ hn, _⟩,
+  rw [fuzzy_zero_iff_gf G, zero_lf_le] at hn,
+  cases hn with i hi,
+  exact ⟨i, (equiv_zero_iff_ge _).2 hi⟩
 end
 
-lemma good_right_move_iff_first_wins (G : pgame) [G.impartial] :
-  (∃ j : G.right_moves, (G.move_right j).first_loses) ↔ G.first_wins :=
+lemma exists_right_move_equiv_iff_fuzzy_zero : (∃ j, G.move_right j ≈ 0) ↔ G ∥ 0 :=
 begin
-  refine ⟨λ ⟨j, hj⟩, (first_wins_symm G).2 (lf_of_exists_le $ or.inr ⟨j, hj.1⟩), λ hn, _⟩,
-  rw [first_wins_symm G, lf_iff_exists_le] at hn,
-  rcases hn with ⟨i, _⟩ | ⟨j, hj⟩,
-  { exact pempty.elim i },
-  { exact ⟨j, (first_loses_symm _).2 hj⟩ }
+  refine ⟨λ ⟨i, hi⟩, (fuzzy_zero_iff_lf G).2 (lf_of_move_right_le hi.1), λ hn, _⟩,
+  rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn,
+  cases hn with i hi,
+  exact ⟨i, (equiv_zero_iff_le _).2 hi⟩
 end
 
 end impartial

src/set_theory/game/nim.lean

@@ -6,6 +6,7 @@ Authors: Fox Thomson, Markus Himmel
 import data.nat.bitwise
 import set_theory.game.birthday
 import set_theory.game.impartial
+
 /-!
 # Nim and the Sprague-Grundy theorem
 
@@ -46,7 +47,9 @@ using_well_founded { dec_tac := tactic.assumption }
 
 namespace pgame
 
+local infix ` ⧏ `:50 := lf
 local infix ` ≈ ` := equiv
+local infix ` ∥ `:50 := fuzzy
 
 namespace nim
 
@@ -159,41 +162,36 @@ lemma exists_ordinal_move_left_eq {O : ordinal} (i) : ∃ O' < O, (nim O).move_l
 lemma exists_move_left_eq {O O' : ordinal} (h : O' < O) : ∃ i, (nim O).move_left i = nim O' :=
 ⟨to_left_moves_nim ⟨O', h⟩, by simp⟩
 
-@[simp] lemma zero_first_loses : (nim (0 : ordinal)).first_loses :=
-equiv.is_empty _
-
-lemma non_zero_first_wins {O : ordinal} (hO : O ≠ 0) : (nim O).first_wins :=
+lemma non_zero_first_wins {O : ordinal} (hO : O ≠ 0) : nim O ∥ 0 :=
 begin
-  rw [impartial.first_wins_symm, nim_def, lf_iff_exists_le],
+  rw [impartial.fuzzy_zero_iff_lf, nim_def, lf_zero_le],
   rw ←ordinal.pos_iff_ne_zero at hO,
-  exact or.inr ⟨(ordinal.principal_seg_out hO).top, by simp⟩
+  exact ⟨(ordinal.principal_seg_out hO).top, by simp⟩
 end
 
-@[simp] lemma sum_first_loses_iff_eq (O₁ O₂ : ordinal) : (nim O₁ + nim O₂).first_loses ↔ O₁ = O₂ :=
+@[simp] lemma add_equiv_zero_iff_eq (O₁ O₂ : ordinal) : nim O₁ + nim O₂ ≈ 0 ↔ O₁ = O₂ :=
 begin
   split,
   { contrapose,
     intro h,
-    rw [impartial.not_first_loses],
+    rw [impartial.not_equiv_zero_iff],
     wlog h' : O₁ ≤ O₂ using [O₁ O₂, O₂ O₁],
     { exact le_total O₁ O₂ },
     { have h : O₁ < O₂ := lt_of_le_of_ne h' h,
-      rw [impartial.first_wins_symm', lf_iff_exists_le, nim_def O₂],
-      refine or.inl ⟨to_left_moves_add (sum.inr _), _⟩,
+      rw [impartial.fuzzy_zero_iff_gf, zero_lf_le, nim_def O₂],
+      refine ⟨to_left_moves_add (sum.inr _), _⟩,
       { exact (ordinal.principal_seg_out h).top },
       { simpa using (impartial.add_self (nim O₁)).2 } },
-    { exact first_wins_of_equiv add_comm_equiv (this (ne.symm h)) } },
+    { exact (fuzzy_congr_left add_comm_equiv).1 (this (ne.symm h)) } },
   { rintro rfl,
     exact impartial.add_self (nim O₁) }
 end
 
-@[simp] lemma sum_first_wins_iff_neq (O₁ O₂ : ordinal) : (nim O₁ + nim O₂).first_wins ↔ O₁ ≠ O₂ :=
-by rw [iff_not_comm, impartial.not_first_wins, sum_first_loses_iff_eq]
+@[simp] lemma add_fuzzy_zero_iff_ne (O₁ O₂ : ordinal) : nim O₁ + nim O₂ ∥ 0 ↔ O₁ ≠ O₂ :=
+by rw [iff_not_comm, impartial.not_fuzzy_zero_iff, add_equiv_zero_iff_eq]
 
 @[simp] lemma equiv_iff_eq (O₁ O₂ : ordinal) : nim O₁ ≈ nim O₂ ↔ O₁ = O₂ :=
-⟨λ h, (sum_first_loses_iff_eq _ _).1 $
-  by rw [first_loses_of_equiv_iff (add_congr_left h), sum_first_loses_iff_eq],
- by { rintro rfl, refl }⟩
+by rw [impartial.equiv_iff_add_equiv_zero, add_equiv_zero_iff_eq]
 
 end nim
 
@@ -213,20 +211,20 @@ theorem equiv_nim_grundy_value : ∀ (G : pgame.{u}) [G.impartial], G ≈ nim (g
 | G :=
 begin
   introI hG,
-  rw [impartial.equiv_iff_sum_first_loses, ←impartial.no_good_left_moves_iff_first_loses],
+  rw [impartial.equiv_iff_add_equiv_zero, ←impartial.forall_left_moves_fuzzy_iff_equiv_zero],
   intro i,
   apply left_moves_add_cases i,
   { intro i₁,
     rw add_move_left_inl,
-    apply first_wins_of_equiv (add_congr_left (equiv_nim_grundy_value (G.move_left i₁)).symm),
-    rw nim.sum_first_wins_iff_neq,
+    apply (fuzzy_congr_left (add_congr_left (equiv_nim_grundy_value (G.move_left i₁)).symm)).1,
+    rw nim.add_fuzzy_zero_iff_ne,
     intro heq,
     rw [eq_comm, grundy_value_def G] at heq,
     have h := ordinal.ne_mex _,
     rw heq at h,
     exact (h i₁).irrefl },
   { intro i₂,
-    rw [add_move_left_inr, ←impartial.good_left_move_iff_first_wins],
+    rw [add_move_left_inr, ←impartial.exists_left_move_equiv_iff_fuzzy_zero],
     revert i₂,
     rw nim.nim_def,
     intro i₂,
@@ -242,8 +240,7 @@ begin
     cases h' with i hi,
     use to_left_moves_add (sum.inl i),
     rw [add_move_left_inl, move_left_mk],
-    apply first_loses_of_equiv
-      (add_congr_left (equiv_nim_grundy_value (G.move_left i)).symm),
+    apply (add_congr_left (equiv_nim_grundy_value (G.move_left i))).trans,
     simpa only [hi] using impartial.add_self (nim (grundy_value (G.move_left i))) }
 end
 using_well_founded { dec_tac := pgame_wf_tac }