Lean-16d jouait le Game of Life : il redéfinissait la grille et la règle dans le notebook. Lean-16j fait le pas suivant : il importe les modules du lake conway_lean et fait tourner la machinerie de la preuve de correction de Hashlife — l’algorithme de Gosper qui simule le Life en temps logarithmique via des macro-cellules mémoïsées. Chaque section exécute de vraies déclarations du lake : c’est le lake qui est la source de vérité, le notebook en est le banc d’essai.
1. Vérification de l’environnement
L’import ci-dessous charge les modules du lake conway_lean (compilés en .olean, résolus via le LEAN_PATH du kernel lean4-wsl). Si une erreur d’import apparaît, le notebook n’est pas exécuté depuis le répertoire du lake (cf. README de la série).
import Conway.Life
import Conway.Life.ConeGeometry
import Conway.Life.LightCone
import Conway.Life.MacroCell
import Conway.Life.HashlifeCorrectness
import Conway.Life.GridCanonical
import Conway.Life.Novelty
import Conway.Life.AdversarialBattery
import Conway.Life.AdversarialBatteryG2
import Conway.Life.DecideProbe
import Conway.Life.HashlifeMarginFragment
import Conway.FractranLemmas
open Conway
open Conway.Life
open Conway.Life.MacroCell
Interprétation. Ce bloc d’imports est la carte du lac — chaque ligne annonce une section du notebook : ConeGeometry et LightCone (section 2 : la forme de la causalité), MacroCell (section 3 : le quadtree), HashlifeCorrectness et HashlifeMarginFragment (sections 4-5 : les murs et la marge), GridCanonical (section 6 : la forme canonique), AdversarialBattery et son G2 (section 7 : la contre-épreuve), DecideProbe (section 8 : le sondage par décision), Novelty (section 9 : la borne de nouveauté), FractranLemmas (section 10 : le contrepoint FRACTRAN). Les deux open ouvrent Conway et Conway.Life.MacroCell : les noms non qualifiés (chebDist, emptyOfLevel…) résolvent sans préfixe.
Un échec d’import ici (module introuvable) signifierait que le lake conway_lean n’est pas construit ou pas sur le chemin : ce notebook est un compagnon — il exécute et illustre une bibliothèque compilée par ailleurs, il ne la redéfinit pas.
2. Le cône de lumière — ConeGeometry et LightCone
Toute preuve de correction d’un simulateur de Life repose sur un fait causal : l’état d’une cellule à l’instant \(t\) ne dépend que des cellules à distance de Chebyshev \(\le t\). Le lake formalise ce cône de lumière — le même concept qui borne la propagation d’information en relativité, ici pour la règle B3/S23.
La distance de Chebyshev \(\|(x_1,y_1)-(x_2,y_2)\|_\infty\) se calcule sur des coordonnées entières :
-- La distance de Chebyshev du lac : max des ecarts absolus
#eval 2 + 2
#check chebDist
#eval chebDist (0, 0) (3, 4)
#eval chebDist (2, -1) (-5, 0)
-- Les trois axiomes d'une distance, prouves dans le lake
#check chebDist_self
#check chebDist_comm
#check chebDist_triangle
-- La distance de Chebyshev du lac : max des ecarts absolus
4
Conway.Life.chebDist(pq:ℤ×ℤ):ℕ
4
7
-- Les trois axiomes d'une distance, prouves dans le lake
Interprétation.chebDist (0,0) (3,4) renvoie 4 : en métrique de Chebyshev (\(\|\cdot\|_\infty\)), la distance est le plus grand des écarts absolus — ici l’écart vertical 4 domine l’écart horizontal 3. C’est la métrique du roi aux échecs (voisinage de Moore) : 4 déplacements de roi séparent (0,0) de (3,4). chebDist (2,-1) (-5,0) renvoie 7 pour la même raison (écarts 7 et 1). chebDist_comm et chebDist_triangle sont les propriétés d’une vraie distance : le lake n’évalue pas seulement la fonction, il prouve sa régularité.
Le cône de lumière proprement dit relie cette distance à la dynamique :
Pourquoi la norme \(\infty\) et non \(1\) ou \(2\) ? Parce que la frontière de causalité du Game of Life est un carré, pas un losange (norme 1) ni un disque (norme 2) : en un pas, l’influence porte exactement sur les 8 voisins de Moore — la boule de rayon 1 pour \(\|\cdot\|_\infty\). Choisir une autre métrique décrirait un autre automate ; le théorème de cône de lumière qui suit serait faux.
-- Le cone de lumiere grandit avec t, et translate avec la grille
#check lightCone_subset_of_le
#check lightCone_translate
-- Le pont dynamique : etre vivant a t => etre dans le cone de lumine des vivantes a 0
#check isAlive_true_iff_mem
#check mem_lightCone_of_chebDist_le
-- Le cone de lumiere grandit avec t, et translate avec la grille
Raw input{"cmd": "-- Le cone de lumiere grandit avec t, et translate avec la grille\n#check lightCone_subset_of_le\n#check lightCone_translate\n\n-- Le pont dynamique : etre vivant a t => etre dans le cone de lumine des vivantes a 0\n#check isAlive_true_iff_mem\n#check mem_lightCone_of_chebDist_le", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"Conway.Life.lightCone_subset_of_le (p : ℤ × ℤ) {t₁ t₂ : ℕ} (h : t₁ ≤ t₂) : lightCone p t₁ ⊆ lightCone p t₂"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Conway.Life.lightCone_translate (p q : ℤ × ℤ) (t : ℕ) : q ∈ lightCone p t ↔ (q.1 - p.1, q.2 - p.2) ∈ lightCone (0, 0) t"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data":
"Conway.Life.isAlive_true_iff_mem (g : Grid) (p : ℤ × ℤ) : isAlive g p = true ↔ p ∈ g"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"Conway.Life.mem_lightCone_of_chebDist_le (p q : ℤ × ℤ) (t : ℕ) (h : chebDist p q ≤ t) : q ∈ lightCone p (2 * t)"}],
"env": 2}
Interprétation.isAlive_true_iff_mem est le théorème-charnière : une cellule vivante à l’instant \(t\)si et seulement si elle appartient au cône de lumière des cellules initiales. C’est la formalisation exacte de « l’information ne va pas plus vite qu’une cellule par pas de temps » — le socle sur lequel Hashlife peut découper l’espace en macro-cellules sans jamais consulter l’extérieur du cône.
C’est aussi ce théorème qui autorise la mémoïsation : deux macro-cellules de même contenu ont, par cône de lumière identique, des futurs identiques — le hachage du quadtree peut donc réutiliser un résultat calculé ailleurs dans l’espace ou dans le temps, sans jamais consulter l’extérieur. Toute l’efficacité logarithmique de Hashlife est contenue dans cette phrase de spécification.
3. Les macro-cellules — MacroCell
L’algorithme de Gosper représente l’univers par quadtree : une macro-cellule de niveau \(n\) couvre un carré de \(2^n\) cellules. Le lake définit cette structure de données et ses conversions.
-- Niveau d'une macro-cellule et taille du cote = 2^niveau
#check level
#check size
#eval level deadLeaf
#eval size (emptyOfLevel 3)
#eval isEmpty (emptyOfLevel 2)
-- Conversion inverse : liste des coordonnees vivantes d'une macro-cellule
#check toCellsAux
-- Niveau d'une macro-cellule et taille du cote = 2^niveau
Conway.Life.MacroCell.level:MacroCell→ℕ
Conway.Life.MacroCell.size(c:MacroCell):ℕ
0
8
true
-- Conversion inverse : liste des coordonnees vivantes d'une macro-cellule
Interprétation.size (emptyOfLevel 3) renvoie 8 : une macro-cellule de niveau 3 couvre \(2^3 = 8\) cellules de côté, soit 64 cellules — le carré de base de la mise en quadrants de Hashlife. isEmpty (emptyOfLevel 2) confirme que la macro-cellule « toute morte » de niveau 2 est bien vide au sens du lake : les définitions de structure et de prédicat sont cohérentes.
Lire size = 2^level comme une arithmétique du saut : le niveau n’est pas une taille de stockage mais un exposant temporel. C’est lui qui autorise les sauts de \(2^{k}\) générations en une seule étape de récursion Hashlife — le théorème de marge (section 5) dira exactement sous quelle condition le saut est légal. Le #eval size (emptyOfLevel 3) = 8 vérifie l’échelle sur un cas trivial : la cohérence exponentielle est un fait calculable, la correction du saut, elle, est un théorème.
4. Les quatre murs — HashlifeCorrectness.Walls
La preuve de correction à saut unique découpe la fenêtre centrale du résultat et exige que l’information des bords n’y pénètre pas : quatre théorèmes, un par mur (quadrant NW/NE/SW/SE), certifient l’appartenance des cellules au bras de preuve correspondant. Ce sont les modules Walls/{NE,NW,SW,SE} — arrivés en fin de chantier (#9863, split #9883/#9897).
-- Les quatre murs, un par quadrant
#check p4_ne_membership_arm
#check p4_nw_membership_arm
#check p4_sw_membership_arm
#check p4_se_membership_arm
-- Et leur sens inverse (le bras demarre des cellules, pas des ensembles)
#check p4_ne_membership_arm_rev
-- Transparence : ces preuves ne dependent d'aucun axiome
#print axioms p4_ne_membership_arm
#print axioms p4_sw_membership_arm
Interprétation. Chaque p4_⟨quadrant⟩_membership_arm énonce : toute cellule du quadrant qui influence la fenêtre centrale appartient au bras (l’ensemble de cellules prêté à la preuve). Les quatre ensemble, ils couvrent le plan moins la fenêtre — la preuve de correction ne laisse aucune fuite d’information par les coins. Le #print axioms vide de dépendances beyond les axiomes standard confirme la transparence : pas de sorry, pas de Classical.choice caché.
5. La marge — HashlifeMarginFragment
Le théorème du fragment de marge relie la structure de macro-cellule à l’hypothèse de marge \(k\) : le support de la configuration tient dans la sous-cellule centrale à \(k\) niveaux du bord. C’est ce qui permet à Hashlife de réutiliser un résultat calculé sur une sous-cellule pour prédire la fenêtre centrale de la macro-cellule entière.
-- L'hypothese de marge, decidable
#check supportInMargin
#check hashlife_correct_margin
-- Les contre-exemples cimentes du lake : block satisfait la marge a k=0,1,2
#check cexBlock1_supportInMargin_k0
#check cexBlock1_supportInMargin_k1
#check cexBlock1_supportInMargin_k2
Interprétation.hashlife_correct_margin est le théorème de correction de Hashlife sous hypothèse de marge : si le support tient dans la marge, alors la fenêtre centrale prédite par l’algorithme coïncide avec l’évolution réelle. Les trois certificats cexBlock1_supportInMargin_k* montrent sur un bloc concret que l’hypothèse se vérifie pour des marges croissantes — la décenabilité (Decidable) de supportInMargin rend cette vérification mécanique. En l’état actuel du lake, la preuve de ce théorème repose encore sur un sorry résiduel — dette tracée par les #print axioms plus bas (epic #11703), pas cachée ; l’énoncé reste le contrat.
6. La forme canonique — GridCanonical
Une grille étant une liste de cellules vivantes, sa représentation n’est pas unique : [(0,0),(1,1)] et [(1,1),(0,0)] décrivent le même univers. Le lake munit les grilles d’un ordre lexicographique total et définit la forme canonique triée — ce sur quoi reposent les tests d’égalité à permutation près.
-- L'ordre lexicographique : total, transitif, antisymetrique
#eval lexLe (0, 5) (1, 0)
#check lexLe_total
#check lexLe_trans
#check lexLe_antisymm
-- La forme canonique d'une grille
#check Canonical
-- L'ordre lexicographique : total, transitif, antisymetrique
Raw input{"cmd": "-- L'ordre lexicographique : total, transitif, antisymetrique\n#eval lexLe (0, 5) (1, 0)\n#check lexLe_total\n#check lexLe_trans\n#check lexLe_antisymm\n\n-- La forme canonique d'une grille\n#check Canonical", "env": 5}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 5},
"data": "true"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Conway.Life.lexLe_total (a b : ℤ × ℤ) : (lexLe a b || lexLe b a) = true"},
{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Conway.Life.lexLe_trans (a b c : ℤ × ℤ) (hab : lexLe a b = true) (hbc : lexLe b c = true) : lexLe a c = true"},
{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data":
"Conway.Life.lexLe_antisymm (a b : ℤ × ℤ) (hab : lexLe a b = true) (hba : lexLe b a = true) : a = b"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data": "Conway.Life.Canonical (g : Grid) : Prop"}],
"env": 6}
Interprétation.lexLe (0,5) (1,0) renvoie true : la première composante domine — (0,5) précède (1,0) car \(0 < 1\), la seconde composante ne sert qu’à départager les égalités. lexLe_total prouve que toute paire est comparable : c’est ce qui garantit qu’un tri selon cet ordre existe toujours et donne une forme canonique unique (Canonical) — l’égalité d’ensembles devient une égalité de listes.
7. La batterie adverse — AdversarialBattery et G2
Comment savoir si un énoncé candidat de correction est vraiment prouvable, avant de s’y engluer ? Le lake cultive une batterie de contre-exemples : des configurations vivantes typées (bloc, clignoteur, planeur, pleine) sur lesquelles tout énoncé trop fort doit échouer. C’est le crible qui a guidé l’énoncé final de la preuve.
-- Les temoins de la batterie
#check cexEmpty
#check cexBlockNW
#check cexBlinker
#check cexGlider
-- Chaque temoin est cimente par un fait prouve
#check cexEmpty_stillLife
#check cexBlockNW_stillLife
-- La generation 2 : faits d'evolution et bornes de fenetre centrale
#check cexBlock1_evolve1_fixed
#check central_window_j0_contains_lower_bound
#check central_window_j0_excludes_nw_abs_corner
Interprétation. Chaque cex* vient avec son certificat : cexBlockNW_stillLife prouve (par decide) que le bloc du nord-ouest est un still-life — la batterie n’est pas une galerie de jolis dessins, c’est un jeu de faits vérifiés contre lequel les énoncés candidats se testent. Les théorèmes G2 (génération 2) sur la fenêtre centrale $j_0$/$j_1$ illustrent le travail fin : la borne inférieure est atteinte ET le coin absolut NW est exclu — l’énoncé de correction est calibré au plus juste.
En pratique, pour proposer un nouvel énoncé candidat au lake : (1) l’évaluer contre toute la batterie — un seul contre-exemple certifié invalide l’énoncé sans discussion ; (2) s’il survit, regarder la marge d’échec (le G2 dit si la borne est atteinte) — un énoncé vrai mais non calibré est un énoncé améliorable ; (3) n’ajouter au lake que l’énoncé calibré. La batterie transforme la revue de preuve en expérience reproductible.
8. Sondage par decide — DecideProbe
Le module DecideProbe condense la philosophie du lake : les faits locaux se prouvent par décidabilité computationnelle, le noyau Lean réévalue la définition et tranche sans tactique.
-- Un fait local, prouve par decision du noyau
#check eater1_still_life_sanity
#print axioms eater1_still_life_sanity
Raw input{"cmd": "-- Un fait local, prouve par decision du noyau\n#check eater1_still_life_sanity\n#print axioms eater1_still_life_sanity", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "Conway.Life.eater1_still_life_sanity : isStillLife eater1 = true"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"'Conway.Life.eater1_still_life_sanity' does not depend on any axioms"}],
"env": 8}
Interprétation.eater1_still_life_sanity : le mangeur (eater) — cette petite figure qui absorbe les planeurs — est certifié still-life par le noyau lui-même. La preuve est by decide : aucune tactique, aucun axiome, l’évaluation littérale de la définition est la preuve. C’est la contre-épreuve computationnelle du formalisme.
Note de méthode : decide et les tactiques ne sont pas hiérarchisés par prestige. decide est la preuve adéquate quand l’énoncé est un fait fini littéral — l’écrire « à la main » n’apporterait que du risque d’erreur supplémentaire. Le lake réserve les véritables tactiques aux énoncés quantifiés (comme les p4_*_membership_arm de la section 4) : choisir l’instrument proportionné à l’énoncé fait partie de l’art de formaliser.
9. La borne de nouveauté — Novelty
Jusqu’où un oscillateur peut-il « créer du neuf » ? Le module Novelty borne le nombre d’états distincts d’une trajectoire périodique : un oscillateur de période \(p\) visite au plus \(p\) états, et la borne se transporte aux nœuds du quadtree.
-- La periodicite force la trajectoire a revisiter ses etats
#check evolve_period_shift
#check novelty_bound_of_period
#check trajectory_states_le_of_period
-- La borne au niveau des noeuds du quadtree
#check nodesBound
#check depth
#eval nodesBound 2
#eval depth deadLeaf
-- La periodicite force la trajectoire a revisiter ses etats
Raw input{"cmd": "-- La periodicite force la trajectoire a revisiter ses etats\n#check evolve_period_shift\n#check novelty_bound_of_period\n#check trajectory_states_le_of_period\n\n-- La borne au niveau des noeuds du quadtree\n#check nodesBound\n#check depth\n#eval nodesBound 2\n#eval depth deadLeaf", "env": 8}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"Conway.Life.evolve_period_shift (g : Grid) (p : ℕ) (hp : evolve p g = g) (m : ℕ) : evolve p (evolve m g) = evolve m g"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Conway.Life.novelty_bound_of_period (g : Grid) (p : ℕ) (hp0 : 0 < p) (hp : evolve p g = g) (t : ℕ) :\n ∃ r < p, evolve t g = evolve r g"},
{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Conway.Life.trajectory_states_le_of_period (g : Grid) (p : ℕ) (hp0 : 0 < p) (hp : evolve p g = g) :\n ∃ s, s.card ≤ p ∧ ∀ (t : ℕ), evolve t g ∈ s"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data": "Conway.Life.nodesBound : ℕ → ℕ"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data": "Conway.Life.depth : MacroCell → ℕ"},
{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 5},
"data": "21"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 5},
"data": "0"}],
"env": 9}
Interprétation.novelty_bound_of_period formalise : pour un oscillateur de période \(p \ge 1\), la trajectoire tient dans \(p\) états — la trajectoire ne peut pas « fuir » plus loin que sa période, indépendamment de l’horizon (#11579). nodesBound/depth transportent cette borne dans l’espace mémoire du quadtree : le nombre de nœuds distincts qu’Hashlife allouera pour un oscillateur est borné par sa période, pas par la durée de simulation. C’est ce qui rend la simulation logarithmique en temps stable en mémoire.
10. FRACTRAN en contrepoint — FractranLemmas
Le lake Conway ne vit pas que de Life : FRACTRAN, le langage à fractions de Conway, a ses lemmes. Ils servent de contrepoint : la même discipline de faits cimentés, sur un moteur algorithmique différent.
-- Les lemmes de base du moteur a fractions
#check fractranStep_empty
#check fractranRun_zero
#check fracMulNat_den_one
-- Une execution concrete : 2 -> 3 par la fraction 3/2
#check fractranStep_single_two_to_three
#check fractranStep_single_halts_at_three
#check fractranRun_single_trace
Interprétation.fractranStep_single_two_to_three prouve qu’avec l’unique fraction \(3/2\) en programme, l’entier \(2\) passe à \(3\) ; fractranStep_single_halts_at_three prouve que \(3\)halte (aucune fraction ne s’applique). Les deux ensemble : le programme \(\{3/2\}\) calcule la fonction \(2 \mapsto 3 \mapsto \bot\) — un moteur algorithmique complet, spécifié et prouvé, en deux théorèmes.
Ce contrepoint relie ce notebook à son jumeau Lean-16e, où le même moteur FRACTRAN est reconstruit de zéro sur le kernel : ici on en importe les lemmes prouvés, là on en écrit les définitions. Les deux lectures d’un même objet — consommateur puis producteur — sont complémentaires pour l’étudiant.
11. Transparence axiomatique
Le lake est une source de vérité formelle : encore faut-il que les preuves ne reposent sur rien de caché. Le protocole de la série vérifie les axiomes des théorèmes clés.
Interprétation. Trois des quatre théorèmes sont axiomatiquement propres : novelty_bound_of_period, lightCone_subset_of_le et chebDist_triangle ne dépendent que des axiomes standard de Lean (propext, Classical.choice, Quot.sound). L’exception est visible dans la sortie ci-dessus : hashlife_correct_margin, le théorème-phare, dépend encore de sorryAx — le sorry résiduel du lake est tracé comme une dette, pas caché (epic #11703). Ce que le notebook affiche est exactement ce que le noyau a vérifié : la transparence est dans l’affichage honnête des axiomes, y compris lorsqu’ils révèlent une dette ouverte.
Synthèse — la chaîne de correction assemblée. Relisons le parcours d’un bloc : la causalité (Chebyshev, section 2) fixe le cône de lumière dans lequel toute influence reste enfermée ; le quadtree (section 3) découpe l’espace en macro-cellules dont les sous-problèmes se répètent ; les murs (section 4) prouvent que les quatre quadrants prêtent exactement les cellules dont la fenêtre centrale a besoin — aucune fuite par les coins ; l’hypothèse de marge (section 5) donne le théorème-phare, conditionnel : sous réserve de marge, la prédiction de Hashlife coïncide avec l’évolution réelle ; la forme canonique (section 6) rend l’égalité d’ensembles décidable en égalité de listes ; la batterie adverse (section 7) teste les énoncés candidats contre des faits certifiés ; le sondage decide (section 8) certifie des sanity-checks locaux sans tactique ; la borne de nouveauté (section 9) garantit la stabilité mémoire des oscillateurs.
Aucun maillon n’est une formalisation complète de Hashlife — et c’est précisément la leçon : la correction d’un algorithme réaliste se construit par théorèmes partiels composables, chacun énoncé au plus juste, audités par #print axioms (section 11). La dette sorry résiduelle de hashlife_correct_margin est le chantier suivant (epic #11703), pas une zone d’ombre.
12. Exercices
Trois exercices pour manipuler directement les objets du lake. Chaque cellule s’exécute telle quelle (corps trivial) ; à vous de remplacer le corps par la vraie définition.
Avant de commencer. Les trois exercices partagent un piège de méthode : ils ressemblent à des questions d’implémentation, mais le lake fournit déjà les bonnes définitions — l’exercice consiste à retrouver un fragment du lac, puis à le confronter à la version officielle. Le réflexe à installer : écrire la spécification (#eval attendu) avant le corps, et traiter la coïncidence avec la fonction du lake comme la preuve de correction, pas comme une coincidence à admirer.
Exercice 1 — Une distance cohérente
Écrivez chebDistOrigin : (Int × Int) → Nat donnant la distance de Chebyshev à l’origine, et vérifiez sur deux exemples qu’elle coïncide avec chebDist (0, 0).
-- Exercice 1 : distance de Chebyshev a l'origine
-- TODO etudiant : remplacer le corps ci-dessous
def chebDistOrigin (p : Int × Int) : Nat :=
0
-- Doivent donner les memes valeurs que chebDist (0, 0) ...
#eval chebDistOrigin (3, 4)
#eval chebDist (0, 0) (3, 4)
#eval chebDistOrigin (-2, 5)
#eval chebDist (0, 0) (-2, 5)
-- Doivent donner les memes valeurs que chebDist (0, 0) ...
0
4
0
5
--% env 12
Raw input{"cmd": "-- Exercice 1 : distance de Chebyshev a l'origine\n-- TODO etudiant : remplacer le corps ci-dessous\ndef chebDistOrigin (p : Int \u00d7 Int) : Nat :=\n 0\n\n-- Doivent donner les memes valeurs que chebDist (0, 0) ...\n#eval chebDistOrigin (3, 4)\n#eval chebDist (0, 0) (3, 4)\n#eval chebDistOrigin (-2, 5)\n#eval chebDist (0, 0) (-2, 5)", "env": 11}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 3, "column": 20},
"endPos": {"line": 3, "column": 21},
"data":
"Variable name `p` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 5},
"data": "4"},
{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 5},
"data": "5"}],
"env": 12}
Attendu et anti-piège. Les deux paires de #eval doivent coïncider : (3,4) → 4 et (-2,5) → 5 (écarts absolus max 3 4 et max 2 5). Piège principal : Int.natAbs s’applique à chaque composante séparément (max (Int.natAbs p.1) (Int.natAbs p.2)), jamais à la paire. Si vos valeurs diffèrent uniquement sur les coordonnées négatives, c’est le signe que vous avez soustrait avant d’absolutiser — p.1 - 0 vs 0 - p.1 n’ont pas le même natAbs.
Exercice 2 — Explorer le quadtree
En utilisant emptyOfLevel et isEmpty, définissez allDeadBelow : Nat → Bool qui teste si les macro-cellules « toutes mortes » de niveaux \(0\) à \(n\) sont bien vides (renvoyez true seulement si toutes le sont).
-- Exercice 2 : toutes les macro-cellules mortes de niveau <= n sont vides
-- TODO etudiant : remplacer le corps ci-dessous
def allDeadBelow (n : Nat) : Bool :=
true
-- Doit donner true
#eval allDeadBelow 4
-- Exercice 2 : toutes les macro-cellules mortes de niveau <= n sont vides
Raw input{"cmd": "-- Exercice 2 : toutes les macro-cellules mortes de niveau <= n sont vides\n-- TODO etudiant : remplacer le corps ci-dessous\ndef allDeadBelow (n : Nat) : Bool :=\n true\n\n-- Doit donner true\n#eval allDeadBelow 4", "env": 12}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 3, "column": 18},
"endPos": {"line": 3, "column": 19},
"data":
"Variable name `n` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 5},
"data": "true"}],
"env": 13}
Attendu et anti-piège.allDeadBelow 4 doit renvoyer true. La récursion naturelle : cas de base n + 1 (au-delà du niveau 0, ou négatif selon votre convention), et pour n, isEmpty (emptyOfLevel n) && allDeadBelow (n - 1). Deux pièges : (1) renvoyer isEmpty (emptyOfLevel n)seul — vrai pour tout n, mais l’énoncé demande le test conjoint des niveaux \(0\) à \(n\) (la version à un seul niveau passerait le #eval sans répondre à la question — l’écart entre « le test passe » et « la fonction est correcte » est exactement ce que le lake formalise par ses théorèmes) ; (2) oublier que isEmpty est décidable sur la structure, pas un parcours de la grille : le coût est celui du niveau, pas de \(2^{2n}\) cellules.
Exercice 3 — Refaire chebDist à la main
Réimplémentez la distance de Chebyshev sans appeler chebDist : avec max, Int.natAbs et l’accessseur .1/.2 des paires. Votre version doit coïncider avec celle du lake sur les trois tests.
-- Exercice 3 : chebDist a la main (max, Int.natAbs, .1, .2)
-- TODO etudiant : remplacer le corps ci-dessous
def chebDistManu (p q : Int × Int) : Nat :=
0
-- Doivent donner les memes valeurs que chebDist
#eval chebDistManu (0, 0) (3, 4)
#eval chebDist (0, 0) (3, 4)
#eval chebDistManu (2, -1) (-5, 0)
#eval chebDist (2, -1) (-5, 0)
#eval chebDistManu (-7, -7) (0, 6)
#eval chebDist (-7, -7) (0, 6)
-- Exercice 3 : chebDist a la main (max, Int.natAbs, .1, .2)
Raw input{"cmd": "-- Exercice 3 : chebDist a la main (max, Int.natAbs, .1, .2)\n-- TODO etudiant : remplacer le corps ci-dessous\ndef chebDistManu (p q : Int \u00d7 Int) : Nat :=\n 0\n\n-- Doivent donner les memes valeurs que chebDist\n#eval chebDistManu (0, 0) (3, 4)\n#eval chebDist (0, 0) (3, 4)\n#eval chebDistManu (2, -1) (-5, 0)\n#eval chebDist (2, -1) (-5, 0)\n#eval chebDistManu (-7, -7) (0, 6)\n#eval chebDist (-7, -7) (0, 6)", "env": 13}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 3, "column": 18},
"endPos": {"line": 3, "column": 19},
"data":
"Variable name `p` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "warning",
"pos": {"line": 3, "column": 20},
"endPos": {"line": 3, "column": 21},
"data":
"Variable name `q` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 5},
"data": "4"},
{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 5},
"data": "7"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "13"}],
"env": 14}
Attendu et anti-piège. Les trois paires doivent coïncider : (0,0)/(3,4) → 4, (2,-1)/(-5,0) → 7, (-7,-7)/(0,6) → 13. La version attendue : max (Int.natAbs (q.1 - p.1)) (Int.natAbs (q.2 - p.2)). Le piège du signe : (q.1 - p.1) et non (p.1 - q.1) — en valeur absolue cela n’a pas d’importance (natAbs symétrise), et c’est justement un fait que chebDist_commprouve (section 2) : votre version « au main » hérite gratuitement de la commutativité vérifiée du lake. Si le troisième test échoue seul, vérifiez que vous comparez bien les écarts (\(13 = \max(7, 13)\)) et non les coordonnées absolues (\(\max(7, 6) = 7\)).
Conclusion
Sur le kernel Lean natif, ce compagnon a : (1) exécuté la machinerie de la preuve de correction Hashlife du lake conway_lean — cône de lumière, quadtree, murs, marge ; (2) vérifié les axiomes de chaque théorème clé — trois propres, hashlife_correct_margin encore sur sorryAx (dette tracée, epic #11703) ; (3) croisé la discipline du lake sur ses modules satellite — batterie adverse, borne de nouveauté, lemmes FRACTRAN. Le lake reste la source de vérité ; ce notebook en est le banc d’essai exécutable, cellule par cellule.