```
Definition fin (n: nat) := { i: nat | i < n }.
Definition vector A n := fin n -> A.
Require Import QArith.
Inductive tree (n: nat) :=
| leaf: vector Q n -> tree n
| node: forall (player: fin n), list (tree n) -> tree n.
```

Formalising (writing down definition of) perfect information games seems easy, if I've not made any mistake.

But how would you formalize imperfect information games? Big thanks for any hints.

(I have a course about Game Theory in my university studies right now and decided to make it more interesting to me by writing down things in Coq.)

My first try...

```
Definition fin (n: nat) := { i: nat | i < n }.
Definition vector A n := fin n -> A.
Require Import QArith.
(* Imperfect information game *)
Inductive nonempty_list A :=
| first: A -> nonempty_list A
| ne_cons: A -> nonempty_list A -> nonempty_list A.
Inductive game (n: nat) :=
| leaf: forall (payout: vector Q n), game n
| node: forall (player: fin n) (information_set: nonempty_list (nonempty_list (game n))), game n.
```

Not sure how easy it will be to reason about this definition later. :sweat_smile:

Hmm, it seems a bit wrong.

maybe useful, there was this formalization of extensive form games by Pierre Lescanne. However, he never merged my PR to fix Coq building issues, so I link to my fork (has paper link): https://github.com/palmskog/DependentTypesForExtensiveGames

Hmm, something like this seems to be correct direction.

```
Require Import QArith List.
Set Implicit Arguments.
(*
'n' is number of players
'score i' is utility for the i-th player (if i >= n, then anything works)
each 'node_id' has to be different
'player' is player, who makes their choice in this node
*)
Inductive tree (n: nat) :=
| leaf: forall (scores: nat -> Q), tree n
| decision_node: forall (node_id: nat) (player: nat) (choices: list (tree n)), tree n.
(* 'partition_function' will have type nat->nat *)
(* there will be function that checks if tree has decision node with given id *)
(* there will be function that, if tree has such id, *)
(* gets subtree with given id of decision node and returns length of 'choices' list. *)
(* let's call it 'length_of_choices' *)
(* 1st property - all node 'id's has to be distinct *)
(* 2nd property - all decision nodes has nonempty 'choices' *)
(* 3rd property - forall id1 and id2, if tree has nodes with id1 and id2 and partition_function id1 = partition_function id2, *)
(* then length_of_choices id1 tree = length_of_choices id2 tree *)
```

Will realize this tomorrow or maybe day after tomorrow. But, if one has some criticism or suggestions, feel free to post and thank you!

Here it is. Should be okay, probably.

```
Require Import QArith List.
Set Implicit Arguments.
Inductive tree (n: nat) :=
| leaf: forall (scores: nat -> Q), tree n
| decision_node: forall (node_id: nat) (player: nat) (choices: list (tree n)), tree n.
Fixpoint ids_with_degree n (t: tree n): list (nat * nat).
Proof.
induction t.
+ exact nil.
+ refine ((node_id, length choices) :: _). induction choices.
- exact nil.
- exact (ids_with_degree n a ++ IHchoices).
Defined.
Fixpoint distinct_elements (L: list nat): Prop :=
match L with
| nil => True
| x :: t => (In x t -> False) /\ distinct_elements t
end.
Definition has_id n id (t: tree n) := In id (map fst (ids_with_degree t)).
Definition get_degree n id (t: tree n) :=
match find (fun p => Nat.eqb id (fst p)) (ids_with_degree t) with
| Some (i, d) => d
| None => O
end.
Structure extensive_form_game (n: nat) := {
underlying_tree: tree n;
information_set: nat -> nat;
property_1: distinct_elements (map fst (ids_with_degree underlying_tree));
property_2: Forall (lt 0) (map snd (ids_with_degree underlying_tree));
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
}.
```

Last updated: Jun 13 2024 at 21:01 UTC