CombinatorialGames.Player

source

inductive Player :

Type

Either the Left or Right player.

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

Instances For

source

@[instance_reducible]

instance instDecidableEqPlayer :

DecidableEq Player

Equations

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

source

@[instance_reducible]

instance instFintypePlayer :

Fintype Player

Equations

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

source

def instInhabitedPlayer.default :

Player

Equations

instInhabitedPlayer.default = Player.left

Instances For

source

@[instance_reducible]

instance instInhabitedPlayer :

Inhabited Player

Equations

instInhabitedPlayer = { default := instInhabitedPlayer.default }

source

@[reducible, inline]

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

Player → α

Specify a function Player → α from its two outputs.

Equations

Player.cases l r Player.left = l
Player.cases l r Player.right = r

Instances For

source

theorem 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 Player.cases_inj {α : Sort u_1} {l₁ r₁ l₂ r₂ : α} :

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

source

theorem 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 Player.const_of_left_eq_right' {f : Player → Prop} (hf : f left ↔ f right) (p q : Player) :

f p ↔ f q

source

@[simp]

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

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

source

@[simp]

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

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

source

@[instance_reducible]

instance Player.instNeg :

Neg Player

Equations

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

source

@[simp]

theorem Player.neg_left :

-left = right

source

@[simp]

theorem Player.neg_right :

-right = left

source

@[instance_reducible]

instance Player.instInvolutiveNeg :

InvolutiveNeg Player

Equations

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

source

@[simp]

theorem Player.ne_iff_eq_neg {a b : Player} :

a ≠ b ↔ a = -b

source

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

False

source

@[instance_reducible]

instance Player.instLE :

LE Player

Equations

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

source

@[instance_reducible]

instance Player.instDecidableLE :

DecidableLE Player

Equations

Player.instDecidableLE = id inferInstance

source

@[simp]

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

p = right

source

@[simp]

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

p = left

source

@[simp]

theorem Player.right_le (p : Player) :

right ≤ p

source

@[simp]

theorem Player.le_left (p : Player) :

p ≤ left

source

@[simp]

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

False