diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb index 429edea13f..303feb7f37 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-2-Dependent-Types.ipynb @@ -34,10 +34,10 @@ "\n", "### Prerequis\n", "\n", - "- Avoir complete le notebook **Lean-1-Setup** (installation fonctionnelle)\n", + "- Avoir complète le notebook **Lean-1-Setup** (installation fonctionnelle)\n", "- Notions de base en programmation fonctionnelle (utile mais non obligatoire)\n", "\n", - "### Duree estimee : 35-40 minutes\n", + "### Duree estimée : 35-40 minutes\n", "\n", "\n", "## Plan de ce Notebook\n", @@ -46,7 +46,7 @@ "- **2** [Types Fonctions](#2-types-fonctions)\n", "- **3** [Types Produits](#3-types-produits)\n", "- **4** [Hiérarchie des Univers](#4-hierarchie-univers)\n", - "- **5** [Definitions Locales](#5-definitions-locales)\n", + "- **5** [Définitions Locales](#5-définitions-locales)\n", "- **6** [Variables et Sections](#6-variables-sections)\n", "- **7** [Types Dependants](#7-types-dependants)\n", "- **8** [Arguments Implicites](#8-arguments-implicites)\n", @@ -255,7 +255,7 @@ } ], "source": [ - "-- Types numeriques\n", + "-- Types numériques\n", "#check Nat -- Nat : Type (entiers naturels 0, 1, 2, ...)\n", "#check Int -- Int : Type (entiers relatifs ..., -1, 0, 1, ...)\n", "#check Float -- Float : Type (nombres flottants)\n", @@ -286,9 +286,9 @@ "tags": [] }, "source": [ - "### 1.2 Definitions de variables\n", + "### 1.2 Définitions de variables\n", "\n", - "En Lean, on définit des constantes avec le mot-cle `def`. Contrairement aux variables mutables, ces definitions sont **immuables** - une fois définies, leur valeur ne peut plus changer.\n", + "En Lean, on définit des constantes avec le mot-cle `def`. Contrairement aux variables mutables, ces définitions sont **immuables** - une fois définies, leur valeur ne peut plus changer.\n", "\n", "### Pourquoi `def`, et pas une « variable » au sens Python\n", "\n", @@ -422,14 +422,14 @@ } ], "source": [ - "-- Definitions simples avec annotation de type\n", + "-- Définitions simples avec annotation de type\n", "def m : Nat := 1\n", "def n : Nat := 0\n", "def b1 : Bool := true\n", "def b2 : Bool := false\n", "def greeting : String := \"Bonjour Lean!\"\n", "\n", - "-- Verification des types\n", + "-- Vérification des types\n", "#check m -- m : Nat\n", "#check b1 -- b1 : Bool\n", "\n", @@ -596,7 +596,7 @@ "#check x -- x : Nat\n", "#check flag -- flag : Bool\n", "\n", - "-- Operations arithmetiques\n", + "-- Opérations arithmetiques\n", "def sum := m + n -- Addition de Nat\n", "def product := m * 5 -- Multiplication\n", "\n", @@ -960,7 +960,7 @@ "\n", "#eval add 3 4 -- 7\n", "\n", - "-- Encore plus court : definition avec arguments nommes\n", + "-- Encore plus court : définition avec arguments nommes\n", "def add' (x y : Nat) : Nat := x + y\n", "\n", "#eval add' 3 4 -- 7" @@ -1518,7 +1518,7 @@ } ], "source": [ - "-- Projection premiere (deja definie dans Lean)\n", + "-- Projection premiere (deja définie dans Lean)\n", "#check @Prod.fst -- Prod.fst : {a : Type} -> {b : Type} -> Prod a b -> a\n", "\n", "-- Notre propre fonction d'echange\n", @@ -1941,7 +1941,7 @@ "#check identity Nat 42 -- Nat\n", "#check identity Bool true -- Bool\n", "\n", - "-- Meme avec des types de niveau superieur\n", + "-- Meme avec des types de niveau supérieur\n", "#check identity Type Nat -- Type\n", "#check identity (Type 1) Type -- Type 1\n", "\n", @@ -1965,10 +1965,10 @@ "tags": [] }, "source": [ - "\n", - "## 5. Definitions Locales avec `let`\n", + "\n", + "## 5. Définitions Locales avec `let`\n", "\n", - "Le mot-cle `let` permet d'introduire des definitions locales dans une expression. Cela ameliore la lisibilite et evite de recalculer des sous-expressions.\n", + "Le mot-cle `let` permet d'introduire des définitions locales dans une expression. Cela ameliore la lisibilite et evite de recalculer des sous-expressions.\n", "\n", "### `let`, le bloc-notes du programmeur Lean\n", "\n", @@ -1982,7 +1982,7 @@ "def exemple : Nat :=\n", " let y := calcul1\n", " let z := calcul2 y\n", - " resultat y z\n", + " résultat y z\n", "```\n", "\n", "Si vous oubliez d'indenter, Lean lèvera une erreur de syntaxe vous indiquant la ligne attendue. Cette discipline d'indentation force les définitions à rester lisibles : un `let` mal indenté devient vite illisible à l'œil." @@ -2122,14 +2122,14 @@ } ], "source": [ - "-- Definition locale simple\n", + "-- Définition locale simple\n", "def example1 : Nat :=\n", " let y := 2 + 2\n", " y * y\n", "\n", "#eval example1 -- 16\n", "\n", - "-- Plusieurs definitions locales\n", + "-- Plusieurs définitions locales\n", "def example2 : Nat :=\n", " let a := 5\n", " let b := 3\n", @@ -2166,8 +2166,8 @@ "| Aspect | `def` | `let` |\n", "|--------|-------|-------|\n", "| Portee | Globale (ou namespace) | Locale a l'expression |\n", - "| Visibilite | Partout après definition | Uniquement dans le corps du let |\n", - "| Usage | Definitions reutilisables | Calculs intermediaires |\n", + "| Visibilite | Partout après définition | Uniquement dans le corps du let |\n", + "| Usage | Définitions reutilisables | Calculs intermediaires |\n", "\n", "### Pourquoi `let` plutôt que `def` pour un sous-calcul\n", "\n", @@ -2430,7 +2430,7 @@ ], "source": [ "-- Exercice 4 : Normalisation d'une paire avec let\n", - "-- TODO etudiant : definir normalize qui reordonne une paire (a, b) en (min, max)\n", + "-- TODO étudiant : définir normalize qui reordonne une paire (a, b) en (min, max)\n", "-- Indice : utiliser des let bindings pour le minimum et le maximum\n", "def normalize (p : Nat × Nat) : Nat × Nat := sorry\n", "-- #eval normalize (7, 3) -- doit retourner (3, 7)\n", @@ -2457,7 +2457,7 @@ "\n", "### 6.1 La commande `variable`\n", "\n", - "La commande `variable` declare des paramètres implicites qui seront automatiquement ajoutes aux definitions suivantes. C'est utile pour eviter de repeter les mêmes paramètres de type.\n", + "La commande `variable` declare des paramètres implicites qui seront automatiquement ajoutes aux définitions suivantes. C'est utile pour eviter de repeter les mêmes paramètres de type.\n", "\n", "### Pourquoi `variable` change l'écriture des signatures\n", "\n", @@ -2621,7 +2621,7 @@ "def id2 (x : a) : a := x\n", "def const2 (x : a) (y : b) : a := x\n", "\n", - "-- Lean ajoute automatiquement les parametres de type\n", + "-- Lean ajoute automatiquement les paramètres de type\n", "#check id2 -- id2 (a : Type) (x : a) : a\n", "#check const2 -- const2 (a b : Type) (x : a) (y : b) : a" ] @@ -2801,7 +2801,7 @@ "source": [ "### 6.3 Namespaces\n", "\n", - "Les **namespaces** organisent les definitions en groupes nommes, evitant les conflits de noms. Contrairement aux sections, les namespaces prefixent les noms des definitions.\n", + "Les **namespaces** organisent les définitions en groupes nommes, evitant les conflits de noms. Contrairement aux sections, les namespaces prefixent les noms des définitions.\n", "\n", "### Namespaces : la version nommable de la section\n", "\n", @@ -3005,16 +3005,16 @@ "\n", "## 6.4 Declarer ses propres types : `inductive` et `structure`\n", "\n", - "Avant les types dependants (`Fin`, `Vector`), il est utile de savoir **construire** un type de donnees :\n", + "Avant les types dependants (`Fin`, `Vector`), il est utile de savoir **construire** un type de données :\n", "un **type somme** (plusieurs constructeurs distincts) et un **record a champs nommes** (`structure`).\n", "\n", "Trois formes a distinguer :\n", "\n", "| Forme | Quand | Exemple canonique deja vu dans ce parcours |\n", "|---|---|---|\n", - "| **type concret** (un seul habitant par definition) | Pour une valeur unique | `Nat`, `Bool`, `String` |\n", - "| **type parametre** | Pour des familles de types indexees | `List a`, `Prod a b` (vu section 3) |\n", - "| **type inductif** (`inductive`) | Pour des donnees *somme* avec plusieurs constructeurs, recursives ou non | on va le voir : `DayOfWeek` |\n", + "| **type concret** (un seul habitant par définition) | Pour une valeur unique | `Nat`, `Bool`, `String` |\n", + "| **type paramètre** | Pour des familles de types indexees | `List a`, `Prod a b` (vu section 3) |\n", + "| **type inductif** (`inductive`) | Pour des données *somme* avec plusieurs constructeurs, recursives ou non | on va le voir : `DayOfWeek` |\n", "| **record** (`structure`) | Pour un *produit* a champs nommes, equivalent a `Prod` mais accessible par `.field` | on va le voir : `MyPoint` |\n", "\n", "**Pont avec la suite** : `Fin n` (section 7) est declare par `inductive` ; `Vector n a` aussi. Le geste appris ici reapparait\n", @@ -3416,7 +3416,7 @@ "#eval p1.y -- 4\n", "#eval origin -- { x := 0, y := 0 } (grace a `deriving Repr`)\n", "\n", - "-- Fonction : distance carree au carre (pas de sqrt, reste en Nat).\n", + "-- Fonction : distance carree au carré (pas de sqrt, reste en Nat).\n", "def distanceSq (a b : MyPoint) : Nat :=\n", " let dx := a.x - b.x\n", " let dy := a.y - b.y\n", @@ -3557,12 +3557,12 @@ "namespace LocalIntro\n", "\n", "-- Exercice 4b : Sign d'un entier\n", - "-- TODO etudiant : declarer un type inductif `Sign` a 3 constructeurs `pos`, `zero`, `neg`\n", - "-- (avec `deriving Repr, BEq`), puis definir `sign : Int -> Sign` par `match` sur `Int`.\n", + "-- TODO étudiant : declarer un type inductif `Sign` a 3 constructeurs `pos`, `zero`, `neg`\n", + "-- (avec `deriving Repr, BEq`), puis définir `sign : Int -> Sign` par `match` sur `Int`.\n", "-- Tester avec `#eval sign 5`, `#eval sign 0`, `#eval sign (-3)`.\n", "-- Indice : `Int` est un type primitif ; `match` fonctionne comme sur `DayOfWeek`.\n", "\n", - "-- cellule neutre : permet l'execution de bout en bout avant que l'etudiant complete l'exercice.\n", + "-- cellule neutre : permet l'exécution de bout en bout avant que l'étudiant complète l'exercice.\n", "def placeholder : Nat := 0\n", "#eval placeholder\n", "\n", @@ -3755,17 +3755,7 @@ "tags": [] }, "source": [ - "### 7.2 Le type `List a` : un type paramètre\n", - "\n", - "Avant les types vraiment dependants, regardons les **types paramètres** comme `List`. Le type `List Nat` est construit en appliquant le constructeur de types `List` au type `Nat`.\n", - "\n", - "### `List`, votre premier **constructeur de types**\n", - "\n", - "Avant `List`, tous les types que vous avez vus étaient des **types concrets** : `Nat`, `Bool`, `String`. `List` est différent : c'est un **constructeur de types** qui prend un type en argument et retourne un nouveau type. `#check List` répond `List : Type u_1 -> Type u_1` : `List` est une fonction qui, étant donné un type `a`, produit le type « liste de `a` ».\n", - "\n", - "Cette distinction — types concrets vs constructeurs de types — est **la** distinction qui prépare Lean-3 (propositions), Lean-4 (quantificateurs) et Lean-12 (Sensitivity). À chaque étape, vous verrez des constructeurs plus expressifs : `Σ` (type sigma, dont le type de la seconde composante dépend de la première), `Finset`, `Set`, etc. Tous partagent la même mécanique : « prenez des arguments, retournez un type ».\n", - "\n", - "Concrètement, `List Nat` est le type des listes de naturels (`[1, 2, 3] : List Nat`), `List Bool` le type des listes de booléens, et `List (List Nat)` le type des listes de listes de naturels. Aucune restriction : `List` accepte n'importe quel type en argument, y compris lui-même." + "### 7.2 Le type `List a` : un type paramètre\n\nAvant les types vraiment dependants, regardons les **types paramètres** comme `List`. Le type `List Nat` est construit en appliquant le constructeur de types `List` au type `Nat`.\n\n### `List`, votre premier **constructeur de types**\n\nAvant `List`, tous les types que vous avez vus étaient des **types concrets** : `Nat`, `Bool`, `String`. `List` est différent : c'est un **constructeur de types** qui prend un type en argument et retourne un nouveau type. `#check List` répond `List : Type u_1 -> Type u_1` : `List` est une fonction qui, étant donné un type `a`, produit le type « liste de `a` ».\n\nCette distinction — types concrets vs constructeurs de types — est **la** distinction qui prépare Lean-3 (propositions), Lean-4 (quantificateurs) et Lean-12 (Sensitivity). À chaque étape, vous verrez des constructeurs plus expressifs : `Σ` (type sigma, dont le type de la seconde composante dépend de la première), `Finset`, `Set`, etc. Tous partagent la même mécanique : « prenez des arguments, retournez un type ».\n\nConcrètement, `List Nat` est le type des listes de naturels (`[1, 2, 3] : List Nat`), `List Bool` le type des listes de booléens, et `List (List Nat)` le type des listes de listes de naturels. Aucune restriction : `List` accepte n'importe quel type en argument, y compris lui-même." ] }, { @@ -3936,7 +3926,7 @@ "#eval numbers -- [1, 2, 3, 4, 5]\n", "#eval numbers.length -- 5\n", "\n", - "-- Fonctions generiques sur les listes\n", + "-- Fonctions génériques sur les listes\n", "#check @List.map -- List.map : {a b : Type} -> (a -> b) -> List a -> List b\n", "#eval numbers.map (fun x => x * 2) -- [2, 4, 6, 8, 10]" ] @@ -3955,7 +3945,7 @@ "tags": [] }, "source": [ - "### 7.3 Types dependants veritables\n", + "### 7.3 Types dependants véritables\n", "\n", "Un vrai type dependant est un type qui depend d'une **valeur** (pas seulement d'un autre type). Le type dependent fondamental est le **Pi-type** (produit dependant) `(x : A) -> B x`.\n", "\n", @@ -4315,7 +4305,7 @@ ], "source": [ "-- Exercice 5 : Fonction a type de retour dependent\n", - "-- TODO etudiant : definir StatusType et statusMessage\n", + "-- TODO étudiant : définir StatusType et statusMessage\n", "-- StatusType (b : Bool) : Type doit retourner Nat si b = true, String si b = false\n", "-- statusMessage (b : Bool) : StatusType b doit retourner 200 si b = true, \"error\" si b = false\n", "def StatusType (b : Bool) : Type := sorry\n", @@ -4692,10 +4682,10 @@ "\n", "## 9. Exemples guides (exercices resolus)\n", "\n", - "> Ces trois exemples reprennent des solutions proposees par les etudiants **Clovis Lefebvre** et **Evariste Balvay** (TP EPITA-IASY). Etudiez-les avant de passer aux exercices de la section 10.\n", + "> Ces trois exemples reprennent des solutions proposees par les étudiants **Clovis Lefebvre** et **Evariste Balvay** (TP EPITA-IASY). Etudiez-les avant de passer aux exercices de la section 10.\n", "\n", - "### Exemple guide 1 : Definitions de base\n", - "Une fonction `square` qui calcule le carre d'un nombre naturel.\n", + "### Exemple guide 1 : Définitions de base\n", + "Une fonction `square` qui calcule le carré d'un nombre naturel.\n", "\n", "### Lire les solutions, c'est apprendre le style\n", "\n", @@ -4808,16 +4798,7 @@ "tags": [] }, "source": [ - "### Exemple guide 2 : Fonctions d'ordre superieur\n", - "Une fonction `applyTwice` qui applique une fonction deux fois a une valeur.\n", - "\n", - "### Fonctions d'ordre supérieur, le pivot du polymorphisme\n", - "\n", - "`applyTwice : {a : Type} -> (a -> a) -> a -> a` est une **fonction d'ordre supérieur** : elle prend une fonction `f` en argument. La signature dit « pour tout type `a`, étant donné une fonction `a -> a` et une valeur `a`, retourner le résultat de `f (f x)` ». Cette signature fonctionne uniformément pour `applyTwice (fun n => n + 1) 5 = 7` (sur les naturels) et `applyTwice String.length \"CoursIA\" = 7` (sur les chaînes), sans duplication de code.\n", - "\n", - "Le **point pédagogique crucial** : sans fonctions d'ordre supérieur, vous devriez écrire `applyTwiceNat`, `applyTwiceString`, `applyTwiceList`... une par type. Le polymorphisme de Lean rend cette duplication **inutile**. C'est la même mécanique qui portera Lean-12 (Sensitivity) : la formule de Huang est définie une seule fois, et le typeur instancie `a := ℝ` au site d'appel.\n", - "\n", - "Les fonctions d'ordre supérieur reviendront en Lean-3 (composition de preuves), Lean-4 (quantificateurs), et Lean-14 (composition d'opérations sur les `Finset`). Préparez-vous à les voir partout." + "### Exemple guide 2 : Fonctions d'ordre supérieur\nUne fonction `applyTwice` qui applique une fonction deux fois a une valeur.\n\n### Fonctions d'ordre supérieur, le pivot du polymorphisme\n\n`applyTwice : {a : Type} -> (a -> a) -> a -> a` est une **fonction d'ordre supérieur** : elle prend une fonction `f` en argument. La signature dit « pour tout type `a`, étant donné une fonction `a -> a` et une valeur `a`, retourner le résultat de `f (f x)` ». Cette signature fonctionne uniformément pour `applyTwice (fun n => n + 1) 5 = 7` (sur les naturels) et `applyTwice String.length \"CoursIA\" = 7` (sur les chaînes), sans duplication de code.\n\nLe **point pédagogique crucial** : sans fonctions d'ordre supérieur, vous devriez écrire `applyTwiceNat`, `applyTwiceString`, `applyTwiceList`... une par type. Le polymorphisme de Lean rend cette duplication **inutile**. C'est la même mécanique qui portera Lean-12 (Sensitivity) : la formule de Huang est définie une seule fois, et le typeur instancie `a := ℝ` au site d'appel.\n\nLes fonctions d'ordre supérieur reviendront en Lean-3 (composition de preuves), Lean-4 (quantificateurs), et Lean-14 (composition d'opérations sur les `Finset`). Préparez-vous à les voir partout." ] }, { @@ -5062,7 +5043,7 @@ "\n", "## 10. Exercices a completer (a vous de jouer)\n", "\n", - "Remplacez chaque `sorry` par votre implementation, puis decommentez la ligne `#eval` pour verifier le résultat attendu indique en commentaire.\n", + "Remplacez chaque `sorry` par votre implémentation, puis decommentez la ligne `#eval` pour vérifier le résultat attendu indique en commentaire.\n", "\n", "### Stratégie pour aborder les exercices\n", "\n", @@ -5072,7 +5053,7 @@ "\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 etudiant` — 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. **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", "\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." ] @@ -5228,19 +5209,19 @@ ], "source": [ "-- Exercice 1 : Parite\n", - "-- TODO etudiant : definir isEven qui retourne true si n est pair (indice : n % 2 == 0)\n", + "-- TODO étudiant : définir isEven qui retourne true si n est pair (indice : n % 2 == 0)\n", "def isEven (n : Nat) : Bool := sorry\n", "-- #eval isEven 4 -- doit retourner true\n", "-- #eval isEven 7 -- doit retourner false\n", "\n", - "-- Exercice 2 : Inversion d'arguments (ordre superieur)\n", - "-- TODO etudiant : definir myFlip qui inverse l'ordre des deux arguments d'une fonction binaire\n", + "-- Exercice 2 : Inversion d'arguments (ordre supérieur)\n", + "-- TODO étudiant : définir myFlip qui inverse l'ordre des deux arguments d'une fonction binaire\n", "-- Note : renomme en myFlip pour eviter collision avec Function.flip de Lean core\n", "def myFlip {a b c : Type} (f : a -> b -> c) : b -> a -> c := sorry\n", "-- #eval myFlip (fun a b : Nat => a - b) 3 10 -- doit retourner 7 (= 10 - 3)\n", "\n", "-- Exercice 3 : Echange des composantes d'une paire\n", - "-- TODO etudiant : definir mySwap qui echange les deux composantes d'une paire\n", + "-- TODO étudiant : définir mySwap qui echange les deux composantes d'une paire\n", "-- Note : renomme en mySwap pour eviter collision avec swap defini en section 3.2\n", "def mySwap {a b : Type} (p : a × b) : b × a := sorry\n", "-- #eval mySwap (1, \"x\") -- doit retourner (\"x\", 1)" @@ -5272,7 +5253,7 @@ "| **Hiérarchie d'univers** | `Type 0`, `Type 1`, ... pour eviter les paradoxes |\n", "| **Lambda expressions** | `fun x => corps` - fonctions anonymes |\n", "| **Curryfication** | Fonctions a un argument retournant des fonctions |\n", - "| **`let` bindings** | Definitions locales |\n", + "| **`let` bindings** | Définitions locales |\n", "| **Sections/Namespaces** | Organisation et portee du code |\n", "| **`inductive` / `structure`** | Declarer ses propres types sommes et records (`DayOfWeek`, `MyPoint`) |\n", "| **`deriving` (Repr, BEq, DecidableEq)** | Generation automatique d'instances standard |\n", @@ -5320,4 +5301,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file