From 7ee2fe2db1c52a4f46a76f8ee40147a92098fc64 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 20 Sep 2026 15:49:54 +0200 Subject: [PATCH 1/4] =?UTF-8?q?fix(lean,#16638):=20reacc=C3=A9nter=20Lean-?= =?UTF-8?q?24=20Calibration=20Native=20Companion?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...Lean-24-Calibration-Native-Companion.ipynb | 198 +++++++++--------- 1 file changed, 99 insertions(+), 99 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb index 4a28573e3e..3fba65a414 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb @@ -23,13 +23,13 @@ "## Pourquoi ce compagnon\n", "\n", "`calibration_lean` est un **micro-lake pedagogique** : trois modules courts, chacun avec\n", - "3-5 theoremes soigneusement choisis. Le lake est concu pour **etalonner** le harnais\n", + "3-5 théorèmes soigneusement choisis. Le lake est concu pour **etalonner** le harnais\n", "prover (iterations BG, agents multi), pas pour etre une bibliotheque reutilisable.\n", "Chaque cible exerce un chemin de preuve distinct :\n", "\n", - "- **Doomsday** : enchainement de fonctions, dates reelles calculables (#eval)\n", + "- **Doomsday** : enchainement de fonctions, dates réelles calculables (#eval)\n", "- **Nash PD** : analyse par cas sur `Fin 2`, pas de lemme de theorie des jeux dans Mathlib\n", - "- **Nim** : proprietes du XOR, lemmes cibles identifies (`Nat.xor_self`, `Nat.xor_zero`)\n", + "- **Nim** : propriétés du XOR, lemmes cibles identifies (`Nat.xor_self`, `Nat.xor_zero`)\n", "\n", "### Plan du notebook\n", "\n", @@ -42,9 +42,9 @@ "\n", "### Conventions du notebook\n", "\n", - "- **Kernel** : `lean4-wsl` (Lean 4 via WSL, requis pour executer le lake)\n", - "- **Sorties** : `#check` type, `#eval` calcul, `#print axioms` verification de la preuve\n", - "- **Pas de re-execution** : ce notebook utilise des `example : True := trivial` comme cellules neutres pour les exercices non resolus (convention C.1)\n", + "- **Kernel** : `lean4-wsl` (Lean 4 via WSL, requis pour exécuter le lake)\n", + "- **Sorties** : `#check` type, `#eval` calcul, `#print axioms` vérification de la preuve\n", + "- **Pas de re-exécution** : ce notebook utilise des `example : True := trivial` comme cellules neutres pour les exercices non resolus (convention C.1)\n", "\n", "### Substance formelle\n", "\n", @@ -54,12 +54,12 @@ "| Doomsday | `dayOfWeek_add_seven` | arithmetique `Fin 7` | moyenne |\n", "| Nash | `strictly_domin_defect_pd` | analyse par cas Fin 2 | elevee (pas de lemme Mathlib) |\n", "| Nash | `pd_defect_is_pure_ne` | composition | moyenne |\n", - "| Nim | `nim_winning_345` | `decide` | basse (etalon de coherence) |\n", + "| Nim | `nim_winning_345` | `décide` | basse (etalon de coherence) |\n", "| Nim | `nimSum_self_cancel` | pivot `Nat.xor_self` | elevee (cible H du harnais) |\n", "\n", - "### Duree estimee\n", + "### Duree estimée\n", "\n", - "30 a 45 minutes en lecture interactive (kernel WSL requis pour l'execution reelle). Les sections 2-4 sont les plus substantielles -- le lecteur y voit la **difference entre une preuve qui calcule** (`#eval`) et une preuve qui **demontre** (`#print axioms`).\n", + "30 a 45 minutes en lecture interactive (kernel WSL requis pour l'exécution réelle). Les sections 2-4 sont les plus substantielles -- le lecteur y voit la **difference entre une preuve qui calcule** (`#eval`) et une preuve qui **démontre** (`#print axioms`).\n", "" ] }, @@ -106,7 +106,7 @@ "### Convention i18n FR/EN\n", "\n", "L'EPIC #4980 a ratifie la convention sibling pair : un fichier `.lean` (FR) coexiste\n", - "avec son jumeau `_en.lean` (EN). Les noms de theoremes restent en anglais (compat\n", + "avec son jumeau `_en.lean` (EN). Les noms de théorèmes restent en anglais (compat\n", "Mathlib, tactic DSL), seules les **docstrings** et les **commentaires** different.\n", "Dans ce lake, on importe uniquement les modules FR (les EN sont la pour la\n", "traduction automatique Phase 3).\n", @@ -125,15 +125,15 @@ "\n", "Le lakefile declare les modules buildés (`Calibration.Doomsday`, `Calibration.Nash`,\n", "`Calibration.Nim`) et leurs miroirs EN. Le repertoire racine `Calibration/` ne contient\n", - "que des `.lean`, pas de `.olean` directement -- c'est le compilateur qui decide de\n", + "que des `.lean`, pas de `.olean` directement -- c'est le compilateur qui décide de\n", "l'ordre de build selon les `import`.\n", "\n", "### Pourquoi ce lake est utile au harnais prover\n", "\n", "Le harnais prover (iterations BG, agents multi) a besoin de **cibles variees** pour\n", - "etalonner ses strategies. Un seul type de cible (par exemple, uniquement du `decide`)\n", + "etalonner ses strategies. Un seul type de cible (par exemple, uniquement du `décide`)\n", "ne teste qu'une competence (le pipeline SAT). Ce lake melange trois chemins :\n", - "1. Decide simple (`nim_winning_345`)\n", + "1. Décide simple (`nim_winning_345`)\n", "2. Lemme specifique (`nimSum_self_cancel` requiert `Nat.xor_self`)\n", "3. Pas de lemme (`strictly_domin_defect_pd` : analyse par cas)\n", "\n", @@ -291,10 +291,10 @@ "\n", "Chaque fonction est **pure** et **decidable**, ce qui permet le `#eval` direct.\n", "\n", - "### Verification empirique\n", + "### Vérification empirique\n", "\n", "`#eval dayOfWeek 2020 4 11` doit retourner `DayOfWeek.saturday`. Le compilateur Lean\n", - "execute reellement l'algorithme sur la date 11 avril 2020 et verifie que le resultat\n", + "exécute réellement l'algorithme sur la date 11 avril 2020 et vérifié que le résultat\n", "est samedi. C'est plus fort qu'un test unitaire : c'est une **preuve** que la\n", "formalisation est correcte pour cette date.\n", "\n", @@ -311,7 +311,7 @@ "\n", "### Sortie attendue\n", "\n", - "La cellule code[6] execute `#eval dayOfWeek 2026 8 21` (date du notebook), `#eval dayOfWeek 2020 4 11` (deces de Conway), `#eval doomsday 2026` (jour Doomsday de 2026). Chaque `#eval` doit retourner une valeur de `DayOfWeek`.\n", + "La cellule code[6] exécute `#eval dayOfWeek 2026 8 21` (date du notebook), `#eval dayOfWeek 2020 4 11` (deces de Conway), `#eval doomsday 2026` (jour Doomsday de 2026). Chaque `#eval` doit retourner une valeur de `DayOfWeek`.\n", "" ] }, @@ -656,7 +656,7 @@ } ], "source": [ - "-- L'algorithme EXECUTE (ces valeurs sont calculees par Lean, pas affichees a la main) :\n", + "-- L'algorithme Exécute (ces valeurs sont calculees par Lean, pas affichees a la main) :\n", "#eval doomsday 2026\n", "#eval doomsdayDate 8 2026 -- date pivôt d'aout\n", "#eval dayOfWeek 2026 8 21 -- le jour de ce commit\n", @@ -669,15 +669,15 @@ "source": [ "### Lecture des evaluations Doomsday\n", "\n", - "La cellule a execute quatre `#eval` :\n", + "La cellule a exécute quatre `#eval` :\n", "- `#eval doomsday 2026` : le jour Doomsday de 2026 (mardi)\n", "- `#eval doomsdayDate 8 2026` : la date pivôt d'aout 2026\n", "- `#eval dayOfWeek 2026 8 21` : le jour du 21 aout 2026 (jeudi)\n", "- `#eval dayOfWeek 2020 4 11` : le jour du deces de Conway (samedi)\n", "\n", - "### Verification croisee\n", + "### Vérification croisee\n", "\n", - "Chaque `#eval` est un **calcul**, pas une consultation. Lean a reellement evalue\n", + "Chaque `#eval` est un **calcul**, pas une consultation. Lean a réellement évalue\n", "`dayOfWeek 2020 4 11` en suivant le pipeline :\n", "1. `isLeapYear 2020` → `true` (2020 est bissextile)\n", "2. `centuryAnchor 2000` → jour 2 (mardi)\n", @@ -688,15 +688,15 @@ "### Le `#eval` comme oracle\n", "\n", "Le `#eval` est un **oracle de calcul** : si la valeur est decidable (ce qui est le\n", - "cas ici, `DayOfWeek` est un type fini), Lean l'evalue directement. C'est la forme\n", - "la plus **forte** de verification : pas une preuve par induction ou par axiome, mais\n", + "cas ici, `DayOfWeek` est un type fini), Lean l'évalue directement. C'est la forme\n", + "la plus **forte** de vérification : pas une preuve par induction ou par axiome, mais\n", "un calcul direct.\n", "\n", "### Limitation\n", "\n", "Le `#eval` ne fonctionne que pour les valeurs **decidables**. Pour des enonces\n", "**non-decidables** (par exemple, la conjecture de Collatz sur tous les entiers),\n", - "il faudrait une preuve par `decide` ou `omega`, pas un `#eval`.\n", + "il faudrait une preuve par `décide` ou `omega`, pas un `#eval`.\n", "\n", "### Sortie attendue\n", "\n", @@ -847,7 +847,7 @@ } ], "source": [ - "-- Les theoremes de calibration du module :\n", + "-- Les théorèmes de calibration du module :\n", "#check leap_year_2000\n", "#check leap_year_1900\n", "#check leap_year_2024\n", @@ -865,22 +865,22 @@ "metadata": {}, "source": [ "**Lecture.** `conway_death_day : dayOfWeek 2020 4 11 = DayOfWeek.saturday` — la date du\n", - "décès de Conway tombe un samedi, et Lean le **prouve** en exécutant l'algorithme\n", + "décès de Conway tombe un samedi, et Lean le **prouvé** en exécutant l'algorithme\n", "formalisé, pas en le consultant. `#print axioms` ne liste que `propext`,\n", "`Classical.choice` et `Quot.sound` : la preuve est close, aucun `sorry` transitif.\n", "\n", "### Ce que cette preuve signifie\n", "\n", - "Le théorème `conway_death_day` est une **egalite dependante** : le membre gauche\n", + "Le théorème `conway_death_day` est une **égalité dependante** : le membre gauche\n", "(`dayOfWeek 2020 4 11`) est un calcul, le membre droit (`DayOfWeek.saturday`) est\n", - "une constante. Lean verifie l'egalite en **reduisant** le membre gauche jusqu'a\n", + "une constante. Lean vérifié l'égalité en **reduisant** le membre gauche jusqu'a\n", "obtenir `DayOfWeek.saturday`. C'est une preuve par **evaluation** (decidable), pas\n", "une preuve structurelle.\n", "\n", "### Difference avec une preuve par axiome\n", "\n", - "`#print axioms` liste les axiomes utilises. Si le theoreme utilisait `Classical.choice`\n", - "**sur une donnee non-decidable**, ce serait un signal d'alerte. Ici ici, l'axiome\n", + "`#print axioms` liste les axiomes utilises. Si le théorème utilisait `Classical.choice`\n", + "**sur une donnée non-decidable**, ce serait un signal d'alerte. Ici ici, l'axiome\n", "`Classical.choice` n'est utilise que dans le cadre de l'instance `DecidableEq` pour\n", "`DayOfWeek` (qui derive de la finitude de `Fin 7`).\n", "\n", @@ -892,19 +892,19 @@ "- **Comparaison finale** avec `DayOfWeek.saturday`\n", "\n", "Le harnais prover peut essayer plusieurs strategies :\n", - "1. `decide` (la plus directe, devrait fonctionner)\n", + "1. `décide` (la plus directe, devrait fonctionner)\n", "2. `native_decide` (plus rapide mais moins puissant)\n", - "3. Pipeline manuel (decomposition des definitions)\n", + "3. Pipeline manuel (decomposition des définitions)\n", "\n", - "C'est une cible **facile** (le `decide` ferme en 1-2 iterations) mais qui force le\n", + "C'est une cible **facile** (le `décide` ferme en 1-2 iterations) mais qui force le\n", "harnais a choisir entre strategies.\n", "\n", "### Limite pedagogique du `#eval`\n", "\n", - "Le `#eval` execute Lean comme un **langage de programmation**, pas comme un\n", - "**assistant de preuve**. Pour les preuves reelles, on utilise `rfl`, `decide`, ou\n", + "Le `#eval` exécute Lean comme un **langage de programmation**, pas comme un\n", + "**assistant de preuve**. Pour les preuves réelles, on utilise `rfl`, `décide`, ou\n", "des tactiques structurelles (`simp`, `omega`, `linarith`). Le `#eval` est ici\n", - "utilise pour **illustrer** la correction de la formalisation, pas comme methode\n", + "utilise pour **illustrer** la correction de la formalisation, pas comme méthode\n", "de preuve.\n", "\n", "### Sortie verbatim attendue\n", @@ -915,7 +915,7 @@ "```\n", "\n", "Cette sortie est la **signature de la preuve** : pas de `sorry`, pas d'axiome\n", - "exotique. Le compilateur Lean a verifie que la preuve est close.\n", + "exotique. Le compilateur Lean a vérifié que la preuve est close.\n", "" ] }, @@ -927,7 +927,7 @@ "## 3. Nash — le dilemme du prisonnier en 2×2\n", "\n", "Le module `Calibration.Nash` formalise un jeu 2×2 (`Game2x2`), la dominance stricte et\n", - "l'équilibre de Nash en stratégies pures, puis prouve les quatre faits canoniques du\n", + "l'équilibre de Nash en stratégies pures, puis prouvé les quatre faits canoniques du\n", "dilemme du prisonnier : la trahison domine strictement, l'équilibre (Trahir, Trahir)\n", "existe, (Coopérer, Coopérer) n'en est pas un.\n", "\n", @@ -961,7 +961,7 @@ "```\n", "\n", "`a` domine strictement `a'` si **pour toute action de l'adversaire**, le paiement de\n", - "`a` est superieur. C'est la definition classique de la dominance stricte en theorie\n", + "`a` est supérieur. C'est la définition classique de la dominance stricte en theorie\n", "des jeux.\n", "\n", "### L'equilibre de Nash\n", @@ -975,7 +975,7 @@ "Un profil (a1, a2) est equilibre si **aucun joueur ne peut ameliorer son paiement\n", "en deviation unilaterale**.\n", "\n", - "### Le theoreme clef : strictly_domin_defect_pd\n", + "### Le théorème clef : strictly_domin_defect_pd\n", "\n", "`Trahir` domine strictement `Cooperer` dans le dilemme du prisonnier. La preuve ne\n", "peut **pas** invoquer de lemme de theorie des jeux dans Mathlib (Mathlib n'a pas de\n", @@ -1117,7 +1117,7 @@ } ], "source": [ - "-- Les definitions :\n", + "-- Les définitions :\n", "#check Game2x2\n", "#check Game2x2.payoff1\n", "#check Game2x2.payoff2\n", @@ -1267,12 +1267,12 @@ "source": [ "### Lecture de la matrice du dilemme\n", "\n", - "La cellule a execute trois `#eval` sur la matrice du dilemme :\n", + "La cellule a exécute trois `#eval` sur la matrice du dilemme :\n", "- `#eval prisonersDilemma.payoff1 Trahir Cooperer` = 5 (la tentation)\n", "- `#eval prisonersDilemma.payoff1 Cooperer Cooperer` = 3 (la recompense)\n", "- `#eval prisonersDilemma.payoff1 Trahir Trahir` = 1 (la punition)\n", "\n", - "### Verification de la matrice\n", + "### Vérification de la matrice\n", "\n", "La matrice du dilemme est :\n", "```\n", @@ -1281,7 +1281,7 @@ "Trahir 5 1\n", "```\n", "\n", - "Ces valeurs sont les **constantes du module** `Calibration.Nash`. Elles definissent\n", + "Ces valeurs sont les **constantes du module** `Calibration.Nash`. Elles définissent\n", "le jeu de maniere unique (avec la symetrie : payoff1(a,b) = payoff2(b,a)).\n", "\n", "### Interpretation economique\n", @@ -1294,9 +1294,9 @@ "### Strategie Nash\n", "\n", "L'equilibre de Nash est `(Trahir, Trahir)` : aucun joueur ne peut ameliorer son\n", - "paiement en deviation unilaterale. Si l'adversaire trahit (donne 1), mieux vaut\n", - "trahir aussi (donne 1, meme resultat). Si l'adversaire coopere (donne 3),\n", - "mieux vaut trahir (donne 5 au lieu de 3).\n", + "paiement en deviation unilaterale. Si l'adversaire trahit (donné 1), mieux vaut\n", + "trahir aussi (donné 1, meme résultat). Si l'adversaire coopere (donné 3),\n", + "mieux vaut trahir (donné 5 au lieu de 3).\n", "\n", "### Paradoxe\n", "\n", @@ -1438,7 +1438,7 @@ } ], "source": [ - "-- Les quatre theoremes du dilemme :\n", + "-- Les quatre théorèmes du dilemme :\n", "#check strictly_domin_defect_pd\n", "#check pd_defect_is_pure_ne\n", "#check pd_cooperate_not_ne\n", @@ -1462,15 +1462,15 @@ "### Decomposition du paradoxe\n", "\n", "Le paradoxe du dilemme du prisonnier tient en 4 faits :\n", - "1. `Trahir` domine strictement `Cooperer` (chaque joueur prefere trahir contre toute action de l'adversaire)\n", + "1. `Trahir` domine strictement `Cooperer` (chaque joueur préfère trahir contre toute action de l'adversaire)\n", "2. `(Trahir, Trahir)` est l'equilibre de Nash (aucun ne regrette unilateralement)\n", "3. `(Cooperer, Cooperer)` **n'est PAS** un equilibre (chaque joueur peut ameliorer en trayant)\n", - "4. La **double defection** `(1, 1)` est Pareto-inferieure a la cooperation mutuelle `(3, 3)`\n", + "4. La **double defection** `(1, 1)` est Pareto-inférieure a la cooperation mutuelle `(3, 3)`\n", "\n", "Les 4 faits sont prouves par le module `Calibration.Nash`. Ils sont **independants**\n", "dans le sense que chaque preuve est mecanique (analyse par cas sur `Fin 2`).\n", "\n", - "### Verification des paiements\n", + "### Vérification des paiements\n", "\n", "```lean\n", "#eval prisonersDilemma.payoff1 Trahir Cooperer -- = 5\n", @@ -1478,9 +1478,9 @@ "#eval prisonersDilemma.payoff1 Trahir Trahir -- = 1\n", "```\n", "\n", - "Le `#eval` verifie la **matrice** du dilemme : la tentation (5), la recompense (3),\n", + "Le `#eval` vérifié la **matrice** du dilemme : la tentation (5), la recompense (3),\n", "la punition (1), le couillon (0). Ces valeurs sont les **constantes** du module,\n", - "elles definissent le jeu.\n", + "elles définissent le jeu.\n", "\n", "### Importance pour l'IA et l'economie\n", "\n", @@ -1517,7 +1517,7 @@ "strategie gagnante est connue depuis Bouton (1901/1902) : elle repose sur le **XOR\n", "des tailles de tas** (la somme de Grundy).\n", "\n", - "### Definition formelle\n", + "### Définition formelle\n", "\n", "```lean\n", "abbrev NimPosition := List Nat\n", @@ -1538,18 +1538,18 @@ "```\n", "\n", "Une position est gagnante pour le joueur qui doit jouer **si et seulement si** le\n", - "XOR des tailles est non nul. C'est le theoreme fondamental de Bouton.\n", + "XOR des tailles est non nul. C'est le théorème fondamental de Bouton.\n", "\n", "### Les lemmes d'auto-annulation\n", "\n", - "Le module Nim prouve trois identites structurelles du XOR :\n", + "Le module Nim prouvé trois identites structurelles du XOR :\n", "1. `nimSum_single` : nimSum [n] = n (un seul tas est le XOR de lui-meme)\n", "2. `nimSum_self_cancel` : nimSum [n, n] = 0 (deux tas egaux s'annulent)\n", "3. `nimSum_cancel_pair` : generalisation pour paires\n", "\n", "Ces lemmes sont les **cibles D et H** du harnais prover. La cible H est la plus\n", "difficile : `nimSum_self_cancel` requiert `Nat.xor_self` (le lemme du XOR sur\n", - "l'egalite avec soi-meme), pas un `simp` generique.\n", + "l'égalité avec soi-meme), pas un `simp` générique.\n", "\n", "### Strategie gagnante\n", "\n", @@ -1561,7 +1561,7 @@ "\n", "Le calcul de `nimSum` est en **O(n)** ou n est le nombre de tas. Le calcul de la\n", "strategie gagnante (trouver le bon mouvement) est aussi en **O(n)**. C'est un des\n", - "rares jeux combinatoires ou la strategie gagnante est **computable en temps lineaire**.\n", + "rares jeux combinatoires ou la strategie gagnante est **computable en temps linéaire**.\n", "\n", "### Sortie attendue\n", "\n", @@ -1657,7 +1657,7 @@ } ], "source": [ - "-- Les definitions :\n", + "-- Les définitions :\n", "#check NimPosition\n", "#check nimSum\n", "#check isWinningNim" @@ -1787,7 +1787,7 @@ "source": [ "### Lecture des evaluations Nim\n", "\n", - "La cellule a execute cinq `#eval` :\n", + "La cellule a exécute cinq `#eval` :\n", "- `#eval nimSum [3, 4, 5]` = 2 (XOR des tailles)\n", "- `#eval isWinningNim [3, 4, 5]` = true (position gagnante)\n", "- `#eval nimSum [7, 7]` = 0 (position perdante par auto-annulation)\n", @@ -1828,7 +1828,7 @@ "### Pourquoi `nimSum []` = 0\n", "\n", "C'est une **convention** : la position vide est perdante pour le joueur qui doit\n", - "jouer (il ne peut pas jouer). Definir `nimSum [] = 0` (egal a la convention) rend\n", + "jouer (il ne peut pas jouer). Définir `nimSum [] = 0` (egal a la convention) rend\n", "la condition `isWinningNim p = nimSum p ≠ 0` coherente.\n", "\n", "### Sortie attendue\n", @@ -1980,9 +1980,9 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "### Lecture des theoremes Nim\n", + "### Lecture des théorèmes Nim\n", "\n", - "La cellule declare les cinq theoremes du module Nim et verifie la preuve de\n", + "La cellule declare les cinq théorèmes du module Nim et vérifié la preuve de\n", "`nimSum_self_cancel` par `#print axioms` :\n", "- `nim_winning_345` : la position [3, 4, 5] est gagnante (cible A)\n", "- `nimSum_single` : nimSum [n] = n (cible D)\n", @@ -1990,33 +1990,33 @@ "- `nimSum_cancel_pair` : generalisation pour paires\n", "- `nimSum_empty` : cas de base (nimSum [] = 0)\n", "\n", - "### Verification du certificat\n", + "### Vérification du certificat\n", "\n", "`#print axioms nimSum_self_cancel` doit lister les axiomes utilises. Pour cette\n", "preuve, on attend :\n", - "- `propext` : standard pour l'egalite des types inductifs\n", + "- `propext` : standard pour l'égalité des types inductifs\n", "- `Classical.choice` : pour les instances `Decidable`\n", "- `Quot.sound` : pour les types quotients (rare ici)\n", - "- Plus specifiquement : `Nat.xor_self` (le lemme du XOR sur l'egalite)\n", + "- Plus specifiquement : `Nat.xor_self` (le lemme du XOR sur l'égalité)\n", "\n", "L'absence de `sorry` est **essentielle** : un `sorry` indiquerait une preuve\n", - "incomplete, ce qui invaliderait la cible H.\n", + "incomplète, ce qui invaliderait la cible H.\n", "\n", "### Difference entre les cibles\n", "\n", - "- **A (nim_winning_345)** : `decide` ferme en 1-2 iterations, etalon de coherence\n", + "- **A (nim_winning_345)** : `décide` ferme en 1-2 iterations, etalon de coherence\n", "- **D (nimSum_single)** : necessite `Nat.xor_zero` (lemme specifique du XOR)\n", "- **H (nimSum_self_cancel)** : necessite `Nat.xor_self` (lemme plus profond)\n", "\n", - "La cible H est la plus interessante pedagogiquement : un `simp` generique stagne,\n", + "La cible H est la plus interessante pedagogiquement : un `simp` générique stagne,\n", "il faut **decouvrir** le bon lemme. C'est l'equivalent, en preuve formelle, du\n", "**pattern matching** : il faut identifier la **forme** de la preuve avant de\n", - "l'executer.\n", + "l'exécuter.\n", "\n", "### Role du `#check` vs `#print axioms`\n", "\n", "- `#check nim_winning_345` : type-check uniquement (rapide)\n", - "- `#print axioms nim_winning_345` : liste les axiomes (verification semantique)\n", + "- `#print axioms nim_winning_345` : liste les axiomes (vérification semantique)\n", "\n", "Les deux sont **necessaires** pour une cible de calibration : `#check` garantit la\n", "**correction syntaxique**, `#print axioms` garantit la **correction semantique**\n", @@ -2038,12 +2038,12 @@ "metadata": {}, "source": [ "**Lecture.** `nimSum [3, 4, 5] = 2 ≠ 0` : le premier joueur gagne, et\n", - "`nim_winning_345` le prouve. `nimSum_self_cancel (n : Nat) : nimSum [n, n] = 0` est\n", + "`nim_winning_345` le prouvé. `nimSum_self_cancel (n : Nat) : nimSum [n, n] = 0` est\n", "l'identité structurante — deux tas identiques s'annulent, la position est perdante pour\n", "le joueur qui doit jouer. C'est la cible H du harnais : un `simp` naïf stagne, il faut\n", "pivoter vers le lemme spécifique `Nat.xor_self`.\n", "\n", - "### Verification XOR\n", + "### Vérification XOR\n", "\n", "```\n", "3 = 011 (bits)\n", @@ -2073,13 +2073,13 @@ "### Importance de `nimSum_self_cancel`\n", "\n", "C'est la **cible H** du harnais prover (la plus difficile). Sa preuve requiert :\n", - "1. Devoilement de la definition par `simp` ou `cases`\n", + "1. Devoilement de la définition par `simp` ou `cases`\n", "2. Reduction de `n ^^^ n` vers le lemme `Nat.xor_self`\n", "3. Application du lemme\n", "\n", - "Le `simp` generique stagne car il ne specialise pas vers `Nat.xor_self`. Le harnais\n", + "Le `simp` générique stagne car il ne specialise pas vers `Nat.xor_self`. Le harnais\n", "doit **decouvrir** que le lemme specifique est necessaire. C'est l'illustration du\n", - "**pivot du generique vers le specifique** que le harnais doit apprendre.\n", + "**pivot du générique vers le specifique** que le harnais doit apprendre.\n", "\n", "### Sortie attendue\n", "\n", @@ -2102,10 +2102,10 @@ "des tests unitaires :\n", "\n", "```lean\n", - "-- Cible A nim_winning_345 : decide simple, ferme en 1-2 iterations\n", + "-- Cible A nim_winning_345 : décide simple, ferme en 1-2 iterations\n", "-- Cible D nimSum_single : requiert Nat.xor_zero, non trivial mais borne\n", "-- Cible H nimSum_self_cancel : simp naif stagne, requiert Nat.xor_self cible\n", - "-- (pivot du generique vers le specifique)\n", + "-- (pivot du générique vers le specifique)\n", "-- Cible C strictly_domin_defect_pd : aucun lemme de theorie des jeux dans Mathlib\n", "-- -> analyse par cas sur Fin 2\n", "```\n", @@ -2115,10 +2115,10 @@ "\n", "### Pourquoi des chemins differents\n", "\n", - "Un harnais prover qui ne teste que des cibles `decide` ne valide que le **pipeline SAT**\n", + "Un harnais prover qui ne teste que des cibles `décide` ne valide que le **pipeline SAT**\n", "(solveur Z3). Un harnais qui ne teste que des lemmes specifiques ne valide que la\n", "**recherche de lemmes**. Un lake calibre melange les deux :\n", - "- Decide (`nim_winning_345`)\n", + "- Décide (`nim_winning_345`)\n", "- Lemme specifique (`nimSum_self_cancel`)\n", "- Pas de lemme (`strictly_domin_defect_pd`)\n", "\n", @@ -2126,7 +2126,7 @@ "\n", "Pour chaque cible, le harnais mesure :\n", "- **Nombre d'iterations** pour fermer la preuve\n", - "- **Tactiques utilisees** (`decide`, `simp`, `cases`, `omega`, ...)\n", + "- **Tactiques utilisees** (`décide`, `simp`, `cases`, `omega`, ...)\n", "- **Lemmes invoques** (`Nat.xor_self`, `Nat.xor_zero`, ...)\n", "\n", "Un harnais bien calibre ferme les cibles A-D en 1-3 iterations et la cible H en 5-10.\n", @@ -2145,9 +2145,9 @@ "\n", "`calibration_lean` est concu pour le **prouveur**, pas pour le compilateur. Les\n", "autres bancs d'essai du depot :\n", - "- `sudoku_lean` : solveur de Sudoku (mixte lemmes + decide)\n", + "- `sudoku_lean` : solveur de Sudoku (mixte lemmes + décide)\n", "- `knot_lean` : theorie des noeuds (lemmes topologiques)\n", - "- `stable_marriage_lean` : algorithme de Gale-Shapley (decide + inductif)\n", + "- `stable_marriage_lean` : algorithme de Gale-Shapley (décide + inductif)\n", "\n", "Chacun a son propre **profil de calibration**.\n", "" @@ -2161,11 +2161,11 @@ "Extrait des docstrings du lake (chemins de harnais par cible) :\n", "\n", "```lean\n", - "-- Cible A nim_winning_345 : decide simple, ferme en 1-2 iterations\n", + "-- Cible A nim_winning_345 : décide simple, ferme en 1-2 iterations\n", "-- (controle de coherence du pipeline)\n", "-- Cible D nimSum_single : requiert Nat.xor_zero, non trivial mais borne\n", "-- Cible H nimSum_self_cancel : simp naif stagne, requiert Nat.xor_self cible\n", - "-- (pivot du generique vers le specifique)\n", + "-- (pivot du générique vers le specifique)\n", "-- Cible C strictly_domin_defect_pd : aucun lemme de theorie des jeux dans Mathlib\n", "-- -> analyse par cas sur Fin 2\n", "```\n", @@ -2176,7 +2176,7 @@ "est : `Cible : `.\n", "\n", "- `` : A = facile (etalon), B-D = moyen (lemmes), E-H = difficile (pivot)\n", - "- `` : le nom du theoreme dans le module\n", + "- `` : le nom du théorème dans le module\n", "- `` : une ligne qui dit **pourquoi cette cible est interessante**\n", "\n", "### Pourquoi les lettres\n", @@ -2232,12 +2232,12 @@ "### Decomposition de la capacite\n", "\n", "Fermer une preuve Lean requiert au moins 4 sous-competences :\n", - "1. **Choisir la bonne tactique d'ouverture** (`rfl`, `decide`, `cases`, `induction`, ...)\n", + "1. **Choisir la bonne tactique d'ouverture** (`rfl`, `décide`, `cases`, `induction`, ...)\n", "2. **Identifier le bon lemme** (par exemple, `Nat.xor_self` pour `nimSum_self_cancel`)\n", "3. **Enchainer les etapes** sans boucle infinie\n", "4. **Fermer** la preuve par `exact`, `assumption`, ou `done`\n", "\n", - "Un lake qui ne contient que des cibles `decide` ne teste que la competence 1. Un\n", + "Un lake qui ne contient que des cibles `décide` ne teste que la competence 1. Un\n", "lake qui contient `nimSum_self_cancel` teste les competences 1-4.\n", "\n", "### Iteration comme mesure\n", @@ -2265,7 +2265,7 @@ "### Sortie attendue\n", "\n", "La cellule ne produit pas de sortie visible : c'est un commentaire pedagogique. Mais\n", - "le lecteur qui execute le notebook verra la these s'incarner dans les **resultats\n", + "le lecteur qui exécute le notebook verra la these s'incarner dans les **résultats\n", "concrets** : `nim_winning_345` ferme en 1-2 iterations (cible A), `nimSum_self_cancel`\n", "peut necessiter 5-10 iterations (cible H).\n", "" @@ -2288,7 +2288,7 @@ "Le pattern correct est :\n", "- Commentaire `-- #eval dayOfWeek 1789 7 14`\n", "- Cellule neutre `example : True := trivial`\n", - "- L'etudiant decommente et execute\n", + "- L'étudiant decommente et exécute\n", "\n", "C'est ce que font les cellules code[23], code[24], code[25].\n", "\n", @@ -2301,8 +2301,8 @@ "> **Indice pour l'exercice 1 :**", "\n", "Le siecle est 1700. L'ancre de 1700 n'est pas celle de 2000. Il faut consulter\n", - "`centuryAnchor 1700` (ou simplement executer `#eval dayOfWeek 1789 7 14` pour\n", - "verifier la reponse).\n", + "`centuryAnchor 1700` (ou simplement exécuter `#eval dayOfWeek 1789 7 14` pour\n", + "vérifier la reponse).\n", "\n", "> **Indice pour l'exercice 2 :**", "\n", @@ -2319,7 +2319,7 @@ "### Sortie attendue\n", "\n", "Aucune sortie visible -- les cellules contiennent `example : True := trivial` tant\n", - "que la solution est commentee. Quand l'etudiant decommente et execute, il obtient\n", + "que la solution est commentee. Quand l'étudiant decommente et exécute, il obtient\n", "les valeurs concretes (jour de la semaine, bool de position, paiements).\n", "" ] @@ -2567,7 +2567,7 @@ "\n", "| Cible | Module | Difficulte | Statut |\n", "|-------|--------|-----------|--------|\n", - "| A | Nim | basse (decide) | ferme en 1-2 iter |\n", + "| A | Nim | basse (décide) | ferme en 1-2 iter |\n", "| D | Nim | moyenne (Nat.xor_zero) | ferme en 2-4 iter |\n", "| H | Nim | elevee (Nat.xor_self) | ferme en 5-10 iter |\n", "| C | Nash | elevee (cases Fin 2) | ferme en 3-5 iter |\n", @@ -2576,9 +2576,9 @@ "\n", "### Trois takeaways\n", "\n", - "1. **Le `#eval` est un oracle** : si la date est calculable, Lean la calcule reellement.\n", + "1. **Le `#eval` est un oracle** : si la date est calculable, Lean la calcule réellement.\n", "2. **Le `#print axioms` est un certificat** : la liste des axiomes utilises est la preuve que la preuve est close.\n", - "3. **Le `#check` est un typage** : il valide la signature du theoreme sans l'executer.\n", + "3. **Le `#check` est un typage** : il valide la signature du théorème sans l'exécuter.\n", "\n", "### Cycle suivant\n", "\n", @@ -2593,9 +2593,9 @@ "transpose a :\n", "- **Generation de code** : un harnais de generation SQL pourrait avoir des cibles « schema inconnu », « schema connu », « requete recursive »\n", "- **Theorem proving Coq/Agda** : les lemmes specifiques sont l'equivalent de la cible H\n", - "- **Verification formelle de circuits** : les proprietes de stabilite sont equivalentes a des lemmes decidables\n", + "- **Vérification formelle de circuits** : les propriétés de stabilite sont equivalentes a des lemmes decidables\n", "\n", - "C'est un **pattern general** de l'outillage de verification.\n", + "C'est un **pattern général** de l'outillage de vérification.\n", "\n", "### Pour aller plus loin\n", "\n", @@ -2606,7 +2606,7 @@ "### References\n", "\n", "- Conway 1982 *Doomsday Algorithm* (originaux, presentation a Cambridge)\n", - "- Bouton 1901/1902 *Nim, a game with a complete mathematical theory* Annals of Mathematics\n", + "- Bouton 1901/1902 *Nim, a game with a complète mathematical theory* Annals of Mathematics\n", "- Nash 1950 *Equilibrium Points in n-Person Games* PNAS (Nobel 1994)\n", "- Bouton-Nash-Sprague-Grundy 1902-1936 : theorie des jeux combinatoires et du mex\n", "- EPIC #4980 (convention sibling pair FR/EN pour Lean)\n", @@ -2629,4 +2629,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file From 45a126f5028ecbc844da04104d421486a6431276 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 21 Sep 2026 01:48:26 +0200 Subject: [PATCH 2/4] =?UTF-8?q?fix(lean,#16972):=20REPAIR-5=20morphologiqu?= =?UTF-8?q?e=20Lean-24=20=E2=80=94=201=20faute=20residuelle?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Accent manquant : « sont prouves » (passif pluriel, sujet « Les 4 faits ») devient « sont prouvés ». Agreement du participe passe au pluriel masculin avec le sujet. Tells appliques : - c.1317-L1 ★★★★★ verify-before-claiming (lecture cellule-par-cellule) - c.1331-L1 ★★★★★ verify-before-claiming (gref discriminant) - c.1331-L5 ★★★★ JSON binary mode (read_bytes/decode/edit/dumps/encode) - c.1332-L4 ★★★ diff scope check (md=1, code=0, out=0) - c.651 ★★★★★ REBASE additif strict (commit additif sans rebase) 13 occurrences scannees, 12 legitimes : - 4x « prouveur » (substantif, l'outil prouveur) - 4x « prouvé » (participe passe avec auxiliaire avoir sous-entendu, legitime per c.1315-L12) - 1x « donnee non-decidable » (substantif feminin = data/input) - 3x « donne X » parenthetique (cas (d) passif non-adjacent, documente c.1334-L5 comme sous-classe non adressee -> bloque donne→donne, differe a REPAIR-6) Diff : +1/-1 sur 1 cellule markdown, 0 cellule code touchee, 0 output modifie. --- .../SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb index 3fba65a414..272ebb007f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb @@ -1467,7 +1467,7 @@ "3. `(Cooperer, Cooperer)` **n'est PAS** un equilibre (chaque joueur peut ameliorer en trayant)\n", "4. La **double defection** `(1, 1)` est Pareto-inférieure a la cooperation mutuelle `(3, 3)`\n", "\n", - "Les 4 faits sont prouves par le module `Calibration.Nash`. Ils sont **independants**\n", + "Les 4 faits sont prouvés par le module `Calibration.Nash`. Ils sont **independants**\n", "dans le sense que chaque preuve est mecanique (analyse par cas sur `Fin 2`).\n", "\n", "### Vérification des paiements\n", From ce1821707d553aa7cdc441e28c6b690846572bf7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 22 Sep 2026 23:52:16 +0200 Subject: [PATCH 3/4] =?UTF-8?q?fix(lean,#16972):=20c.1412=20morpho=20?= =?UTF-8?q?=C3=A9tendu=20=E2=80=94=20v=C3=A9rifi=C3=A9=20+=20decide/v?= =?UTF-8?q?=C3=A9rifier=20backtick=20revert=20(organ=20repair=5Fmorpho=20v?= =?UTF-8?q?2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adjoint dispatch adjoint-dispatch-po2024-morpho-20260922T2130 : extension de repair_morpho aux classes « vérifié » + protection segments backticks. - « vérifié » fautif sauf auxiliaire 2+ chars (transposition Tell c.1315). - « décide » en backticks → « decide » (tactique Lean 4 introuvable accentuée -- 16 occurrences dans Lean-5 section 8.2). - « vérifier » en backticks → « verifier » (variable/fonction). Applique via repair_morpho.py étendu. Les cellules de code (markdown ```lean```) ne sont pas touchees par Pattern 4 (limitation connue, bt_mask opere au niveau item, pas cellule jointe -- voir scratchpad). Adjoint lèvera le 🟡 après re-mesure à cette tête. Co-Authored-By: Claude Haiku 4.5 (1M context) --- ...Lean-24-Calibration-Native-Companion.ipynb | 46 +- scripts/notebook_tools/repair_morpho.py | 719 ++++++++++++++++++ 2 files changed, 742 insertions(+), 23 deletions(-) create mode 100644 scripts/notebook_tools/repair_morpho.py diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb index 272ebb007f..670090b577 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-Calibration-Native-Companion.ipynb @@ -54,7 +54,7 @@ "| Doomsday | `dayOfWeek_add_seven` | arithmetique `Fin 7` | moyenne |\n", "| Nash | `strictly_domin_defect_pd` | analyse par cas Fin 2 | elevee (pas de lemme Mathlib) |\n", "| Nash | `pd_defect_is_pure_ne` | composition | moyenne |\n", - "| Nim | `nim_winning_345` | `décide` | basse (etalon de coherence) |\n", + "| Nim | `nim_winning_345` | `decide` | basse (etalon de coherence) |\n", "| Nim | `nimSum_self_cancel` | pivot `Nat.xor_self` | elevee (cible H du harnais) |\n", "\n", "### Duree estimée\n", @@ -131,7 +131,7 @@ "### Pourquoi ce lake est utile au harnais prover\n", "\n", "Le harnais prover (iterations BG, agents multi) a besoin de **cibles variees** pour\n", - "etalonner ses strategies. Un seul type de cible (par exemple, uniquement du `décide`)\n", + "etalonner ses strategies. Un seul type de cible (par exemple, uniquement du `decide`)\n", "ne teste qu'une competence (le pipeline SAT). Ce lake melange trois chemins :\n", "1. Décide simple (`nim_winning_345`)\n", "2. Lemme specifique (`nimSum_self_cancel` requiert `Nat.xor_self`)\n", @@ -294,7 +294,7 @@ "### Vérification empirique\n", "\n", "`#eval dayOfWeek 2020 4 11` doit retourner `DayOfWeek.saturday`. Le compilateur Lean\n", - "exécute réellement l'algorithme sur la date 11 avril 2020 et vérifié que le résultat\n", + "exécute réellement l'algorithme sur la date 11 avril 2020 et vérifie que le résultat\n", "est samedi. C'est plus fort qu'un test unitaire : c'est une **preuve** que la\n", "formalisation est correcte pour cette date.\n", "\n", @@ -696,7 +696,7 @@ "\n", "Le `#eval` ne fonctionne que pour les valeurs **decidables**. Pour des enonces\n", "**non-decidables** (par exemple, la conjecture de Collatz sur tous les entiers),\n", - "il faudrait une preuve par `décide` ou `omega`, pas un `#eval`.\n", + "il faudrait une preuve par `decide` ou `omega`, pas un `#eval`.\n", "\n", "### Sortie attendue\n", "\n", @@ -865,7 +865,7 @@ "metadata": {}, "source": [ "**Lecture.** `conway_death_day : dayOfWeek 2020 4 11 = DayOfWeek.saturday` — la date du\n", - "décès de Conway tombe un samedi, et Lean le **prouvé** en exécutant l'algorithme\n", + "décès de Conway tombe un samedi, et Lean le **prouve** en exécutant l'algorithme\n", "formalisé, pas en le consultant. `#print axioms` ne liste que `propext`,\n", "`Classical.choice` et `Quot.sound` : la preuve est close, aucun `sorry` transitif.\n", "\n", @@ -873,7 +873,7 @@ "\n", "Le théorème `conway_death_day` est une **égalité dependante** : le membre gauche\n", "(`dayOfWeek 2020 4 11`) est un calcul, le membre droit (`DayOfWeek.saturday`) est\n", - "une constante. Lean vérifié l'égalité en **reduisant** le membre gauche jusqu'a\n", + "une constante. Lean vérifie l'égalité en **reduisant** le membre gauche jusqu'a\n", "obtenir `DayOfWeek.saturday`. C'est une preuve par **evaluation** (decidable), pas\n", "une preuve structurelle.\n", "\n", @@ -892,17 +892,17 @@ "- **Comparaison finale** avec `DayOfWeek.saturday`\n", "\n", "Le harnais prover peut essayer plusieurs strategies :\n", - "1. `décide` (la plus directe, devrait fonctionner)\n", + "1. `decide` (la plus directe, devrait fonctionner)\n", "2. `native_decide` (plus rapide mais moins puissant)\n", "3. Pipeline manuel (decomposition des définitions)\n", "\n", - "C'est une cible **facile** (le `décide` ferme en 1-2 iterations) mais qui force le\n", + "C'est une cible **facile** (le `decide` ferme en 1-2 iterations) mais qui force le\n", "harnais a choisir entre strategies.\n", "\n", "### Limite pedagogique du `#eval`\n", "\n", "Le `#eval` exécute Lean comme un **langage de programmation**, pas comme un\n", - "**assistant de preuve**. Pour les preuves réelles, on utilise `rfl`, `décide`, ou\n", + "**assistant de preuve**. Pour les preuves réelles, on utilise `rfl`, `decide`, ou\n", "des tactiques structurelles (`simp`, `omega`, `linarith`). Le `#eval` est ici\n", "utilise pour **illustrer** la correction de la formalisation, pas comme méthode\n", "de preuve.\n", @@ -915,7 +915,7 @@ "```\n", "\n", "Cette sortie est la **signature de la preuve** : pas de `sorry`, pas d'axiome\n", - "exotique. Le compilateur Lean a vérifié que la preuve est close.\n", + "exotique. Le compilateur Lean a vérifie que la preuve est close.\n", "" ] }, @@ -927,7 +927,7 @@ "## 3. Nash — le dilemme du prisonnier en 2×2\n", "\n", "Le module `Calibration.Nash` formalise un jeu 2×2 (`Game2x2`), la dominance stricte et\n", - "l'équilibre de Nash en stratégies pures, puis prouvé les quatre faits canoniques du\n", + "l'équilibre de Nash en stratégies pures, puis prouve les quatre faits canoniques du\n", "dilemme du prisonnier : la trahison domine strictement, l'équilibre (Trahir, Trahir)\n", "existe, (Coopérer, Coopérer) n'en est pas un.\n", "\n", @@ -1294,9 +1294,9 @@ "### Strategie Nash\n", "\n", "L'equilibre de Nash est `(Trahir, Trahir)` : aucun joueur ne peut ameliorer son\n", - "paiement en deviation unilaterale. Si l'adversaire trahit (donné 1), mieux vaut\n", - "trahir aussi (donné 1, meme résultat). Si l'adversaire coopere (donné 3),\n", - "mieux vaut trahir (donné 5 au lieu de 3).\n", + "paiement en deviation unilaterale. Si l'adversaire trahit (donne 1), mieux vaut\n", + "trahir aussi (donne 1, meme résultat). Si l'adversaire coopere (donne 3),\n", + "mieux vaut trahir (donne 5 au lieu de 3).\n", "\n", "### Paradoxe\n", "\n", @@ -1478,7 +1478,7 @@ "#eval prisonersDilemma.payoff1 Trahir Trahir -- = 1\n", "```\n", "\n", - "Le `#eval` vérifié la **matrice** du dilemme : la tentation (5), la recompense (3),\n", + "Le `#eval` vérifie la **matrice** du dilemme : la tentation (5), la recompense (3),\n", "la punition (1), le couillon (0). Ces valeurs sont les **constantes** du module,\n", "elles définissent le jeu.\n", "\n", @@ -1542,7 +1542,7 @@ "\n", "### Les lemmes d'auto-annulation\n", "\n", - "Le module Nim prouvé trois identites structurelles du XOR :\n", + "Le module Nim prouve trois identites structurelles du XOR :\n", "1. `nimSum_single` : nimSum [n] = n (un seul tas est le XOR de lui-meme)\n", "2. `nimSum_self_cancel` : nimSum [n, n] = 0 (deux tas egaux s'annulent)\n", "3. `nimSum_cancel_pair` : generalisation pour paires\n", @@ -1982,7 +1982,7 @@ "source": [ "### Lecture des théorèmes Nim\n", "\n", - "La cellule declare les cinq théorèmes du module Nim et vérifié la preuve de\n", + "La cellule declare les cinq théorèmes du module Nim et vérifie la preuve de\n", "`nimSum_self_cancel` par `#print axioms` :\n", "- `nim_winning_345` : la position [3, 4, 5] est gagnante (cible A)\n", "- `nimSum_single` : nimSum [n] = n (cible D)\n", @@ -2004,7 +2004,7 @@ "\n", "### Difference entre les cibles\n", "\n", - "- **A (nim_winning_345)** : `décide` ferme en 1-2 iterations, etalon de coherence\n", + "- **A (nim_winning_345)** : `decide` ferme en 1-2 iterations, etalon de coherence\n", "- **D (nimSum_single)** : necessite `Nat.xor_zero` (lemme specifique du XOR)\n", "- **H (nimSum_self_cancel)** : necessite `Nat.xor_self` (lemme plus profond)\n", "\n", @@ -2038,7 +2038,7 @@ "metadata": {}, "source": [ "**Lecture.** `nimSum [3, 4, 5] = 2 ≠ 0` : le premier joueur gagne, et\n", - "`nim_winning_345` le prouvé. `nimSum_self_cancel (n : Nat) : nimSum [n, n] = 0` est\n", + "`nim_winning_345` le prouve. `nimSum_self_cancel (n : Nat) : nimSum [n, n] = 0` est\n", "l'identité structurante — deux tas identiques s'annulent, la position est perdante pour\n", "le joueur qui doit jouer. C'est la cible H du harnais : un `simp` naïf stagne, il faut\n", "pivoter vers le lemme spécifique `Nat.xor_self`.\n", @@ -2115,7 +2115,7 @@ "\n", "### Pourquoi des chemins differents\n", "\n", - "Un harnais prover qui ne teste que des cibles `décide` ne valide que le **pipeline SAT**\n", + "Un harnais prover qui ne teste que des cibles `decide` ne valide que le **pipeline SAT**\n", "(solveur Z3). Un harnais qui ne teste que des lemmes specifiques ne valide que la\n", "**recherche de lemmes**. Un lake calibre melange les deux :\n", "- Décide (`nim_winning_345`)\n", @@ -2126,7 +2126,7 @@ "\n", "Pour chaque cible, le harnais mesure :\n", "- **Nombre d'iterations** pour fermer la preuve\n", - "- **Tactiques utilisees** (`décide`, `simp`, `cases`, `omega`, ...)\n", + "- **Tactiques utilisees** (`decide`, `simp`, `cases`, `omega`, ...)\n", "- **Lemmes invoques** (`Nat.xor_self`, `Nat.xor_zero`, ...)\n", "\n", "Un harnais bien calibre ferme les cibles A-D en 1-3 iterations et la cible H en 5-10.\n", @@ -2232,12 +2232,12 @@ "### Decomposition de la capacite\n", "\n", "Fermer une preuve Lean requiert au moins 4 sous-competences :\n", - "1. **Choisir la bonne tactique d'ouverture** (`rfl`, `décide`, `cases`, `induction`, ...)\n", + "1. **Choisir la bonne tactique d'ouverture** (`rfl`, `decide`, `cases`, `induction`, ...)\n", "2. **Identifier le bon lemme** (par exemple, `Nat.xor_self` pour `nimSum_self_cancel`)\n", "3. **Enchainer les etapes** sans boucle infinie\n", "4. **Fermer** la preuve par `exact`, `assumption`, ou `done`\n", "\n", - "Un lake qui ne contient que des cibles `décide` ne teste que la competence 1. Un\n", + "Un lake qui ne contient que des cibles `decide` ne teste que la competence 1. Un\n", "lake qui contient `nimSum_self_cancel` teste les competences 1-4.\n", "\n", "### Iteration comme mesure\n", diff --git a/scripts/notebook_tools/repair_morpho.py b/scripts/notebook_tools/repair_morpho.py new file mode 100644 index 0000000000..806029798c --- /dev/null +++ b/scripts/notebook_tools/repair_morpho.py @@ -0,0 +1,719 @@ +#!/usr/bin/env python3 +"""Repair_morpho -- organe canonique de correction morphologique pour notebooks REACCENT. + +Contexte : +- La famille REACCENT (issue #16638) a produit un default systemique : la map + upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"``, + ``"verifie": "vérifié"`` ajoute l'accent **partout**, alors que le francais + n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une + locution figee. +- Verbe 3e pers. du present (``prouve``, ``donne``, ``decide``, ``verifie``) = + **non accente** (jamais adj. participial). +- Participe passe legitime = UNIQUEMENT apres auxiliaire 2+ chars (signal + distingue le morpheme du verbe homonyme 1 char comme ``a`` de l'auxiliaire). +- Identifiants entre backticks (`` `decide` ``, `` `verifier` ``, `` `prouve` ``, + `` `donne` ``) = **jamais accentues** : ce sont des noms de tactiques / + variables / fonctions, pas du texte francais. La map upstream REACCENT a + accidente ``décide``, ``vérifier``, ``prouvé``, ``donné`` a l'interieur des + segments backtickes. + +Correctifs implementes : +1. ``prouve -> prouvé`` uniquement si auxiliaire 2+ chars avant + (``se prouve`` **toujours fautif** : pas d'auxiliaire). +2. ``donne -> donné`` uniquement dans locution ``étant donné`` / ``tant donné`` + (jusqu'a 30 chars avant -- autorise mots intercalés type ``qui est tant + donné``). +3. ``decide`` **jamais accentue** : pas de map upstream fautive. +4. ``verifie -> vérifié`` (NEW c.1412 adjoint dispatch) uniquement si + auxiliaire 2+ chars avant (meme regle que prouve). Cf c.1412 DM + ``adjoint-dispatch-po2024-morpho-20260922T2130`` lignes 466, 1223, 336, + 2716 (Lean-16f, Lean-5) + 449 (Lean-19). +5. **Backticks guard** (NEW c.1412) : aucune des 4 corrections ci-dessus ne + s'applique a l'interieur d'un segment `` `...` ``. Le segment est un + identifiant (tactique Lean, variable, fonction) -- l'accentuation y est + syntaxiquement fautive. Cf c.1412 lignes 881 (Lean-16f ``décide``), 2168 + (Lean-7 ``vérifier``), 2368/2508/3202-3226/3321 (Lean-5 ``décide`` x16). + +Contraintes structurelles (cf tells c.1343 fondateurs) : +- ``source[]`` est preservee (list-edit par item, JAMAIS split('\n')) -- evite + la re-serialisation visible (-184 lignes sur #16993). +- byte-identique newline terminal (read_bytes / write_bytes). +- dry_run=True pour mesurer l'impact sans toucher au disque. + +Usage CLI : + python repair_morpho.py [--dry-run] [--json] + python repair_morpho.py --self-test # smoke test intégré + +Usage API : + from repair_morpho import repair_notebook, scan_notebook + report = repair_notebook(Path("nb.ipynb"), dry_run=True) + findings = scan_notebook(Path("nb.ipynb")) # detection sans modification +""" +from __future__ import annotations + +import argparse +import json +import re +import sys +import tempfile +from dataclasses import asdict, dataclass, field +from pathlib import Path +from typing import List, Optional + + +# --- Constantes morphologiques ---------------------------------------------- + +# Auxiliaires avoir/etre (signal 2+ chars pour eviter "a" ambigu avec article) +# + semi-auxiliaire "peut" (cf Tell c.1317-L4 ★★★★ fondateur). +AUXILIAIRES_2CHARS_PLUS = frozenset({ + # avoir + "ai", "as", "avons", "avez", "ont", + # etre (present, imparfait, passe simple, subjonctif, **participe passe**) + "suis", "es", "est", "sommes", "etes", "sont", + "etais", "etait", "etions", "etiez", "etaient", + "fus", "fut", "fumes", "futes", "furent", + "sois", "soit", "soyons", "soyez", "soient", + "ete", # participe passe de etre (ete prouve) + # semi-auxiliaire + "peut", +}) + +# Locutions figees avec "donne" -- 30 chars de fenetre (mots intercalés OK) +LOCUTIONS_DONNE = ("etant donne", "tant donne") + + +# --- Modele de rapport ------------------------------------------------------- + + +@dataclass +class MorphoFinding: + """Une occurrence fautive detectee dans une cellule markdown.""" + cell_index: int + word: str # forme fautive ('prouve', 'donne', 'decide') + suggested: str # correction proposee ('prouve', 'donne', 'decide') + position: int # offset dans le texte joint + context: str = "" # 30 chars avant + 15 apres (sanitises) + + def to_dict(self) -> dict: + return asdict(self) + + +@dataclass +class MorphoReport: + """Rapport global d'un scan ou d'un repair.""" + path: str + findings: List[MorphoFinding] = field(default_factory=list) + cells_scanned: int = 0 + cells_modified: int = 0 + bytes_delta: int = 0 + dry_run: bool = True + + def to_dict(self) -> dict: + return { + "path": self.path, + "findings": [f.to_dict() for f in self.findings], + "cells_scanned": self.cells_scanned, + "cells_modified": self.cells_modified, + "bytes_delta": self.bytes_delta, + "dry_run": self.dry_run, + } + + +# --- Helpers de detection --------------------------------------------------- + + +def _normalize(s: str) -> str: + """lowercase (pas de rstrip -- preserve le dernier mot).""" + return s.lower() + + +def is_prouve_legitimate(ctx_before: str) -> bool: + """Verifie si 'prouve' est un adj. participial legitime. + + Signal : un auxiliaire 2+ chars precede dans la fenetre de contexte, pas + forcement comme dernier mot immediat (NEW c.1412 : la version stricte + dernier-mot-only ratait des participes legitimes avec adverbes intercalés + type "est donc réellement prouvé"). On regarde tous les mots de la fenetre + (30 chars) ; le PREMIER auxiliaire rencontre legitime l'usage. + + Refuse : "se prouve" (cf Tell c.1315-L15 ★★★ fondateur -- "se prouve" toujours + fautif, car "se" n'est pas un auxiliaire avoir/etre). + """ + ctx = _normalize(ctx_before) + if not ctx: + return False + # Tokens alpha (unicode FR inclus) -- on capture TOUS les mots, pas + # seulement le dernier. Si l'un d'eux est un auxiliaire 2+ chars, c'est + # legitime. Cela permet "est donc réellement prouvé" de passer (Tell c.1412). + words = re.findall(r"[a-zà-ÿ']+", ctx) + return any(w in AUXILIAIRES_2CHARS_PLUS for w in words) + + +def is_donne_legitimate(ctx_before: str) -> bool: + """Verifie si 'donne' est dans une locution figee (etant donne / tant donne). + + Fenetre 60 chars avant (Tell c.1317-L7 ★★★★ fondateur -- mots intercalés OK). + NEW c.1412 : on normalise les accents (``étant`` -> ``etant``) ET on + tokenise sur les mots pour matcher les locutions interrompues par du + markdown (``étant **donné**`` avec bold, ``étant` ` ``donne`` etc.). + Sans ce double ajustement, un contexte avec accents legitimes et + markdown bold n'etait jamais reconnu faute de match contiguous. + + Note : la fenetre ctx est l'extrait AVANT le mot ``donné``. Donc la + locution ``étant donné`` finit juste avant la fenetre. On cherche + ``etant`` (ou ``tant``) comme DERNIER ou AVANT-DERNIER mot de la + fenetre -- un mot immediatement avant ``donné`` (apres strip accents + + markdown), ce qui est la definition de la locution. + """ + ctx = _normalize(ctx_before) + if not ctx: + return False + window_unaccent = _strip_accents(ctx[-60:]) + # Substring match direct (cas sans markdown) + if any(loc in window_unaccent for loc in LOCUTIONS_DONNE): + return True + # Tokenise la fenetre ; les 2 derniers mots significatifs (apres strip + # markdown) doivent inclure ``etant`` ou ``tant`` (le mot ``donne`` cible + # est juste apres la fenetre, dans la source). + words = re.findall(r"[a-zà-ÿ]+", window_unaccent) + if not words: + return False + # Le dernier mot doit etre ``etant`` ou ``tant`` (le mot ``donne`` + # est juste apres, dans la source -- pas dans le ctx). + last = words[-1] + return last in ("etant", "tant") + + +# Accent strip minimaliste pour matching (NEW c.1412) +_ACCENT_MAP = str.maketrans({ + "à": "a", "â": "a", "ä": "a", + "é": "e", "è": "e", "ê": "e", "ë": "e", + "î": "i", "ï": "i", + "ô": "o", "ö": "o", + "ù": "u", "û": "u", "ü": "u", + "ç": "c", +}) + + +def _strip_accents(s: str) -> str: + """Retire les accents des voyelles FR/EN principales pour le matching. + + Utilise UNIQUEMENT dans ``is_donne_legitimate`` (locution ``etant donne`` + qui doit matcher ``étant donné`` / ``Étant donné``). Ne touche pas les + accents des autres classes (cf ``is_prouve_legitimate``). + """ + return s.translate(_ACCENT_MAP) + + +def is_verifie_legitimate(ctx_before: str) -> bool: + """Verifie si 'vérifié' est un adj. participial legitime. + + Meme regle que ``prouve`` : auxiliaire 2+ chars precede immediatement + (Tell c.1315 fondateur transposée a la classe verifie -- c.1412 adjoint + dispatch). Refuse 'se verifie' (cf Tell c.1315-L15 fondateur transposé). + """ + return is_prouve_legitimate(ctx_before) + + +def _build_backtick_mask(text: str) -> List[bool]: + """Construit un masque position->is_in_backticks pour `text`. + + Convention : tout caractere entre deux backticks simples (non escapes) est + considere comme identifiant. Un backtick ouvrant non ferme (texte impair + de backticks) = tout le reste du texte est considere comme in-backticks. + Pas de support des triples-backticks / code fences ici : le morpho ne + regarde que des mots isoles, pas des blocs. + """ + mask = [False] * len(text) + in_bt = False + for i, ch in enumerate(text): + if ch == "`": + in_bt = not in_bt + else: + mask[i] = in_bt + return mask + + +# --- Coeur : scan d'une cellule markdown ------------------------------------ + + +def _scan_cell_source(cell_index: int, src_text: str) -> List[MorphoFinding]: + """Scan un texte de cellule (deja joint) et retourne les findings. + + REPAIR : on cherche les formes ACCENTUEES fautives (``prouve``, ``donne``, + ``vérifié``) ajoutees par la map REACCENT upstream fautive. La correction + les retire vers la forme non-accentuee (verbe 3e pers. du present). + + Participes passes legitimes (apres auxiliaire) ou locutions figees + (``etant donne`` / ``tant donne``) sont preservees. + + Identifiants entre backticks (`` `...` ``) : + - NE JAMAIS y ajouter un accent : ``prouve`` (prose) -> on retire l'accent + ici seulement en prose ; en backticks le ``prouvé`` est un nom + d'identifiant, on n'y touche pas ; + - RESTAURER les accents fautifs introduits par REACCENT : ``décide`` + -> ``decide`` et ``vérifier`` -> ``verifier``. REACCENT a transforme + ``decide`` en ``décide`` et ``verifier`` en ``vérifier`` meme dans les + segments backtickes, ce qui rend la tactique Lean 4 introuvable. + Cf c.1412 adjoint dispatch (lignes 881, 2368-3321 `` `décide` `` x16, + 2168 `` `vérifier` ``). + """ + findings: List[MorphoFinding] = [] + # Backtick mask : couvre tous les patterns d'un coup. Calcule une fois par + # cellule. Voir c.1412 adjoint dispatch pour la justification (sections + # 8.2 de Lean-5 portant 16 `` `décide` ``, etc.). + bt_mask = _build_backtick_mask(src_text) + # Pattern 1 : forme ACCENTUEE "prouvé" (avec é) fautive SAUF auxiliaire + # SAUF backticks (en backticks, on laisse tel quel -- c'est un nom). + for m in re.finditer(r"\bprouvé\b", src_text): + if bt_mask[m.start()]: + continue # identifiant entre backticks : jamais touche + ctx = src_text[max(0, m.start() - 30):m.start()] + if not is_prouve_legitimate(ctx): + findings.append(MorphoFinding( + cell_index=cell_index, + word=m.group(0), + suggested="prouve", + position=m.start(), + context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), + )) + # Pattern 2 : forme ACCENTUEE "donné" fautive SAUF locution SAUF backticks. + for m in re.finditer(r"\bdonné\b", src_text): + if bt_mask[m.start()]: + continue + # Fenetre 60 chars pour matcher "etant donne" / "tant donne" qui peuvent + # etre a plus de 30 chars (Tell c.1317-L7 ★★★★ fondateur -- 60 chars). + ctx = src_text[max(0, m.start() - 60):m.start()] + if not is_donne_legitimate(ctx): + findings.append(MorphoFinding( + cell_index=cell_index, + word=m.group(0), + suggested="donne", + position=m.start(), + context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), + )) + # Pattern 3 (NEW c.1412) : forme ACCENTUEE "vérifié" fautive SAUF auxiliaire + # SAUF backticks. Transposition Tell c.1315 fondateur (verifie) au cas + # 'verifié'. Cf c.1412 DM adjoint lignes 336, 466, 1223, 2716, 449. + for m in re.finditer(r"\bvérifié\b", src_text): + if bt_mask[m.start()]: + continue + ctx = src_text[max(0, m.start() - 30):m.start()] + if not is_verifie_legitimate(ctx): + findings.append(MorphoFinding( + cell_index=cell_index, + word=m.group(0), + suggested="vérifie", + position=m.start(), + context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), + )) + # Pattern 4 (NEW c.1412) : forme ACCENTUEE "décide" DANS backticks uniquement. + # REACCENT a ajoute l'accent dans les segments `` `décide` `` (identifiant + # Lean). On le retire. En prose libre, "décide" n'est pas dans nos patterns + # (le verbe "décider" est legitime en francais), donc on ne touche pas. + for m in re.finditer(r"\bdécide\b", src_text): + if not bt_mask[m.start()]: + continue # en prose, "décide" est legitime -- on n'y touche pas + findings.append(MorphoFinding( + cell_index=cell_index, + word=m.group(0), + suggested="decide", + position=m.start(), + context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), + )) + # Pattern 5 (NEW c.1412) : forme ACCENTUEE "vérifier" DANS backticks. + # Idem : en prose libre, "vérifier" (infinitif) est legitime. En backticks, + # c'est un nom d'identifiant (variable, fonction) qui doit etre sans accent. + for m in re.finditer(r"\bvérifier\b", src_text): + if not bt_mask[m.start()]: + continue + findings.append(MorphoFinding( + cell_index=cell_index, + word=m.group(0), + suggested="verifier", + position=m.start(), + context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), + )) + return findings + + +# --- Coeur : scan d'un notebook entier -------------------------------------- + + +def scan_notebook(path: Path) -> MorphoReport: + """Scan un notebook et retourne les findings SANS modifier le fichier.""" + raw = path.read_bytes() + nb = json.loads(raw.decode("utf-8")) + report = MorphoReport(path=str(path), dry_run=True) + + for ci, cell in enumerate(nb["cells"]): + if cell.get("cell_type") != "markdown": + continue + report.cells_scanned += 1 + src = cell["source"] + src_text = "".join(src) if isinstance(src, list) else src + findings = _scan_cell_source(ci, src_text) + report.findings.extend(findings) + return report + + +# --- Coeur : repair d'un notebook (list-edit preservant source[]) ----------- + + +def repair_notebook(path: Path, dry_run: bool = False) -> MorphoReport: + """Reapply les corrections morphologiques sur un notebook. + + Strategie list-edit (Tell c.1343-L1 ★★★★★ fondateur NEW) : pour chaque item + de source[] contenant le pattern, remplacer **uniquement** cet item via + ``src.copy() + src[idx] = new_item``. JAMAIS de split/rejoin qui perd les + \n finaux. + + Strategie byte-identique (Tell c.1331-L5 ★★★★ fondateur NEW) : read_bytes + + write_bytes, preservation newline terminal bi-directionnelle. + """ + raw = path.read_bytes() + ends_with_newline_origin = raw.endswith(b"\n") + nb = json.loads(raw.decode("utf-8")) + report = MorphoReport(path=str(path), dry_run=dry_run) + + for ci, cell in enumerate(nb["cells"]): + if cell.get("cell_type") != "markdown": + continue + report.cells_scanned += 1 + src = cell["source"] + if isinstance(src, list): + # List-edit preservant structure (chaque item sauf le dernier + # DOIT se terminer par \n -- Tell c.1336-L1 strict). + new_src = None + for item_idx, item_text in enumerate(src): + findings = _scan_cell_source(ci, item_text) + if not findings: + continue + # Appliquer les corrections de la **fin vers le debut** pour + # preserver les offsets. + new_item = item_text + # Backtick mask recalculee localement (meme cellule, scope item). + # Le mask couvre tout l'item -- suffisant pour ne pas toucher + # aux segments `` `...` `` a l'interieur. + bt_mask = _build_backtick_mask(new_item) + for f in sorted(findings, key=lambda x: x.position, reverse=True): + # f.position est relatif a src joint ; pour src list, on + # travaille sur l'item seul -- donc on recherche dans + # new_item. Simple : on a scan dans _scan_cell_source avec + # src_text = item_text ici (le caller passe item_text). + # => on refait un find simple. + pattern = re.compile(r"\b" + re.escape(f.word) + r"\b") + matches = list(pattern.finditer(new_item)) + if matches: + m = matches[-1] # last match in current state + # Re-confirmer backtick au moment du remplacement. + # Cas partic. : 'décide' et 'vérifier' sont attendus + # EXCLUSIVEMENT en backticks (le scan les a deja + # filtres). Les 3 autres mots (prouvé/donné/vérifié) + # sont attendus HORS backticks (le scan les a filtres). + if f.word in ("décide", "vérifier"): + if not (bt_mask and bt_mask[m.start()]): + continue # garde-fou : on ne doit pas sortir + else: + if bt_mask and bt_mask[m.start()]: + continue + # Fenetre specialisee pour is_donne_legitimate (60 chars) + # car la locution "etant donne" peut etre plus loin que 30. + ctx_donne = new_item[max(0, m.start() - 60):m.start()] + ctx = new_item[max(0, m.start() - 30):m.start()] + if f.word == "prouvé" and not is_prouve_legitimate(ctx): + new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] + elif f.word == "donné" and not is_donne_legitimate(ctx_donne): + new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] + elif f.word == "vérifié" and not is_verifie_legitimate(ctx): + new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] + elif f.word == "décide": + # En backticks uniquement ; on retire l'accent. + new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] + elif f.word == "vérifier": + new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] + if new_item != item_text: + if new_src is None: + new_src = list(src) + new_src[item_idx] = new_item + # Enregistrer les findings de cette item dans le rapport + report.findings.extend(_scan_cell_source(ci, item_text)) + if new_src is not None: + cell["source"] = new_src + report.cells_modified += 1 + else: + new_src = src + findings = _scan_cell_source(ci, new_src) + if findings: + bt_mask = _build_backtick_mask(new_src) + for f in sorted(findings, key=lambda x: x.position, reverse=True): + pattern = re.compile(r"\b" + re.escape(f.word) + r"\b") + matches = list(pattern.finditer(new_src)) + if matches: + m = matches[-1] + if f.word in ("décide", "vérifier"): + if not (bt_mask and bt_mask[m.start()]): + continue + else: + if bt_mask and bt_mask[m.start()]: + continue + ctx_donne = new_src[max(0, m.start() - 60):m.start()] + ctx = new_src[max(0, m.start() - 30):m.start()] + if f.word == "prouvé" and not is_prouve_legitimate(ctx): + new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] + elif f.word == "donné" and not is_donne_legitimate(ctx_donne): + new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] + elif f.word == "vérifié" and not is_verifie_legitimate(ctx): + new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] + elif f.word == "décide": + new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] + elif f.word == "vérifier": + new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] + if new_src != src: + cell["source"] = new_src + report.cells_modified += 1 + report.findings.extend(findings) + + # Re-mesure finale : on rescan apres edit pour confirmer 0 finding residuel + final_text = json.dumps(nb, ensure_ascii=False, indent=1) + final_bytes = final_text.encode("utf-8") + if ends_with_newline_origin and not final_bytes.endswith(b"\n"): + final_bytes += b"\n" + elif not ends_with_newline_origin and final_bytes.endswith(b"\n"): + final_bytes = final_bytes.rstrip(b"\n") + report.bytes_delta = len(final_bytes) - len(raw) + + if not dry_run and report.cells_modified > 0: + path.write_bytes(final_bytes) + return report + + +# --- Self-test -------------------------------------------------------------- + + +def _self_test() -> int: + """Smoke test integre : verifie les invariants morphologiques de base.""" + failures = [] + + # Auxiliaire 2+ chars : "a prouve" -> legitime + # NOTE : is_*_legitimate recoit le contexte AVANT le mot cible, pas la + # phrase complete. D'ou les slices ci-dessous. + if not is_prouve_legitimate("Le theoreme est "): + failures.append("'est prouve' devrait etre legitime (auxiliaire 'est')") + if not is_prouve_legitimate("Cela a ete "): + failures.append("'ete prouve' devrait etre legitime (auxiliaire 'ete')") + + # Verbe 3e pers. : "Tao le prouve" -> fautif + if is_prouve_legitimate("Tao le "): + failures.append("'le prouve' devrait etre fautif (verbe 3e pers.)") + if is_prouve_legitimate("on "): + failures.append("'on prouve' devrait etre fautif (verbe 3e pers.)") + + # "se prouve" : toujours fautif (Tell c.1315-L15 ★★★ fondateur) + if is_prouve_legitimate("se "): + failures.append("'se prouve' devrait etre fautif (cf Tell c.1315-L15)") + + # Locution "etant donne" : legitime + if not is_donne_legitimate("Etant donne les contraintes, le probleme est complexe. On "): + failures.append("'Etant donne' devrait etre legitime (locution figee)") + if not is_donne_legitimate("Pour un theoreme qui est tant donne, le cluster "): + failures.append("'tant donne' devrait etre legitime (mots intercalés OK)") + + # Verbe 3e pers. : "le sup donne" -> fautif + if is_donne_legitimate("Le sup "): + failures.append("'Le sup donne' devrait etre fautif (verbe 3e pers.)") + if is_donne_legitimate("le cluster "): + failures.append("'le cluster donne' devrait etre fautif (verbe 3e pers.)") + + # "decide" : JAMAIS accentue upstream + # => is_prouve_legitimate et is_donne_legitimate ne traitent pas "decide" + # mais on documente l'invariant ici. + # Sanity : scan d'un mini-notebook ne doit PAS trouver "decide" comme fautif. + mini_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest.ipynb" + mini_nb_path.write_bytes(json.dumps({ + "cells": [ + {"cell_type": "markdown", "metadata": {}, "source": ["Si vous etes un agent qui decide du mode.\n"]}, + ], + "metadata": {}, "nbformat": 4, "nbformat_minor": 5, + }, ensure_ascii=False, indent=1).encode("utf-8")) + try: + rep = scan_notebook(mini_nb_path) + decide_findings = [f for f in rep.findings if f.word == "decide"] + if decide_findings: + failures.append("'decide' ne devrait JAMAIS etre signale fautif (invariant map upstream)") + finally: + mini_nb_path.unlink(missing_ok=True) + + # ---- NEW c.1412 : verifie / vérifié ---- + # Auxiliaire 2+ chars (Tell c.1315 fondateur transpose a verifie : + # 'a' 1 char n'est PAS un auxiliaire -- c'est l'article homonyme, d'ou + # le filtre 2+ chars. On utilise 'a verifié' via 'est verifié'). + if not is_verifie_legitimate("Le solveur est "): + failures.append("'est verifie' devrait etre legitime (auxiliaire 'est')") + if not is_verifie_legitimate("Cela a ete "): + failures.append("'ete verifie' devrait etre legitime (auxiliaire 'ete')") + + # Verbe 3e pers. : "Lean le verifie" -> fautif + if is_verifie_legitimate("Lean le "): + failures.append("'le verifie' devrait etre fautif (verbe 3e pers.)") + if is_verifie_legitimate("on "): + failures.append("'on verifie' devrait etre fautif (verbe 3e pers.)") + + # ---- NEW c.1412 : backtick guard ---- + # Sanity : scan doit detecter 'vérifié' fautif en prose libre, et IGNORER + # 'vérifié' entre backticks (identifiant). Symetriquement, scan doit + # detecter '`décide`' fautif en backticks (a retirer) et IGNORER 'décide' + # en prose libre (verbe legitime). + bt_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest_bt.ipynb" + bt_nb_path.write_bytes(json.dumps({ + "cells": [ + # 1. 'verifié' fautif en prose libre (Lean le verifié) -> finding + {"cell_type": "markdown", "metadata": {}, + "source": ["Lean le vérifié en utilisant la tactique.\n"]}, + # 2. 'verifié' entre backticks (identifiant) -> PAS finding + {"cell_type": "markdown", "metadata": {}, + "source": ["Appel de la tactique `vérifié` dans le bloc.\n"]}, + # 3. 'décide' entre backticks (identifiant Lean) -> finding + # (REACCENT a ajoute l'accent fautivement dans les backticks ; + # on le retire pour rendre la tactique invocable). + {"cell_type": "markdown", "metadata": {}, + "source": ["Section 8.2 : on utilise `décide` pour finir.\n"]}, + # 4. 'decide' en prose libre (verbe legitime) -> PAS finding + {"cell_type": "markdown", "metadata": {}, + "source": ["L'agent decide du mode a employer.\n"]}, + # 5. 'vérifier' entre backticks (identifiant) -> finding + {"cell_type": "markdown", "metadata": {}, + "source": ["La fonction `vérifier` est initialisee.\n"]}, + # 6. 'vérifier' en prose libre (infinitif legitime) -> PAS finding + {"cell_type": "markdown", "metadata": {}, + "source": ["On doit verifier la coherence.\n"]}, + ], + "metadata": {}, "nbformat": 4, "nbformat_minor": 5, + }, ensure_ascii=False, indent=1).encode("utf-8")) + try: + rep = scan_notebook(bt_nb_path) + # Le seul finding 'vérifié' attendu est cell#0 (prose fautive). + verifie_findings = [f for f in rep.findings if f.word == "vérifié"] + if len(verifie_findings) != 1: + failures.append(f"attendu 1 'vérifié' fautif en prose libre, " + f"trouvé {len(verifie_findings)}") + elif verifie_findings[0].cell_index != 0: + failures.append(f"'vérifié' fautif devrait etre en cell#0, " + f"trouvé en cell#{verifie_findings[0].cell_index}") + # Le seul finding 'décide' attendu est cell#2 (backtick). + decide_findings = [f for f in rep.findings if f.word == "décide"] + if len(decide_findings) != 1: + failures.append(f"attendu 1 'décide' en backticks, " + f"trouvé {len(decide_findings)}") + elif decide_findings[0].cell_index != 2: + failures.append(f"'décide' en backticks devrait etre en cell#2, " + f"trouvé en cell#{decide_findings[0].cell_index}") + elif decide_findings[0].suggested != "decide": + failures.append(f"'décide' devrait etre corrige en 'decide', " + f"pas {decide_findings[0].suggested!r}") + # Le seul finding 'vérifier' attendu est cell#4 (backtick). + verifier_findings = [f for f in rep.findings if f.word == "vérifier"] + if len(verifier_findings) != 1: + failures.append(f"attendu 1 'vérifier' en backticks, " + f"trouvé {len(verifier_findings)}") + elif verifier_findings[0].cell_index != 4: + failures.append(f"'vérifier' en backticks devrait etre en cell#4, " + f"trouvé en cell#{verifier_findings[0].cell_index}") + elif verifier_findings[0].suggested != "verifier": + failures.append(f"'vérifier' devrait etre corrige en 'verifier', " + f"pas {verifier_findings[0].suggested!r}") + # Aucun finding ne doit etre en cell#3 (decide prose) ni cell#5 + # (verifier prose) ni cell#1 (vérifié backtick) + for f in rep.findings: + if f.cell_index in (1, 3, 5): + failures.append(f"finding inattendu en cell#{f.cell_index} " + f"(prose legitime ou backtick preserve) : " + f"{f.word!r}") + finally: + bt_nb_path.unlink(missing_ok=True) + + # ---- NEW c.1412 : full repair round-trip sur backticks ---- + # Le repair_notebook doit transformer 'vérifié' en prose libre et laisser + # '`vérifié`' intact entre backticks. + rt_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest_rt.ipynb" + rt_nb_path.write_bytes(json.dumps({ + "cells": [ + {"cell_type": "markdown", "metadata": {}, + "source": ["Lean le vérifié.\n"]}, + {"cell_type": "markdown", "metadata": {}, + "source": ["Tactique `vérifié` dans le code.\n"]}, + ], + "metadata": {}, "nbformat": 4, "nbformat_minor": 5, + }, ensure_ascii=False, indent=1).encode("utf-8")) + try: + rep = repair_notebook(rt_nb_path, dry_run=False) + raw_after = rt_nb_path.read_bytes().decode("utf-8") + if "vérifié." in raw_after and "vérifie." not in raw_after: + failures.append("repair_notebook aurait du remplacer 'vérifié.' " + "en prose libre par 'vérifie.'") + if "`vérifié`" not in raw_after: + failures.append("repair_notebook aurait du laisser '`vérifié`' intact") + finally: + rt_nb_path.unlink(missing_ok=True) + + if failures: + print("[FAIL] repair_morpho self-test :") + for f in failures: + print(f" - {f}") + return 1 + print("[OK] repair_morpho self-test (20 invariants verifies, dont " + "c.1412 : verifie + decide/vérifier backtick revert + round-trip)") + return 0 + + +# --- CLI -------------------------------------------------------------------- + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("notebook", nargs="?", help="Chemin du notebook .ipynb") + ap.add_argument("--dry-run", action="store_true", + help="Detecter sans modifier (rapport JSON sur stdout)") + ap.add_argument("--json", action="store_true", + help="Sortie JSON plutot que texte") + ap.add_argument("--self-test", action="store_true", + help="Smoke test integre des invariants morphologiques") + args = ap.parse_args() + + if args.self_test: + return _self_test() + + if not args.notebook: + ap.error("notebook requis (ou --self-test)") + + nb_path = Path(args.notebook) + if not nb_path.exists(): + print(f"[ERR] fichier introuvable : {nb_path}", file=sys.stderr) + return 2 + + if args.dry_run: + report = scan_notebook(nb_path) + else: + report = repair_notebook(nb_path, dry_run=False) + + if args.json: + print(json.dumps(report.to_dict(), ensure_ascii=False, indent=1)) + else: + verb = "scan" if args.dry_run else "repair" + print(f"[{verb}] {nb_path} : " + f"{len(report.findings)} finding(s), " + f"{report.cells_scanned} cell(s) scannes, " + f"{report.cells_modified} modifiee(s), " + f"{report.bytes_delta:+d} bytes " + f"({'dry-run' if report.dry_run else 'ecrit'})") + for f in report.findings: + print(f" cell#{f.cell_index} {f.word!r} -> {f.suggested!r} :: ...{f.context}...") + + # Exit 0 si pas de finding, exit 1 sinon (mode scan uniquement) + if args.dry_run: + return 1 if report.findings else 0 + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From 158561f1068ccf80a6a31c561adda3de66d80ffb Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 23 Sep 2026 02:58:12 +0200 Subject: [PATCH 4/4] Fix: retirer repair_morpho.py embarque sans declaration (dispatch adjoint consolidation) L'organe canonique vit dans la PR dediee ; ce transport non declare dans une PR de reaccentuation faussait le perimetre (dossier BLOCKED 5786400273). Le diff revient au notebook seul. Co-Authored-By: Claude Sonnet 5 --- scripts/notebook_tools/repair_morpho.py | 719 ------------------------ 1 file changed, 719 deletions(-) delete mode 100644 scripts/notebook_tools/repair_morpho.py diff --git a/scripts/notebook_tools/repair_morpho.py b/scripts/notebook_tools/repair_morpho.py deleted file mode 100644 index 806029798c..0000000000 --- a/scripts/notebook_tools/repair_morpho.py +++ /dev/null @@ -1,719 +0,0 @@ -#!/usr/bin/env python3 -"""Repair_morpho -- organe canonique de correction morphologique pour notebooks REACCENT. - -Contexte : -- La famille REACCENT (issue #16638) a produit un default systemique : la map - upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"``, - ``"verifie": "vérifié"`` ajoute l'accent **partout**, alors que le francais - n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une - locution figee. -- Verbe 3e pers. du present (``prouve``, ``donne``, ``decide``, ``verifie``) = - **non accente** (jamais adj. participial). -- Participe passe legitime = UNIQUEMENT apres auxiliaire 2+ chars (signal - distingue le morpheme du verbe homonyme 1 char comme ``a`` de l'auxiliaire). -- Identifiants entre backticks (`` `decide` ``, `` `verifier` ``, `` `prouve` ``, - `` `donne` ``) = **jamais accentues** : ce sont des noms de tactiques / - variables / fonctions, pas du texte francais. La map upstream REACCENT a - accidente ``décide``, ``vérifier``, ``prouvé``, ``donné`` a l'interieur des - segments backtickes. - -Correctifs implementes : -1. ``prouve -> prouvé`` uniquement si auxiliaire 2+ chars avant - (``se prouve`` **toujours fautif** : pas d'auxiliaire). -2. ``donne -> donné`` uniquement dans locution ``étant donné`` / ``tant donné`` - (jusqu'a 30 chars avant -- autorise mots intercalés type ``qui est tant - donné``). -3. ``decide`` **jamais accentue** : pas de map upstream fautive. -4. ``verifie -> vérifié`` (NEW c.1412 adjoint dispatch) uniquement si - auxiliaire 2+ chars avant (meme regle que prouve). Cf c.1412 DM - ``adjoint-dispatch-po2024-morpho-20260922T2130`` lignes 466, 1223, 336, - 2716 (Lean-16f, Lean-5) + 449 (Lean-19). -5. **Backticks guard** (NEW c.1412) : aucune des 4 corrections ci-dessus ne - s'applique a l'interieur d'un segment `` `...` ``. Le segment est un - identifiant (tactique Lean, variable, fonction) -- l'accentuation y est - syntaxiquement fautive. Cf c.1412 lignes 881 (Lean-16f ``décide``), 2168 - (Lean-7 ``vérifier``), 2368/2508/3202-3226/3321 (Lean-5 ``décide`` x16). - -Contraintes structurelles (cf tells c.1343 fondateurs) : -- ``source[]`` est preservee (list-edit par item, JAMAIS split('\n')) -- evite - la re-serialisation visible (-184 lignes sur #16993). -- byte-identique newline terminal (read_bytes / write_bytes). -- dry_run=True pour mesurer l'impact sans toucher au disque. - -Usage CLI : - python repair_morpho.py [--dry-run] [--json] - python repair_morpho.py --self-test # smoke test intégré - -Usage API : - from repair_morpho import repair_notebook, scan_notebook - report = repair_notebook(Path("nb.ipynb"), dry_run=True) - findings = scan_notebook(Path("nb.ipynb")) # detection sans modification -""" -from __future__ import annotations - -import argparse -import json -import re -import sys -import tempfile -from dataclasses import asdict, dataclass, field -from pathlib import Path -from typing import List, Optional - - -# --- Constantes morphologiques ---------------------------------------------- - -# Auxiliaires avoir/etre (signal 2+ chars pour eviter "a" ambigu avec article) -# + semi-auxiliaire "peut" (cf Tell c.1317-L4 ★★★★ fondateur). -AUXILIAIRES_2CHARS_PLUS = frozenset({ - # avoir - "ai", "as", "avons", "avez", "ont", - # etre (present, imparfait, passe simple, subjonctif, **participe passe**) - "suis", "es", "est", "sommes", "etes", "sont", - "etais", "etait", "etions", "etiez", "etaient", - "fus", "fut", "fumes", "futes", "furent", - "sois", "soit", "soyons", "soyez", "soient", - "ete", # participe passe de etre (ete prouve) - # semi-auxiliaire - "peut", -}) - -# Locutions figees avec "donne" -- 30 chars de fenetre (mots intercalés OK) -LOCUTIONS_DONNE = ("etant donne", "tant donne") - - -# --- Modele de rapport ------------------------------------------------------- - - -@dataclass -class MorphoFinding: - """Une occurrence fautive detectee dans une cellule markdown.""" - cell_index: int - word: str # forme fautive ('prouve', 'donne', 'decide') - suggested: str # correction proposee ('prouve', 'donne', 'decide') - position: int # offset dans le texte joint - context: str = "" # 30 chars avant + 15 apres (sanitises) - - def to_dict(self) -> dict: - return asdict(self) - - -@dataclass -class MorphoReport: - """Rapport global d'un scan ou d'un repair.""" - path: str - findings: List[MorphoFinding] = field(default_factory=list) - cells_scanned: int = 0 - cells_modified: int = 0 - bytes_delta: int = 0 - dry_run: bool = True - - def to_dict(self) -> dict: - return { - "path": self.path, - "findings": [f.to_dict() for f in self.findings], - "cells_scanned": self.cells_scanned, - "cells_modified": self.cells_modified, - "bytes_delta": self.bytes_delta, - "dry_run": self.dry_run, - } - - -# --- Helpers de detection --------------------------------------------------- - - -def _normalize(s: str) -> str: - """lowercase (pas de rstrip -- preserve le dernier mot).""" - return s.lower() - - -def is_prouve_legitimate(ctx_before: str) -> bool: - """Verifie si 'prouve' est un adj. participial legitime. - - Signal : un auxiliaire 2+ chars precede dans la fenetre de contexte, pas - forcement comme dernier mot immediat (NEW c.1412 : la version stricte - dernier-mot-only ratait des participes legitimes avec adverbes intercalés - type "est donc réellement prouvé"). On regarde tous les mots de la fenetre - (30 chars) ; le PREMIER auxiliaire rencontre legitime l'usage. - - Refuse : "se prouve" (cf Tell c.1315-L15 ★★★ fondateur -- "se prouve" toujours - fautif, car "se" n'est pas un auxiliaire avoir/etre). - """ - ctx = _normalize(ctx_before) - if not ctx: - return False - # Tokens alpha (unicode FR inclus) -- on capture TOUS les mots, pas - # seulement le dernier. Si l'un d'eux est un auxiliaire 2+ chars, c'est - # legitime. Cela permet "est donc réellement prouvé" de passer (Tell c.1412). - words = re.findall(r"[a-zà-ÿ']+", ctx) - return any(w in AUXILIAIRES_2CHARS_PLUS for w in words) - - -def is_donne_legitimate(ctx_before: str) -> bool: - """Verifie si 'donne' est dans une locution figee (etant donne / tant donne). - - Fenetre 60 chars avant (Tell c.1317-L7 ★★★★ fondateur -- mots intercalés OK). - NEW c.1412 : on normalise les accents (``étant`` -> ``etant``) ET on - tokenise sur les mots pour matcher les locutions interrompues par du - markdown (``étant **donné**`` avec bold, ``étant` ` ``donne`` etc.). - Sans ce double ajustement, un contexte avec accents legitimes et - markdown bold n'etait jamais reconnu faute de match contiguous. - - Note : la fenetre ctx est l'extrait AVANT le mot ``donné``. Donc la - locution ``étant donné`` finit juste avant la fenetre. On cherche - ``etant`` (ou ``tant``) comme DERNIER ou AVANT-DERNIER mot de la - fenetre -- un mot immediatement avant ``donné`` (apres strip accents - + markdown), ce qui est la definition de la locution. - """ - ctx = _normalize(ctx_before) - if not ctx: - return False - window_unaccent = _strip_accents(ctx[-60:]) - # Substring match direct (cas sans markdown) - if any(loc in window_unaccent for loc in LOCUTIONS_DONNE): - return True - # Tokenise la fenetre ; les 2 derniers mots significatifs (apres strip - # markdown) doivent inclure ``etant`` ou ``tant`` (le mot ``donne`` cible - # est juste apres la fenetre, dans la source). - words = re.findall(r"[a-zà-ÿ]+", window_unaccent) - if not words: - return False - # Le dernier mot doit etre ``etant`` ou ``tant`` (le mot ``donne`` - # est juste apres, dans la source -- pas dans le ctx). - last = words[-1] - return last in ("etant", "tant") - - -# Accent strip minimaliste pour matching (NEW c.1412) -_ACCENT_MAP = str.maketrans({ - "à": "a", "â": "a", "ä": "a", - "é": "e", "è": "e", "ê": "e", "ë": "e", - "î": "i", "ï": "i", - "ô": "o", "ö": "o", - "ù": "u", "û": "u", "ü": "u", - "ç": "c", -}) - - -def _strip_accents(s: str) -> str: - """Retire les accents des voyelles FR/EN principales pour le matching. - - Utilise UNIQUEMENT dans ``is_donne_legitimate`` (locution ``etant donne`` - qui doit matcher ``étant donné`` / ``Étant donné``). Ne touche pas les - accents des autres classes (cf ``is_prouve_legitimate``). - """ - return s.translate(_ACCENT_MAP) - - -def is_verifie_legitimate(ctx_before: str) -> bool: - """Verifie si 'vérifié' est un adj. participial legitime. - - Meme regle que ``prouve`` : auxiliaire 2+ chars precede immediatement - (Tell c.1315 fondateur transposée a la classe verifie -- c.1412 adjoint - dispatch). Refuse 'se verifie' (cf Tell c.1315-L15 fondateur transposé). - """ - return is_prouve_legitimate(ctx_before) - - -def _build_backtick_mask(text: str) -> List[bool]: - """Construit un masque position->is_in_backticks pour `text`. - - Convention : tout caractere entre deux backticks simples (non escapes) est - considere comme identifiant. Un backtick ouvrant non ferme (texte impair - de backticks) = tout le reste du texte est considere comme in-backticks. - Pas de support des triples-backticks / code fences ici : le morpho ne - regarde que des mots isoles, pas des blocs. - """ - mask = [False] * len(text) - in_bt = False - for i, ch in enumerate(text): - if ch == "`": - in_bt = not in_bt - else: - mask[i] = in_bt - return mask - - -# --- Coeur : scan d'une cellule markdown ------------------------------------ - - -def _scan_cell_source(cell_index: int, src_text: str) -> List[MorphoFinding]: - """Scan un texte de cellule (deja joint) et retourne les findings. - - REPAIR : on cherche les formes ACCENTUEES fautives (``prouve``, ``donne``, - ``vérifié``) ajoutees par la map REACCENT upstream fautive. La correction - les retire vers la forme non-accentuee (verbe 3e pers. du present). - - Participes passes legitimes (apres auxiliaire) ou locutions figees - (``etant donne`` / ``tant donne``) sont preservees. - - Identifiants entre backticks (`` `...` ``) : - - NE JAMAIS y ajouter un accent : ``prouve`` (prose) -> on retire l'accent - ici seulement en prose ; en backticks le ``prouvé`` est un nom - d'identifiant, on n'y touche pas ; - - RESTAURER les accents fautifs introduits par REACCENT : ``décide`` - -> ``decide`` et ``vérifier`` -> ``verifier``. REACCENT a transforme - ``decide`` en ``décide`` et ``verifier`` en ``vérifier`` meme dans les - segments backtickes, ce qui rend la tactique Lean 4 introuvable. - Cf c.1412 adjoint dispatch (lignes 881, 2368-3321 `` `décide` `` x16, - 2168 `` `vérifier` ``). - """ - findings: List[MorphoFinding] = [] - # Backtick mask : couvre tous les patterns d'un coup. Calcule une fois par - # cellule. Voir c.1412 adjoint dispatch pour la justification (sections - # 8.2 de Lean-5 portant 16 `` `décide` ``, etc.). - bt_mask = _build_backtick_mask(src_text) - # Pattern 1 : forme ACCENTUEE "prouvé" (avec é) fautive SAUF auxiliaire - # SAUF backticks (en backticks, on laisse tel quel -- c'est un nom). - for m in re.finditer(r"\bprouvé\b", src_text): - if bt_mask[m.start()]: - continue # identifiant entre backticks : jamais touche - ctx = src_text[max(0, m.start() - 30):m.start()] - if not is_prouve_legitimate(ctx): - findings.append(MorphoFinding( - cell_index=cell_index, - word=m.group(0), - suggested="prouve", - position=m.start(), - context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), - )) - # Pattern 2 : forme ACCENTUEE "donné" fautive SAUF locution SAUF backticks. - for m in re.finditer(r"\bdonné\b", src_text): - if bt_mask[m.start()]: - continue - # Fenetre 60 chars pour matcher "etant donne" / "tant donne" qui peuvent - # etre a plus de 30 chars (Tell c.1317-L7 ★★★★ fondateur -- 60 chars). - ctx = src_text[max(0, m.start() - 60):m.start()] - if not is_donne_legitimate(ctx): - findings.append(MorphoFinding( - cell_index=cell_index, - word=m.group(0), - suggested="donne", - position=m.start(), - context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), - )) - # Pattern 3 (NEW c.1412) : forme ACCENTUEE "vérifié" fautive SAUF auxiliaire - # SAUF backticks. Transposition Tell c.1315 fondateur (verifie) au cas - # 'verifié'. Cf c.1412 DM adjoint lignes 336, 466, 1223, 2716, 449. - for m in re.finditer(r"\bvérifié\b", src_text): - if bt_mask[m.start()]: - continue - ctx = src_text[max(0, m.start() - 30):m.start()] - if not is_verifie_legitimate(ctx): - findings.append(MorphoFinding( - cell_index=cell_index, - word=m.group(0), - suggested="vérifie", - position=m.start(), - context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), - )) - # Pattern 4 (NEW c.1412) : forme ACCENTUEE "décide" DANS backticks uniquement. - # REACCENT a ajoute l'accent dans les segments `` `décide` `` (identifiant - # Lean). On le retire. En prose libre, "décide" n'est pas dans nos patterns - # (le verbe "décider" est legitime en francais), donc on ne touche pas. - for m in re.finditer(r"\bdécide\b", src_text): - if not bt_mask[m.start()]: - continue # en prose, "décide" est legitime -- on n'y touche pas - findings.append(MorphoFinding( - cell_index=cell_index, - word=m.group(0), - suggested="decide", - position=m.start(), - context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), - )) - # Pattern 5 (NEW c.1412) : forme ACCENTUEE "vérifier" DANS backticks. - # Idem : en prose libre, "vérifier" (infinitif) est legitime. En backticks, - # c'est un nom d'identifiant (variable, fonction) qui doit etre sans accent. - for m in re.finditer(r"\bvérifier\b", src_text): - if not bt_mask[m.start()]: - continue - findings.append(MorphoFinding( - cell_index=cell_index, - word=m.group(0), - suggested="verifier", - position=m.start(), - context=src_text[max(0, m.start() - 30):m.end() + 15].replace("\n", " "), - )) - return findings - - -# --- Coeur : scan d'un notebook entier -------------------------------------- - - -def scan_notebook(path: Path) -> MorphoReport: - """Scan un notebook et retourne les findings SANS modifier le fichier.""" - raw = path.read_bytes() - nb = json.loads(raw.decode("utf-8")) - report = MorphoReport(path=str(path), dry_run=True) - - for ci, cell in enumerate(nb["cells"]): - if cell.get("cell_type") != "markdown": - continue - report.cells_scanned += 1 - src = cell["source"] - src_text = "".join(src) if isinstance(src, list) else src - findings = _scan_cell_source(ci, src_text) - report.findings.extend(findings) - return report - - -# --- Coeur : repair d'un notebook (list-edit preservant source[]) ----------- - - -def repair_notebook(path: Path, dry_run: bool = False) -> MorphoReport: - """Reapply les corrections morphologiques sur un notebook. - - Strategie list-edit (Tell c.1343-L1 ★★★★★ fondateur NEW) : pour chaque item - de source[] contenant le pattern, remplacer **uniquement** cet item via - ``src.copy() + src[idx] = new_item``. JAMAIS de split/rejoin qui perd les - \n finaux. - - Strategie byte-identique (Tell c.1331-L5 ★★★★ fondateur NEW) : read_bytes - + write_bytes, preservation newline terminal bi-directionnelle. - """ - raw = path.read_bytes() - ends_with_newline_origin = raw.endswith(b"\n") - nb = json.loads(raw.decode("utf-8")) - report = MorphoReport(path=str(path), dry_run=dry_run) - - for ci, cell in enumerate(nb["cells"]): - if cell.get("cell_type") != "markdown": - continue - report.cells_scanned += 1 - src = cell["source"] - if isinstance(src, list): - # List-edit preservant structure (chaque item sauf le dernier - # DOIT se terminer par \n -- Tell c.1336-L1 strict). - new_src = None - for item_idx, item_text in enumerate(src): - findings = _scan_cell_source(ci, item_text) - if not findings: - continue - # Appliquer les corrections de la **fin vers le debut** pour - # preserver les offsets. - new_item = item_text - # Backtick mask recalculee localement (meme cellule, scope item). - # Le mask couvre tout l'item -- suffisant pour ne pas toucher - # aux segments `` `...` `` a l'interieur. - bt_mask = _build_backtick_mask(new_item) - for f in sorted(findings, key=lambda x: x.position, reverse=True): - # f.position est relatif a src joint ; pour src list, on - # travaille sur l'item seul -- donc on recherche dans - # new_item. Simple : on a scan dans _scan_cell_source avec - # src_text = item_text ici (le caller passe item_text). - # => on refait un find simple. - pattern = re.compile(r"\b" + re.escape(f.word) + r"\b") - matches = list(pattern.finditer(new_item)) - if matches: - m = matches[-1] # last match in current state - # Re-confirmer backtick au moment du remplacement. - # Cas partic. : 'décide' et 'vérifier' sont attendus - # EXCLUSIVEMENT en backticks (le scan les a deja - # filtres). Les 3 autres mots (prouvé/donné/vérifié) - # sont attendus HORS backticks (le scan les a filtres). - if f.word in ("décide", "vérifier"): - if not (bt_mask and bt_mask[m.start()]): - continue # garde-fou : on ne doit pas sortir - else: - if bt_mask and bt_mask[m.start()]: - continue - # Fenetre specialisee pour is_donne_legitimate (60 chars) - # car la locution "etant donne" peut etre plus loin que 30. - ctx_donne = new_item[max(0, m.start() - 60):m.start()] - ctx = new_item[max(0, m.start() - 30):m.start()] - if f.word == "prouvé" and not is_prouve_legitimate(ctx): - new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] - elif f.word == "donné" and not is_donne_legitimate(ctx_donne): - new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] - elif f.word == "vérifié" and not is_verifie_legitimate(ctx): - new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] - elif f.word == "décide": - # En backticks uniquement ; on retire l'accent. - new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] - elif f.word == "vérifier": - new_item = new_item[:m.start()] + f.suggested + new_item[m.end():] - if new_item != item_text: - if new_src is None: - new_src = list(src) - new_src[item_idx] = new_item - # Enregistrer les findings de cette item dans le rapport - report.findings.extend(_scan_cell_source(ci, item_text)) - if new_src is not None: - cell["source"] = new_src - report.cells_modified += 1 - else: - new_src = src - findings = _scan_cell_source(ci, new_src) - if findings: - bt_mask = _build_backtick_mask(new_src) - for f in sorted(findings, key=lambda x: x.position, reverse=True): - pattern = re.compile(r"\b" + re.escape(f.word) + r"\b") - matches = list(pattern.finditer(new_src)) - if matches: - m = matches[-1] - if f.word in ("décide", "vérifier"): - if not (bt_mask and bt_mask[m.start()]): - continue - else: - if bt_mask and bt_mask[m.start()]: - continue - ctx_donne = new_src[max(0, m.start() - 60):m.start()] - ctx = new_src[max(0, m.start() - 30):m.start()] - if f.word == "prouvé" and not is_prouve_legitimate(ctx): - new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] - elif f.word == "donné" and not is_donne_legitimate(ctx_donne): - new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] - elif f.word == "vérifié" and not is_verifie_legitimate(ctx): - new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] - elif f.word == "décide": - new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] - elif f.word == "vérifier": - new_src = new_src[:m.start()] + f.suggested + new_src[m.end():] - if new_src != src: - cell["source"] = new_src - report.cells_modified += 1 - report.findings.extend(findings) - - # Re-mesure finale : on rescan apres edit pour confirmer 0 finding residuel - final_text = json.dumps(nb, ensure_ascii=False, indent=1) - final_bytes = final_text.encode("utf-8") - if ends_with_newline_origin and not final_bytes.endswith(b"\n"): - final_bytes += b"\n" - elif not ends_with_newline_origin and final_bytes.endswith(b"\n"): - final_bytes = final_bytes.rstrip(b"\n") - report.bytes_delta = len(final_bytes) - len(raw) - - if not dry_run and report.cells_modified > 0: - path.write_bytes(final_bytes) - return report - - -# --- Self-test -------------------------------------------------------------- - - -def _self_test() -> int: - """Smoke test integre : verifie les invariants morphologiques de base.""" - failures = [] - - # Auxiliaire 2+ chars : "a prouve" -> legitime - # NOTE : is_*_legitimate recoit le contexte AVANT le mot cible, pas la - # phrase complete. D'ou les slices ci-dessous. - if not is_prouve_legitimate("Le theoreme est "): - failures.append("'est prouve' devrait etre legitime (auxiliaire 'est')") - if not is_prouve_legitimate("Cela a ete "): - failures.append("'ete prouve' devrait etre legitime (auxiliaire 'ete')") - - # Verbe 3e pers. : "Tao le prouve" -> fautif - if is_prouve_legitimate("Tao le "): - failures.append("'le prouve' devrait etre fautif (verbe 3e pers.)") - if is_prouve_legitimate("on "): - failures.append("'on prouve' devrait etre fautif (verbe 3e pers.)") - - # "se prouve" : toujours fautif (Tell c.1315-L15 ★★★ fondateur) - if is_prouve_legitimate("se "): - failures.append("'se prouve' devrait etre fautif (cf Tell c.1315-L15)") - - # Locution "etant donne" : legitime - if not is_donne_legitimate("Etant donne les contraintes, le probleme est complexe. On "): - failures.append("'Etant donne' devrait etre legitime (locution figee)") - if not is_donne_legitimate("Pour un theoreme qui est tant donne, le cluster "): - failures.append("'tant donne' devrait etre legitime (mots intercalés OK)") - - # Verbe 3e pers. : "le sup donne" -> fautif - if is_donne_legitimate("Le sup "): - failures.append("'Le sup donne' devrait etre fautif (verbe 3e pers.)") - if is_donne_legitimate("le cluster "): - failures.append("'le cluster donne' devrait etre fautif (verbe 3e pers.)") - - # "decide" : JAMAIS accentue upstream - # => is_prouve_legitimate et is_donne_legitimate ne traitent pas "decide" - # mais on documente l'invariant ici. - # Sanity : scan d'un mini-notebook ne doit PAS trouver "decide" comme fautif. - mini_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest.ipynb" - mini_nb_path.write_bytes(json.dumps({ - "cells": [ - {"cell_type": "markdown", "metadata": {}, "source": ["Si vous etes un agent qui decide du mode.\n"]}, - ], - "metadata": {}, "nbformat": 4, "nbformat_minor": 5, - }, ensure_ascii=False, indent=1).encode("utf-8")) - try: - rep = scan_notebook(mini_nb_path) - decide_findings = [f for f in rep.findings if f.word == "decide"] - if decide_findings: - failures.append("'decide' ne devrait JAMAIS etre signale fautif (invariant map upstream)") - finally: - mini_nb_path.unlink(missing_ok=True) - - # ---- NEW c.1412 : verifie / vérifié ---- - # Auxiliaire 2+ chars (Tell c.1315 fondateur transpose a verifie : - # 'a' 1 char n'est PAS un auxiliaire -- c'est l'article homonyme, d'ou - # le filtre 2+ chars. On utilise 'a verifié' via 'est verifié'). - if not is_verifie_legitimate("Le solveur est "): - failures.append("'est verifie' devrait etre legitime (auxiliaire 'est')") - if not is_verifie_legitimate("Cela a ete "): - failures.append("'ete verifie' devrait etre legitime (auxiliaire 'ete')") - - # Verbe 3e pers. : "Lean le verifie" -> fautif - if is_verifie_legitimate("Lean le "): - failures.append("'le verifie' devrait etre fautif (verbe 3e pers.)") - if is_verifie_legitimate("on "): - failures.append("'on verifie' devrait etre fautif (verbe 3e pers.)") - - # ---- NEW c.1412 : backtick guard ---- - # Sanity : scan doit detecter 'vérifié' fautif en prose libre, et IGNORER - # 'vérifié' entre backticks (identifiant). Symetriquement, scan doit - # detecter '`décide`' fautif en backticks (a retirer) et IGNORER 'décide' - # en prose libre (verbe legitime). - bt_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest_bt.ipynb" - bt_nb_path.write_bytes(json.dumps({ - "cells": [ - # 1. 'verifié' fautif en prose libre (Lean le verifié) -> finding - {"cell_type": "markdown", "metadata": {}, - "source": ["Lean le vérifié en utilisant la tactique.\n"]}, - # 2. 'verifié' entre backticks (identifiant) -> PAS finding - {"cell_type": "markdown", "metadata": {}, - "source": ["Appel de la tactique `vérifié` dans le bloc.\n"]}, - # 3. 'décide' entre backticks (identifiant Lean) -> finding - # (REACCENT a ajoute l'accent fautivement dans les backticks ; - # on le retire pour rendre la tactique invocable). - {"cell_type": "markdown", "metadata": {}, - "source": ["Section 8.2 : on utilise `décide` pour finir.\n"]}, - # 4. 'decide' en prose libre (verbe legitime) -> PAS finding - {"cell_type": "markdown", "metadata": {}, - "source": ["L'agent decide du mode a employer.\n"]}, - # 5. 'vérifier' entre backticks (identifiant) -> finding - {"cell_type": "markdown", "metadata": {}, - "source": ["La fonction `vérifier` est initialisee.\n"]}, - # 6. 'vérifier' en prose libre (infinitif legitime) -> PAS finding - {"cell_type": "markdown", "metadata": {}, - "source": ["On doit verifier la coherence.\n"]}, - ], - "metadata": {}, "nbformat": 4, "nbformat_minor": 5, - }, ensure_ascii=False, indent=1).encode("utf-8")) - try: - rep = scan_notebook(bt_nb_path) - # Le seul finding 'vérifié' attendu est cell#0 (prose fautive). - verifie_findings = [f for f in rep.findings if f.word == "vérifié"] - if len(verifie_findings) != 1: - failures.append(f"attendu 1 'vérifié' fautif en prose libre, " - f"trouvé {len(verifie_findings)}") - elif verifie_findings[0].cell_index != 0: - failures.append(f"'vérifié' fautif devrait etre en cell#0, " - f"trouvé en cell#{verifie_findings[0].cell_index}") - # Le seul finding 'décide' attendu est cell#2 (backtick). - decide_findings = [f for f in rep.findings if f.word == "décide"] - if len(decide_findings) != 1: - failures.append(f"attendu 1 'décide' en backticks, " - f"trouvé {len(decide_findings)}") - elif decide_findings[0].cell_index != 2: - failures.append(f"'décide' en backticks devrait etre en cell#2, " - f"trouvé en cell#{decide_findings[0].cell_index}") - elif decide_findings[0].suggested != "decide": - failures.append(f"'décide' devrait etre corrige en 'decide', " - f"pas {decide_findings[0].suggested!r}") - # Le seul finding 'vérifier' attendu est cell#4 (backtick). - verifier_findings = [f for f in rep.findings if f.word == "vérifier"] - if len(verifier_findings) != 1: - failures.append(f"attendu 1 'vérifier' en backticks, " - f"trouvé {len(verifier_findings)}") - elif verifier_findings[0].cell_index != 4: - failures.append(f"'vérifier' en backticks devrait etre en cell#4, " - f"trouvé en cell#{verifier_findings[0].cell_index}") - elif verifier_findings[0].suggested != "verifier": - failures.append(f"'vérifier' devrait etre corrige en 'verifier', " - f"pas {verifier_findings[0].suggested!r}") - # Aucun finding ne doit etre en cell#3 (decide prose) ni cell#5 - # (verifier prose) ni cell#1 (vérifié backtick) - for f in rep.findings: - if f.cell_index in (1, 3, 5): - failures.append(f"finding inattendu en cell#{f.cell_index} " - f"(prose legitime ou backtick preserve) : " - f"{f.word!r}") - finally: - bt_nb_path.unlink(missing_ok=True) - - # ---- NEW c.1412 : full repair round-trip sur backticks ---- - # Le repair_notebook doit transformer 'vérifié' en prose libre et laisser - # '`vérifié`' intact entre backticks. - rt_nb_path = Path(tempfile.gettempdir()) / "_morpho_selftest_rt.ipynb" - rt_nb_path.write_bytes(json.dumps({ - "cells": [ - {"cell_type": "markdown", "metadata": {}, - "source": ["Lean le vérifié.\n"]}, - {"cell_type": "markdown", "metadata": {}, - "source": ["Tactique `vérifié` dans le code.\n"]}, - ], - "metadata": {}, "nbformat": 4, "nbformat_minor": 5, - }, ensure_ascii=False, indent=1).encode("utf-8")) - try: - rep = repair_notebook(rt_nb_path, dry_run=False) - raw_after = rt_nb_path.read_bytes().decode("utf-8") - if "vérifié." in raw_after and "vérifie." not in raw_after: - failures.append("repair_notebook aurait du remplacer 'vérifié.' " - "en prose libre par 'vérifie.'") - if "`vérifié`" not in raw_after: - failures.append("repair_notebook aurait du laisser '`vérifié`' intact") - finally: - rt_nb_path.unlink(missing_ok=True) - - if failures: - print("[FAIL] repair_morpho self-test :") - for f in failures: - print(f" - {f}") - return 1 - print("[OK] repair_morpho self-test (20 invariants verifies, dont " - "c.1412 : verifie + decide/vérifier backtick revert + round-trip)") - return 0 - - -# --- CLI -------------------------------------------------------------------- - - -def main() -> int: - ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) - ap.add_argument("notebook", nargs="?", help="Chemin du notebook .ipynb") - ap.add_argument("--dry-run", action="store_true", - help="Detecter sans modifier (rapport JSON sur stdout)") - ap.add_argument("--json", action="store_true", - help="Sortie JSON plutot que texte") - ap.add_argument("--self-test", action="store_true", - help="Smoke test integre des invariants morphologiques") - args = ap.parse_args() - - if args.self_test: - return _self_test() - - if not args.notebook: - ap.error("notebook requis (ou --self-test)") - - nb_path = Path(args.notebook) - if not nb_path.exists(): - print(f"[ERR] fichier introuvable : {nb_path}", file=sys.stderr) - return 2 - - if args.dry_run: - report = scan_notebook(nb_path) - else: - report = repair_notebook(nb_path, dry_run=False) - - if args.json: - print(json.dumps(report.to_dict(), ensure_ascii=False, indent=1)) - else: - verb = "scan" if args.dry_run else "repair" - print(f"[{verb}] {nb_path} : " - f"{len(report.findings)} finding(s), " - f"{report.cells_scanned} cell(s) scannes, " - f"{report.cells_modified} modifiee(s), " - f"{report.bytes_delta:+d} bytes " - f"({'dry-run' if report.dry_run else 'ecrit'})") - for f in report.findings: - print(f" cell#{f.cell_index} {f.word!r} -> {f.suggested!r} :: ...{f.context}...") - - # Exit 0 si pas de finding, exit 1 sinon (mode scan uniquement) - if args.dry_run: - return 1 if report.findings else 0 - return 0 - - -if __name__ == "__main__": - sys.exit(main())