CombinatorialGames.Outcome

source

inductive Outcome :

Type

L : Outcome
Left always wins, regardless of who starts.
N : Outcome
The Next (first) player wins.
P : Outcome
The Previous (second) player wins.
R : Outcome
Right always wins, regardless of who starts.

Instances For

source

@[instance_reducible]

instance instDecidableEqOutcome :

DecidableEq Outcome

Equations

instDecidableEqOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[instance_reducible]

instance Outcome.instLT :

LT Outcome

Game outcomes are partially ordered in favour of Left, as illustrated in the following Hasse diagram:

  L
 / \
N   P
 \ /
  R

Equations

Outcome.instLT = { lt := fun (lhs rhs : Outcome) => lhs ≠ Outcome.L ∧ rhs = Outcome.L ∨ lhs = Outcome.R ∧ rhs = Outcome.N ∨ lhs = Outcome.R ∧ rhs = Outcome.P }

source

@[instance_reducible]

instance Outcome.instDecidableLT :

DecidableLT Outcome

Equations

Outcome.instDecidableLT = id inferInstance

source

@[instance_reducible]

instance Outcome.instLE :

LE Outcome

Equations

Outcome.instLE = { le := fun (lhs rhs : Outcome) => lhs = rhs ∨ lhs < rhs }

source

@[instance_reducible]

instance Outcome.instDecidableLE :

DecidableLE Outcome

Equations

Outcome.instDecidableLE = id inferInstance

source

@[instance_reducible]

instance Outcome.instPreorder :

Preorder Outcome

Equations

Outcome.instPreorder = { toLE := Outcome.instLE, toLT := Outcome.instLT, le_refl := Outcome.instPreorder._proof_3, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

source

@[instance_reducible]

instance Outcome.instPartialOrder :

PartialOrder Outcome

Equations

Outcome.instPartialOrder = { toPreorder := Outcome.instPreorder, le_antisymm := ⋯ }

source

@[simp]

theorem Outcome.ge_R (o : Outcome) :

o ≥ R

source

@[simp]

theorem Outcome.le_R_iff (o : Outcome) :

o ≤ R ↔ o = R

source

@[simp]

theorem Outcome.L_ge (o : Outcome) :

L ≥ o

source

theorem Outcome.ge_P_ge_N_eq_L {o : Outcome} (hp : o ≥ P) (hn : o ≥ N) :

o = L

source

@[simp]

theorem Outcome.le_N_eq_N_or_R {o : Outcome} (hp : o ≤ N) :

o = N ∨ o = R

source

def Outcome.Conjugate :

Outcome → Outcome

Equations

Instances For

source

theorem Outcome.conjugate_conjugate_eq_self {o : Outcome} :

o.Conjugate.Conjugate = o

source

theorem Outcome.outcome_ge_conjugate_le {x y : Outcome} (h1 : x ≥ y) :

x.Conjugate ≤ y.Conjugate

source

def Outcome.ofPlayers :

Player → Player → Outcome

Equations

Instances For

source

def Outcome.ofPlayer :

Player → Outcome

Equations

Instances For

source

@[simp]

theorem Outcome.ofPlayer_left :

ofPlayer Player.left = L

source

@[simp]

theorem Outcome.ofPlayer_right :

ofPlayer Player.right = R

source

@[simp]

theorem Outcome.ofPlayer_eq_ofPlayer {p q : Player} :

ofPlayer p = ofPlayer q ↔ p = q