LeanPool.MisereGames.Player

Misere combinatorial games.

source

inductive MisereGames.Player :

Type

Either the Left or Right player.

left : Player
The Left player.
right : Player
The Right player.

Instances For

source

@[implicit_reducible]

instance MisereGames.instDecidableEqPlayer :

DecidableEq Player

Equations

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

source

@[implicit_reducible]

instance MisereGames.instFintypePlayer :

Fintype Player

Equations

MisereGames.instFintypePlayer = { elems := { val := ↑MisereGames.Player.enumList, nodup := MisereGames.Player.enumList_nodup }, complete := MisereGames.instFintypePlayer._proof_1 }

source

@[implicit_reducible]

instance MisereGames.instInhabitedPlayer :

Inhabited Player

Equations

MisereGames.instInhabitedPlayer = { default := MisereGames.instInhabitedPlayer.default }

source

@[reducible, inline]

abbrev MisereGames.Player.cases {α : Sort u_1} (l r : α) :

Player → α

Specify a function Player → α from its two outputs.

Equations

Instances For

source

theorem MisereGames.Player.apply_cases {α : Sort u_1} {β : Sort u_2} (f : α → β) (l r : α) (p : Player) :

f (cases l r p) = cases (f l) (f r) p

source

@[simp]

theorem MisereGames.Player.cases_inj {α : Sort u_1} {l₁ r₁ l₂ r₂ : α} :

cases l₁ r₁ = cases l₂ r₂ ↔ l₁ = l₂ ∧ r₁ = r₂

source

theorem MisereGames.Player.const_of_left_eq_right {α : Sort u_1} {f : Player → α} (hf : f left = f right) (p q : Player) :

f p = f q

source

theorem MisereGames.Player.const_of_left_eq_right' {f : Player → Prop} (hf : f left ↔ f right) (p q : Player) :

f p ↔ f q

source

@[simp]

theorem MisereGames.Player.forall {p : Player → Prop} :

(∀ (x : Player), p x) ↔ p left ∧ p right

source

@[simp]

theorem MisereGames.Player.exists {p : Player → Prop} :

(∃ (x : Player), p x) ↔ p left ∨ p right

source

@[implicit_reducible]

instance MisereGames.Player.instNeg :

Neg Player

Equations

MisereGames.Player.instNeg = { neg := MisereGames.Player.cases MisereGames.Player.right MisereGames.Player.left }

source

@[simp]

theorem MisereGames.Player.neg_left :

-left = right

source

@[simp]

theorem MisereGames.Player.neg_right :

-right = left

source

@[implicit_reducible]

instance MisereGames.Player.instInvolutiveNeg :

InvolutiveNeg Player

Equations

MisereGames.Player.instInvolutiveNeg = { toNeg := MisereGames.Player.instNeg, neg_neg := MisereGames.Player.instInvolutiveNeg._proof_1 }

source

@[simp]

theorem MisereGames.Player.ne_iff_eq_neg {a b : Player} :

a ≠ b ↔ a = -b

source

theorem MisereGames.Player.absurd {p q : Player} (h1 : p = q) (h2 : p = -q) :

False

source

@[implicit_reducible]

instance MisereGames.Player.instLE :

LE Player

Equations

MisereGames.Player.instLE = { le := fun (lhs rhs : MisereGames.Player) => lhs = MisereGames.Player.right ∨ lhs = MisereGames.Player.left ∧ rhs = MisereGames.Player.left }

source

@[implicit_reducible]

instance MisereGames.Player.instDecidableLE :

DecidableLE Player

Equations

MisereGames.Player.instDecidableLE = id inferInstance

source

theorem MisereGames.Player.le_right_eq (p : Player) (h1 : p ≤ right) :

p = right

source

@[simp]

theorem MisereGames.Player.le_right_iff (p : Player) :

p ≤ right ↔ p = right

source

theorem MisereGames.Player.le_left_eq (p : Player) (h1 : left ≤ p) :

p = left

source

@[simp]

theorem MisereGames.Player.left_le_iff (p : Player) :

left ≤ p ↔ p = left

source

@[simp]

theorem MisereGames.Player.right_le (p : Player) :

right ≤ p

source

@[simp]

theorem MisereGames.Player.le_left (p : Player) :

p ≤ left

source

theorem MisereGames.Player.left_le_right (h1 : left ≤ right) :

False

source

theorem MisereGames.Player.not_left_le_right :

¬left ≤ right