Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-17 18:02 b41277c7

View on Github →

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

Estimated changes

added theorem exists_pempty
added theorem forall_pempty
deleted theorem nonempty_pempty
added theorem not_nonempty_pempty
added def game.add
added theorem game.add_assoc
added theorem game.add_comm
added theorem game.add_le_add_left
added theorem game.add_left_neg
added theorem game.add_zero
added def game.le
added theorem game.le_antisymm
added theorem game.le_refl
added theorem game.le_trans
added def game.lt
added def game.neg
added theorem game.not_le
added theorem game.zero_add
added def game
added def pgame.add
added theorem pgame.add_assoc_equiv
added theorem pgame.add_comm_equiv
added theorem pgame.add_comm_le
added theorem pgame.add_congr
added theorem pgame.add_le_add_left
added theorem pgame.add_le_add_right
added theorem pgame.add_lt_add_left
added theorem pgame.add_lt_add_right
added def pgame.equiv
added theorem pgame.equiv_refl
added theorem pgame.equiv_symm
added theorem pgame.equiv_trans
added theorem pgame.le_congr
added theorem pgame.le_def
added theorem pgame.le_def_lt
added theorem pgame.le_iff_neg_ge
added def pgame.le_lt
added theorem pgame.le_of_restricted
added theorem pgame.le_refl
added theorem pgame.le_trans
added theorem pgame.le_trans_aux
added theorem pgame.le_zero
added def pgame.left_moves
added theorem pgame.left_moves_mk
added theorem pgame.lt_congr
added theorem pgame.lt_def
added theorem pgame.lt_def_le
added theorem pgame.lt_iff_neg_gt
added theorem pgame.lt_iff_sub_pos
added theorem pgame.lt_irrefl
added theorem pgame.lt_mk_of_le
added theorem pgame.lt_of_le_mk
added theorem pgame.lt_of_le_of_lt
added theorem pgame.lt_of_lt_of_le
added theorem pgame.lt_of_mk_le
added theorem pgame.lt_zero
added theorem pgame.mk_le_mk
added theorem pgame.mk_lt_mk
added theorem pgame.mk_lt_of_le
added def pgame.move_left
added theorem pgame.move_left_mk
added def pgame.move_right
added theorem pgame.move_right_mk
added theorem pgame.ne_of_lt
added def pgame.neg
added theorem pgame.neg_add_le
added theorem pgame.neg_congr
added theorem pgame.neg_def
added theorem pgame.neg_neg
added theorem pgame.neg_zero
added theorem pgame.not_le
added theorem pgame.not_le_lt
added theorem pgame.not_lt
added def pgame.of_lists
added def pgame.omega
added theorem pgame.one_left_moves
added theorem pgame.one_move_left
added theorem pgame.one_right_moves
added def pgame.relabel
added inductive pgame.relabelling
added inductive pgame.restricted
added theorem pgame.right_moves_mk
added def pgame.star
added theorem pgame.star_lt_zero
added inductive pgame.subsequent
added theorem pgame.wf_subsequent
added theorem pgame.zero_le
added theorem pgame.zero_left_moves
added theorem pgame.zero_lt
added theorem pgame.zero_lt_star
added theorem pgame.zero_right_moves
added inductive pgame
deleted def pSurreal.add
deleted def pSurreal.equiv
deleted theorem pSurreal.equiv_refl
deleted theorem pSurreal.equiv_symm
deleted theorem pSurreal.equiv_trans
deleted def pSurreal.inv'
deleted def pSurreal.inv_val
deleted theorem pSurreal.le_congr
deleted def pSurreal.le_lt
deleted theorem pSurreal.le_of_lt
deleted theorem pSurreal.le_refl
deleted theorem pSurreal.le_trans
deleted theorem pSurreal.le_trans_aux
deleted theorem pSurreal.lt_asymm
deleted theorem pSurreal.lt_congr
deleted theorem pSurreal.lt_iff_le_not_le
deleted theorem pSurreal.lt_irrefl
deleted theorem pSurreal.lt_mk_of_le
deleted theorem pSurreal.lt_of_le_mk
deleted theorem pSurreal.lt_of_mk_le
deleted theorem pSurreal.mk_le_mk
deleted theorem pSurreal.mk_lt_mk
deleted theorem pSurreal.mk_lt_of_le
deleted def pSurreal.mul
deleted theorem pSurreal.ne_of_lt
deleted def pSurreal.neg
deleted theorem pSurreal.not_le
deleted theorem pSurreal.not_le_lt
deleted theorem pSurreal.not_lt
deleted def pSurreal.ok
deleted theorem pSurreal.ok_rec
deleted def pSurreal.omega
deleted inductive pSurreal.{u}
added theorem pgame.add_lt_add
added def pgame.inv'
added inductive pgame.inv_ty
added def pgame.inv_val
added theorem pgame.le_of_lt
added theorem pgame.lt_asymm
added theorem pgame.lt_iff_le_not_le
added def pgame.mul
added def pgame.numeric
added theorem pgame.numeric_add
added theorem pgame.numeric_neg
added theorem pgame.numeric_one
added theorem pgame.numeric_rec
added theorem pgame.numeric_zero
added def surreal.add
added theorem surreal.add_assoc
modified def surreal.equiv
modified def surreal.lift
modified def surreal.lift₂
modified def surreal.mk
deleted inductive {u}