refactor(set_theory/game): make impartial a class (#3974)

* Misc. style cleanups and code golf
* Changed naming and namespace to adhere more closely to the naming convention
* Changed `impartial` to be a `class`. I am aware that @semorrison explicitly requested not to make `impartial` a class in the #3855, but after working with the definition a bit I concluded that making it a class is worth it, simply because writing `impartial_add (nim_impartial _) (nim_impartial _)` gets annoying quite quickly, but also because you tend to get goal states of the form `Grundy_value _ = Grundy_value _`. By making `impartial` a class and making the game argument explicit, these goal states look like `grundy_value G = grundy_value H`, which is much nicer to work with.

Author: TwoFX

src/set_theory/game/impartial.lean

@@ -10,7 +10,7 @@ import tactic.equiv_rw
 universe u
 
 /-!
-# Basic deinitions about impartial (pre-)games
+# Basic definitions about impartial (pre-)games
 
 We will define an impartial game, one in which left and right can make exactly the same moves.
 Our definition differs slightly by saying that the game is always equivalent to its negative,
@@ -22,12 +22,10 @@ namespace pgame
 
 local infix ` ≈ ` := equiv
 
-/-- The definiton for a impartial game, defined using Conway induction -/
-def impartial : pgame → Prop
+/-- The definition for a impartial game, defined using Conway induction -/
+@[class] def impartial : pgame → Prop
 | G := G ≈ -G ∧ (∀ i, impartial (G.move_left i)) ∧ (∀ j, impartial (G.move_right j))
-using_well_founded {dec_tac := pgame_wf_tac}
-
-lemma zero_impartial : impartial 0 := by tidy
+using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma impartial_def {G : pgame} :
   G.impartial ↔ G ≈ -G ∧ (∀ i, impartial (G.move_left i)) ∧ (∀ j, impartial (G.move_right j)) :=
@@ -41,204 +39,166 @@ begin
     exact hi }
 end
 
-lemma impartial_neg_equiv_self {G : pgame} (h : G.impartial) : G ≈ -G := (impartial_def.1 h).1
+namespace impartial
+
+instance impartial_zero : impartial 0 := by tidy
+
+lemma neg_equiv_self (G : pgame) [h : G.impartial] : G ≈ -G := (impartial_def.1 h).1
 
-lemma impartial_move_left_impartial {G : pgame} (h : G.impartial) (i : G.left_moves) :
-  impartial (G.move_left i) :=
+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
 
-lemma impartial_move_right_impartial {G : pgame} (h : G.impartial) (j : G.right_moves) :
-  impartial (G.move_right j) :=
+instance move_right_impartial {G : pgame} [h : G.impartial] (j : G.right_moves) :
+  (G.move_right j).impartial :=
 (impartial_def.1 h).2.2 j
 
-lemma impartial_add : ∀ {G H : pgame}, G.impartial → H.impartial → (G + H).impartial
+instance impartial_add : ∀ (G H : pgame) [G.impartial] [H.impartial], (G + H).impartial
 | G H :=
 begin
-  intros hG hH,
+  introsI hG hH,
   rw impartial_def,
   split,
   { apply equiv_trans _ (equiv_of_relabelling (neg_add_relabelling G H)).symm,
-    apply add_congr,
-    exact impartial_neg_equiv_self hG,
-    exact impartial_neg_equiv_self hH },
+    exact add_congr (neg_equiv_self _) (neg_equiv_self _) },
   split,
+  all_goals
   { intro i,
-    equiv_rw pgame.left_moves_add G H at i,
-    cases i with iG iH,
-    { rw add_move_left_inl,
-      exact impartial_add (impartial_move_left_impartial hG _) hH },
-    { rw add_move_left_inr,
-      exact impartial_add hG (impartial_move_left_impartial hH _) } },
-  { intro j,
-    equiv_rw pgame.right_moves_add G H at j,
-    cases j with jG jH,
-    { rw add_move_right_inl,
-      exact impartial_add (impartial_move_right_impartial hG _) hH },
-    { rw add_move_right_inr,
-      exact impartial_add hG (impartial_move_right_impartial hH _) } }
+    equiv_rw pgame.left_moves_add G H at i <|> equiv_rw pgame.right_moves_add G H at i,
+    cases i },
+  all_goals
+  { simp only [add_move_left_inl, add_move_right_inl, add_move_left_inr, add_move_right_inr],
+    exact impartial_add _ _ }
 end
-using_well_founded {dec_tac := pgame_wf_tac}
+using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma impartial_neg : ∀ {G : pgame}, G.impartial → (-G).impartial
+instance impartial_neg : ∀ (G : pgame) [G.impartial], (-G).impartial
 | G :=
 begin
-  intro hG,
+  introI hG,
   rw impartial_def,
   split,
   { rw neg_neg,
     symmetry,
-    exact impartial_neg_equiv_self hG },
+    exact neg_equiv_self G },
   split,
+  all_goals
   { intro i,
-    equiv_rw G.left_moves_neg at i,
-    rw move_left_left_moves_neg_symm,
-    exact impartial_neg (impartial_move_right_impartial hG _) },
-  { intro j,
-    equiv_rw G.right_moves_neg at j,
-    rw move_right_right_moves_neg_symm,
-    exact impartial_neg (impartial_move_left_impartial hG _) }
+    equiv_rw G.left_moves_neg at i <|> equiv_rw G.right_moves_neg at i,
+    simp only [move_left_left_moves_neg_symm, move_right_right_moves_neg_symm],
+    exact impartial_neg _ }
 end
-using_well_founded {dec_tac := pgame_wf_tac}
+using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma impartial_winner_cases {G : pgame} (hG : G.impartial) : G.first_loses ∨ G.first_wins :=
+lemma winner_cases (G : pgame) [G.impartial] : G.first_loses ∨ G.first_wins :=
 begin
   rcases G.winner_cases with hl | hr | hp | hn,
   { cases hl with hpos hnonneg,
     rw ←not_lt at hnonneg,
-    have hneg := lt_of_lt_of_equiv hpos (impartial_neg_equiv_self hG),
+    have hneg := lt_of_lt_of_equiv hpos (neg_equiv_self G),
     rw [lt_iff_neg_gt, neg_neg, neg_zero] at hneg,
     contradiction },
   { cases hr with hnonpos hneg,
     rw ←not_lt at hnonpos,
-    have hpos := lt_of_equiv_of_lt (impartial_neg_equiv_self hG).symm hneg,
+    have hpos := lt_of_equiv_of_lt (neg_equiv_self G).symm hneg,
     rw [lt_iff_neg_gt, neg_neg, neg_zero] at hpos,
     contradiction },
   { left, assumption },
   { right, assumption }
 end
 
-lemma impartial_not_first_wins {G : pgame} (hG : G.impartial) : ¬G.first_wins ↔ G.first_loses :=
-by cases impartial_winner_cases hG; finish using [not_first_loses_of_first_wins]
+lemma not_first_wins (G : pgame) [G.impartial] : ¬G.first_wins ↔ G.first_loses :=
+by cases winner_cases G; finish using [not_first_loses_of_first_wins]
 
-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 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
 
-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)
+lemma add_self (G : pgame) [G.impartial] : (G + G).first_loses :=
+  first_loses_is_zero.2 $ equiv_trans (add_congr (neg_equiv_self G) G.equiv_refl)
   add_left_neg_equiv
 
-lemma equiv_iff_sum_first_loses {G H : pgame} (hG : G.impartial) (hH : H.impartial) :
+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 (equiv_refl _) heq) (impartial_add_self hG) },
+    exact first_loses_of_equiv (add_congr (equiv_refl _) heq) (add_self G) },
   { intro hGHp,
     split,
     { rw le_iff_sub_nonneg,
       exact le_trans hGHp.2
         (le_trans add_comm_le $ le_of_le_of_equiv (le_refl _) $ add_congr (equiv_refl _)
-        (impartial_neg_equiv_self hG)) },
+        (neg_equiv_self G)) },
     { rw le_iff_sub_nonneg,
       exact le_trans hGHp.2
-        (le_of_le_of_equiv (le_refl _) $ add_congr (equiv_refl _) (impartial_neg_equiv_self hH)) } }
+        (le_of_le_of_equiv (le_refl _) $ add_congr (equiv_refl _) (neg_equiv_self H)) } }
 end
 
-lemma impartial_first_loses_symm {G : pgame} (hG : G.impartial) : G.first_loses ↔ G ≤ 0 :=
-begin
-  use and.left,
-  { intro hneg,
-    use hneg,
-    exact zero_le_iff_neg_le_zero.2 (le_of_equiv_of_le (impartial_neg_equiv_self hG).symm hneg) }
-end
+lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G :=
+by rw [le_zero_iff_zero_le_neg, le_congr (equiv_refl 0) (neg_equiv_self G)]
 
-lemma impartial_first_wins_symm {G : pgame} (hG : G.impartial) : G.first_wins ↔ G < 0 :=
-begin
-  use and.right,
-  { intro hneg,
-    split,
-    rw lt_iff_neg_gt,
-    rw neg_zero,
-    exact lt_of_equiv_of_lt (impartial_neg_equiv_self hG).symm hneg,
-    exact hneg }
-end
+lemma lt_zero_iff {G : pgame} [G.impartial] : G < 0 ↔ 0 < G :=
+by rw [lt_iff_neg_gt, neg_zero, lt_congr (equiv_refl 0) (neg_equiv_self G)]
 
-lemma impartial_first_loses_symm' {G : pgame} (hG : G.impartial) : G.first_loses ↔ 0 ≤ G :=
-begin
-  use and.right,
-  { intro hpos,
-    use le_zero_iff_zero_le_neg.2 (le_of_le_of_equiv hpos $ impartial_neg_equiv_self hG),
-    exact hpos }
-end
+lemma first_loses_symm (G : pgame) [G.impartial] : G.first_loses ↔ G ≤ 0 :=
+⟨and.left, λ h, ⟨h, le_zero_iff.1 h⟩⟩
 
-lemma impartial_first_wins_symm' {G : pgame} (hG : G.impartial) : G.first_wins ↔ 0 < G :=
-begin
-  use and.left,
-  { intro hpos,
-    use hpos,
-    rw lt_iff_neg_gt,
-    rw neg_zero,
-    exact lt_of_lt_of_equiv hpos (impartial_neg_equiv_self hG) }
-end
+lemma first_wins_symm (G : pgame) [G.impartial] : G.first_wins ↔ G < 0 :=
+⟨and.right, λ h, ⟨lt_zero_iff.1 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.left, λ h, ⟨h, lt_zero_iff.2 h⟩⟩
 
-lemma no_good_left_moves_iff_first_loses {G : pgame} (hG : G.impartial) :
+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 :=
 begin
   split,
   { intro hbad,
-    rw [impartial_first_loses_symm hG, le_def_lt],
+    rw [first_loses_symm G, le_def_lt],
     split,
     { intro i,
       specialize hbad i,
       exact hbad.2 },
     { intro j,
       exact pempty.elim j } },
   { intros hp i,
-    rw impartial_first_wins_symm (impartial_move_left_impartial hG _),
-    exact (le_def_lt.1 $ (impartial_first_loses_symm hG).1 hp).1 i }
+    rw first_wins_symm,
+    exact (le_def_lt.1 $ (first_loses_symm G).1 hp).1 i }
 end
 
-lemma no_good_right_moves_iff_first_loses {G : pgame} (hG : G.impartial) :
+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 :=
 begin
-  split,
-  { intro hbad,
-    rw [impartial_first_loses_symm' hG, le_def_lt],
-    split,
-    { intro i,
-      exact pempty.elim i },
-    { intro j,
-      specialize hbad j,
-      exact hbad.1 } },
-  { intros hp j,
-    rw impartial_first_wins_symm' (impartial_move_right_impartial hG _),
-    exact ((le_def_lt.1 $ (impartial_first_loses_symm' hG).1 hp).2 j) }
+  rw [first_loses_of_equiv_iff (neg_equiv_self G), ←no_good_left_moves_iff_first_loses],
+  refine ⟨λ h i, _, λ h i, _⟩,
+  { simpa [first_wins_of_equiv_iff (neg_equiv_self ((-G).move_left i))]
+    using h (left_moves_neg _ i) },
+  { simpa [first_wins_of_equiv_iff (neg_equiv_self (G.move_right i))]
+      using h ((left_moves_neg _).symm i) }
 end
 
-lemma good_left_move_iff_first_wins {G : pgame} (hG : G.impartial) :
+lemma good_left_move_iff_first_wins (G : pgame) [G.impartial] :
   (∃ (i : G.left_moves), (G.move_left i).first_loses) ↔ G.first_wins :=
 begin
-  split,
-  { rintro ⟨ i, hi ⟩,
-    exact (impartial_first_wins_symm' hG).2 (lt_def_le.2 $ or.inl ⟨ i, hi.2 ⟩) },
-  { intro hn,
-    rw [impartial_first_wins_symm' hG, lt_def_le] at hn,
-    rcases hn with ⟨ i, hi ⟩ | ⟨ j, _ ⟩,
-    { exact ⟨ i, (impartial_first_loses_symm' $ impartial_move_left_impartial hG _).2 hi ⟩ },
-    { exact pempty.elim j } }
+  refine ⟨λ ⟨i, hi⟩, (first_wins_symm' G).2 (lt_def_le.2 $ or.inl ⟨i, hi.2⟩), λ hn, _⟩,
+  rw [first_wins_symm' G, lt_def_le] at hn,
+  rcases hn with ⟨i, hi⟩ | ⟨j, _⟩,
+  { exact ⟨i, (first_loses_symm' _).2 hi⟩ },
+  { exact pempty.elim j }
 end
 
-lemma good_right_move_iff_first_wins {G : pgame} (hG : G.impartial) :
+lemma good_right_move_iff_first_wins (G : pgame) [G.impartial] :
   (∃ j : G.right_moves, (G.move_right j).first_loses) ↔ G.first_wins :=
 begin
-  split,
-  { rintro ⟨ j, hj ⟩,
-    exact (impartial_first_wins_symm hG).2 (lt_def_le.2 $ or.inr ⟨ j, hj.1 ⟩) },
-  { intro hn,
-    rw [impartial_first_wins_symm hG, lt_def_le] at hn,
-    rcases hn with ⟨ i, _ ⟩ | ⟨ j, hj ⟩,
-    { exact pempty.elim i },
-    { exact ⟨ j, (impartial_first_loses_symm $ impartial_move_right_impartial hG _).2 hj ⟩ } }
+  refine ⟨λ ⟨j, hj⟩, (first_wins_symm G).2 (lt_def_le.2 $ or.inr ⟨j, hj.1⟩), λ hn, _⟩,
+  rw [first_wins_symm G, lt_def_le] at hn,
+  rcases hn with ⟨i, _⟩ | ⟨j, hj⟩,
+  { exact pempty.elim i },
+  { exact ⟨j, (first_loses_symm _).2 hj⟩ }
 end
 
+end impartial
 end pgame