LeanPool.MisereGames.Outcome

source

inductive MisereGames.Outcome :

Type

The four outcome classes of a short partizan game.

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

@[implicit_reducible]

instance MisereGames.instDecidableEqOutcome :

DecidableEq Outcome

Equations

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

source

@[implicit_reducible]

instance MisereGames.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

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance MisereGames.Outcome.instDecidableLT :

DecidableLT Outcome

Equations

MisereGames.Outcome.instDecidableLT = id inferInstance

source

@[implicit_reducible]

instance MisereGames.Outcome.instLE :

LE Outcome

Equations

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

source

@[implicit_reducible]

instance MisereGames.Outcome.instDecidableLE :

DecidableLE Outcome

Equations

MisereGames.Outcome.instDecidableLE = id inferInstance

source

@[implicit_reducible]

instance MisereGames.Outcome.instPreorder :

Preorder Outcome

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance MisereGames.Outcome.instPartialOrder :

PartialOrder Outcome

Equations

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

source

@[simp]

theorem MisereGames.Outcome.ge_R (o : Outcome) :

o ≥ R

source

@[simp]

theorem MisereGames.Outcome.le_R_iff (o : Outcome) :

o ≤ R ↔ o = R

source

@[simp]

theorem MisereGames.Outcome.L_ge (o : Outcome) :

L ≥ o

source

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

o = L

source

@[simp]

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

o = N ∨ o = R

source

def MisereGames.Outcome.Conjugate :

Outcome → Outcome

Conjugate an outcome by swapping the players.

Equations

Instances For

source

theorem MisereGames.Outcome.conjugate_conjugate_eq_self {o : Outcome} :

o.Conjugate.Conjugate = o

source

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

x.Conjugate ≤ y.Conjugate

source

def MisereGames.Outcome.ofPlayers :

Player → Player → Outcome

The outcome determined by the winners when Left and Right start.

Equations

Instances For

source

def MisereGames.Outcome.ofPlayer :

Player → Outcome

The outcome where the given player wins no matter who starts.

Equations

Instances For

source

@[simp]

theorem MisereGames.Outcome.ofPlayer_left :

ofPlayer Player.left = L

source

@[simp]

theorem MisereGames.Outcome.ofPlayer_right :

ofPlayer Player.right = R