feat(set_theory/game/pgame): define pgame.identical pgame.memₗ pgame.memᵣ

src/set_theory/game/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Apurva Nakade
+Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Apurva Nakade, Yuyang Zhao
 -/
 import set_theory.game.pgame
 import tactic.abel
@@ -146,7 +146,7 @@ but to prove their properties we need to use the abelian group structure of game
 Hence we define them here. -/
 
 /-- The product of `x = {xL | xR}` and `y = {yL | yR}` is
-`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, x*yL + xR*y - xR*yL }`. -/
+`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL}`. -/
 instance : has_mul pgame.{u} :=
 ⟨λ x y, begin
   induction x with xl xr xL xR IHxl IHxr generalizing y,
@@ -263,6 +263,57 @@ begin
   { apply hr }
 end
 
+lemma exists_left_moves_mul {x y : pgame.{u}} {p : (x * y).left_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i j, p (to_left_moves_mul (sum.inl (i, j)))) ∨
+    (∃ i j, p (to_left_moves_mul (sum.inr (i, j)))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨i, j, hi⟩, or.inr ⟨i, j, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨_, h⟩, ⟨_, h⟩], },
+end
+
+lemma exists_right_moves_mul {x y : pgame.{u}} {p : (x * y).right_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i j, p (to_right_moves_mul (sum.inl (i, j)))) ∨
+    (∃ i j, p (to_right_moves_mul (sum.inr (i, j)))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨i, j, hi⟩, or.inr ⟨i, j, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨_, h⟩, ⟨_, h⟩], },
+end
+
+lemma memₗ_mul_iff : Π {x y₁ y₂ : pgame},
+  x ∈ₗ y₁ * y₂ ↔
+    (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_left j - y₁.move_left i * y₂.move_left j) ∨
+    (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_right j - y₁.move_right i * y₂.move_right j)
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_left_moves_mul
+
+lemma memᵣ_mul_iff : Π {x y₁ y₂ : pgame},
+  x ∈ᵣ y₁ * y₂ ↔
+    (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_right j - y₁.move_left i * y₂.move_right j) ∨
+    (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_left j - y₁.move_right i * y₂.move_left j)
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_mul
+
+/-- `x * y` and `y * x` have the same moves. -/
+protected lemma mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
+| ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_mul_iff], dsimp, rw [@exists_comm xl, @exists_comm xr],
+    simp_rw [((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xL _).add_comm _)).sub
+        (mul_comm _ _)).congr_right,
+      ((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xR _).add_comm _)).sub
+        (mul_comm _ _)).congr_right], },
+  { simp_rw [memᵣ_mul_iff], dsimp, rw [@exists_comm xl, @exists_comm xr, or.comm],
+    simp_rw [((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xL _).add_comm _)).sub
+        (mul_comm _ _)).congr_right,
+      ((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xR _).add_comm _)).sub
+        (mul_comm _ _)).congr_right], },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
 /-- `x * y` and `y * x` have the same moves. -/
 def mul_comm_relabelling : Π (x y : pgame.{u}), x * y ≡r y * x
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
@@ -291,6 +342,9 @@ by { cases x, apply sum.is_empty }
 instance is_empty_zero_mul_right_moves (x : pgame.{u}) : is_empty (0 * x).right_moves :=
 by { cases x, apply sum.is_empty }
 
+/-- `x * 0` has exactly the same moves as `0`. -/
+protected lemma mul_zero (x : pgame) : x * 0 ≡ 0 := identical_zero _
+
 /-- `x * 0` has exactly the same moves as `0`. -/
 def mul_zero_relabelling (x : pgame) : x * 0 ≡r 0 := relabelling.is_empty _
 
@@ -300,6 +354,9 @@ theorem mul_zero_equiv (x : pgame) : x * 0 ≈ 0 := (mul_zero_relabelling x).equ
 @[simp] theorem quot_mul_zero (x : pgame) : ⟦x * 0⟧ = ⟦0⟧ :=
 @quotient.sound _ _ (x * 0) _ x.mul_zero_equiv
 
+/-- `0 * x` has exactly the same moves as `0`. -/
+protected lemma zero_mul (x : pgame) : 0 * x ≡ 0 := identical_zero _
+
 /-- `0 * x` has exactly the same moves as `0`. -/
 def zero_mul_relabelling (x : pgame) : 0 * x ≡r 0 := relabelling.is_empty _
 
@@ -321,6 +378,39 @@ def neg_mul_relabelling : Π (x y : pgame.{u}), -x * y ≡r -(x * y)
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+/-- `x * -y` and `-(x * y)` have the same moves. -/
+lemma mul_neg : Π (x y : pgame.{u}), x * -y = -(x * y)
+| (mk xl xr xL xR) (mk yl yr yL yR) := begin
+  refine ext rfl rfl _ _,
+  { rintros (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩,
+    { refine (@mul_move_left_inl (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], },
+    { refine (@mul_move_left_inr (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], }, },
+  { rintros (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩,
+    { refine (@mul_move_right_inl (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], },
+    { refine (@mul_move_right_inr (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], }, },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+/-- `-x * y` and `-(x * y)` have the same moves. -/
+lemma neg_mul (x y : pgame.{u}) : -x * y ≡ -(x * y) :=
+((pgame.mul_comm _ _).trans (of_eq (mul_neg _ _))).trans (pgame.mul_comm _ _).neg
+
 @[simp] theorem quot_neg_mul (x y : pgame) : ⟦-x * y⟧ = -⟦x * y⟧ :=
 quot.sound (neg_mul_relabelling x y).equiv
 
@@ -408,11 +498,29 @@ def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
   try { rintro (⟨i, ⟨ ⟩⟩ | ⟨i, ⟨ ⟩⟩) }; try { intro i };
   dsimp;
   apply (relabelling.sub_congr (relabelling.refl _) (mul_zero_relabelling _)).trans;
-  rw sub_zero;
+  rw sub_zero_eq_add_zero;
   exact (add_zero_relabelling _).trans (((mul_one_relabelling _).add_congr
     (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
 end
 
+/-- `1 * x` has the same moves as `x`. -/
+lemma one_mul : Π (x : pgame.{u}), 1 * x ≡ x
+| ⟨xl, xr, xL, xR⟩ := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_mul_iff], dsimp, simp_rw [is_empty.exists_iff, or_false, exists_const],
+    simp_rw [(((((pgame.zero_mul _).add (one_mul _)).trans (pgame.zero_add _)).sub
+      (xL _).zero_mul).trans (pgame.sub_zero _)).congr_right],
+    refl, },
+  { simp_rw [memᵣ_mul_iff], dsimp, simp_rw [is_empty.exists_iff, or_false, exists_const],
+    simp_rw [(((((pgame.zero_mul _).add (one_mul _)).trans (pgame.zero_add _)).sub
+      (xR _).zero_mul).trans (pgame.sub_zero _)).congr_right],
+    refl, },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+/-- `x * 1` has the same moves as `x`. -/
+lemma mul_one (x : pgame.{u}) : x * 1 ≡ x := (x.mul_comm _).trans x.one_mul
+
 @[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
 
 /-- `x * 1` is equivalent to `x`. -/
@@ -553,6 +661,15 @@ def inv' : pgame → pgame
 theorem zero_lf_inv' : ∀ (x : pgame), 0 ⧏ inv' x
 | ⟨xl, xr, xL, xR⟩ := by { convert lf_mk _ _ inv_ty.zero, refl }
 
+/-- `inv' 0` has exactly the same moves as `1`. -/
+lemma inv'_zero' : inv' 0 ≡ (1 : pgame.{u}) :=
+begin
+  refine ⟨_, _⟩,
+  { simp_rw [unique.forall_iff, unique.exists_iff, and_self, pgame.inv_val_is_empty],
+    exact identical_zero _, },
+  { simp_rw [is_empty.forall_iff, and_self], },
+end
+
 /-- `inv' 0` has exactly the same moves as `1`. -/
 def inv'_zero : inv' 0 ≡r 1 :=
 begin
@@ -569,6 +686,19 @@ end
 
 theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
 
+universe v
+
+/-- `inv' 1` has exactly the same moves as `1`. -/
+lemma inv'_one' : inv'.{u} 1 ≡ 1 :=
+begin
+  haveI inst : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
+  { rw lt_self_iff_false, apply_instance },
+  refine ⟨_, _⟩,
+  { simp_rw [unique.forall_iff, unique.exists_iff, pgame.inv_val_is_empty, and_self],
+    exact identical_zero _, },
+  { simp_rw [is_empty.forall_iff, and_true], },
+end
+
 /-- `inv' 1` has exactly the same moves as `1`. -/
 def inv'_one : inv' 1 ≡r (1 : pgame.{u}) :=
 begin
@@ -602,6 +732,10 @@ by { classical, exact (if_neg h.lf.not_equiv').trans (if_pos h) }
 theorem inv_eq_of_lf_zero {x : pgame} (h : x ⧏ 0) : x⁻¹ = -inv' (-x) :=
 by { classical, exact (if_neg h.not_equiv).trans (if_neg h.not_gt) }
 
+/-- `1⁻¹` has exactly the same moves as `1`. -/
+lemma inv_one' : 1⁻¹ ≡ 1 :=
+by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one' }
+
 /-- `1⁻¹` has exactly the same moves as `1`. -/
 def inv_one : 1⁻¹ ≡r 1 :=
 by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one }