Skip to content

Commit bf1157d

Browse files
int-y1int-y1
committed
feat: port SetTheory.Game.Impartial (#5517)
1 parent 0894eca commit bf1157d

File tree

2 files changed

+241
-0
lines changed

2 files changed

+241
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2752,6 +2752,7 @@ import Mathlib.SetTheory.Cardinal.Finite
27522752
import Mathlib.SetTheory.Cardinal.Ordinal
27532753
import Mathlib.SetTheory.Cardinal.SchroederBernstein
27542754
import Mathlib.SetTheory.Game.Basic
2755+
import Mathlib.SetTheory.Game.Impartial
27552756
import Mathlib.SetTheory.Game.Ordinal
27562757
import Mathlib.SetTheory.Game.PGame
27572758
import Mathlib.SetTheory.Lists

‎Mathlib/SetTheory/Game/Impartial.lean‎

Lines changed: 240 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,240 @@
1+
/-
2+
Copyright (c) 2020 Fox Thomson. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fox Thomson
5+
6+
! This file was ported from Lean 3 source module set_theory.game.impartial
7+
! leanprover-community/mathlib commit 2e0975f6a25dd3fbfb9e41556a77f075f6269748
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.Basic
12+
import Mathlib.Tactic.NthRewrite
13+
14+
/-!
15+
# Basic definitions about impartial (pre-)games
16+
17+
We will define an impartial game, one in which left and right can make exactly the same moves.
18+
Our definition differs slightly by saying that the game is always equivalent to its negative,
19+
no matter what moves are played. This allows for games such as poker-nim to be classifed as
20+
impartial.
21+
-/
22+
23+
24+
universe u
25+
26+
open scoped PGame
27+
28+
namespace PGame
29+
30+
/-- The definition for a impartial game, defined using Conway induction. -/
31+
def ImpartialAux : PGame → Prop
32+
| G => (G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
33+
termination_by _ G => G -- Porting note: Added `termination_by`
34+
decreasing_by pgame_wf_tac
35+
#align pgame.impartial_aux PGame.ImpartialAux
36+
37+
theorem impartialAux_def {G : PGame} :
38+
G.ImpartialAux ↔
39+
(G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j) := by
40+
rw [ImpartialAux]
41+
#align pgame.impartial_aux_def PGame.impartialAux_def
42+
43+
/-- A typeclass on impartial games. -/
44+
class Impartial (G : PGame) : Prop where
45+
out : ImpartialAux G
46+
#align pgame.impartial PGame.Impartial
47+
48+
theorem impartial_iff_aux {G : PGame} : G.Impartial ↔ G.ImpartialAux :=
49+
⟨fun h => h.1, fun h => ⟨h⟩⟩
50+
#align pgame.impartial_iff_aux PGame.impartial_iff_aux
51+
52+
theorem impartial_def {G : PGame} :
53+
G.Impartial ↔ (G ≈ -G) ∧ (∀ i, Impartial (G.moveLeft i)) ∧ ∀ j, Impartial (G.moveRight j) := by
54+
simpa only [impartial_iff_aux] using impartialAux_def
55+
#align pgame.impartial_def PGame.impartial_def
56+
57+
namespace Impartial
58+
59+
instance impartial_zero : Impartial 0 := by rw [impartial_def]; dsimp; simp
60+
#align pgame.impartial.impartial_zero PGame.Impartial.impartial_zero
61+
62+
instance impartial_star : Impartial star := by
63+
rw [impartial_def]; simpa using Impartial.impartial_zero
64+
#align pgame.impartial.impartial_star PGame.Impartial.impartial_star
65+
66+
theorem neg_equiv_self (G : PGame) [h : G.Impartial] : G ≈ -G :=
67+
(impartial_def.1 h).1
68+
#align pgame.impartial.neg_equiv_self PGame.Impartial.neg_equiv_self
69+
70+
-- Porting note: Changed `-⟦G⟧` to `-(⟦G⟧ : Quotient setoid)`
71+
@[simp]
72+
theorem mk'_neg_equiv_self (G : PGame) [G.Impartial] : -(⟦G⟧ : Quotient setoid) = ⟦G⟧ :=
73+
Quot.sound (Equiv.symm (neg_equiv_self G))
74+
#align pgame.impartial.mk_neg_equiv_self PGame.Impartial.mk'_neg_equiv_self
75+
76+
instance moveLeft_impartial {G : PGame} [h : G.Impartial] (i : G.LeftMoves) :
77+
(G.moveLeft i).Impartial :=
78+
(impartial_def.1 h).2.1 i
79+
#align pgame.impartial.move_left_impartial PGame.Impartial.moveLeft_impartial
80+
81+
instance moveRight_impartial {G : PGame} [h : G.Impartial] (j : G.RightMoves) :
82+
(G.moveRight j).Impartial :=
83+
(impartial_def.1 h).2.2 j
84+
#align pgame.impartial.move_right_impartial PGame.Impartial.moveRight_impartial
85+
86+
theorem impartial_congr : ∀ {G H : PGame} (_ : G ≡r H) [G.Impartial], H.Impartial
87+
| G, H => fun e => by
88+
intro h
89+
exact impartial_def.2
90+
⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)),
91+
fun i => impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
92+
termination_by _ G H => (G, H)
93+
decreasing_by pgame_wf_tac
94+
#align pgame.impartial.impartial_congr PGame.Impartial.impartial_congr
95+
96+
instance impartial_add : ∀ (G H : PGame) [G.Impartial] [H.Impartial], (G + H).Impartial
97+
| G, H, _, _ => by
98+
rw [impartial_def]
99+
refine' ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _))
100+
(Equiv.symm (negAddRelabelling _ _).equiv), fun k => _, fun k => _⟩
101+
· apply leftMoves_add_cases k
102+
all_goals
103+
intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
104+
apply impartial_add
105+
· apply rightMoves_add_cases k
106+
all_goals
107+
intro i; simp only [add_moveRight_inl, add_moveRight_inr]
108+
apply impartial_add
109+
termination_by _ G H _ _ => (G, H)
110+
decreasing_by pgame_wf_tac
111+
#align pgame.impartial.impartial_add PGame.Impartial.impartial_add
112+
113+
instance impartial_neg : ∀ (G : PGame) [G.Impartial], (-G).Impartial
114+
| G, _ => by
115+
rw [impartial_def]
116+
refine' ⟨_, fun i => _, fun i => _⟩
117+
· rw [neg_neg]
118+
exact Equiv.symm (neg_equiv_self G)
119+
· rw [moveLeft_neg']
120+
apply impartial_neg
121+
· rw [moveRight_neg']
122+
apply impartial_neg
123+
termination_by _ G _ => G
124+
decreasing_by pgame_wf_tac
125+
#align pgame.impartial.impartial_neg PGame.Impartial.impartial_neg
126+
127+
variable (G : PGame) [Impartial G]
128+
129+
theorem nonpos : ¬0 < G := fun h => by
130+
have h' := neg_lt_neg_iff.2 h
131+
rw [neg_zero, lt_congr_left (Equiv.symm (neg_equiv_self G))] at h'
132+
exact (h.trans h').false
133+
#align pgame.impartial.nonpos PGame.Impartial.nonpos
134+
135+
theorem nonneg : ¬G < 0 := fun h => by
136+
have h' := neg_lt_neg_iff.2 h
137+
rw [neg_zero, lt_congr_right (Equiv.symm (neg_equiv_self G))] at h'
138+
exact (h.trans h').false
139+
#align pgame.impartial.nonneg PGame.Impartial.nonneg
140+
141+
/-- In an impartial game, either the first player always wins, or the second player always wins. -/
142+
theorem equiv_or_fuzzy_zero : (G ≈ 0) ∨ G ‖ 0 := by
143+
rcases lt_or_equiv_or_gt_or_fuzzy G 0 with (h | h | h | h)
144+
· exact ((nonneg G) h).elim
145+
· exact Or.inl h
146+
· exact ((nonpos G) h).elim
147+
· exact Or.inr h
148+
#align pgame.impartial.equiv_or_fuzzy_zero PGame.Impartial.equiv_or_fuzzy_zero
149+
150+
@[simp]
151+
theorem not_equiv_zero_iff : ¬(G ≈ 0) ↔ G ‖ 0 :=
152+
⟨(equiv_or_fuzzy_zero G).resolve_left, Fuzzy.not_equiv⟩
153+
#align pgame.impartial.not_equiv_zero_iff PGame.Impartial.not_equiv_zero_iff
154+
155+
@[simp]
156+
theorem not_fuzzy_zero_iff : ¬G ‖ 0 ↔ (G ≈ 0) :=
157+
⟨(equiv_or_fuzzy_zero G).resolve_right, Equiv.not_fuzzy⟩
158+
#align pgame.impartial.not_fuzzy_zero_iff PGame.Impartial.not_fuzzy_zero_iff
159+
160+
theorem add_self : G + G ≈ 0 :=
161+
Equiv.trans (add_congr_left (neg_equiv_self G)) (add_left_neg_equiv G)
162+
#align pgame.impartial.add_self PGame.Impartial.add_self
163+
164+
-- Porting note: Changed `⟦G⟧` to `(⟦G⟧ : Quotient setoid)`
165+
@[simp]
166+
theorem mk'_add_self : (⟦G⟧ : Quotient setoid) + ⟦G⟧ = 0 :=
167+
Quot.sound (add_self G)
168+
#align pgame.impartial.mk_add_self PGame.Impartial.mk'_add_self
169+
170+
/-- This lemma doesn't require `H` to be impartial. -/
171+
theorem equiv_iff_add_equiv_zero (H : PGame) : (H ≈ G) ↔ (H + G ≈ 0) := by
172+
rw [Game.PGame.equiv_iff_game_eq, ← @add_right_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
173+
Game.PGame.equiv_iff_game_eq]
174+
rfl
175+
#align pgame.impartial.equiv_iff_add_equiv_zero PGame.Impartial.equiv_iff_add_equiv_zero
176+
177+
/-- This lemma doesn't require `H` to be impartial. -/
178+
theorem equiv_iff_add_equiv_zero' (H : PGame) : (G ≈ H) ↔ (G + H ≈ 0) := by
179+
rw [Game.PGame.equiv_iff_game_eq, ← @add_left_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
180+
Game.PGame.equiv_iff_game_eq]
181+
exact ⟨Eq.symm, Eq.symm⟩
182+
#align pgame.impartial.equiv_iff_add_equiv_zero' PGame.Impartial.equiv_iff_add_equiv_zero'
183+
184+
theorem le_zero_iff {G : PGame} [G.Impartial] : G ≤ 0 ↔ 0 ≤ G := by
185+
rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
186+
#align pgame.impartial.le_zero_iff PGame.Impartial.le_zero_iff
187+
188+
theorem lf_zero_iff {G : PGame} [G.Impartial] : G ⧏ 0 ↔ 0 ⧏ G := by
189+
rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]
190+
#align pgame.impartial.lf_zero_iff PGame.Impartial.lf_zero_iff
191+
192+
theorem equiv_zero_iff_le : (G ≈ 0) ↔ G ≤ 0 :=
193+
⟨And.left, fun h => ⟨h, le_zero_iff.1 h⟩⟩
194+
#align pgame.impartial.equiv_zero_iff_le PGame.Impartial.equiv_zero_iff_le
195+
196+
theorem fuzzy_zero_iff_lf : G ‖ 0 ↔ G ⧏ 0 :=
197+
⟨And.left, fun h => ⟨h, lf_zero_iff.1 h⟩⟩
198+
#align pgame.impartial.fuzzy_zero_iff_lf PGame.Impartial.fuzzy_zero_iff_lf
199+
200+
theorem equiv_zero_iff_ge : (G ≈ 0) ↔ 0 ≤ G :=
201+
⟨And.right, fun h => ⟨le_zero_iff.2 h, h⟩⟩
202+
#align pgame.impartial.equiv_zero_iff_ge PGame.Impartial.equiv_zero_iff_ge
203+
204+
theorem fuzzy_zero_iff_gf : G ‖ 0 ↔ 0 ⧏ G :=
205+
⟨And.right, fun h => ⟨lf_zero_iff.2 h, h⟩⟩
206+
#align pgame.impartial.fuzzy_zero_iff_gf PGame.Impartial.fuzzy_zero_iff_gf
207+
208+
theorem forall_leftMoves_fuzzy_iff_equiv_zero : (∀ i, G.moveLeft i ‖ 0) ↔ (G ≈ 0) := by
209+
refine' ⟨fun hb => _, fun hp i => _⟩
210+
· rw [equiv_zero_iff_le G, le_zero_lf]
211+
exact fun i => (hb i).1
212+
· rw [fuzzy_zero_iff_lf]
213+
exact hp.1.moveLeft_lf i
214+
#align pgame.impartial.forall_left_moves_fuzzy_iff_equiv_zero PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero
215+
216+
theorem forall_rightMoves_fuzzy_iff_equiv_zero : (∀ j, G.moveRight j ‖ 0) ↔ (G ≈ 0) := by
217+
refine' ⟨fun hb => _, fun hp i => _⟩
218+
· rw [equiv_zero_iff_ge G, zero_le_lf]
219+
exact fun i => (hb i).2
220+
· rw [fuzzy_zero_iff_gf]
221+
exact hp.2.lf_moveRight i
222+
#align pgame.impartial.forall_right_moves_fuzzy_iff_equiv_zero PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero
223+
224+
theorem exists_left_move_equiv_iff_fuzzy_zero : (∃ i, G.moveLeft i ≈ 0) ↔ G ‖ 0 := by
225+
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_gf G).2 (lf_of_le_moveLeft hi.2), fun hn => _⟩
226+
rw [fuzzy_zero_iff_gf G, zero_lf_le] at hn
227+
cases' hn with i hi
228+
exact ⟨i, (equiv_zero_iff_ge _).2 hi⟩
229+
#align pgame.impartial.exists_left_move_equiv_iff_fuzzy_zero PGame.Impartial.exists_left_move_equiv_iff_fuzzy_zero
230+
231+
theorem exists_right_move_equiv_iff_fuzzy_zero : (∃ j, G.moveRight j ≈ 0) ↔ G ‖ 0 := by
232+
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_lf G).2 (lf_of_moveRight_le hi.1), fun hn => _⟩
233+
rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn
234+
cases' hn with i hi
235+
exact ⟨i, (equiv_zero_iff_le _).2 hi⟩
236+
#align pgame.impartial.exists_right_move_equiv_iff_fuzzy_zero PGame.Impartial.exists_right_move_equiv_iff_fuzzy_zero
237+
238+
end Impartial
239+
240+
end PGame

0 commit comments

Comments
 (0)