EconCSLib.GameTheory.ExtensiveGame.GameTree

Finite extensive-form games of perfect information, without chance, encoded as a generic inductive type.

Design

inductive GameTree (N U : Type*)
  | Leaf (payoff : N → U)
  | Node (mover : N) (head : GameTree N U) (tail : List (GameTree N U))

• N — the player set (need not be finite or decidable).
• U — the payoff type (will acquire [TotalPreorder U] at theorem sites, not in the type definition — Bourbaki discipline).
• Finite via inductive structure.
• Non-empty children at each Node via the head : GameTree + tail : List ... split — head provides a witness, tail the rest.
• No Nature / chance constructor: chance is deferred to a future StochasticGameTree module (see project memory 2026-04-20).

Main definitions

• GameTree — the inductive type itself
• GameTree.size — structural size (well-founded recursion helper)
• GameTree.children — the full child list head :: tail at a Node
• GameTree.mapChildren — apply a function to every child of a Node

References

• [MSZ, Ch. 3] Maschler, Solan, Zamir, Game Theory (Cambridge, 2013) — extensive games (backward induction; Kuhn 1953)

inductive GameTree (N : Type u_1) (U : Type u_2) : Type (max u_1 u_2)

A finite extensive-form game of perfect information, without chance.

• Leaf payoff — a terminal state with a payoff vector N → U.
• Node mover head tail — a decision node owned by mover, with non-empty children head :: tail.

Finiteness is built into the inductive type; non-emptiness of children is built into the Node constructor via head + tail.

• Leaf {N : Type u_1} {U : Type u_2} (payoff : N → U) : GameTree N U
• Node {N : Type u_1} {U : Type u_2} (mover : N) (head : GameTree N U) (tail : List (GameTree N U)) : GameTree N U

def GameTree.children {N : Type u_1} {U : Type u_2} : GameTree N U → List (GameTree N U)

The full child list at a Node, as a guaranteed non-empty list.

Equations

• (GameTree.Leaf payoff).children = []
• (GameTree.Node mover h t).children = h :: t

theorem GameTree.children_node_ne_nil {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) : (Node m h t).children ≠ []

Children of a Node are never empty.

@[irreducible]

def GameTree.size {N : Type u_1} {U : Type u_2} : GameTree N U → ℕ

Structural size, used for well-founded recursion.

Equations

• (GameTree.Leaf payoff).size = 1
• (GameTree.Node mover h t).size = 1 + h.size + (List.map GameTree.size t).sum

theorem GameTree.size_pos {N : Type u_1} {U : Type u_2} (g : GameTree N U) : 0 < g.size

Size is always positive.

theorem GameTree.size_head_lt {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) : h.size < (Node m h t).size

The head of a Node's children is structurally smaller.

theorem GameTree.size_mem_tail_lt {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) {c : GameTree N U} (hmem : c ∈ t) : c.size < (Node m h t).size

Any tail child is structurally smaller.

theorem GameTree.size_mem_children_lt {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) {c : GameTree N U} (hmem : c ∈ (Node m h t).children) : c.size < (Node m h t).size

Any child (head or in tail) is structurally smaller than the node.

Subtree relation

Subtree s g means the tree s occurs somewhere inside g (reflexively, or as the head / a tail element, recursively). Useful for stating subgame-perfect properties quantified over all reachable subgames.

inductive GameTree.Subtree {N : Type u_1} {U : Type u_2} : GameTree N U → GameTree N U → Prop

Subtree s g — s occurs as a subtree of g.

• refl {N : Type u_1} {U : Type u_2} (g : GameTree N U) : g.Subtree g
• inHead {N : Type u_1} {U : Type u_2} (s : GameTree N U) (m : N) (h : GameTree N U) (t : List (GameTree N U)) (hs : s.Subtree h) : s.Subtree (Node m h t)
• inTail {N : Type u_1} {U : Type u_2} (s : GameTree N U) (m : N) (h : GameTree N U) (t : List (GameTree N U)) {c : GameTree N U} (hmem : c ∈ t) (hs : s.Subtree c) : s.Subtree (Node m h t)

theorem GameTree.Subtree.self {N : Type u_1} {U : Type u_2} (g : GameTree N U) : g.Subtree g

Every tree is a subtree of itself.

theorem GameTree.Subtree.head {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) : h.Subtree (Node m h t)

The head of a Node is a subtree of the node.

theorem GameTree.Subtree.tail_mem {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) {c : GameTree N U} (hmem : c ∈ t) : c.Subtree (Node m h t)

Any tail member of a Node is a subtree of the node.

theorem GameTree.Subtree.child_mem {N : Type u_1} {U : Type u_2} (m : N) (h : GameTree N U) (t : List (GameTree N U)) {c : GameTree N U} (hmem : c ∈ h :: t) : c.Subtree (Node m h t)

Any child (head or tail) is a subtree.

theorem GameTree.Subtree.trans {N : Type u_1} {U : Type u_2} {r s g : GameTree N U} (hrs : r.Subtree s) (hsg : s.Subtree g) : r.Subtree g

The subtree relation is transitive. In game-theoretic terms, a subgame of a subgame is also a subgame of the original game.

Strong induction on size

A size-based strong induction principle: to prove motive g, assume motive c for every child c ∈ h :: t of a Node. Stronger than the default inductive recursor (which only gives IH on the head), and precisely what backward-induction proofs need.

theorem GameTree.strong_induction {N : Type u_1} {U : Type u_2} {motive : GameTree N U → Prop} (base : ∀ (p : N → U), motive (Leaf p)) (step : ∀ (m : N) (h : GameTree N U) (t : List (GameTree N U)), (∀ (c : GameTree N U), c ∈ h :: t → motive c) → motive (Node m h t)) (g : GameTree N U) : motive g

Strong induction: to prove motive g, it suffices to handle Leaf and, for each Node, to prove the motive given the motive for every child (head or tail).