feat(set_theory/game): the theory of combinatorial games (#1274)

* correcting definition of addition, and splitting content into two files, one about games, one about surreals

* add_le_zero_of_le_zero, but without well-foundedness

* progress

* Mario's well-foundedness proof

* getting there!

* success!

* minor

* almost there

* progress

* off to write some tactics

* not quite there

* hmmm

* getting there!

* domineering is hard

* removing unneeded theorems

* cleanup

* add_semigroup surreal

* cleanup

* short proof

* cleaning up

* remove equiv_rw

* move lemmas about pempty to logic.basic

* slightly more comments; still lots to go

* documentation

* finishing documentation

* typo

* Update src/logic/basic.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* fix references

* oops

* change statement of equiv.refl_symm

* more card_erase lemmas; golf domineering proofs

* style changes

* fix comment

* fixes after Reid's review

* some improvements

* golfing

* subsingleton short

* diagnosing decidable

* hmmmhmmm

* computational domineering

* fix missing proofs (need golfing?)

* minor

* short_of_relabelling

* abbreviating

* various minor

* removing short games and domineering from this PR

* style / proof simplification / golfing

* some minor golfing

* adding Reid to the author line

* add @[simp]

* adding two lemmas characterising the order relation

* separating out game and pgame, and discarding lame lemmas

* comment

* fixes

Author: kim-em

docs/references.bib

@@ -4,6 +4,23 @@
 %                                                                     %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+@article {MR1167694,
+    AUTHOR = {Blass, Andreas},
+     TITLE = {A game semantics for linear logic},
+   JOURNAL = {Ann. Pure Appl. Logic},
+  FJOURNAL = {Annals of Pure and Applied Logic},
+    VOLUME = {56},
+      YEAR = {1992},
+    NUMBER = {1-3},
+     PAGES = {183--220},
+      ISSN = {0168-0072},
+   MRCLASS = {03B70 (68Q55)},
+  MRNUMBER = {1167694},
+MRREVIEWER = {Fangmin Song},
+       DOI = {10.1016/0168-0072(92)90073-9},
+       URL = {https://doi.org/10.1016/0168-0072(92)90073-9},
+}
+
 @book {bourbaki1966,
     AUTHOR = {Bourbaki, Nicolas},
      TITLE = {Elements of mathematics. {G}eneral topology. {P}art 1},
@@ -15,6 +32,18 @@ @book {bourbaki1966
   MRNUMBER = {0205210},
 }
 
+@book {conway2001,
+    AUTHOR = {Conway, J. H.},
+     TITLE = {On numbers and games},
+   EDITION = {Second},
+ PUBLISHER = {A K Peters, Ltd., Natick, MA},
+      YEAR = {2001},
+     PAGES = {xii+242},
+      ISBN = {1-56881-127-6},
+   MRCLASS = {00A08 (05-01 91A05)},
+  MRNUMBER = {1803095},
+}
+
 @book {gouvea1997,
     AUTHOR = {Gouv\^{e}a, Fernando Q.},
      TITLE = {{$p$}-adic numbers},
@@ -48,9 +77,20 @@ @book {james1999
        URL = {https://doi.org/10.1007/978-1-4471-3994-2},
 }
 
+@article {joyal1977,
+ author = {André Joyal},
+ title = {Remarques sur la théorie des jeux à deux personnes},
+ journal = {Gazette des Sciences Mathematiques du Québec},
+ volume = {1},
+ number = {4},
+ pages = {46--52},
+ year = {1977},
+ note = {(English translation at https://bosker.files.wordpress.com/2010/12/joyal-games.pdf)}
+}
+
 @inproceedings{lewis2019,
  author = {Lewis, Robert Y.},
- title = {A Formal Proof of Hensel\&\#39;s Lemma over the P-adic Integers},
+ title = {A Formal Proof of {H}ensel's Lemma over the {$p$}-adic Integers},
  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  series = {CPP 2019},
  year = {2019},
@@ -63,7 +103,7 @@ @inproceedings{lewis2019
  acmid = {3294089},
  publisher = {ACM},
  address = {New York, NY, USA},
- keywords = {Hensel\&\#39;s lemma, Lean, formal proof, p-adic},
+ keywords = {Hensel's lemma, Lean, formal proof, p-adic},
 }
 
 @book {riehl2017,

src/algebra/ordered_group.lean

@@ -470,6 +470,29 @@ by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
 end ordered_cancel_comm_monoid
 
 section ordered_comm_group
+
+/--
+The `add_lt_add_left` field of `ordered_comm_group` is redundant, but it is in core so
+we can't remove it for now. This alternative constructor is the best we can do.
+-/
+def ordered_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
+  (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) :
+  ordered_comm_group α :=
+{ add_le_add_left := add_le_add_left,
+  add_lt_add_left := λ a b h c,
+  begin
+    rw lt_iff_le_not_le at h,
+    rw lt_iff_le_not_le,
+    split,
+    { apply add_le_add_left _ _ h.1 },
+    { intro w,
+      replace w : -c + (c + b) ≤ -c + (c + a) := add_le_add_left _ _ w _,
+      simp only [add_zero, add_comm, add_left_neg, add_left_comm] at w,
+      exact h.2 w },
+  end,
+  ..(by apply_instance : add_comm_group α),
+  ..(by apply_instance : partial_order α)  }
+
 variables [ordered_comm_group α] {a b c : α}
 
 lemma neg_neg_iff_pos {α : Type} [_inst_1 : ordered_comm_group α] {a : α} : -a < 0 ↔ 0 < a :=

src/data/equiv/basic.lean

@@ -112,6 +112,8 @@ lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
 
 @[simp] theorem trans_refl (e : α ≃ β) : e.trans (equiv.refl β) = e := by { cases e, refl }
 
+@[simp] theorem refl_symm : (equiv.refl α).symm = equiv.refl α := rfl
+
 @[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }
 
 @[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β :=  ext _ _ (by simp)
@@ -348,6 +350,10 @@ by { cases e₁, cases e₂, refl }
   sum_congr e₁ e₂ (inr b) = inr (e₂ b) :=
 by { cases e₁, cases e₂, refl }
 
+@[simp] lemma sum_congr_symm {α β γ δ : Type u} (e : α ≃ β) (f : γ ≃ δ) (x) :
+  (equiv.sum_congr e f).symm x = (equiv.sum_congr (e.symm) (f.symm)) x :=
+by { cases e, cases f, cases x; refl }
+
 def bool_equiv_punit_sum_punit : bool ≃ punit.{u+1} ⊕ punit.{v+1} :=
 ⟨λ b, cond b (inr punit.star) (inl punit.star),
  λ s, sum.rec_on s (λ_, ff) (λ_, tt),

src/data/finset.lean

@@ -1002,6 +1002,9 @@ card_eq_zero.trans val_eq_zero
 theorem card_pos {s : finset α} : 0 < card s ↔ s ≠ ∅ :=
 pos_iff_ne_zero.trans $ not_congr card_eq_zero
 
+theorem card_ne_zero_of_mem {s : finset α} {a : α} (h : a ∈ s) : card s ≠ 0 :=
+(not_congr card_eq_zero).2 (ne_empty_of_mem h)
+
 theorem card_eq_one {s : finset α} : s.card = 1 ↔ ∃ a, s = finset.singleton a :=
 by cases s; simp [multiset.card_eq_one, finset.singleton, finset.card]
 
@@ -1018,6 +1021,10 @@ rw [card_insert_of_not_mem h]]
 
 theorem card_erase_of_mem [decidable_eq α] {a : α} {s : finset α} : a ∈ s → card (erase s a) = pred (card s) := card_erase_of_mem
 
+theorem card_erase_lt_of_mem [decidable_eq α] {a : α} {s : finset α} : a ∈ s → card (erase s a) < card s := card_erase_lt_of_mem
+
+theorem card_erase_le [decidable_eq α] {a : α} {s : finset α} : card (erase s a) ≤ card s := card_erase_le
+
 @[simp] theorem card_range (n : ℕ) : card (range n) = n := card_range n
 
 @[simp] theorem card_attach {s : finset α} : card (attach s) = card s := multiset.card_attach

src/data/multiset.lean

@@ -534,9 +534,6 @@ theorem le_cons_erase (s : multiset α) (a : α) : s ≤ a :: s.erase a :=
 if h : a ∈ s then le_of_eq (cons_erase h).symm
 else by rw erase_of_not_mem h; apply le_cons_self
 
-@[simp] theorem card_erase_of_mem {a : α} {s : multiset α} : a ∈ s → card (s.erase a) = pred (card s) :=
-quot.induction_on s $ λ l, length_erase_of_mem
-
 theorem erase_add_left_pos {a : α} {s : multiset α} (t) : a ∈ s → (s + t).erase a = s.erase a + t :=
 quotient.induction_on₂ s t $ λ l₁ l₂ h, congr_arg coe $ erase_append_left l₂ h
 
@@ -577,6 +574,15 @@ theorem erase_le_iff_le_cons {s t : multiset α} {a : α} : s.erase a ≤ t ↔
   then by rw ← cons_erase m at h; exact (cons_le_cons_iff _).1 h
   else le_trans (erase_le _ _) ((le_cons_of_not_mem m).1 h)⟩
 
+@[simp] theorem card_erase_of_mem {a : α} {s : multiset α} : a ∈ s → card (s.erase a) = pred (card s) :=
+quot.induction_on s $ λ l, length_erase_of_mem
+
+theorem card_erase_lt_of_mem {a : α} {s : multiset α} : a ∈ s → card (s.erase a) < card s :=
+λ h, card_lt_of_lt (erase_lt.mpr h)
+
+theorem card_erase_le {a : α} {s : multiset α} : card (s.erase a) ≤ card s :=
+card_le_of_le (erase_le a s)
+
 end erase
 
 @[simp] theorem coe_reverse (l : list α) : (reverse l : multiset α) = l :=

src/linear_algebra/dimension.lean

@@ -115,7 +115,7 @@ cardinal.lift_inj.1 $ hb.mk_eq_dim.symm.trans (f.is_basis hb).mk_eq_dim
 
 @[simp] lemma dim_bot : dim α (⊥ : submodule α β) = 0 :=
 by letI := classical.dec_eq β;
-  rw [← cardinal.lift_inj, ← (@is_basis_empty_bot pempty α β _ _ _ _ _ _ nonempty_pempty).mk_eq_dim,
+  rw [← cardinal.lift_inj, ← (@is_basis_empty_bot pempty α β _ _ _ _ _ _ not_nonempty_pempty).mk_eq_dim,
     cardinal.mk_pempty]
 
 @[simp] lemma dim_top : dim α (⊤ : submodule α β) = dim α β :=

src/logic/basic.lean

@@ -2,19 +2,17 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
+-/
 
+/-!
 Theorems that require decidability hypotheses are in the namespace "decidable".
 Classical versions are in the namespace "classical".
 
 Note: in the presence of automation, this whole file may be unnecessary. On the other hand,
 maybe it is useful for writing automation.
 -/
 
-/-
-    miscellany
 
-    TODO: move elsewhere
--/
 
 section miscellany
 
@@ -67,15 +65,21 @@ def pempty.elim {C : Sort*} : pempty → C.
 
 instance subsingleton_pempty : subsingleton pempty := ⟨λa, a.elim⟩
 
+@[simp] lemma not_nonempty_pempty : ¬ nonempty pempty :=
+assume ⟨h⟩, h.elim
+
+@[simp] theorem forall_pempty {P : pempty → Prop} : (∀ x : pempty, P x) ↔ true :=
+⟨λ h, trivial, λ h x, by cases x⟩
+
+@[simp] theorem exists_pempty {P : pempty → Prop} : (∃ x : pempty, P x) ↔ false :=
+⟨λ h, by { cases h with w, cases w }, false.elim⟩
+
 lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂
 | a _ rfl := heq.rfl
 
 lemma plift.down_inj {α : Sort*} : ∀ (a b : plift α), a.down = b.down → a = b
 | ⟨a⟩ ⟨b⟩ rfl := rfl
 
-@[simp] lemma nonempty_pempty : ¬ nonempty pempty :=
-assume ⟨h⟩, h.elim
-
 -- missing [symm] attribute for ne in core.
 attribute [symm] ne.symm
 

src/set_theory/game.lean

@@ -0,0 +1,165 @@
+/-
+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
+-/
+import set_theory.pgame
+
+/-!
+# Combinatorial games.
+
+In this file we define the quotient of pre-games by the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤
+p`, and construct an instance `add_comm_group game`, as well as an instance `partial_order game`
+(although note carefully the warning that the `<` field in this instance is not the usual relation
+on combinatorial games).
+-/
+
+universes u
+
+local infix ` ≈ ` := pgame.equiv
+
+instance pgame.setoid : setoid pgame :=
+⟨λ x y, x ≈ y,
+ λ x, pgame.equiv_refl _,
+ λ x y, pgame.equiv_symm,
+ λ x y z, pgame.equiv_trans⟩
+
+/-- The type of combinatorial games. In ZFC, a combinatorial game is constructed from
+  two sets of combinatorial games that have been constructed at an earlier
+  stage. To do this in type theory, we say that a combinatorial pre-game is built
+  inductively from two families of combinatorial games indexed over any type
+  in Type u. The resulting type `pgame.{u}` lives in `Type (u+1)`,
+  reflecting that it is a proper class in ZFC.
+  A combinatorial game is then constructed by quotienting by the equivalence
+  `x ≈ y ↔ x ≤ y ∧ y ≤ x`. -/
+def game := quotient pgame.setoid
+
+open pgame
+
+namespace game
+
+/-- The relation `x ≤ y` on games. -/
+def le : game → game → Prop :=
+quotient.lift₂ (λ x y, x ≤ y) (λ x₁ y₁ x₂ y₂ hx hy, propext (le_congr hx hy))
+
+instance : has_le game :=
+{ le := le }
+
+@[refl] theorem le_refl : ∀ x : game, x ≤ x :=
+by { rintro ⟨x⟩, apply pgame.le_refl }
+@[trans] theorem le_trans : ∀ x y z : game, x ≤ y → y ≤ z → x ≤ z :=
+by { rintro ⟨x⟩ ⟨y⟩ ⟨z⟩, apply pgame.le_trans }
+theorem le_antisymm : ∀ x y : game, x ≤ y → y ≤ x → x = y :=
+by { rintro ⟨x⟩ ⟨y⟩ h₁ h₂, apply quot.sound, exact ⟨h₁, h₂⟩ }
+
+/-- The relation `x < y` on games. -/
+-- We don't yet make this into an instance, because it will conflict with the (incorrect) notion
+-- of `<` provided by `partial_order` later.
+def lt : game → game → Prop :=
+quotient.lift₂ (λ x y, x < y) (λ x₁ y₁ x₂ y₂ hx hy, propext (lt_congr hx hy))
+
+theorem not_le : ∀ {x y : game}, ¬ (x ≤ y) ↔ (lt y x) :=
+by { rintro ⟨x⟩ ⟨y⟩, exact not_le }
+
+instance : has_zero game := ⟨⟦0⟧⟩
+instance : has_one game := ⟨⟦1⟧⟩
+
+/-- The negation of `{L | R}` is `{-R | -L}`. -/
+def neg : game → game :=
+quot.lift (λ x, ⟦-x⟧) (λ x y h, quot.sound (@neg_congr x y h))
+
+instance : has_neg game :=
+{ neg := neg }
+
+/-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
+def add : game → game → game :=
+quotient.lift₂ (λ x y : pgame, ⟦x + y⟧) (λ x₁ y₁ x₂ y₂ hx hy, quot.sound (pgame.add_congr hx hy))
+
+instance : has_add game := ⟨add⟩
+
+theorem add_assoc : ∀ (x y z : game), (x + y) + z = x + (y + z) :=
+begin
+  rintros ⟨x⟩ ⟨y⟩ ⟨z⟩,
+  apply quot.sound,
+  exact add_assoc_equiv
+end
+
+instance : add_semigroup game.{u} :=
+{ add_assoc := add_assoc,
+  ..game.has_add }
+
+theorem add_zero : ∀ (x : game), x + 0 = x :=
+begin
+  rintro ⟨x⟩,
+  apply quot.sound,
+  apply add_zero_equiv
+end
+theorem zero_add : ∀ (x : game), 0 + x = x :=
+begin
+  rintro ⟨x⟩,
+  apply quot.sound,
+  apply zero_add_equiv
+end
+
+instance : add_monoid game :=
+{ add_zero := add_zero,
+  zero_add := zero_add,
+  ..game.has_zero,
+  ..game.add_semigroup }
+
+theorem add_left_neg : ∀ (x : game), (-x) + x = 0 :=
+begin
+  rintro ⟨x⟩,
+  apply quot.sound,
+  apply add_left_neg_equiv
+end
+
+instance : add_group game :=
+{ add_left_neg := add_left_neg,
+  ..game.has_neg,
+  ..game.add_monoid }
+
+theorem add_comm : ∀ (x y : game), x + y = y + x :=
+begin
+  rintros ⟨x⟩ ⟨y⟩,
+  apply quot.sound,
+  exact add_comm_equiv
+end
+
+instance : add_comm_semigroup game :=
+{ add_comm := add_comm,
+  ..game.add_semigroup }
+
+instance : add_comm_group game :=
+{ ..game.add_comm_semigroup,
+  ..game.add_group }
+
+theorem add_le_add_left : ∀ (a b : game), a ≤ b → ∀ (c : game), c + a ≤ c + b :=
+begin rintro ⟨a⟩ ⟨b⟩ h ⟨c⟩, apply pgame.add_le_add_left h, end
+
+-- While it is very tempting to define a `partial_order` on games, and prove
+-- that games form an `ordered_comm_group`, it is a bit dangerous.
+
+-- The relations `≤` and `<` on games do not satisfy
+-- `lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)`
+-- (Consider `a = 0`, `b = star`.)
+-- (`lt_iff_le_not_le` is satisfied by surreal numbers, however.)
+-- Thus we can not use `<` when defining a `partial_order`.
+
+-- Because of this issue, we define the `partial_order` and `ordered_comm_group` instances,
+-- but do not actually mark them as instances, for safety.
+
+/-- The `<` operation provided by this partial order is not the usual `<` on games! -/
+def game_partial_order : partial_order game :=
+{ le_refl := le_refl,
+  le_trans := le_trans,
+  le_antisymm := le_antisymm,
+  ..game.has_le }
+
+local attribute [instance] game_partial_order
+
+/-- The `<` operation provided by this `ordered_comm_group` is not the usual `<` on games! -/
+def ordered_comm_group_game : ordered_comm_group game :=
+ordered_comm_group.mk' add_le_add_left
+
+end game