chore(set_theory/game): various cleanup and code golf (#3939)

src/set_theory/game/impartial.lean

@@ -117,6 +117,18 @@ begin
   { right, assumption }
 end
 
+lemma impartial_not_first_wins {G : pgame} (hG : G.impartial) : ¬G.first_wins ↔ G.first_loses :=
+begin
+  cases impartial_winner_cases hG,
+  { have := not_first_wins_of_first_loses h,
+    tauto },
+  { have := not_first_loses_of_first_wins h,
+    tauto }
+end
+
+lemma impartial_not_first_loses {G : pgame} (hG : G.impartial) : ¬G.first_loses ↔ G.first_wins :=
+iff.symm $ iff_not_comm.1 $ iff.symm $ impartial_not_first_wins hG
+
 lemma impartial_add_self {G : pgame} (hG : G.impartial) : (G + G).first_loses :=
   first_loses_is_zero.2 $ equiv_trans (add_congr (impartial_neg_equiv_self hG) G.equiv_refl)
   add_left_neg_equiv

src/set_theory/game/nim.lean

@@ -17,6 +17,16 @@ This file contains the definition for nim for any ordinal `O`. In the game of `n
 may move to `nim O₂` for any `O₂ < O₁`.
 We also define a Grundy value for an impartial game `G` and prove the Sprague-Grundy theorem, that
 `G` is equivalent to `nim (Grundy_value G)`.
+
+## Implementation details
+
+The pen-and-paper definition of nim defines the possible moves of `nim O` to be `{ O' | O' < O}`.
+However, this definition does not work for us because it would make the type of nim
+`ordinal.{u} → pgame.{u + 1}`, which would make it impossible for us to state the Sprague-Grundy
+theorem, since that requires the type of `nim` to be `ordinal.{u} → pgame.{u}`. For this reason, we
+instead use `O.out.α` for the possible moves, which makes proofs significantly more messy and
+tedious, but avoids the universe bump.
+
 -/
 
 open pgame
@@ -41,12 +51,11 @@ def nim : ordinal → pgame
   λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁,
     from begin nth_rewrite_rhs 0 ←ordinal.type_out' O₁, exact ordinal.typein_lt_type _ _ end,
     nim (ordinal.typein O₁.out.r O₂)⟩
-using_well_founded {dec_tac := tactic.assumption}
+using_well_founded { dec_tac := tactic.assumption }
 
 namespace nim
 
-lemma nim_def (O : ordinal) : nim O = pgame.mk
-  O.out.α O.out.α
+lemma nim_def (O : ordinal) : nim O = pgame.mk O.out.α O.out.α
   (λ O₂, nim (ordinal.typein O.out.r O₂))
   (λ O₂, nim (ordinal.typein O.out.r O₂)) :=
 by rw nim
@@ -67,107 +76,68 @@ begin
     split,
     { intro i,
       let hwf : (ordinal.typein O.out.r i) < O := nim_wf_lemma i,
-      left,
-      exact ⟨ i, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r i).1 ⟩ },
+      exact or.inl ⟨i, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r i).1⟩ },
     { intro j,
       let hwf : (ordinal.typein O.out.r j) < O := nim_wf_lemma j,
-      right,
-      exact ⟨ j, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r j).1 ⟩ } },
+      exact or.inr ⟨j, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r j).1⟩ } },
   { rw pgame.le_def,
     split,
     { intro i,
       let hwf : (ordinal.typein O.out.r i) < O := nim_wf_lemma i,
-      left,
-      exact ⟨ i, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r i).2 ⟩ },
+      exact or.inl ⟨i, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r i).2⟩ },
     { intro j,
       let hwf : (ordinal.typein O.out.r j) < O := nim_wf_lemma j,
-      right,
-      exact ⟨ j, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r j).2 ⟩ } },
+      exact or.inr ⟨j, (impartial_neg_equiv_self $ nim_impartial $ ordinal.typein O.out.r j).2⟩ } },
   split,
   { intro i,
     let hwf : (ordinal.typein O.out.r i) < O := nim_wf_lemma i,
-    rw move_left_mk,
-    exact nim_impartial (ordinal.typein O.out.r i) },
+    simpa using nim_impartial (ordinal.typein O.out.r i) },
   { intro j,
     let hwf : (ordinal.typein O.out.r j) < O := nim_wf_lemma j,
-    rw move_right_mk,
-    exact nim_impartial (ordinal.typein O.out.r j) }
+    simpa using nim_impartial (ordinal.typein O.out.r j) }
 end
-using_well_founded {dec_tac := tactic.assumption}
+using_well_founded { dec_tac := tactic.assumption }
 
-lemma nim_zero_first_loses : (nim (0:ordinal)).first_loses :=
+lemma nim_zero_first_loses : (nim (0 : ordinal)).first_loses :=
 begin
-  rw nim_def,
-  split;
-  rw le_def_lt;
-  split;
-  intro i;
-  try {rw left_moves_mk at i};
-  try {rw right_moves_mk at i};
-  try { have h := ordinal.typein_lt_type (quotient.out (0:ordinal)).r i,
+  rw [impartial_first_loses_symm (nim_impartial _), nim_def, le_def_lt],
+  split,
+  { rintro (i : (0 : ordinal).out.α),
+    have h := ordinal.typein_lt_type _ i,
     rw ordinal.type_out at h,
-    have hcontra := ordinal.zero_le (ordinal.typein (quotient.out (0:ordinal)).r i),
-    have h := not_le_of_lt h,
-    contradiction };
-  try { exact pempty.elim i }
+    exact false.elim (not_le_of_lt h (ordinal.zero_le (ordinal.typein _ i))) },
+  { tidy }
 end
 
 lemma nim_non_zero_first_wins (O : ordinal) (hO : O ≠ 0) : (nim O).first_wins :=
 begin
-  rw nim_def,
+  rw [impartial_first_wins_symm (nim_impartial _), nim_def, lt_def_le],
   rw ←ordinal.pos_iff_ne_zero at hO,
-  split;
-  rw lt_def_le,
-  { left,
-    use (ordinal.principal_seg_out hO).top,
-    rw [move_left_mk, ordinal.typein_top, ordinal.type_out],
-    exact nim_zero_first_loses.2 },
-  { right,
-    use (ordinal.principal_seg_out hO).top,
-    rw [move_right_mk, ordinal.typein_top, ordinal.type_out],
-    exact nim_zero_first_loses.1 }
+  exact or.inr ⟨(ordinal.principal_seg_out hO).top, by simpa using nim_zero_first_loses.1⟩
 end
 
 lemma nim_sum_first_loses_iff_eq (O₁ O₂ : ordinal) : (nim O₁ + nim O₂).first_loses ↔ O₁ = O₂ :=
 begin
   split,
   { contrapose,
-    intros hneq hp,
-    wlog h : O₁ ≤ O₂ using [O₁ O₂, O₂ O₁],
-    exact ordinal.le_total O₁ O₂,
-    { have h : O₁ < O₂ := lt_of_le_of_ne h hneq,
-      rw ←(no_good_left_moves_iff_first_loses $ impartial_add (nim_impartial O₁) (nim_impartial O₂))
-        at hp,
-      equiv_rw left_moves_add (nim O₁) (nim O₂) at hp,
-      rw nim_def O₂ at hp,
-      specialize hp (sum.inr (ordinal.principal_seg_out h).top),
-      rw [id, add_move_left_inr, move_left_mk, ordinal.typein_top, ordinal.type_out] at hp,
-      cases hp,
-      have hcontra := (impartial_add_self $ nim_impartial O₁).1,
-      rw ←pgame.not_lt at hcontra,
-      contradiction },
-    exact this (λ h, hneq h.symm) (first_loses_of_equiv add_comm_equiv hp) },
-  { intro h,
-    rw h,
-    exact impartial_add_self (nim_impartial O₂) }
+    intro h,
+    rw [impartial_not_first_loses (impartial_add (nim_impartial _) (nim_impartial _))],
+    wlog h' : O₁ ≤ O₂ using [O₁ O₂, O₂ O₁],
+    { exact ordinal.le_total O₁ O₂ },
+    { have h : O₁ < O₂ := lt_of_le_of_ne h' h,
+      rw [impartial_first_wins_symm' (impartial_add (nim_impartial _) (nim_impartial _)),
+        lt_def_le, nim_def O₂],
+      refine or.inl ⟨(left_moves_add (nim O₁) _).symm (sum.inr _), _⟩,
+      { exact (ordinal.principal_seg_out h).top },
+      { simpa using (impartial_add_self (nim_impartial _)).2 } },
+    { exact first_wins_of_equiv add_comm_equiv (this (ne.symm h)) } },
+  { rintro rfl,
+    exact impartial_add_self (nim_impartial O₁) }
 end
 
 lemma nim_sum_first_wins_iff_neq (O₁ O₂ : ordinal) : (nim O₁ + nim O₂).first_wins ↔ O₁ ≠ O₂ :=
-begin
-  split,
-  { intros hn heq,
-    cases hn,
-    rw ←nim_sum_first_loses_iff_eq at heq,
-    cases heq with h,
-    rw ←pgame.not_lt at h,
-    contradiction },
-  { contrapose,
-    intro hnp,
-    rw [not_not, ←nim_sum_first_loses_iff_eq],
-    cases impartial_winner_cases (impartial_add (nim_impartial O₁) (nim_impartial O₂)),
-    assumption,
-    contradiction }
-end
+by rw [iff_not_comm, impartial_not_first_wins (impartial_add (nim_impartial _) (nim_impartial _)),
+  nim_sum_first_loses_iff_eq]
 
 lemma nim_equiv_iff_eq (O₁ O₂ : ordinal) : nim O₁ ≈ nim O₂ ↔ O₁ = O₂ :=
 ⟨λ h, (nim_sum_first_loses_iff_eq _ _).1 $
@@ -185,26 +155,19 @@ lemma nonmoves_nonempty {α : Type u} (M : α → ordinal.{u}) : ∃ O : ordinal
 begin
   classical,
   by_contra h,
-  rw nonmoves at h,
-  simp only [not_exists, not_forall, set.mem_set_of_eq, not_not] at h,
+  simp only [nonmoves, not_exists, not_forall, set.mem_set_of_eq, not_not] at h,
 
   have hle : cardinal.univ.{u (u+1)} ≤ cardinal.lift.{u (u+1)} (cardinal.mk α),
-  { split,
-    fconstructor,
-    { rintro ⟨ O ⟩,
-      exact ⟨ (classical.indefinite_description _ $ h O).val ⟩ },
-    { rintros ⟨ O₁ ⟩ ⟨ O₂ ⟩ heq,
-      ext,
-      transitivity,
-      symmetry,
-      exact (classical.indefinite_description _ (h O₁)).prop,
-      injection heq with heq,
-      rw subtype.val_eq_coe at heq,
-      rw heq,
-      exact (classical.indefinite_description _ (h O₂)).prop } },
+  { refine ⟨⟨λ ⟨O⟩, ⟨classical.some (h O)⟩, _⟩⟩,
+    rintros ⟨O₁⟩ ⟨O₂⟩ heq,
+    ext,
+    refine eq.trans (classical.some_spec (h O₁)).symm _,
+    injection heq with heq,
+    rw heq,
+    exact classical.some_spec (h O₂) },
 
   have hlt : cardinal.lift.{u (u+1)} (cardinal.mk α) < cardinal.univ.{u (u+1)} :=
-    cardinal.lt_univ.2 ⟨ cardinal.mk α, rfl ⟩,
+    cardinal.lt_univ.2 ⟨cardinal.mk α, rfl⟩,
 
   cases hlt,
   contradiction
@@ -216,7 +179,7 @@ noncomputable def Grundy_value : Π {G : pgame.{u}}, G.impartial → ordinal.{u}
 | G :=
   λ hG, ordinal.omin (nonmoves (λ i, Grundy_value $ impartial_move_left_impartial hG i))
     (nonmoves_nonempty (λ i, Grundy_value (impartial_move_left_impartial hG i)))
-using_well_founded {dec_tac := pgame_wf_tac}
+using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma Grundy_value_def {G : pgame} (hG : G.impartial) :
 Grundy_value hG = ordinal.omin (nonmoves (λ i, (Grundy_value $ impartial_move_left_impartial hG i)))
@@ -239,23 +202,20 @@ begin
   equiv_rw left_moves_add G (nim $ Grundy_value hG) at i,
   cases i with i₁ i₂,
   { rw add_move_left_inl,
-    apply first_wins_of_equiv,
-    exact (add_congr (Sprague_Grundy $ impartial_move_left_impartial hG i₁).symm (equiv_refl _)),
+    apply first_wins_of_equiv
+     (add_congr (Sprague_Grundy $ impartial_move_left_impartial hG i₁).symm (equiv_refl _)),
     rw nim_sum_first_wins_iff_neq,
     intro heq,
-    have heq := symm heq,
-    rw Grundy_value_def hG at heq,
+    rw [eq_comm, Grundy_value_def hG] at heq,
     have h := ordinal.omin_mem
       (nonmoves (λ (i : G.left_moves), Grundy_value (impartial_move_left_impartial hG i)))
       (nonmoves_nonempty _),
     rw heq at h,
     have hcontra : ∃ (i' : G.left_moves),
       (λ (i'' : G.left_moves), Grundy_value $ impartial_move_left_impartial hG i'') i' =
-        Grundy_value (impartial_move_left_impartial hG i₁) :=
-      ⟨ i₁, rfl ⟩,
+        Grundy_value (impartial_move_left_impartial hG i₁) := ⟨i₁, rfl⟩,
     contradiction },
-  { rw [add_move_left_inr,
-    ←good_left_move_iff_first_wins
+  { rw [add_move_left_inr, ←good_left_move_iff_first_wins
       (impartial_add hG $ impartial_move_left_impartial (nim_impartial _) _)],
     revert i₂,
     rw nim_def,
@@ -264,35 +224,28 @@ begin
     have h' : ∃ i : G.left_moves, (Grundy_value $ impartial_move_left_impartial hG i) =
       ordinal.typein (quotient.out $ Grundy_value hG).r i₂,
     { have hlt : ordinal.typein (quotient.out $ Grundy_value hG).r i₂ <
-        ordinal.type (quotient.out $ Grundy_value hG).r :=
-        ordinal.typein_lt_type _ _,
+        ordinal.type (quotient.out $ Grundy_value hG).r := ordinal.typein_lt_type _ _,
       rw ordinal.type_out at hlt,
       revert i₂ hlt,
       rw Grundy_value_def,
       intros i₂ hlt,
-      have hnotin :
-        ordinal.typein (quotient.out (ordinal.omin
-        (nonmoves (λ i, Grundy_value (impartial_move_left_impartial hG i))) _)).r i₂ ∉
+      have hnotin : ordinal.typein (quotient.out (ordinal.omin
+          (nonmoves (λ i, Grundy_value (impartial_move_left_impartial hG i))) _)).r i₂ ∉
         (nonmoves (λ (i : G.left_moves), Grundy_value (impartial_move_left_impartial hG i))),
       { intro hin,
         have hge := ordinal.omin_le hin,
         have hcontra := (le_not_le_of_lt hlt).2,
         contradiction },
-      unfold nonmoves at hnotin,
-      simpa using hnotin },
+      simpa [nonmoves] using hnotin },
 
     cases h' with i hi,
     use (left_moves_add _ _).symm (sum.inl i),
     rw [add_move_left_inl, move_left_mk],
-    apply first_loses_of_equiv,
-    apply add_congr,
-    symmetry,
-    exact Sprague_Grundy (impartial_move_left_impartial hG i),
-    refl,
-    rw hi,
-    exact impartial_add_self (nim_impartial _) }
+    apply first_loses_of_equiv
+      (add_congr (equiv_symm (Sprague_Grundy (impartial_move_left_impartial hG i))) (equiv_refl _)),
+    simpa only [hi] using impartial_add_self (nim_impartial _) }
 end
-using_well_founded {dec_tac := pgame_wf_tac}
+using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma equiv_nim_iff_Grundy_value_eq {G : pgame.{u}} (hG : impartial G) (O : ordinal) :
   G ≈ nim O ↔ Grundy_value hG = O :=
@@ -303,3 +256,4 @@ lemma Grundy_value_nim (O : ordinal.{u}) : Grundy_value (nim_impartial O) = O :=
 by rw ←equiv_nim_iff_Grundy_value_eq
 
 end nim
+#lint

src/set_theory/game/winner.lean

@@ -9,7 +9,7 @@ import set_theory.pgame
 # Basic definitions about who has a winning stratergy
 
 We define `G.first_loses`, `G.first_wins`, `G.left_wins` and `G.right_wins` for a pgame `G`, which
-means the second, first, left and right players have a winning stratergy respectively.
+means the second, first, left and right players have a winning strategy respectively.
 These are defined by inequalities which can be unfolded with `pgame.lt_def` and `pgame.le_def`.
 -/
 
@@ -79,4 +79,14 @@ lemma left_wins_of_equiv_iff {G H : pgame} (h : G ≈ H) : G.left_wins ↔ H.lef
 lemma right_wins_of_equiv_iff {G H : pgame} (h : G ≈ H) : G.right_wins ↔ H.right_wins :=
 ⟨ right_wins_of_equiv h, right_wins_of_equiv h.symm ⟩
 
+lemma not_first_wins_of_first_loses {G : pgame} : G.first_loses → ¬G.first_wins :=
+begin
+  rw first_loses_is_zero,
+  rintros h ⟨h₀, -⟩,
+  exact lt_irrefl 0 (lt_of_lt_of_equiv h₀ h)
+end
+
+lemma not_first_loses_of_first_wins {G : pgame} : G.first_wins → ¬G.first_loses :=
+imp_not_comm.1 $ not_first_wins_of_first_loses
+
 end pgame