Skip to content

Commit 247ff18

Browse files
vihdzpvihdzp
committed
chore(SetTheory/Game/Impartial): cleanup proofs (#16517)
We clean up remnants of the Lean 3 `termination_by` syntax, as well as some exposed setoid API.
1 parent 329f679 commit 247ff18

File tree

2 files changed

+69
-79
lines changed

2 files changed

+69
-79
lines changed

‎Mathlib/SetTheory/Game/Basic.lean‎

Lines changed: 17 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -219,23 +219,17 @@ end Game
219219

220220
namespace PGame
221221

222-
@[simp]
223-
theorem quot_neg (a : PGame) : (⟦-a⟧ : Game) = -⟦a⟧ :=
224-
rfl
225-
226-
@[simp]
227-
theorem quot_add (a b : PGame) : ⟦a + b⟧ = (⟦a⟧ : Game) + ⟦b⟧ :=
228-
rfl
229-
230-
@[simp]
231-
theorem quot_sub (a b : PGame) : ⟦a - b⟧ = (⟦a⟧ : Game) - ⟦b⟧ :=
232-
rfl
222+
@[simp] theorem quot_zero : (⟦0⟧ : Game) = 0 := rfl
223+
@[simp] theorem quot_one : (⟦1⟧ : Game) = 1 := rfl
224+
@[simp] theorem quot_neg (a : PGame) : (⟦-a⟧ : Game) = -⟦a⟧ := rfl
225+
@[simp] theorem quot_add (a b : PGame) : ⟦a + b⟧ = (⟦a⟧ : Game) + ⟦b⟧ := rfl
226+
@[simp] theorem quot_sub (a b : PGame) : ⟦a - b⟧ = (⟦a⟧ : Game) - ⟦b⟧ := rfl
233227

234228
theorem quot_eq_of_mk'_quot_eq {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves)
235229
(R : x.RightMoves ≃ y.RightMoves) (hl : ∀ i, (⟦x.moveLeft i⟧ : Game) = ⟦y.moveLeft (L i)⟧)
236-
(hr : ∀ j, (⟦x.moveRight j⟧ : Game) = ⟦y.moveRight (R j)⟧) : (⟦x⟧ : Game) = ⟦y⟧ := by
237-
exact Quot.sound (equiv_of_mk_equiv L R (fun _ => equiv_iff_game_eq.2 (hl _))
238-
(fun _ => equiv_iff_game_eq.2 (hr _)))
230+
(hr : ∀ j, (⟦x.moveRight j⟧ : Game) = ⟦y.moveRight (R j)⟧) : (⟦x⟧ : Game) = ⟦y⟧ :=
231+
game_eq (equiv_of_mk_equiv L R (fun _ => equiv_iff_game_eq.2 (hl _))
232+
(fun _ => equiv_iff_game_eq.2 (hr _)))
239233

240234
/-! Multiplicative operations can be defined at the level of pre-games,
241235
but to prove their properties we need to use the abelian group structure of games.
@@ -392,7 +386,7 @@ def mulCommRelabelling (x y : PGame.{u}) : x * y ≡r y * x :=
392386
termination_by (x, y)
393387

394388
theorem quot_mul_comm (x y : PGame.{u}) : (⟦x * y⟧ : Game) = ⟦y * x⟧ :=
395-
Quot.sound (mulCommRelabelling x y).equiv
389+
game_eq (mulCommRelabelling x y).equiv
396390

397391
/-- `x * y` is equivalent to `y * x`. -/
398392
theorem mul_comm_equiv (x y : PGame) : x * y ≈ y * x :=
@@ -421,8 +415,8 @@ theorem mul_zero_equiv (x : PGame) : x * 0 ≈ 0 :=
421415
(mulZeroRelabelling x).equiv
422416

423417
@[simp]
424-
theorem quot_mul_zero (x : PGame) : (⟦x * 0⟧ : Game) = ⟦0⟧ :=
425-
@Quotient.sound _ _ (x * 0) _ x.mul_zero_equiv
418+
theorem quot_mul_zero (x : PGame) : (⟦x * 0⟧ : Game) = 0 :=
419+
game_eq x.mul_zero_equiv
426420

427421
/-- `0 * x` has exactly the same moves as `0`. -/
428422
def zeroMulRelabelling (x : PGame) : 0 * x ≡r 0 :=
@@ -433,8 +427,8 @@ theorem zero_mul_equiv (x : PGame) : 0 * x ≈ 0 :=
433427
(zeroMulRelabelling x).equiv
434428

435429
@[simp]
436-
theorem quot_zero_mul (x : PGame) : (⟦0 * x⟧ : Game) = ⟦0⟧ :=
437-
@Quotient.sound _ _ (0 * x) _ x.zero_mul_equiv
430+
theorem quot_zero_mul (x : PGame) : (⟦0 * x⟧ : Game) = 0 :=
431+
game_eq x.zero_mul_equiv
438432

439433
/-- `-x * y` and `-(x * y)` have the same moves. -/
440434
def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
@@ -457,15 +451,15 @@ def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
457451

458452
@[simp]
459453
theorem quot_neg_mul (x y : PGame) : (⟦-x * y⟧ : Game) = -⟦x * y⟧ :=
460-
Quot.sound (negMulRelabelling x y).equiv
454+
game_eq (negMulRelabelling x y).equiv
461455

462456
/-- `x * -y` and `-(x * y)` have the same moves. -/
463457
def mulNegRelabelling (x y : PGame) : x * -y ≡r -(x * y) :=
464458
(mulCommRelabelling x _).trans <| (negMulRelabelling _ x).trans (mulCommRelabelling y x).negCongr
465459

466460
@[simp]
467461
theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
468-
Quot.sound (mulNegRelabelling x y).equiv
462+
game_eq (mulNegRelabelling x y).equiv
469463

470464
theorem quot_neg_mul_neg (x y : PGame) : ⟦-x * -y⟧ = (⟦x * y⟧ : Game) := by simp
471465

@@ -607,7 +601,7 @@ def mulOneRelabelling : ∀ x : PGame.{u}, x * 1 ≡r x
607601

608602
@[simp]
609603
theorem quot_mul_one (x : PGame) : (⟦x * 1⟧ : Game) = ⟦x⟧ :=
610-
Quot.sound <| PGame.Relabelling.equiv <| mulOneRelabelling x
604+
game_eq <| PGame.Relabelling.equiv <| mulOneRelabelling x
611605

612606
/-- `x * 1` is equivalent to `x`. -/
613607
theorem mul_one_equiv (x : PGame) : x * 1 ≈ x :=
@@ -619,7 +613,7 @@ def oneMulRelabelling (x : PGame) : 1 * x ≡r x :=
619613

620614
@[simp]
621615
theorem quot_one_mul (x : PGame) : (⟦1 * x⟧ : Game) = ⟦x⟧ :=
622-
Quot.sound <| PGame.Relabelling.equiv <| oneMulRelabelling x
616+
game_eq <| PGame.Relabelling.equiv <| oneMulRelabelling x
623617

624618
/-- `1 * x` is equivalent to `x`. -/
625619
theorem one_mul_equiv (x : PGame) : 1 * x ≈ x :=

‎Mathlib/SetTheory/Game/Impartial.lean‎

Lines changed: 52 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -25,13 +25,12 @@ open scoped PGame
2525
namespace PGame
2626

2727
/-- The definition for an impartial game, defined using Conway induction. -/
28-
def ImpartialAux : PGame → Prop
29-
| G => (G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
30-
termination_by G => G -- Porting note: Added `termination_by`
28+
def ImpartialAux (G : PGame) : Prop :=
29+
(G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
30+
termination_by G
3131

32-
theorem impartialAux_def {G : PGame} :
33-
G.ImpartialAux ↔
34-
(G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j) := by
32+
theorem impartialAux_def {G : PGame} : G.ImpartialAux ↔
33+
(G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j) := by
3534
rw [ImpartialAux]
3635

3736
/-- A typeclass on impartial games. -/
@@ -47,18 +46,20 @@ theorem impartial_def {G : PGame} :
4746

4847
namespace Impartial
4948

50-
instance impartial_zero : Impartial 0 := by rw [impartial_def]; dsimp; simp
49+
instance impartial_zero : Impartial 0 := by
50+
rw [impartial_def]
51+
simp
5152

5253
instance impartial_star : Impartial star := by
53-
rw [impartial_def]; simpa using Impartial.impartial_zero
54+
rw [impartial_def]
55+
simpa using Impartial.impartial_zero
5456

5557
theorem neg_equiv_self (G : PGame) [h : G.Impartial] : G ≈ -G :=
5658
(impartial_def.1 h).1
5759

58-
-- Porting note: Changed `-⟦G⟧` to `-(⟦G⟧ : Quotient setoid)`
5960
@[simp]
60-
theorem mk'_neg_equiv_self (G : PGame) [G.Impartial] : -(⟦G⟧ : Quotient setoid) = ⟦G⟧ :=
61-
Quot.sound (Equiv.symm (neg_equiv_self G))
61+
theorem mk'_neg_equiv_self (G : PGame) [G.Impartial] : -(⟦G⟧ : Game) = ⟦G⟧ :=
62+
game_eq (Equiv.symm (neg_equiv_self G))
6263

6364
instance moveLeft_impartial {G : PGame} [h : G.Impartial] (i : G.LeftMoves) :
6465
(G.moveLeft i).Impartial :=
@@ -68,49 +69,47 @@ instance moveRight_impartial {G : PGame} [h : G.Impartial] (j : G.RightMoves) :
6869
(G.moveRight j).Impartial :=
6970
(impartial_def.1 h).2.2 j
7071

71-
theorem impartial_congr : ∀ {G H : PGame} (_ : G ≡r H) [G.Impartial], H.Impartial
72-
| G, H => fun e => by
73-
intro h
74-
exact impartial_def.2
75-
⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)),
76-
fun i => impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
77-
termination_by G H => (G, H)
78-
79-
instance impartial_add : ∀ (G H : PGame) [G.Impartial] [H.Impartial], (G + H).Impartial
80-
| G, H, _, _ => by
81-
rw [impartial_def]
82-
refine ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _))
83-
(Equiv.symm (negAddRelabelling _ _).equiv), fun k => ?_, fun k => ?_⟩
84-
· apply leftMoves_add_cases k
85-
all_goals
86-
intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
87-
apply impartial_add
88-
· apply rightMoves_add_cases k
89-
all_goals
90-
intro i; simp only [add_moveRight_inl, add_moveRight_inr]
91-
apply impartial_add
92-
termination_by G H => (G, H)
93-
94-
instance impartial_neg : ∀ (G : PGame) [G.Impartial], (-G).Impartial
95-
| G, _ => by
96-
rw [impartial_def]
97-
refine ⟨?_, fun i => ?_, fun i => ?_⟩
98-
· rw [neg_neg]
99-
exact Equiv.symm (neg_equiv_self G)
100-
· rw [moveLeft_neg']
101-
apply impartial_neg
102-
· rw [moveRight_neg']
103-
apply impartial_neg
104-
termination_by G => G
72+
theorem impartial_congr {G H : PGame} (e : G ≡r H) [G.Impartial] : H.Impartial :=
73+
impartial_def.2
74+
⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)),
75+
fun i => impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
76+
termination_by G
77+
78+
instance impartial_add (G H : PGame) [G.Impartial] [H.Impartial] : (G + H).Impartial := by
79+
rw [impartial_def]
80+
refine ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _))
81+
(Equiv.symm (negAddRelabelling _ _).equiv), fun k => ?_, fun k => ?_⟩
82+
· apply leftMoves_add_cases k
83+
all_goals
84+
intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
85+
apply impartial_add
86+
· apply rightMoves_add_cases k
87+
all_goals
88+
intro i; simp only [add_moveRight_inl, add_moveRight_inr]
89+
apply impartial_add
90+
termination_by (G, H)
91+
92+
instance impartial_neg (G : PGame) [G.Impartial] : (-G).Impartial := by
93+
rw [impartial_def]
94+
refine ⟨?_, fun i => ?_, fun i => ?_⟩
95+
· rw [neg_neg]
96+
exact Equiv.symm (neg_equiv_self G)
97+
· rw [moveLeft_neg']
98+
exact impartial_neg _
99+
· rw [moveRight_neg']
100+
exact impartial_neg _
101+
termination_by G
105102

106103
variable (G : PGame) [Impartial G]
107104

108-
theorem nonpos : ¬0 < G := fun h => by
105+
theorem nonpos : ¬0 < G := by
106+
intro h
109107
have h' := neg_lt_neg_iff.2 h
110108
rw [neg_zero, lt_congr_left (Equiv.symm (neg_equiv_self G))] at h'
111109
exact (h.trans h').false
112110

113-
theorem nonneg : ¬G < 0 := fun h => by
111+
theorem nonneg : ¬G < 0 := by
112+
intro h
114113
have h' := neg_lt_neg_iff.2 h
115114
rw [neg_zero, lt_congr_right (Equiv.symm (neg_equiv_self G))] at h'
116115
exact (h.trans h').false
@@ -134,22 +133,19 @@ theorem not_fuzzy_zero_iff : ¬G ‖ 0 ↔ (G ≈ 0) :=
134133
theorem add_self : G + G ≈ 0 :=
135134
Equiv.trans (add_congr_left (neg_equiv_self G)) (neg_add_cancel_equiv G)
136135

137-
-- Porting note: Changed `⟦G⟧` to `(⟦G⟧ : Quotient setoid)`
138136
@[simp]
139-
theorem mk'_add_self : (⟦G⟧ : Quotient setoid) + ⟦G⟧ = 0 :=
140-
Quot.sound (add_self G)
137+
theorem mk'_add_self : (⟦G⟧ : Game) + ⟦G⟧ = 0 :=
138+
game_eq (add_self G)
141139

142140
/-- This lemma doesn't require `H` to be impartial. -/
143141
theorem equiv_iff_add_equiv_zero (H : PGame) : (H ≈ G) ↔ (H + G ≈ 0) := by
144-
rw [equiv_iff_game_eq, ← @add_right_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
145-
equiv_iff_game_eq]
146-
rfl
142+
rw [equiv_iff_game_eq, ← add_right_cancel_iff (a := ⟦G⟧), mk'_add_self, ← quot_add,
143+
equiv_iff_game_eq, quot_zero]
147144

148145
/-- This lemma doesn't require `H` to be impartial. -/
149146
theorem equiv_iff_add_equiv_zero' (H : PGame) : (G ≈ H) ↔ (G + H ≈ 0) := by
150-
rw [equiv_iff_game_eq, ← @add_left_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
151-
equiv_iff_game_eq]
152-
exact ⟨Eq.symm, Eq.symm⟩
147+
rw [equiv_iff_game_eq, ← add_left_cancel_iff, mk'_add_self, ← quot_add, equiv_iff_game_eq,
148+
Eq.comm, quot_zero]
153149

154150
theorem le_zero_iff {G : PGame} [G.Impartial] : G ≤ 0 ↔ 0 ≤ G := by
155151
rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]

0 commit comments

Comments
 (0)