Skip to content

Commit b411eb9

Browse files
timotree3timotree3
committed
feat: port SetTheory.Game.State (#5653)
1 parent b4a49ec commit b411eb9

File tree

2 files changed

+246
-0
lines changed

2 files changed

+246
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2814,6 +2814,7 @@ import Mathlib.SetTheory.Game.Nim
28142814
import Mathlib.SetTheory.Game.Ordinal
28152815
import Mathlib.SetTheory.Game.PGame
28162816
import Mathlib.SetTheory.Game.Short
2817+
import Mathlib.SetTheory.Game.State
28172818
import Mathlib.SetTheory.Lists
28182819
import Mathlib.SetTheory.Ordinal.Arithmetic
28192820
import Mathlib.SetTheory.Ordinal.Basic

‎Mathlib/SetTheory/Game/State.lean‎

Lines changed: 245 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,245 @@
1+
/-
2+
Copyright (c) 2019 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module set_theory.game.state
7+
! leanprover-community/mathlib commit b134b2f5cf6dd25d4bbfd3c498b6e36c11a17225
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.SetTheory.Game.Short
12+
13+
/-!
14+
# Games described via "the state of the board".
15+
16+
We provide a simple mechanism for constructing combinatorial (pre-)games, by describing
17+
"the state of the board", and providing an upper bound on the number of turns remaining.
18+
19+
20+
## Implementation notes
21+
22+
We're very careful to produce a computable definition, so small games can be evaluated
23+
using `decide`. To achieve this, I've had to rely solely on induction on natural numbers:
24+
relying on general well-foundedness seems to be poisonous to computation?
25+
26+
See `SetTheory/Game/Domineering` for an example using this construction.
27+
-/
28+
29+
universe u
30+
31+
namespace PGame
32+
33+
/-- `PGame.State S` describes how to interpret `s : S` as a state of a combinatorial game.
34+
Use `PGame.ofState s` or `Game.ofState s` to construct the game.
35+
36+
`PGame.State.l : S → Finset S` and `PGame.State.r : S → Finset S` describe the states reachable
37+
by a move by Left or Right. `PGame.State.turnBound : S → ℕ` gives an upper bound on the number of
38+
possible turns remaining from this state.
39+
-/
40+
class State (S : Type u) where
41+
turnBound : S → ℕ
42+
l : S → Finset S
43+
r : S → Finset S
44+
left_bound : ∀ {s t : S}, t ∈ l s → turnBound t < turnBound s
45+
right_bound : ∀ {s t : S}, t ∈ r s → turnBound t < turnBound s
46+
#align pgame.state PGame.State
47+
48+
open State
49+
50+
variable {S : Type u} [State S]
51+
52+
theorem turnBound_ne_zero_of_left_move {s t : S} (m : t ∈ l s) : turnBound s ≠ 0 := by
53+
intro h
54+
have t := left_bound m
55+
rw [h] at t
56+
exact Nat.not_succ_le_zero _ t
57+
#align pgame.turn_bound_ne_zero_of_left_move PGame.turnBound_ne_zero_of_left_move
58+
59+
theorem turnBound_ne_zero_of_right_move {s t : S} (m : t ∈ r s) : turnBound s ≠ 0 := by
60+
intro h
61+
have t := right_bound m
62+
rw [h] at t
63+
exact Nat.not_succ_le_zero _ t
64+
#align pgame.turn_bound_ne_zero_of_right_move PGame.turnBound_ne_zero_of_right_move
65+
66+
theorem turnBound_of_left {s t : S} (m : t ∈ l s) (n : ℕ) (h : turnBound s ≤ n + 1) :
67+
turnBound t ≤ n :=
68+
Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (left_bound m) h)
69+
#align pgame.turn_bound_of_left PGame.turnBound_of_left
70+
71+
theorem turnBound_of_right {s t : S} (m : t ∈ r s) (n : ℕ) (h : turnBound s ≤ n + 1) :
72+
turnBound t ≤ n :=
73+
Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (right_bound m) h)
74+
#align pgame.turn_bound_of_right PGame.turnBound_of_right
75+
76+
/-- Construct a `PGame` from a state and a (not necessarily optimal) bound on the number of
77+
turns remaining.
78+
-/
79+
def ofStateAux : ∀ (n : ℕ) (s : S), turnBound s ≤ n → PGame
80+
| 0, s, h =>
81+
PGame.mk { t // t ∈ l s } { t // t ∈ r s }
82+
(fun t => by exfalso; exact turnBound_ne_zero_of_left_move t.2 (nonpos_iff_eq_zero.mp h))
83+
fun t => by exfalso; exact turnBound_ne_zero_of_right_move t.2 (nonpos_iff_eq_zero.mp h)
84+
| n + 1, s, h =>
85+
PGame.mk { t // t ∈ l s } { t // t ∈ r s }
86+
(fun t => ofStateAux n t (turnBound_of_left t.2 n h)) fun t =>
87+
ofStateAux n t (turnBound_of_right t.2 n h)
88+
#align pgame.of_state_aux PGame.ofStateAux
89+
90+
/-- Two different (valid) turn bounds give equivalent games. -/
91+
def ofStateAuxRelabelling :
92+
∀ (s : S) (n m : ℕ) (hn : turnBound s ≤ n) (hm : turnBound s ≤ m),
93+
Relabelling (ofStateAux n s hn) (ofStateAux m s hm)
94+
| s, 0, 0, hn, hm => by
95+
dsimp [PGame.ofStateAux]
96+
fconstructor; rfl; rfl
97+
· intro i; dsimp at i ; exfalso
98+
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
99+
· intro j; dsimp at j ; exfalso
100+
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
101+
| s, 0, m + 1, hn, hm => by
102+
dsimp [PGame.ofStateAux]
103+
fconstructor; rfl; rfl
104+
· intro i; dsimp at i ; exfalso
105+
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
106+
· intro j; dsimp at j ; exfalso
107+
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hn)
108+
| s, n + 1, 0, hn, hm => by
109+
dsimp [PGame.ofStateAux]
110+
fconstructor; rfl; rfl
111+
· intro i; dsimp at i ; exfalso
112+
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hm)
113+
· intro j; dsimp at j ; exfalso
114+
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
115+
| s, n + 1, m + 1, hn, hm => by
116+
dsimp [PGame.ofStateAux]
117+
fconstructor; rfl; rfl
118+
· intro i
119+
apply ofStateAuxRelabelling
120+
· intro j
121+
apply ofStateAuxRelabelling
122+
#align pgame.of_state_aux_relabelling PGame.ofStateAuxRelabelling
123+
124+
/-- Construct a combinatorial `PGame` from a state. -/
125+
def ofState (s : S) : PGame :=
126+
ofStateAux (turnBound s) s (refl _)
127+
#align pgame.of_state PGame.ofState
128+
129+
/-- The equivalence between `leftMoves` for a `PGame` constructed using `ofStateAux _ s _`, and
130+
`L s`. -/
131+
def leftMovesOfStateAux (n : ℕ) {s : S} (h : turnBound s ≤ n) :
132+
LeftMoves (ofStateAux n s h) ≃ { t // t ∈ l s } := by induction n <;> rfl
133+
#align pgame.left_moves_of_state_aux PGame.leftMovesOfStateAux
134+
135+
/-- The equivalence between `leftMoves` for a `PGame` constructed using `ofState s`, and `l s`. -/
136+
def leftMovesOfState (s : S) : LeftMoves (ofState s) ≃ { t // t ∈ l s } :=
137+
leftMovesOfStateAux _ _
138+
#align pgame.left_moves_of_state PGame.leftMovesOfState
139+
140+
/-- The equivalence between `rightMoves` for a `PGame` constructed using `ofStateAux _ s _`, and
141+
`R s`. -/
142+
def rightMovesOfStateAux (n : ℕ) {s : S} (h : turnBound s ≤ n) :
143+
RightMoves (ofStateAux n s h) ≃ { t // t ∈ r s } := by induction n <;> rfl
144+
#align pgame.right_moves_of_state_aux PGame.rightMovesOfStateAux
145+
146+
/-- The equivalence between `rightMoves` for a `PGame` constructed using `ofState s`, and
147+
`R s`. -/
148+
def rightMovesOfState (s : S) : RightMoves (ofState s) ≃ { t // t ∈ r s } :=
149+
rightMovesOfStateAux _ _
150+
#align pgame.right_moves_of_state PGame.rightMovesOfState
151+
152+
/-- The relabelling showing `moveLeft` applied to a game constructed using `ofStateAux`
153+
has itself been constructed using `ofStateAux`.
154+
-/
155+
def relabellingMoveLeftAux (n : ℕ) {s : S} (h : turnBound s ≤ n)
156+
(t : LeftMoves (ofStateAux n s h)) :
157+
Relabelling (moveLeft (ofStateAux n s h) t)
158+
(ofStateAux (n - 1) ((leftMovesOfStateAux n h) t : S)
159+
(turnBound_of_left ((leftMovesOfStateAux n h) t).2 (n - 1)
160+
(Nat.le_trans h le_tsub_add))) := by
161+
induction n
162+
· have t' := (leftMovesOfStateAux 0 h) t
163+
exfalso; exact turnBound_ne_zero_of_left_move t'.2 (nonpos_iff_eq_zero.mp h)
164+
· rfl
165+
#align pgame.relabelling_move_left_aux PGame.relabellingMoveLeftAux
166+
167+
/-- The relabelling showing `moveLeft` applied to a game constructed using `of`
168+
has itself been constructed using `of`.
169+
-/
170+
def relabellingMoveLeft (s : S) (t : LeftMoves (ofState s)) :
171+
Relabelling (moveLeft (ofState s) t) (ofState ((leftMovesOfState s).toFun t : S)) := by
172+
trans
173+
apply relabellingMoveLeftAux
174+
apply ofStateAuxRelabelling
175+
#align pgame.relabelling_move_left PGame.relabellingMoveLeft
176+
177+
/-- The relabelling showing `moveRight` applied to a game constructed using `ofStateAux`
178+
has itself been constructed using `ofStateAux`.
179+
-/
180+
def relabellingMoveRightAux (n : ℕ) {s : S} (h : turnBound s ≤ n)
181+
(t : RightMoves (ofStateAux n s h)) :
182+
Relabelling (moveRight (ofStateAux n s h) t)
183+
(ofStateAux (n - 1) ((rightMovesOfStateAux n h) t : S)
184+
(turnBound_of_right ((rightMovesOfStateAux n h) t).2 (n - 1)
185+
(Nat.le_trans h le_tsub_add))) := by
186+
induction n
187+
· have t' := (rightMovesOfStateAux 0 h) t
188+
exfalso; exact turnBound_ne_zero_of_right_move t'.2 (nonpos_iff_eq_zero.mp h)
189+
· rfl
190+
#align pgame.relabelling_move_right_aux PGame.relabellingMoveRightAux
191+
192+
/-- The relabelling showing `moveRight` applied to a game constructed using `of`
193+
has itself been constructed using `of`.
194+
-/
195+
def relabellingMoveRight (s : S) (t : RightMoves (ofState s)) :
196+
Relabelling (moveRight (ofState s) t) (ofState ((rightMovesOfState s).toFun t : S)) := by
197+
trans
198+
apply relabellingMoveRightAux
199+
apply ofStateAuxRelabelling
200+
#align pgame.relabelling_move_right PGame.relabellingMoveRight
201+
202+
instance fintypeLeftMovesOfStateAux (n : ℕ) (s : S) (h : turnBound s ≤ n) :
203+
Fintype (LeftMoves (ofStateAux n s h)) := by
204+
apply Fintype.ofEquiv _ (leftMovesOfStateAux _ _).symm
205+
#align pgame.fintype_left_moves_of_state_aux PGame.fintypeLeftMovesOfStateAux
206+
207+
instance fintypeRightMovesOfStateAux (n : ℕ) (s : S) (h : turnBound s ≤ n) :
208+
Fintype (RightMoves (ofStateAux n s h)) := by
209+
apply Fintype.ofEquiv _ (rightMovesOfStateAux _ _).symm
210+
#align pgame.fintype_right_moves_of_state_aux PGame.fintypeRightMovesOfStateAux
211+
212+
instance shortOfStateAux : ∀ (n : ℕ) {s : S} (h : turnBound s ≤ n), Short (ofStateAux n s h)
213+
| 0, s, h =>
214+
Short.mk'
215+
(fun i => by
216+
have i := (leftMovesOfStateAux _ _).toFun i
217+
exfalso
218+
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp h))
219+
fun j => by
220+
have j := (rightMovesOfStateAux _ _).toFun j
221+
exfalso
222+
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp h)
223+
| n + 1, s, h =>
224+
Short.mk'
225+
(fun i =>
226+
shortOfRelabelling (relabellingMoveLeftAux (n + 1) h i).symm (shortOfStateAux n _))
227+
fun j =>
228+
shortOfRelabelling (relabellingMoveRightAux (n + 1) h j).symm (shortOfStateAux n _)
229+
#align pgame.short_of_state_aux PGame.shortOfStateAux
230+
231+
instance shortOfState (s : S) : Short (ofState s) := by
232+
dsimp [PGame.ofState]
233+
infer_instance
234+
#align pgame.short_of_state PGame.shortOfState
235+
236+
end PGame
237+
238+
namespace Game
239+
240+
/-- Construct a combinatorial `Game` from a state. -/
241+
def ofState {S : Type u} [PGame.State S] (s : S) : Game :=
242+
⟦PGame.ofState s⟧
243+
#align game.of_state Game.ofState
244+
245+
end Game

0 commit comments

Comments
 (0)