refactor(set_theory/game/state): rename pgame.of to pgame.of_state (

#14658)

This is so that we can redefine `pgame.of x y = {x | y}` in #14659. Further, this is just a much clearer name.

src/set_theory/game/domineering.lean

@@ -137,7 +137,7 @@ instance state : state board :=
 end domineering
 
 /-- Construct a pre-game from a Domineering board. -/
-def domineering (b : domineering.board) : pgame := pgame.of b
+def domineering (b : domineering.board) : pgame := pgame.of_state b
 
 /-- All games of Domineering are short, because each move removes two squares. -/
 instance short_domineering (b : domineering.board) : short (domineering b) :=

src/set_theory/game/state.lean

@@ -27,7 +27,7 @@ namespace pgame
 
 /--
 `pgame_state S` describes how to interpret `s : S` as a state of a combinatorial game.
-Use `pgame.of s` or `game.of s` to construct the game.
+Use `pgame.of_state s` or `game.of_state s` to construct the game.
 
 `pgame_state.L : S → finset S` and `pgame_state.R : S → finset S` describe the states reachable
 by a move by Left or Right. `pgame_state.turn_bound : S → ℕ` gives an upper bound on the number of
@@ -70,21 +70,21 @@ nat.le_of_lt_succ (nat.lt_of_lt_of_le (right_bound m) h)
 Construct a `pgame` from a state and a (not necessarily optimal) bound on the number of
 turns remaining.
 -/
-def of_aux : Π (n : ℕ) (s : S) (h : turn_bound s ≤ n), pgame
+def of_state_aux : Π (n : ℕ) (s : S) (h : turn_bound s ≤ n), pgame
 | 0 s h     := pgame.mk {t // t ∈ L s} {t // t ∈ R s}
     (λ t, begin exfalso, exact turn_bound_ne_zero_of_left_move t.2 (nonpos_iff_eq_zero.mp h) end)
     (λ t, begin exfalso, exact turn_bound_ne_zero_of_right_move t.2 (nonpos_iff_eq_zero.mp h) end)
 | (n+1) s h :=
   pgame.mk {t // t ∈ L s} {t // t ∈ R s}
-    (λ t, of_aux n t (turn_bound_of_left t.2 n h))
-    (λ t, of_aux n t (turn_bound_of_right t.2 n h))
+    (λ t, of_state_aux n t (turn_bound_of_left t.2 n h))
+    (λ t, of_state_aux n t (turn_bound_of_right t.2 n h))
 
 /-- Two different (valid) turn bounds give equivalent games. -/
-def of_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm : turn_bound s ≤ m),
-  relabelling (of_aux n s hn) (of_aux m s hm)
+def of_state_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm : turn_bound s ≤ m),
+  relabelling (of_state_aux n s hn) (of_state_aux m s hm)
 | s 0 0 hn hm :=
   begin
-    dsimp [pgame.of_aux],
+    dsimp [pgame.of_state_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
       exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn) },
@@ -93,7 +93,7 @@ def of_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm :
   end
 | s 0 (m+1) hn hm :=
   begin
-    dsimp [pgame.of_aux],
+    dsimp [pgame.of_state_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
       exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn) },
@@ -102,7 +102,7 @@ def of_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm :
   end
 | s (n+1) 0 hn hm :=
   begin
-    dsimp [pgame.of_aux],
+    dsimp [pgame.of_state_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
       exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hm) },
@@ -111,133 +111,133 @@ def of_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm :
   end
 | s (n+1) (m+1) hn hm :=
   begin
-    dsimp [pgame.of_aux],
+    dsimp [pgame.of_state_aux],
     fsplit, refl, refl,
     { intro i,
-      apply of_aux_relabelling, },
+      apply of_state_aux_relabelling, },
     { intro j,
-      apply of_aux_relabelling, }
+      apply of_state_aux_relabelling, }
   end
 
 /-- Construct a combinatorial `pgame` from a state. -/
-def of (s : S) : pgame := of_aux (turn_bound s) s (refl _)
+def of_state (s : S) : pgame := of_state_aux (turn_bound s) s (refl _)
 
-/--
-The equivalence between `left_moves` for a `pgame` constructed using `of_aux _ s _`, and `L s`.
--/
-def left_moves_of_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n) :
-  left_moves (of_aux n s h) ≃ {t // t ∈ L s} :=
+/-- The equivalence between `left_moves` for a `pgame` constructed using `of_state_aux _ s _`, and
+`L s`. -/
+def left_moves_of_state_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n) :
+  left_moves (of_state_aux n s h) ≃ {t // t ∈ L s} :=
 by induction n; refl
-/--
-The equivalence between `left_moves` for a `pgame` constructed using `of s`, and `L s`.
--/
-def left_moves_of (s : S) : left_moves (of s) ≃ {t // t ∈ L s} :=
-left_moves_of_aux _ _
-/--
-The equivalence between `right_moves` for a `pgame` constructed using `of_aux _ s _`, and `R s`.
--/
-def right_moves_of_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n) :
-  right_moves (of_aux n s h) ≃ {t // t ∈ R s} :=
+
+/-- The equivalence between `left_moves` for a `pgame` constructed using `of_state s`, and `L s`. -/
+def left_moves_of_state (s : S) : left_moves (of_state s) ≃ {t // t ∈ L s} :=
+left_moves_of_state_aux _ _
+
+/-- The equivalence between `right_moves` for a `pgame` constructed using `of_state_aux _ s _`, and
+`R s`. -/
+def right_moves_of_state_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n) :
+  right_moves (of_state_aux n s h) ≃ {t // t ∈ R s} :=
 by induction n; refl
-/-- The equivalence between `right_moves` for a `pgame` constructed using `of s`, and `R s`. -/
-def right_moves_of (s : S) : right_moves (of s) ≃ {t // t ∈ R s} :=
-right_moves_of_aux _ _
+
+/-- The equivalence between `right_moves` for a `pgame` constructed using `of_state s`, and
+`R s`. -/
+def right_moves_of_state (s : S) : right_moves (of_state s) ≃ {t // t ∈ R s} :=
+right_moves_of_state_aux _ _
 
 /--
-The relabelling showing `move_left` applied to a game constructed using `of_aux`
-has itself been constructed using `of_aux`.
+The relabelling showing `move_left` applied to a game constructed using `of_state_aux`
+has itself been constructed using `of_state_aux`.
 -/
 def relabelling_move_left_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n)
-  (t : left_moves (of_aux n s h)) :
+  (t : left_moves (of_state_aux n s h)) :
   relabelling
-    (move_left (of_aux n s h) t)
-    (of_aux (n-1) (((left_moves_of_aux n h) t) : S)
-      ((turn_bound_of_left ((left_moves_of_aux n h) t).2 (n-1)
+    (move_left (of_state_aux n s h) t)
+    (of_state_aux (n-1) (((left_moves_of_state_aux n h) t) : S)
+      ((turn_bound_of_left ((left_moves_of_state_aux n h) t).2 (n-1)
         (nat.le_trans h le_tsub_add)))) :=
 begin
   induction n,
-  { have t' := (left_moves_of_aux 0 h) t,
+  { have t' := (left_moves_of_state_aux 0 h) t,
     exfalso, exact turn_bound_ne_zero_of_left_move t'.2 (nonpos_iff_eq_zero.mp h), },
   { refl },
 end
 /--
 The relabelling showing `move_left` applied to a game constructed using `of`
 has itself been constructed using `of`.
 -/
-def relabelling_move_left (s : S) (t : left_moves (of s)) :
+def relabelling_move_left (s : S) (t : left_moves (of_state s)) :
   relabelling
-    (move_left (of s) t)
-    (of (((left_moves_of s).to_fun t) : S)) :=
+    (move_left (of_state s) t)
+    (of_state (((left_moves_of_state s).to_fun t) : S)) :=
 begin
   transitivity,
   apply relabelling_move_left_aux,
-  apply of_aux_relabelling,
+  apply of_state_aux_relabelling,
 end
 /--
-The relabelling showing `move_right` applied to a game constructed using `of_aux`
-has itself been constructed using `of_aux`.
+The relabelling showing `move_right` applied to a game constructed using `of_state_aux`
+has itself been constructed using `of_state_aux`.
 -/
 def relabelling_move_right_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n)
-  (t : right_moves (of_aux n s h)) :
+  (t : right_moves (of_state_aux n s h)) :
   relabelling
-    (move_right (of_aux n s h) t)
-    (of_aux (n-1) (((right_moves_of_aux n h) t) : S)
-      ((turn_bound_of_right ((right_moves_of_aux n h) t).2 (n-1)
+    (move_right (of_state_aux n s h) t)
+    (of_state_aux (n-1) (((right_moves_of_state_aux n h) t) : S)
+      ((turn_bound_of_right ((right_moves_of_state_aux n h) t).2 (n-1)
         (nat.le_trans h le_tsub_add)))) :=
 begin
   induction n,
-  { have t' := (right_moves_of_aux 0 h) t,
+  { have t' := (right_moves_of_state_aux 0 h) t,
     exfalso, exact turn_bound_ne_zero_of_right_move t'.2 (nonpos_iff_eq_zero.mp h), },
   { refl },
 end
 /--
 The relabelling showing `move_right` applied to a game constructed using `of`
 has itself been constructed using `of`.
 -/
-def relabelling_move_right (s : S) (t : right_moves (of s)) :
+def relabelling_move_right (s : S) (t : right_moves (of_state s)) :
   relabelling
-    (move_right (of s) t)
-    (of (((right_moves_of s).to_fun t) : S)) :=
+    (move_right (of_state s) t)
+    (of_state (((right_moves_of_state s).to_fun t) : S)) :=
 begin
   transitivity,
   apply relabelling_move_right_aux,
-  apply of_aux_relabelling,
+  apply of_state_aux_relabelling,
 end
 
-instance fintype_left_moves_of_aux (n : ℕ) (s : S) (h : turn_bound s ≤ n) :
-  fintype (left_moves (of_aux n s h)) :=
+instance fintype_left_moves_of_state_aux (n : ℕ) (s : S) (h : turn_bound s ≤ n) :
+  fintype (left_moves (of_state_aux n s h)) :=
 begin
-  apply fintype.of_equiv _ (left_moves_of_aux _ _).symm,
+  apply fintype.of_equiv _ (left_moves_of_state_aux _ _).symm,
   apply_instance,
 end
-instance fintype_right_moves_of_aux (n : ℕ) (s : S) (h : turn_bound s ≤ n) :
-  fintype (right_moves (of_aux n s h)) :=
+instance fintype_right_moves_of_state_aux (n : ℕ) (s : S) (h : turn_bound s ≤ n) :
+  fintype (right_moves (of_state_aux n s h)) :=
 begin
-  apply fintype.of_equiv _ (right_moves_of_aux _ _).symm,
+  apply fintype.of_equiv _ (right_moves_of_state_aux _ _).symm,
   apply_instance,
 end
 
-instance short_of_aux : Π (n : ℕ) {s : S} (h : turn_bound s ≤ n), short (of_aux n s h)
+instance short_of_state_aux : Π (n : ℕ) {s : S} (h : turn_bound s ≤ n), short (of_state_aux n s h)
 | 0 s h :=
   short.mk'
   (λ i, begin
-    have i := (left_moves_of_aux _ _).to_fun i,
+    have i := (left_moves_of_state_aux _ _).to_fun i,
     exfalso,
     exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp h),
   end)
   (λ j, begin
-    have j := (right_moves_of_aux _ _).to_fun j,
+    have j := (right_moves_of_state_aux _ _).to_fun j,
     exfalso,
     exact turn_bound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp h),
   end)
 | (n+1) s h :=
   short.mk'
-  (λ i, short_of_relabelling (relabelling_move_left_aux (n+1) h i).symm (short_of_aux n _))
-  (λ j, short_of_relabelling (relabelling_move_right_aux (n+1) h j).symm (short_of_aux n _))
+  (λ i, short_of_relabelling (relabelling_move_left_aux (n+1) h i).symm (short_of_state_aux n _))
+  (λ j, short_of_relabelling (relabelling_move_right_aux (n+1) h j).symm (short_of_state_aux n _))
 
-instance short_of (s : S) : short (of s) :=
+instance short_of_state (s : S) : short (of_state s) :=
 begin
-  dsimp [pgame.of],
+  dsimp [pgame.of_state],
   apply_instance
 end
 
@@ -246,6 +246,6 @@ end pgame
 namespace game
 
 /-- Construct a combinatorial `game` from a state. -/
-def of {S : Type u} [pgame.state S] (s : S) : game := ⟦pgame.of s⟧
+def of_state {S : Type u} [pgame.state S] (s : S) : game := ⟦pgame.of_state s⟧
 
 end game