feat(set_theory/game/basic): Basic lemmas on inv (#13840)

Note that we've redefined `inv` so that `inv x = 0` when `x ≈ 0`. This is because, in order to lift it to an operation on surreals, we need to prove that equivalent numeric games give equivalent numeric values, and this isn't the case otherwise.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

Author: 4 people

src/set_theory/game/basic.lean

@@ -26,6 +26,7 @@ open function pgame
 universes u
 
 local infix ` ≈ ` := pgame.equiv
+local infix ` ⧏ `:50 := pgame.lf
 local infix ` ≡r `:50 := pgame.relabelling
 
 instance pgame.setoid : setoid pgame :=
@@ -501,8 +502,15 @@ inductive inv_ty (l r : Type u) : bool → Type u
 | right₁ : l → inv_ty ff → inv_ty tt
 | right₂ : r → inv_ty tt → inv_ty tt
 
+instance (l r : Type u) [is_empty l] [is_empty r] : is_empty (inv_ty l r tt) :=
+⟨by rintro (_|_|_|a|a); exact is_empty_elim a⟩
+
 instance (l r : Type u) : inhabited (inv_ty l r ff) := ⟨inv_ty.zero⟩
 
+instance unique_inv_ty (l r : Type u) [is_empty l] [is_empty r] : unique (inv_ty l r ff) :=
+{ uniq := by { rintro (a|a|a), refl, all_goals { exact is_empty_elim a } },
+  ..inv_ty.inhabited l r }
+
 /-- Because the two halves of the definition of `inv` produce more elements
 of each side, we have to define the two families inductively.
 This is the function part, defined by recursion on `inv_ty`. -/
@@ -514,6 +522,14 @@ def inv_val {l r} (L : l → pgame) (R : r → pgame)
 | _ (inv_ty.right₁ i j) := (1 + (L i - mk l r L R) * inv_val j) * IHl i
 | _ (inv_ty.right₂ i j) := (1 + (R i - mk l r L R) * inv_val j) * IHr i
 
+@[simp] theorem inv_val_is_empty {l r : Type u} {b} (L R IHl IHr) (i : inv_ty l r b)
+  [is_empty l] [is_empty r] : inv_val L R IHl IHr i = 0 :=
+begin
+  cases i with a _ a _ a _ a,
+  { refl },
+  all_goals { exact is_empty_elim a }
+end
+
 /-- The inverse of a positive surreal number `x = {L | R}` is
 given by `x⁻¹ = {0,
   (1 + (R - x) * x⁻¹L) * R, (1 + (L - x) * x⁻¹R) * L |
@@ -529,10 +545,56 @@ def inv' : pgame → pgame
   ⟨inv_ty l' r ff, inv_ty l' r tt,
     inv_val L' R IHl' IHr, inv_val L' R IHl' IHr⟩
 
-/-- The inverse of a surreal number in terms of the inverse on positive surreals. -/
+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`. -/
+def inv'_zero : inv' 0 ≡r 1 :=
+begin
+  change mk _ _ _ _ ≡r 1,
+  refine ⟨_, _, λ i, _, is_empty_elim⟩; dsimp,
+  { apply equiv.equiv_punit },
+  { apply equiv.equiv_pempty },
+  { simp }
+end
+
+theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
+
+/-- `inv' 1` has exactly the same moves as `1`. -/
+def inv'_one : inv' 1 ≡r (1 : pgame.{u}) :=
+begin
+  change relabelling (mk _ _ _ _) 1,
+  haveI : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
+  { rw lt_self_iff_false, apply_instance },
+  refine ⟨_, _, λ i, _, is_empty_elim⟩; dsimp,
+  { apply equiv.equiv_punit },
+  { apply equiv.equiv_pempty },
+  { simp }
+end
+
+theorem inv'_one_equiv : inv' 1 ≈ 1 := inv'_one.equiv
+
+/-- The inverse of a pre-game in terms of the inverse on positive pre-games. -/
 noncomputable instance : has_inv pgame :=
-⟨by { classical, exact λ x, if x = 0 then 0 else if 0 < x then inv' x else inv' (-x) }⟩
+⟨by { classical, exact λ x, if x ≈ 0 then 0 else if 0 < x then inv' x else -inv' (-x) }⟩
 
 noncomputable instance : has_div pgame := ⟨λ x y, x * y⁻¹⟩
 
+theorem inv_eq_of_equiv_zero {x : pgame} (h : x ≈ 0) : x⁻¹ = 0 := if_pos h
+
+@[simp] theorem inv_zero : (0 : pgame)⁻¹ = 0 :=
+inv_eq_of_equiv_zero (equiv_refl _)
+
+theorem inv_eq_of_pos {x : pgame} (h : 0 < x) : x⁻¹ = inv' x :=
+(if_neg h.lf.not_equiv').trans (if_pos h)
+
+theorem inv_eq_of_lf_zero {x : pgame} (h : x ⧏ 0) : x⁻¹ = -inv' (-x) :=
+(if_neg h.not_equiv).trans (if_neg h.not_gt)
+
+/-- `1⁻¹` has exactly the same moves as `1`. -/
+def inv_one : 1⁻¹ ≡r 1 :=
+by { rw inv_eq_of_pos zero_lt_one, exact inv'_one }
+
+theorem inv_one_equiv : 1⁻¹ ≈ 1 := inv_one.equiv
+
 end pgame