EconCSLib.GameTheory.ExtensiveGame.FiniteArenaExtraction

Interfaces for extracting finite no-chance Arena-style games into GameTree.

The general reverse bridge from ExtensiveGame to GameTree cannot be total: the Arena API allows infinite state spaces, cycles, chance states, and histories that merge. This file records the assumptions needed for extraction and gives small certified extraction constructors that can be extended case by case.

Main definitions

• ExtensiveGame.NoChance — every nonterminal state has a strategic mover.
• ExtensiveGame.TreeShapedFrom — uniqueness of histories into a state.
• ExtensiveGame.FiniteExtractable — explicit assumption package for reverse extraction.
• ExtensiveGame.ActionListComplete — an explicit finite action enumeration at one state.
• ExtensiveGame.ExtractsGameTree — relational extraction from a state to a GameTree.
• ExtensiveGame.extractTerminalGameTree — certified extraction of a terminal state to a one-leaf GameTree.
• ExtensiveGame.ExtractsGameTree.leaf_payoff — extracted leaves preserve the Arena payoff vector.
• ExtensiveGame.ExtractsGameTree.node_head_reachable — the extracted head child is reached by one Arena transition.

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

A weak tree-shapedness condition: any two paths from the root to the same state are equal as reachability proofs.

This is intentionally proof-valued. Concrete finite extraction modules may replace it with a computable predecessor/history representation.

Equations

• G.TreeShapedFrom root = ∀ (s : G.State), Subsingleton (G.Reachable root s)

structure ExtensiveGame.FiniteExtractable {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : Prop

Assumptions under which an Arena-style game can be extracted to a finite no-chance GameTree. The actual recursive extraction is intentionally not bundled here; users provide a finite unfolding depth or well-founded child enumeration appropriate for their concrete game.

• state_finite : Nonempty (Fintype G.State)
• no_chance : G.NoChance
• tree_shaped : G.TreeShapedFrom G.init

def ExtensiveGame.ActionListComplete {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (head : G.Action s) (tail : List (G.Action s)) : Prop

A nonempty action list head :: tail contains every available action at state s. The list is an explicit finite enumeration supplied by the concrete game.

Equations

• G.ActionListComplete s head tail = ∀ (a : G.Action s), a ∈ head :: tail

inductive ExtensiveGame.ExtractsGameTree {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : G.State → GameTree N U → Prop

• leaf {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} (s : G.State) (hs : G.isTerminal s) : G.ExtractsGameTree s (GameTree.Leaf (G.payoff s))
• node {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} (s : G.State) (i : N) (head : G.Action s) (tail : List (G.Action s)) (headTree : GameTree N U) (tailTrees : List (GameTree N U)) (hm : G.mover s = some i) (hcomplete : G.ActionListComplete s head tail) (hhead : G.ExtractsGameTree (G.next s head) headTree) (htail : G.ExtractsGameTreeList s tail tailTrees) : G.ExtractsGameTree s (GameTree.Node i headTree tailTrees)

inductive ExtensiveGame.ExtractsGameTreeList {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : List (G.Action s) → List (GameTree N U) → Prop

• nil {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} (s : G.State) : G.ExtractsGameTreeList s [] []
• cons {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} (s : G.State) (head : G.Action s) (tail : List (G.Action s)) (headTree : GameTree N U) (tailTrees : List (GameTree N U)) (hhead : G.ExtractsGameTree (G.next s head) headTree) (htail : G.ExtractsGameTreeList s tail tailTrees) : G.ExtractsGameTreeList s (head :: tail) (headTree :: tailTrees)

def ExtensiveGame.extractTerminalGameTree {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (_hs : G.isTerminal s) : GameTree N U

Terminal states extract to one-leaf GameTrees.

Equations

• G.extractTerminalGameTree s _hs = GameTree.Leaf (G.payoff s)

theorem ExtensiveGame.extractTerminal_payoff {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (hs : G.isTerminal s) : G.extractTerminalGameTree s hs = GameTree.Leaf (G.payoff s)

theorem ExtensiveGame.extractTerminal_extracts {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) (hs : G.isTerminal s) : G.ExtractsGameTree s (G.extractTerminalGameTree s hs)

The certified terminal-state extractor satisfies the relational extraction interface.

theorem ExtensiveGame.ExtractsGameTree.leaf_payoff {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) {s : G.State} {p : N → U} (h : G.ExtractsGameTree s (GameTree.Leaf p)) : p = G.payoff s

If an Arena state extracts to a leaf, the leaf payoff is exactly the Arena payoff at that state.

theorem ExtensiveGame.ExtractsGameTree.node_head_reachable {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) {s : G.State} {i : N} {headTree : GameTree N U} {tailTrees : List (GameTree N U)} (h : G.ExtractsGameTree s (GameTree.Node i headTree tailTrees)) : ∃ (head : G.Action s), G.Reachable s (G.next s head) ∧ G.ExtractsGameTree (G.next s head) headTree

At an extracted decision node, the head child is reached by one Arena transition and itself has an extracted subtree.

theorem ExtensiveGame.ExtractsGameTree.spe_on_to_nash_at {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) [TotalPreorder U] {s : G.State} {tree : GameTree N U} (_h : G.ExtractsGameTree s tree) {σ : GameTree.Strategy N U} (hspe : GameTree.IsSubgamePerfectOn σ tree) : GameTree.IsNashAt σ tree

On any extracted tree, root-scoped subgame perfection implies root Nash equilibrium through the ordinary GameTree equilibrium API.