Extensive form games, how to formalize information sets?

Stream: Is there code for X?

[Lessness]

(Those who lurk in Coq zulip chat too, hi! I'm from there. Greetings and best wishes to Lean zulip chat! :smile:)

Ok, to the question - is there some formalization of extensive form games with information sets in Lean?

Thank you!

[Lessness]

Karl Palmskog in the Coq zulip chat gave me link to his repository which contained some interesting formalization of game theory, but without information sets (as far as I could tell): https://github.com/palmskog/DependentTypesForExtensiveGames

Also, Wikipedia has section "Formal definition": https://en.wikipedia.org/wiki/Extensive-form_game#Formal_definition
Maybe this is useful.

[Floris van Doorn]

Hello! I think that this doesn't exist yet in Lean.

[Lessness]

This is my try which I'm proud about. :sweat_smile: Beginner's happiness. :grinning:
Of course, I still need to formalize strategies of players etc., for this to have any use.

Anyway, if there are any mistakes, please tell me. And, if you want, suggestions of better ways how to formalize this are welcome.

import Std

inductive Tree (n: Nat) (q: Type) where
  | leaf (payouts: Nat -> q)
  | decision_node (node_id player: Nat) (choices: List (Tree n q))

def ids_with_degree {n q} (t: Tree n q): List (Prod Nat Nat) :=
  match t with
  | Tree.leaf _ => []
  | Tree.decision_node id _ choices =>
    (id, List.length choices) :: List.join (choices.attach.map (fun ⟨x,_⟩ => ids_with_degree x))

def distinct_elements {A: Type} (L: List A): Prop :=
  match L with
  | [] => True
  | x :: t => (List.Mem x t -> False) /\ distinct_elements t

def has_id {n q} (id: Nat) (t: Tree n q): Prop :=
  List.Mem id (List.map Prod.fst (ids_with_degree t))

def find_first {A: Type} (f: A -> Bool) (L: List A): Option A :=
  match L with
  | [] => none
  | x :: t => match f x with
              | true => some x
              | false => find_first f t

def get_degree {n q} (id: Nat) (t: Tree n q): Nat :=
  match find_first (fun p => id == Prod.fst p) (ids_with_degree t) with
  | some p => Prod.snd p
  | none => 0

structure extensive_form_game (n: Nat) (q: Type) where
  underlying_tree: Tree n q
  information_set: Nat -> Nat
  property_1: distinct_elements (List.map Prod.fst (ids_with_degree underlying_tree))
  property_2: forall x, List.Mem x (List.map Prod.snd (ids_with_degree underlying_tree)) -> 0 < x
  property_3: forall id1 id2,
              has_id id1 underlying_tree -> has_id id2 underlying_tree ->
              information_set id1 = information_set id2 ->
              get_degree id1 underlying_tree = get_degree id2 underlying_tree