Ce notebook explore les jeux combinatoires formalises dans mathlib4. Contrairement aux jeux stratégiques (Nash, stratégies mixtes), les jeux combinatoires sont des jeux a information parfaite ou deux joueurs jouent alternativement jusqu’a ce qu’un joueur ne puisse plus jouer.
Jeux stratégiques vs Jeux combinatoires
Aspect
Jeux stratégiques
Jeux combinatoires
Joueurs
N joueurs simultanement
2 joueurs alternativement
Information
Peut etre incomplete
Parfaite
Hasard
Possible
Aucun
Fin
Gains continus
Un joueur gagne/perd
Exemples
Poker, Auctions
Echecs, Go, Nim
Théorie
Nash, mécanismes
Conway, Sprague-Grundy
Objectifs d’apprentissage
Comprendre la structure inductive PGame de mathlib
Explorer le jeu de Nim et sa valeur de Grundy
Decouvrir le theoreme de Sprague-Grundy
Introduction aux nombres surreels
Prerequis
Notebook 8-CombinatorialGames : Théorie des jeux combinatoires (Python)
Bases de Lean 4 : types inductifs, definitions, #check
Notions de théorie des types (optionnel mais utile)
Duree estimee : 50 minutes
1. Théorie des Jeux Combinatoires
Un jeu combinatoire (au sens de Conway) est défini par : - Deux joueurs : Gauche (L) et Droite (R) - Un ensemble de positions legales - Des règles de deplacement pour chaque joueur - Une condition de fin : le joueur qui ne peut plus jouer perd
Classification
Type
Description
Exemple
Impartial
Mêmes coups pour les deux joueurs
Nim
Partizan
Coups différents selon le joueur
Echecs, Domineering
2. PGame dans Lean
La notion de jeu combinatoire se traduit naturellement en un type inductif en Lean. L’idee cle de Conway est qu’un jeu est entierement determine par les positions que chaque joueur peut atteindre. Formellement :
\[G = \{G^L \mid G^R\}\]
ou \(G^L\) est l’ensemble des positions atteignables par Gauche et \(G^R\) par Droite.
En Lean, cela se traduit par un type inductif paramètre par deux types L et R (representant les ensembles de coups) et deux fonctions L -> PGame et R -> PGame (representant les positions resultantes). La recursion structurelle garantit que tout jeu ainsi défini est bien fonde.
La definition simplifiee ci-dessous utilise Type (univers 0). La version complete de mathlib utilise des univers pour supporter les jeux de cardinalite arbitraire.
-- Definition simplifiee de PGame
-- (mathlib utilise une version plus elaboree avec univers)
inductive SimplePGame where
| mk : (L : Type) -> (R : Type) -> (L -> SimplePGame) -> (R -> SimplePGame) -> SimplePGame
-- L = type des coups de Gauche
-- R = type des coups de Droite
-- moveL : L -> SimplePGame = position apres coup de Gauche
-- moveR : R -> SimplePGame = position apres coup de Droite
#check SimplePGame
-- Definition simplifiee de PGame
-- (mathlib utilise une version plus elaboree avec univers)
-- moveL : L -> SimplePGame = position apres coup de Gauche
-- moveR : R -> SimplePGame = position apres coup de Droite
SimplePGame:Type1
--% env 0
Raw input{"cmd": "-- Definition simplifiee de PGame\n-- (mathlib utilise une version plus elaboree avec univers)\n\ninductive SimplePGame where\n | mk : (L : Type) -> (R : Type) -> (L -> SimplePGame) -> (R -> SimplePGame) -> SimplePGame\n\n-- L = type des coups de Gauche\n-- R = type des coups de Droite\n-- moveL : L -> SimplePGame = position apres coup de Gauche\n-- moveR : R -> SimplePGame = position apres coup de Droite\n\n#check SimplePGame"}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "SimplePGame : Type 1"}],
"env": 0}
Jeux primitifs
A partir du type PG, nous pouvons définir les quatre jeux fondamentaux de la théorie combinatoire. Ces quatre briques servent de base a toutes les constructions ulterieures :
Zero (\(0\)) : le jeu nul, personne ne peut jouer
Un (\(1\)) : seul Gauche peut jouer un coup, vers 0
Moins un (\(-1\)) : seul Droite peut jouer un coup, vers 0
Etoile (\(*\)) : les deux joueurs peuvent aller vers 0
Chaque jeu utilise Empty (pas de coup possible) ou Unit (exactement un coup) comme type de coups.
-- Jeux fondamentaux
inductive PG where
| mk : (L R : Type) -> (L -> PG) -> (R -> PG) -> PG
-- 0 : aucun coup pour personne
def PG.zero : PG := PG.mk Empty Empty (fun e => e.elim) (fun e => e.elim)
-- 1 : Gauche peut bouger vers 0, Droite ne peut pas
def PG.one : PG := PG.mk Unit Empty (fun _ => PG.zero) (fun e => e.elim)
-- -1 : Droite peut bouger vers 0, Gauche ne peut pas
def PG.negOne : PG := PG.mk Empty Unit (fun e => e.elim) (fun _ => PG.zero)
-- * (star) : les deux peuvent bouger vers 0
def PG.star : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.zero)
#check PG.zero
#check PG.one
#check PG.negOne
#check PG.star
Raw input{"cmd": "-- Jeux fondamentaux\n\ninductive PG where\n | mk : (L R : Type) -> (L -> PG) -> (R -> PG) -> PG\n\n-- 0 : aucun coup pour personne\ndef PG.zero : PG := PG.mk Empty Empty (fun e => e.elim) (fun e => e.elim)\n\n-- 1 : Gauche peut bouger vers 0, Droite ne peut pas\ndef PG.one : PG := PG.mk Unit Empty (fun _ => PG.zero) (fun e => e.elim)\n\n-- -1 : Droite peut bouger vers 0, Gauche ne peut pas\ndef PG.negOne : PG := PG.mk Empty Unit (fun e => e.elim) (fun _ => PG.zero)\n\n-- * (star) : les deux peuvent bouger vers 0\ndef PG.star : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.zero)\n\n#check PG.zero\n#check PG.one\n#check PG.negOne\n#check PG.star", "env": 0}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 6},
"data": "PG.zero : PG"},
{"severity": "info",
"pos": {"line": 19, "column": 0},
"endPos": {"line": 19, "column": 6},
"data": "PG.one : PG"},
{"severity": "info",
"pos": {"line": 20, "column": 0},
"endPos": {"line": 20, "column": 6},
"data": "PG.negOne : PG"},
{"severity": "info",
"pos": {"line": 21, "column": 0},
"endPos": {"line": 21, "column": 6},
"data": "PG.star : PG"}],
"env": 1}
Interpretation des jeux primitifs
Les commandes #check ont confirme que les quatre jeux fondamentaux sont bien définis dans notre type PG. Chacun encode un comportement stratégique distinct :
Jeu
Notation
Type des coups L/R
Qui gagne ?
Pourquoi ?
\(0\)
{ \| }
Empty / Empty
Second joueur (P-position)
Aucun coup : le joueur actif perd immédiatement
\(1\)
{0\|}
Unit / Empty
Gauche (même en second)
Gauche joue vers 0, Droite ne peut pas jouer
\(-1\)
{\|0}
Empty / Unit
Droite (même en second)
Symétrique de 1, Droite a l’avantage
\(*\)
{0\|0}
Unit / Unit
Premier joueur (N-position)
Les deux peuvent aller vers 0, donc le premier arrive à 0 en premier
Classification P/N : - P-position (Previous) : le joueur qui vient de jouer gagne, c’est-à-dire le second joueur. C’est le cas de \(0\). - N-position (Next) : le prochain joueur (celui dont c’est le tour) gagne. C’est le cas de \(*\). - L-position : Gauche gagne quel que soit qui commence. C’est le cas de \(1\). - R-position : Droite gagne quel que soit qui commence. C’est le cas de \(-1\).
Note technique : La notation fun e => e.elim exploite le fait qu’il n’existe aucun terme de type Empty. Cette fonction est donc “irréalisable” : elle encode l’absence de coup pour un joueur. C’est l’équivalent Lean de l’ensemble vide d’options dans la notation \({\mid}\).
3. Le jeu de Nim
Le jeu de Nim est le jeu impartial le plus fondamental en théorie des jeux combinatoires. Il se joue avec des tas d’objets : a chaque tour, un joueur retire un nombre quelconque d’objets d’un seul tas. Le joueur qui prend le dernier objet gagne (convention “normal play”).
La puissance du jeu de Nim vient du theoreme de Sprague-Grundy : tout jeu impartial est equivalent a une variante de Nim. Comprendre Nim, c’est donc comprendre tous les jeux impartiaux.
Definition formelle
En notation de Conway, le jeu de Nim avec un tas de \(n\) objets est : - \(\text{nim}(0) = \{|\}\) (le jeu nul, aucun coup) - \(\text{nim}(n) = \{\text{nim}(0), \ldots, \text{nim}(n-1) \mid \text{nim}(0), \ldots, \text{nim}(n-1)\}\) pour \(n \geq 1\)
Les coups de Gauche et de Droite sont identiques car Nim est un jeu impartial : chaque joueur peut reduire le tas a n’importe quelle taille inferieure.
-- Nim avec un tas de n objets
-- nim(0) = 0 (pas de coup)
-- nim(n) = {nim(0), ..., nim(n-1) | nim(0), ..., nim(n-1)}
def nim : Nat -> PG
| 0 => PG.mk Empty Empty (fun e => e.elim) (fun e => e.elim)
| n + 1 => PG.mk (Fin (n + 1)) (Fin (n + 1))
(fun k => nim k.val) -- Gauche peut aller vers nim(0), ..., nim(n)
(fun k => nim k.val) -- Droite aussi (jeu impartial)
#check nim
#check nim 0 -- = 0
#check nim 1 -- = *
#check nim 3
(funk=>nimk.val)-- Gauche peut aller vers nim(0), ..., nim(n)
(funk=>nimk.val)-- Droite aussi (jeu impartial)
nim:Nat→PG
nim0:PG
nim1:PG
nim3:PG
--% env 2
Raw input{"cmd": "-- Nim avec un tas de n objets\n-- nim(0) = 0 (pas de coup)\n-- nim(n) = {nim(0), ..., nim(n-1) | nim(0), ..., nim(n-1)}\n\ndef nim : Nat -> PG\n | 0 => PG.mk Empty Empty (fun e => e.elim) (fun e => e.elim)\n | n + 1 => PG.mk (Fin (n + 1)) (Fin (n + 1))\n (fun k => nim k.val) -- Gauche peut aller vers nim(0), ..., nim(n)\n (fun k => nim k.val) -- Droite aussi (jeu impartial)\n\n#check nim\n#check nim 0 -- = 0\n#check nim 1 -- = *\n#check nim 3", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data": "nim : Nat → PG"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "nim 0 : PG"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data": "nim 1 : PG"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data": "nim 3 : PG"}],
"env": 2}
Interpretation : definition de Nim en Lean
Les sorties #check confirment que notre fonction nim a le type attendu Nat -> PG. Chaque appel nim k produit bien une valeur de type PG (notre type de jeu). Notons que :
nim 0 est equivalent a PG.zero (le jeu nul, aucun coup)
nim 1 est equivalent a PG.star (le jeu etoile, premier joueur gagne)
nim 3 a 4 coups pour chaque joueur (vers nim(0), nim(1), nim(2), nim(3))
La recursion sur Nat avec Fin (n+1) pour les types de coups est le pattern canonique pour définir un jeu impartial en Lean : chaque joueur peut reduire le tas a n’importe quelle taille de 0 a n.
Valeur de Grundy
La valeur de Grundy (ou nimber) d’un jeu impartial \(G\) est définie par l’opérateur mex (minimum excludant) :
\[\text{grundy}(G) = \text{mex}\{\text{grundy}(G') : G' \text{ accessible depuis } G\}\]
Le mex d’un ensemble d’entiers est le plus petit entier non present dans cet ensemble. Par exemple : - \(\text{mex}\{0, 1, 2\} = 3\) - \(\text{mex}\{0, 2\} = 1\) - \(\text{mex}\{\} = 0\)
Pour nim(n), la valeur de Grundy est exactement \(n\) car les successeurs sont \(\{0, 1, \ldots, n-1\}\) et \(\text{mex}\{0, 1, \ldots, n-1\} = n\).
Theoreme de Sprague-Grundy
Theoreme : Tout jeu impartial est equivalent a un jeu de Nim.
\[G \equiv \text{nim}(\text{grundy}(G))\]
Pour une somme de jeux independants : \[\text{grundy}(G_1 + G_2 + \ldots + G_n) = \text{grundy}(G_1) \oplus \text{grundy}(G_2) \oplus \ldots \oplus \text{grundy}(G_n)\]
ou \(\oplus\) est le XOR binaire (ou exclusif bit a bit).
Consequence pratique : Pour determiner qui gagne une position composee de plusieurs sous-jeux impartiaux, il suffit de calculer les valeurs de Grundy individuelles et de les combiner par XOR. Si le résultat est 0, le second joueur gagne ; sinon, le premier joueur a une stratégie gagnante.
Exercice 1 : Stratégie gagnante au Nim multi-tas
Le Nim multi-tas est la forme classique du jeu : plusieurs tas independants, et a chaque tour un joueur retire des objets d’un seul tas. Le theoreme de Sprague-Grundy nous dit que la valeur de Grundy d’une position multi-tas est le XOR (ou exclusif) des valeurs de Grundy de chaque tas.
Position a analyser : 3 tas de tailles respectives 3, 5 et 6.
Questions : 1. Calculer la valeur de Grundy de chaque tas (indice : pour un tas de taille \(n\), la valeur de Grundy est \(n\)) 2. Calculer le XOR des trois valeurs : \(3 \oplus 5 \oplus 6\) 3. Determiner qui a une stratégie gagnante (premier ou second joueur) 4. Si le premier joueur gagne, trouver un coup gagnant
Rappel XOR (opération bit a bit) :
a
b
a XOR b
0
0
0
0
1
1
1
0
1
1
1
0
Indice pour le coup gagnant : si \(g = g_1 \oplus g_2 \oplus g_3 \neq 0\), il faut trouver un tas \(i\) tel que \(g_i \oplus g < g_i\). Le coup gagnant est de reduire ce tas a \(g_i \oplus g\).
-- Exercice 1 : Strategie gagnante au Nim multi-tas
-- Position : 3 tas de tailles 3, 5, 6
-- Etape 1 : Calculez le XOR binaire de 3, 5 et 6
-- Indice : ecrivez chaque nombre en binaire puis XOR colonne par colonne
-- 3 = 011, 5 = 101, 6 = 110
-- 3 XOR 5 = ? puis ? XOR 6 = ?
-- Etape 2 : Le resultat est-il 0 ?
-- Si oui : second joueur gagne (P-position)
-- Si non : premier joueur gagne (N-position), trouver le coup gagnant
-- TODO etudiant : ecrire la reponse dans un commentaire ci-dessous
-- Reponse : le XOR est _____ , donc _____ joueur gagne
-- Coup gagnant : reduire le tas de taille _____ a _____
#check Nat -- Exercice a completer
-- Exercice 1 : Strategie gagnante au Nim multi-tas
-- Position : 3 tas de tailles 3, 5, 6
-- Etape 1 : Calculez le XOR binaire de 3, 5 et 6
-- Indice : ecrivez chaque nombre en binaire puis XOR colonne par colonne
-- 3 = 011, 5 = 101, 6 = 110
-- 3 XOR 5 = ? puis ? XOR 6 = ?
-- Etape 2 : Le resultat est-il 0 ?
-- Si oui : second joueur gagne (P-position)
-- Si non : premier joueur gagne (N-position), trouver le coup gagnant
-- TODO etudiant : ecrire la reponse dans un commentaire ci-dessous
-- Reponse : le XOR est _____ , donc _____ joueur gagne
-- Coup gagnant : reduire le tas de taille _____ a _____
Nat:Type
--% env 3
Raw input{"cmd": "-- Exercice 1 : Strategie gagnante au Nim multi-tas\n-- Position : 3 tas de tailles 3, 5, 6\n\n-- Etape 1 : Calculez le XOR binaire de 3, 5 et 6\n-- Indice : ecrivez chaque nombre en binaire puis XOR colonne par colonne\n-- 3 = 011, 5 = 101, 6 = 110\n-- 3 XOR 5 = ? puis ? XOR 6 = ?\n\n-- Etape 2 : Le resultat est-il 0 ?\n-- Si oui : second joueur gagne (P-position)\n-- Si non : premier joueur gagne (N-position), trouver le coup gagnant\n\n-- TODO etudiant : ecrire la reponse dans un commentaire ci-dessous\n-- Reponse : le XOR est _____ , donc _____ joueur gagne\n-- Coup gagnant : reduire le tas de taille _____ a _____\n\n#check Nat -- Exercice a completer", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 17, "column": 0},
"endPos": {"line": 17, "column": 6},
"data": "Nat : Type"}],
"env": 3}
4. Exemples guides
Maintenant que nous avons défini les jeux primitifs et le jeu de Nim, nous pouvons construire des jeux plus complexes en combinant ces briques. La notation conventionnelle {L | R} ou L et R sont des ensembles de positions atteignables permet de définir n’importe quel jeu combinatoire.
Exemple guide 1 : Construire des jeux
L’objectif est de construire trois jeux qui illustrent des aspects différents de la théorie :
Le jeu \(2 = \{1|\}\) : un entier positif, ou Gauche a un avantage croissant. Gauche peut aller vers 1, qui lui-même va vers 0. C’est un jeu “positif” : Gauche gagne même en deuxieme.
Le jeu \(1/2 = \{0|1\}\) : un nombre surreel. Ce jeu est entre 0 et 1 — Gauche peut aller vers 0 (neutre) mais Droite peut aller vers 1 (avantage Gauche). C’est un “demi” avantage pour Gauche.
Le jeu \(\uparrow = \{0|*\}\) : un jeu “infinitesimal” positif. Plus petit que tout nombre positif mais pas nul. Il est utile dans l’analyse des jeux partizans.
Indices : - Pour un jeu avec un seul coup d’un cote, utiliser Unit comme type et Empty pour le cote sans coup - Pour un jeu avec un seul coup de chaque cote, utiliser Unit des deux cotes - fun e => e.elim est le terme prouvant l’impossibilite a partir de Empty
-- Correction Exemple guide 1
-- 1. Le jeu 2 = {1|}
def PG.two : PG := PG.mk Unit Empty (fun _ => PG.one) (fun e => e.elim)
-- 2. Le jeu 1/2 = {0|1}
def PG.half : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.one)
-- 3. Le jeu up = {0|*}
def PG.up : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.star)
#check PG.two
#check PG.half
#check PG.up
Raw input{"cmd": "-- Correction Exemple guide 1\n\n-- 1. Le jeu 2 = {1|}\ndef PG.two : PG := PG.mk Unit Empty (fun _ => PG.one) (fun e => e.elim)\n\n-- 2. Le jeu 1/2 = {0|1}\ndef PG.half : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.one)\n\n-- 3. Le jeu up = {0|*}\ndef PG.up : PG := PG.mk Unit Unit (fun _ => PG.zero) (fun _ => PG.star)\n\n#check PG.two\n#check PG.half\n#check PG.up", "env": 3}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "PG.two : PG"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data": "PG.half : PG"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data": "PG.up : PG"}],
"env": 4}
5. Nombres Surreels
Le theoreme de Sprague-Grundy nous a montre que tout jeu impartial se ramene a Nim. Mais les jeux partizans (coups différents selon le joueur) ouvrent un monde bien plus riche : les nombres surreels, decouverts par Conway en 1969.
L’idee profonde est qu’un nombre surreal est un jeu ou les options de Gauche sont toutes inferieures aux options de Droite. Autrement dit, un nombre est un jeu “ordonne” :
\[\text{Si } x^L < x^R \text{ pour tout } x^L \in L, x^R \in R, \text{ alors } \{L \mid R\} \text{ est un nombre surreal}\]
Les nombres surreels forment un corps ordonne qui contient a la fois les reels, les ordinaux transfinis, et des infiniment petits non standards.
Jeu
Notation
Valeur
Construction
\({\mid}\)
PG.zero
\(0\)
Aucune option : le jeu nul
\({0\mid}\)
PG.one
\(1\)
Gauche peut aller a 0
\({\mid 0}\)
PG.negOne
\(-1\)
Droite peut aller a 0
\({0\mid 1}\)
PG.half
\(1/2\)
Entre 0 et 1 (premier “demi”)
\({0,1\mid}\)
PG.two
\(2\)
Gauche peut aller a 0 ou 1
Remarque : Les nombres surreels n’existent pas seulement en mathematiques abstraites. Dans le jeu de Domineering par exemple, certaines positions ont des valeurs surreelles comme \({1/2}\) ou \({\uparrow} = {0 \mid *}\). Connaitre ces valeurs permet de determiner qui gagne une position sans explorer l’arbre de jeu complet.
Dans mathlib4 : Mathlib.SetTheory.Surreal.Basic
Exercice 2 : Construire un jeu partizan
Le jeu de Domineering se joue sur une grille. Gauche place des dominos verticaux (2x1), Droite place des dominos horizontaux (1x2). Considerez la position la plus simple : une grille \(2 \times 1\) (2 cases en colonne).
Sur cette grille : - Gauche peut placer un domino vertical (il prend les 2 cases) et le jeu se termine - Droite ne peut pas placer de domino horizontal (pas assez de cases en largeur)
Votre tâche : définir ce jeu dans le type PG en utilisant les constructions vues precedemment.
Indices : - Quel type utiliser pour les coups de Gauche ? (1 coup possible) - Quel type utiliser pour les coups de Droite ? (0 coup possible) - Vers quelle position Gauche arrive-t-il après son coup ? - Ce jeu est-il un nombre surreal ? Lequel ?
-- Exercice 2 : Domineering 2x1
-- Definissez le jeu Domineering sur une grille 2x1
-- Indice : Gauche a 1 coup, Droite en a 0
-- def domineering2x1 : PG := sorry -- TODO etudiant : definir le jeu
-- Questions supplementaires :
-- 1. Quelle est la valeur de ce jeu ? (indice : c'est un entier)
-- 2. Qui gagne cette position ?
-- 3. Que se passe-t-il sur une grille 1x2 ?
#check Nat -- Exercice a completer
-- Exercice 2 : Domineering 2x1
-- Definissez le jeu Domineering sur une grille 2x1
-- Indice : Gauche a 1 coup, Droite en a 0
-- def domineering2x1 : PG := sorry -- TODO etudiant : definir le jeu
-- Questions supplementaires :
-- 1. Quelle est la valeur de ce jeu ? (indice : c'est un entier)
-- 2. Qui gagne cette position ?
-- 3. Que se passe-t-il sur une grille 1x2 ?
Nat:Type
--% env 5
Raw input{"cmd": "-- Exercice 2 : Domineering 2x1\n-- Definissez le jeu Domineering sur une grille 2x1\n\n-- Indice : Gauche a 1 coup, Droite en a 0\n-- def domineering2x1 : PG := sorry -- TODO etudiant : definir le jeu\n\n-- Questions supplementaires :\n-- 1. Quelle est la valeur de ce jeu ? (indice : c'est un entier)\n-- 2. Qui gagne cette position ?\n-- 3. Que se passe-t-il sur une grille 1x2 ?\n\n#check Nat -- Exercice a completer", "env": 4}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "Nat : Type"}],
"env": 5}
6. API mathlib4
Les definitions que nous avons utilisees (PG, SimplePGame) sont des versions simplifiees pour comprendre les concepts. En production, mathlib4 offre une API complete et formellement verifiee. Cette section presente les modules cles et leurs signatures, pour servir de reference lors de l’exploration de la bibliotheque.
Modules principaux
Module
Contenu
Usage dans ce notebook
Mathlib.SetTheory.PGame.Basic
Definition inductive PGame, relations d’equivalence et d’ordre
Equivalent de notre SimplePGame avec univers
Mathlib.SetTheory.Game.Nim
nim, grundyValue, theoreme de Sprague-Grundy
Equivalent de notre fonction nim sur Nat
Mathlib.SetTheory.Surreal.Basic
Nombres surreels comme quotient de jeux
Equivalent de nos constructions ad hoc
Principales definitions
-- PGame (version mathlib avec univers)
inductive PGame
| mk : (a b : Type u) -> (a -> PGame) -> (b -> PGame) -> PGame
-- Accesseurs
def LeftMoves (G : PGame) : Type
def RightMoves (G : PGame) : Type
def moveLeft (G : PGame) : G.LeftMoves -> PGame
def moveRight (G : PGame) : G.RightMoves -> PGame
-- Nim et Grundy (sur les ordinaux, pas seulement Nat)
def nim (n : Ordinal) : PGame
def grundyValue (G : Game) : Ordinal
-- Theoreme Sprague-Grundy
theorem equiv_nim_grundyValue (G : Game) [G.Impartial] :
G ~ nim (grundyValue G)
Différence cle avec nos definitions : mathlib4 utilise Ordinal (et non Nat) pour les valeurs de Grundy, ce qui permet de traiter des jeux infinis. De plus, la classe Impartial formalise la propriete d’impartialite comme une instance de typeclass, permettant au compilateur de verifier automatiquement cette condition.
Note technique : Le theoreme equiv_nim_grundyValue est le résultat central : il affirme que tout jeu impartial G est equivalent (au sens de la relation ~) au jeu de nim avec un seul tas de taille grundyValue G. C’est la formalisation complete du theoreme de Sprague-Grundy.
Resume et synthese
Ce notebook a permis de decouvrir comment la théorie des jeux combinatoires de Conway se formalise en Lean 4. Voici les acquis principaux :
Concept
Definition Lean
Insight cle
PGame
Type inductif paramètre par les types de coups L et R
Un jeu = ses positions atteignables, rien d’autre
Jeux primitifs
zero, one, negOne, star
Les 4 briques de base : P-position, L-win, R-win, N-position
Nim
Recursion sur Nat avec Fin n pour les coups
Jeu impartial par excellence : les mêmes coups pour les deux joueurs
Sprague-Grundy
grundyValue + XOR pour les sommes
Tout jeu impartial se ramene a un tas de Nim
Nombres surreels
Jeux numériques quotientes
0, 1, -1, 1/2… sont des jeux avant d’etre des nombres
Points cles a retenir :
La structure PG.mk L R moveL moveR est universelle : elle encode n’importe quel jeu combinatoire a deux joueurs, impartial ou partizan. Les types L et R definissent l’ensemble des coups ; les fonctions moveL et moveR definissent les positions resultantes.
L’impartialite se traduit par L = R : quand les types de coups gauches et droits sont identiques et les fonctions de mouvement coincident, le jeu est impartial. C’est le cas de nim.
Le mex (minimum excludant) est l’opération fondamentale de la théorie des jeux impartiaux. La valeur de Grundy d’un jeu est le plus petit entier non atteignable par ses successeurs, ce qui garantit l’unicite de la decomposition en somme de Nim.
Les nombres surreels sont des jeux : Conway a montre que les reels (et au-dela) emergent naturellement de la théorie des jeux combinatoires. Le nombre 1/2 par exemple est le jeu {0 | 1}.
Note technique : Nos definitions PG, SimplePGame sont des versions simplifiees. La vraie API mathlib4 (Mathlib.SetTheory.PGame) utilise des univers de types et des constructions plus elaborees pour supporter les ordinaux transfinis et les preuves formelles.
Pour aller plus loin
8c-CombinatorialGames-Python : Implementations Python des algorithmes de Grundy, resolution de Nim, et visualisations
Lien avec lean_game_defs : Les concepts de ce notebook — arbres de jeux, minimax, Nim, Sprague-Grundy — sont définis dans lean_game_defs/Combinatorial.lean (0 sorry). On y trouve le type inductif GameTree (feuilles et nœuds), la fonction minimax (évaluation alternée max/min), les définitions Nim (NimHeap, NimPosition, nimSum pour le XOR, isWinningNim pour la détermination du gagnant, nimMoves pour les coups valides), le type TwoPlayerGame (structure générique pour jeux à information parfaite avec état, alternance, coups, terminaux, gagnant), la fonction isWinning (induction à rebours), l’instance nimGame (Nim comme TwoPlayerGame), et les fonctions mex (minimum excludant) et grundyValue (calcul de la valeur de Grundy). Le module Basic.lean (0 sorry) fournit les types de base sous-jacents.
Exercice 3 : Classification d’un jeu
Parmi les quatre classes de la théorie des jeux combinatoires (P-position, N-position, L-position, R-position), determinez la classe du jeu suivant et justifiez votre reponse en identifiant les coups disponibles pour chaque joueur :
Jeu a analyser : \(G = \{1, * \mid 0\}\)
Indices : - Enumerez d’abord les coups de Gauche et de Droite - Determinez si le jeu est impartial (mêmes coups) ou partizan - Testez chaque scénario : Gauche commence, puis Droite commence - Rappel : P = second joueur gagne, N = premier joueur gagne, L = Gauche gagne toujours, R = Droite gagne toujours
-- Exercice 3 : Classification d'un jeu
-- G = {1, * | 0} — determinez la classe (P/N/L/R) de ce jeu
-- Etape 1 : Definissez le jeu G dans notre type PG
-- Indice : Gauche a 2 coups (vers 1 et vers *), Droite a 1 coup (vers 0)
-- Pour 2 coups, utiliser `Fin 2` comme type (valeurs 0 et 1)
-- def myGame : PG := sorry -- TODO etudiant : definir G = {1, * | 0}
-- Etape 2 : Analysez les scenarios
-- Si Gauche commence : peut aller vers 1 (L-win) ou * (N-position, premier gagne)
-- Si Droite commence : peut aller vers 0 (P-position, second gagne = Gauche)
-- TODO etudiant : ecrire la classification et la justification
-- Classification : _____ -position
-- Justification : _____
#check Nat -- Exercice a completer
-- Exercice 3 : Classification d'un jeu
-- G = {1, * | 0} — determinez la classe (P/N/L/R) de ce jeu
-- Etape 1 : Definissez le jeu G dans notre type PG
-- Indice : Gauche a 2 coups (vers 1 et vers *), Droite a 1 coup (vers 0)
-- Pour 2 coups, utiliser `Fin 2` comme type (valeurs 0 et 1)
-- def myGame : PG := sorry -- TODO etudiant : definir G = {1, * | 0}
-- Etape 2 : Analysez les scenarios
-- Si Gauche commence : peut aller vers 1 (L-win) ou * (N-position, premier gagne)
-- Si Droite commence : peut aller vers 0 (P-position, second gagne = Gauche)
-- TODO etudiant : ecrire la classification et la justification
-- Classification : _____ -position
-- Justification : _____
Nat:Type
--% env 6
Raw input{"cmd": "-- Exercice 3 : Classification d'un jeu\n-- G = {1, * | 0} \u2014 determinez la classe (P/N/L/R) de ce jeu\n\n-- Etape 1 : Definissez le jeu G dans notre type PG\n-- Indice : Gauche a 2 coups (vers 1 et vers *), Droite a 1 coup (vers 0)\n-- Pour 2 coups, utiliser `Fin 2` comme type (valeurs 0 et 1)\n\n-- def myGame : PG := sorry -- TODO etudiant : definir G = {1, * | 0}\n\n-- Etape 2 : Analysez les scenarios\n-- Si Gauche commence : peut aller vers 1 (L-win) ou * (N-position, premier gagne)\n-- Si Droite commence : peut aller vers 0 (P-position, second gagne = Gauche)\n\n-- TODO etudiant : ecrire la classification et la justification\n-- Classification : _____ -position\n-- Justification : _____\n\n#check Nat -- Exercice a completer", "env": 5}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 6},
"data": "Nat : Type"}],
"env": 6}