From de25f2a205e895ae3267d3a4b10d760e1a106ea2 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Fri, 9 Oct 2026 19:20:19 +0200 Subject: [PATCH] Fix(notebooks,#17357): Lean-02 -- renvois de cellules perimes, plan incomplet, enumeration d'exercices fausse MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Quatre constats de l'audit #17357 revérifiés sur main, tous CONFIRMÉS, plus un cinquième de la même classe que l'audit n'énumérait pas. Corrections markdown uniquement (exception C.2 : aucune cellule de code touchée, aucune ré-exécution requise). - F1 (renvois « cellule N » perimes, décalage -5 constant) : §9 citait `square` (46), `applyTwice` (48), `mapPair` (50) ; les définitions sont en 51, 53 et 55. §10 citait `isEven` (52) ; `def isEven` est en 57. Les renvois par numéro sont remplacés par des renvois par nom, qui ne dérivent pas. - F1 étendu (non listé par l'audit) : §7.3 renvoyait à « la cellule 38 » pour `TypeSelector` ; la définition est en 43. - F2 (progression) : le plan ne listait que 9 entrées alors que le carnet porte 10 sections — « 10. Exercices à compléter » n'y figurait pas. - F3 (exercices) : §10 annonçait trois exercices en citant `isEven` deux fois et en omettant `myFlip` et `mySwap` ; l'énumération décrit maintenant les trois stubs réels. - F3 aggravant : le conseil méthodologique décrivait un stub `result := ... # TODO étudiant` qui n'existe dans aucune cellule — les stubs réels s'écrivent `def nom ... := sorry` avec l'énoncé en `-- TODO étudiant`. - F4 (sections) : §6.2 affirmait que le carnet « utilise deux sections » ; `grep '^\s*section'` sur les 29 cellules de code en trouve une seule (`ExempleSection`). La prose décrit désormais ce que la cellule montre réellement (variable partagée, définitions accessibles hors de la section). See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Lean/Lean-02-Dependent-Types-Lean.ipynb | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-02-Dependent-Types-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-02-Dependent-Types-Lean.ipynb index d5cdc048a6..63420c7a78 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-02-Dependent-Types-Lean.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-02-Dependent-Types-Lean.ipynb @@ -50,7 +50,8 @@ "- **6** [Variables et Sections](#6-variables-sections)\n", "- **7** [Types Dependants](#7-types-dependants)\n", "- **8** [Arguments Implicites](#8-arguments-implicites)\n", - "- **9** [Exercices](#9-exercices)\n", + "- **9** [Exemples guidés](#9-exercices)\n", + "- **10** [Exercices à compléter](#10-exercices)\n", "\n", "***\n", "\n", @@ -2648,7 +2649,7 @@ "\n", "Une section s'ouvre avec `section Nom` (le nom est optionnel) et se ferme avec `end` ou `end Nom`. Tout ce qui est déclaré entre les deux — variables, définitions, lemmes — **disparaît du namespace global** au moment du `end`. C'est l'outil de structuration des unités de cours et de preuves : on isole un mini-contexte avec ses propres conventions, et le lecteur sait que rien ne fuit.\n", "\n", - "L'usage pédagogique est important : Lean-2 utilise deux sections (`section ExempleSection` à la cellule 30) pour démontrer qu'on peut écrire deux `def` avec la même signature dans des sections différentes sans collision. C'est ce qui rend possible d'écrire des notebooks entiers sans se soucier des conflits de noms : chaque « exemple » est dans sa propre section.\n", + "L'usage pédagogique est important : la section `ExempleSection` déclare `variable (x y : Nat)` une seule fois, puis deux définitions `addXY` et `mulXY` qui s'en servent sans les répéter dans leur signature. Après le `end ExempleSection`, `x` et `y` ne sont plus dans la portée, mais `addXY` et `mulXY` restent accessibles avec leurs arguments — `#eval addXY 3 4` rend `7`. C'est cette économie d'écriture qui rend les sections utiles : on déclare le contexte une fois, au lieu de le répéter sur chaque signature.\n", "\n", "**Convention de la série Lean** : les sections servent à grouper les définitions par thème (section 2 = types fonctions, section 3 = types produits, etc.), les namespaces servent à organiser les **exports nommés** que d'autres modules importeront (par exemple `Conway.Life.step`). Vous verrez les sections rester locales aux notebooks, et les namespaces envahir les lakes entiers à partir de Lean-9." ] @@ -3965,7 +3966,7 @@ "\n", "Cette mécanique est le **cœur** de Lean-12 et Lean-14. Vous y verrez des définitions comme `(ε : ℝ) -> Sensitivity.formula ε : Prop` : la formule de sensibilité dépend du paramètre `ε`. Sans Pi-type, cette formulation serait impossible : il faudrait encoder `ε` dans un type produit et naviguer entre les composantes à la main.\n", "\n", - "La cellule 38 va plus loin avec `TypeSelector : Bool -> Type`, qui retourne un type différent selon l'argument. C'est le même mécanisme : la sortie dépend de l'entrée, et le typeur de Lean le suit à la trace. Vous retrouverez cette forme dans Lean-4 (quantificateurs) où `∀ x : A, P x` n'est que du sucre pour `(x : A) -> P x`, et dans Lean-16b où les Game-of-Life patterns sont paramétrés par leur position dans la grille." + "Le type `TypeSelector : Bool -> Type`, défini un peu plus bas dans cette section, va plus loin : il retourne un type différent selon l'argument. C'est le même mécanisme : la sortie dépend de l'entrée, et le typeur de Lean le suit à la trace. Vous retrouverez cette forme dans Lean-4 (quantificateurs) où `∀ x : A, P x` n'est que du sucre pour `(x : A) -> P x`, et dans Lean-16b où les Game-of-Life patterns sont paramétrés par leur position dans la grille." ] }, { @@ -4699,7 +4700,7 @@ "\n", "### Lire les solutions, c'est apprendre le style\n", "\n", - "Les trois exemples qui suivent sont des **solutions corrigées** de TP EPITA-IASY : `square` (cellule 46), `applyTwice` (cellule 48), `mapPair` (cellule 50). Avant de plonger dans les exercices de la section 10, prenez 5 minutes pour **lire ces solutions comme du texte**, pas comme du code :\n", + "Les trois exemples qui suivent sont des **solutions corrigées** de TP EPITA-IASY : `square` (exemple guidé 1), `applyTwice` (exemple guidé 2), `mapPair` (exemple guidé 3). Avant de plonger dans les exercices de la section 10, prenez 5 minutes pour **lire ces solutions comme du texte**, pas comme du code :\n", "\n", "1. **Les signatures** : notez comment les annotations de type sont placées (`def square (n : Nat) : Nat := n * n` — annotation retour, pas d'implicite). C'est la convention de la série Lean : explicite pour les API, implicite pour les sous-calculs.\n", "\n", @@ -5066,13 +5067,13 @@ "\n", "### Stratégie pour aborder les exercices\n", "\n", - "Les exercices à compléter sont au nombre de trois : `isEven` (cellule 52), un exercice de parité, et la normalisation de paire déjà vue en §5 (cellule 26). Trois principes pour les résoudre :\n", + "Les exercices à compléter sont au nombre de trois : `isEven` (parité d'un `Nat`), `myFlip` (inversion des deux arguments d'une fonction binaire) et `mySwap` (échange des composantes d'une paire). Trois principes pour les résoudre :\n", "\n", "1. **Lisez la signature** : chaque exercice déclare son type de retour et ses arguments. C'est votre contrat. Si vous voyez `def isEven : Nat -> Bool`, vous savez que la fonction prend un `Nat` et retourne un `Bool`. Pas de retour ambigu.\n", "\n", "2. **Utilisez `#eval` pour tester** : chaque stub est suivi d'un `#eval` commenté. Décommentez-le après votre implémentation pour vérifier que la sortie est celle attendue. Lean exécutera votre code et affichera le résultat dans la cellule suivante.\n", "\n", - "3. **Ne remplacez pas le `# TODO`** : le stub contient `result := ... # TODO étudiant` — c'est votre espace de travail. Remplacer le `# TODO` par votre solution est correct ; supprimer toute la cellule ou la réécrire viole la convention C.1.\n", + "3. **Remplacez le `sorry`, gardez l'énoncé** : chaque stub s'écrit `def nom ... := sorry` et porte son énoncé en commentaire `-- TODO étudiant`. Remplacez le `sorry` par votre implémentation, puis supprimez le commentaire `-- TODO étudiant`. Garder la cellule, sa signature et son `#eval` commenté rend votre travail vérifiable ; réécrire ou supprimer la cellule viole la convention C.1.\n", "\n", "**Pour aller plus loin** : une fois les trois stubs résolus, vous pouvez tester votre code avec `#reduce isEven 42` (réduit l'expression en sa valeur normale, étape par étape) ou `#check isEven` (vérifie le type de votre fonction sans l'exécuter). Ces deux commandes sont vos outils de mise au point." ]