EconCSLib.GameTheory.ExtensiveGame.ImperfectInformation

A finite interface for imperfect-information extensive games.

This is intentionally a lightweight structural layer. It records vertices, available actions, transitions, mover ownership, terminal payoffs, and information-set labels. Well-formedness conditions are predicates, not fields, so examples can start small while later theorem statements can assume exactly the conditions they need.

Main definitions

• FiniteImperfectGame — finite imperfect-information extensive game data.
• FiniteImperfectGame.subgameAt — the same game rooted at a chosen state.
• SameMoverOnInfo — nodes in one information set have the same mover.
• SameActionsOnInfo — nodes in one information set have the same action type.
• NoChanceOnDecisionInfo — information sets are only used at player nodes.
• PureStrategy — choices indexed by player and information set.
• PureStrategy.actionAt — induced action at a concrete state.

structure FiniteImperfectGame (N : Type u_1) (U : Type u_2) : Type (max (max (max (max u_1 u_2) (u_3 + 1)) (u_4 + 1)) (u_5 + 1))

Finite imperfect-information extensive game data.

info s = none means the state is not in a strategic information set, typically because it is terminal or chance-controlled. info s = some k places state s in information set k.

• State : Type u_3
• stateFintype : Fintype self.State
• stateDecidableEq : DecidableEq self.State
• InfoSet : Type u_4
• infoDecidableEq : DecidableEq self.InfoSet
• Action : self.State → Type u_5
• next (s : self.State) : self.Action s → self.State
• init : self.State
• mover : self.State → Option N
• info : self.State → Option self.InfoSet
• payoff : self.State → N → U

def FiniteImperfectGame.IsTerminal {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) (s : G.State) : Prop

A state is terminal when it has no available actions.

Equations

• G.IsTerminal s = IsEmpty (G.Action s)

def FiniteImperfectGame.subgameAt {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) (s : G.State) : FiniteImperfectGame N U

The subgame starting at state s: same finite game data with a different initial state. Extra validity conditions, such as whether s is a legitimate imperfect-information subroot, can be imposed by theorem statements using this operation.

Equations

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

theorem FiniteImperfectGame.subgameAt_init {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) (s : G.State) : (G.subgameAt s).init = s

The initial state of subgameAt is the chosen root.

def FiniteImperfectGame.SameMoverOnInfo {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) : Prop

States in the same information set have the same mover.

Equations

• G.SameMoverOnInfo = ∀ {s t : G.State} {k : G.InfoSet}, G.info s = some k → G.info t = some k → G.mover s = G.mover t

def FiniteImperfectGame.SameActionsOnInfo {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) : Prop

States in the same information set expose equivalent action types.

Equations

• G.SameActionsOnInfo = ∀ {s t : G.State} {k : G.InfoSet}, G.info s = some k → G.info t = some k → Nonempty (G.Action s ≃ G.Action t)

def FiniteImperfectGame.NoChanceOnDecisionInfo {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) : Prop

Strategic information sets are attached only to player-controlled states.

Equations

• G.NoChanceOnDecisionInfo = ∀ {s : G.State} {k : G.InfoSet}, G.info s = some k → ∃ (i : N), G.mover s = some i

def FiniteImperfectGame.InfoWellFormed {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) : Prop

Basic well-formedness package for information-set reasoning.

Equations

• G.InfoWellFormed = (G.SameMoverOnInfo ∧ G.SameActionsOnInfo ∧ G.NoChanceOnDecisionInfo)

theorem FiniteImperfectGame.subgameAt_infoWellFormed {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) {s : G.State} (h : G.InfoWellFormed) : (G.subgameAt s).InfoWellFormed

Re-rooting a finite imperfect-information game preserves the local information-set well-formedness package.

def FiniteImperfectGame.PureStrategy {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) (i : N) : Type (max (max u_5 u_4) u_3)

A pure strategy chooses one abstract action for each player and information set.

The action type is indexed by a representative state for that information set. For a concrete state s, actionAt below specializes this choice at s, so choices are constant on information sets by construction at the API boundary.

Equations

• G.PureStrategy i = ((k : G.InfoSet) → (s : G.State) → G.info s = some k → G.mover s = some i → G.Action s)

def FiniteImperfectGame.PureStrategyProfile {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) : Type (max (max (max u_1 u_5) u_4) u_3)

A pure strategy profile.

Equations

• G.PureStrategyProfile = ((i : N) → G.PureStrategy i)

def FiniteImperfectGame.PureStrategy.actionAt {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) {i : N} (σ : G.PureStrategy i) {s : G.State} {k : G.InfoSet} (hinfo : G.info s = some k) (hmover : G.mover s = some i) : G.Action s

The action prescribed at a concrete player-controlled state in an information set.

Equations

• FiniteImperfectGame.PureStrategy.actionAt G σ hinfo hmover = σ k s hinfo hmover

theorem FiniteImperfectGame.actionAt_same_info_label {N : Type u_1} {U : Type u_2} (G : FiniteImperfectGame N U) {i : N} (σ : G.PureStrategy i) {s t : G.State} {k : G.InfoSet} (hs : G.info s = some k) (ht : G.info t = some k) (hms : G.mover s = some i) (hmt : G.mover t = some i) : PureStrategy.actionAt G σ hs hms = σ k s hs hms ∧ PureStrategy.actionAt G σ ht hmt = σ k t ht hmt

If two states are in the same information set, a strategy is queried through the same information-set label at both states. This is the formal constancy-by-indexing property; comparing concrete action values requires an action equivalence from SameActionsOnInfo.

Small example

inductive Examples.ImperfectInformation.Player : Type

• P0 : Player
• P1 : Player

@[implicit_reducible]

instance Examples.ImperfectInformation.instDecidableEqPlayer : DecidableEq Player

Equations

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

inductive Examples.ImperfectInformation.State : Type

• root : State
• left : State
• right : State
• stop : State

@[implicit_reducible]

instance Examples.ImperfectInformation.instDecidableEqState : DecidableEq State

Equations

• Examples.ImperfectInformation.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Examples.ImperfectInformation.instFintypeState : Fintype State

Equations

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

inductive Examples.ImperfectInformation.Info : Type

• hiddenChoice : Info

@[implicit_reducible]

instance Examples.ImperfectInformation.instDecidableEqInfo : DecidableEq Info

Equations

• Examples.ImperfectInformation.instDecidableEqInfo x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Examples.ImperfectInformation.RootAction : Type

• L : RootAction
• R : RootAction

@[implicit_reducible]

instance Examples.ImperfectInformation.instDecidableEqRootAction : DecidableEq RootAction

Equations

• Examples.ImperfectInformation.instDecidableEqRootAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Examples.ImperfectInformation.P1Action : Type

• Stop : P1Action

@[implicit_reducible]

instance Examples.ImperfectInformation.instDecidableEqP1Action : DecidableEq P1Action

Equations

• Examples.ImperfectInformation.instDecidableEqP1Action x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Examples.ImperfectInformation.tiny : FiniteImperfectGame Player ℤ

A tiny imperfect-information game where player 1 cannot distinguish two singleton-action states reached after player 0's root choice.

Equations

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

theorem Examples.ImperfectInformation.tiny_same_mover : tiny.SameMoverOnInfo

theorem Examples.ImperfectInformation.tiny_no_chance_on_info : tiny.NoChanceOnDecisionInfo