Skip to content

fix(notebooks,#17357): Lean-02 — renvois de cellules perimes, plan incomplet, enumeration d'exercices fausse #20150

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 11, 2026
Merged

fix(notebooks,#17357): Lean-02 — renvois de cellules perimes, plan incomplet, enumeration d'exercices fausse #20150

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-02-Dependent-Types-Lean.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -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."
]
Expand Down Expand Up @@ -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."
]
},
{
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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."
]
Expand Down
Loading