EconCSLib.GameTheory.ExtensiveGame.Basic

Payoff-aware compatibility for the minimal Arena-based EFG core.

Design

The payoff-free Arena and ControlledGame carriers live in ExtensiveGame.Structural.Basic. This module preserves the historical Basic import path and adds only the endpoint-state-payoff ExtensiveGame compatibility carrier.

Main definitions

• ExtensiveGame — controlled game + state payoff

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Chapter 3

Extensive-form game

structure ExtensiveGame (N : Type u_1) (U : Type u_2) extends ControlledGame N : Type (max (max (max u_1 u_2) (u_3 + 1)) (u_4 + 1))

A state-payoff extensive game: a payoff-free controlled game together with a convenient endpoint-state payoff.

* `mover s` = who controls state `s` (`none` = non-player-controlled)
* `payoff s i` = payoff for player `i` at state `s` (meaningful at terminal states)

General terminal-history, complete-path, and winning-condition semantics
are separate objective layers; this field is not their authoritative
definition.

No `isTerminal` field — terminal states are detected by `IsEmpty (Action s)`.
No proof terms to carry around. 

• State : Type u_3
• Action : self.State → Type u_4
• next (s : self.State) : self.Action s → self.State
• init : self.State
• mover : self.State → Option N
• payoff : self.State → N → U

  Payoff at each state for each player. Meaningful at terminal states; may be arbitrary elsewhere.

@[reducible, inline]

abbrev ExtensiveGame.ofControlledGame {N : Type u_1} {U : Type u_2} (base : ControlledGame N) (payoff : base.State → N → U) : ExtensiveGame N U

Add a state-based payoff interpretation to a payoff-free controlled game.

Forgetting the result with ExtensiveGame.toControlledGame recovers base definitionally.

Equations

• ExtensiveGame.ofControlledGame base payoff = { toControlledGame := base, payoff := payoff }

@[simp]

theorem ExtensiveGame.ofControlledGame_toControlledGame {N : Type u_1} {U : Type u_2} (base : ControlledGame N) (payoff : base.State → N → U) : (ofControlledGame base payoff).toControlledGame = base

@[simp]

theorem ExtensiveGame.ofControlledGame_payoff {N : Type u_1} {U : Type u_2} (base : ControlledGame N) (payoff : base.State → N → U) (state : base.State) (i : N) : (ofControlledGame base payoff).payoff state i = payoff state i

@[simp]

theorem ExtensiveGame.ofControlledGame_toControlledGame_self {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : ofControlledGame G.toControlledGame G.payoff = G

Forgetting an existing payoff-aware game and then reattaching its payoff recovers the original game definitionally.

@[reducible, inline]

abbrev ExtensiveGame.ofArena {N : Type u_1} {U : Type u_2} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (payoff : arena.State → N → U) : ExtensiveGame N U

Add an initial state, mover assignment, and payoff function to an ordinary arena.

All game-semantic data are explicit arguments; in particular this constructor does not infer chance nodes or terminal payoffs from the arena. It composes with observed-game presentation constructors without duplicating the arena's state, action, or transition fields.

Equations

• ExtensiveGame.ofArena arena init mover payoff = ExtensiveGame.ofControlledGame (ControlledGame.ofArena arena init mover) payoff

@[simp]

theorem ExtensiveGame.ofArena_toArena {N : Type u_1} {U : Type u_2} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (payoff : arena.State → N → U) : (ofArena arena init mover payoff).toArena = arena

@[simp]

theorem ExtensiveGame.ofArena_init {N : Type u_1} {U : Type u_2} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (payoff : arena.State → N → U) : (ofArena arena init mover payoff).init = init

@[simp]

theorem ExtensiveGame.ofArena_mover {N : Type u_1} {U : Type u_2} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (payoff : arena.State → N → U) (state : arena.State) : (ofArena arena init mover payoff).mover state = mover state

@[simp]

theorem ExtensiveGame.ofArena_payoff {N : Type u_1} {U : Type u_2} (arena : Arena) (init : arena.State) (mover : arena.State → Option N) (payoff : arena.State → N → U) (state : arena.State) (i : N) : (ofArena arena init mover payoff).payoff state i = payoff state i

@[reducible, inline]

abbrev ExtensiveGame.arena {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : Arena

The arena of a game.

Equations

• G.arena = G.toArena

@[reducible, inline]

abbrev ExtensiveGame.controlledGame {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : ControlledGame N

Forget only the state-payoff interpretation.

This is a lossless projection for dynamics, the initial root, and mover data. It is the canonical migration path from payoff-aware APIs to structural or logical-game APIs.

Equations

• G.controlledGame = G.toControlledGame

@[reducible, inline]

abbrev ExtensiveGame.actions {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : Type u_4

Available actions at a state.

Equations

• G.actions s = G.Action s

@[reducible, inline]

abbrev ExtensiveGame.isTerminal {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : Prop

A state is terminal.

Equations

• G.isTerminal s = G.IsTerminal s

def ExtensiveGame.isPlayerState {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (i : N) : Prop

A state is controlled by player i.

Equations

• G.isPlayerState s i = G.isPlayerState s i

@[simp]

theorem ExtensiveGame.isPlayerState_iff_toControlledGame {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (i : N) : G.isPlayerState s i ↔ G.isPlayerState s i

The historical payoff-aware player-state predicate is exactly the canonical controlled-game predicate.

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

A nonterminal state carrying the non-player-control label.

This predicate supplies no probability law.

Equations

• G.isNonPlayerState s = G.isNonPlayerState s

@[simp]

theorem ExtensiveGame.isNonPlayerState_iff_toControlledGame {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : G.isNonPlayerState s ↔ G.isNonPlayerState s

The historical payoff-aware non-player-state predicate is exactly the canonical controlled-game predicate.

@[reducible, inline]

abbrev ExtensiveGame.isChanceState {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : Prop

Compatibility name for isNonPlayerState.

No chance law is implied by this predicate alone.

Equations

• G.isChanceState s = G.isNonPlayerState s

def ExtensiveGame.NoChance {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : Prop

No chance nodes: every nonterminal state has a strategic mover.

Equations

• G.NoChance = G.NoChance

@[simp]

theorem ExtensiveGame.noChance_iff_toControlledGame {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : G.NoChance ↔ G.NoChance

The historical payoff-aware no-chance predicate is exactly the canonical controlled-game predicate.