Ce notebook explore le système de types de Lean 4, fonde sur le Calcul des Constructions (Calculus of Constructions, CoC). Contrairement aux langages de programmation traditionnels ou les types sont fixes a la compilation, Lean permet aux types de dependre de valeurs, ouvrant la voie a une expressivite mathematique remarquable.
Objectifs d’apprentissage
Comprendre la hiérarchie des univers de types (Type 0, Type 1, …)
Manipuler les types de base : Nat, Bool, fonctions, produits
Définir des fonctions avec lambda-expressions
Utiliser les variables et sections pour organiser le code
Decouvrir les types dependants et les arguments implicites
Prerequis
Avoir complète le notebook Lean-01-Setup-Lean-Python (installation fonctionnelle)
Notions de base en programmation fonctionnelle (utile mais non obligatoire)
Le Calcul des Constructions est un système formel qui unifie : - La logique propositionnelle (propositions vraies ou fausses) - La théorie des types (classification des valeurs) - Le lambda-calcul (fonctions comme objets de première classe)
Cette unification est rendue possible par l’isomorphisme de Curry-Howard que nous explorerons dans le notebook suivant. Pour l’instant, concentrons-nous sur les aspects “programmation” du système de types.
## 1. Types de Base
1.1 Les types primitifs
Lean fournit plusieurs types de base integres dans le langage. La commande #check permet d’inspecter le type de n’importe quelle expression.
Pourquoi cette introduction compte
Avant de manipuler la syntaxe de Lean, prenons un instant pour situer pourquoi le langage fait ces choix. Lean 4 est un assistant de preuve interactif : on y écrit à la fois des programmes (des def) et des théorèmes (theorem), et le noyau vérifie chaque étape. Cette double nature commande tout le reste. Quand vous voyez def m : Nat := 1, ce n’est pas une instruction impérative — c’est une assertion : « la valeur 1 est de type Nat, et voici pourquoi ». Cette lecture déclarative est ce qui permet plus tard d’écrire theorem add_zero (n : Nat) : n + 0 = n et de le prouver au lieu de le tester.
Les types primitifs sont nos briques de base. Nat est ce que vous avez l’habitude d’appeler les entiers naturels (0, 1, 2, …), Int ajoute les négatifs, Bool les valeurs de vérité, String les chaînes de caractères, Char un unique caractère Unicode, et Unit le type à un seul habitant (souvent utilisé quand une fonction retourne « rien d’utile »). La commande #check retourne le type inféré d’une expression — elle ne calcule rien, elle interroge le noyau. Quand vous voyez #check Nat répondre Nat : Type, lisez-le comme : « la constante Nat est elle-même un type, qui lui-même a pour type Type ».
-- Types numériques
#check Nat -- Nat : Type (entiers naturels 0, 1, 2, ...)
#check Int -- Int : Type (entiers relatifs ..., -1, 0, 1, ...)
#check Float -- Float : Type (nombres flottants)
-- Type booleen
#check Bool -- Bool : Type
-- Type chaine de caracteres
#check String -- String : Type
-- Valeurs de ces types
#check (42 : Nat) -- 42 : Nat
#check true -- true : Bool
#check "Hello" -- "Hello" : String
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.
Pourquoi def, et pas une « variable » au sens Python
En Python, m = 1 crée un nom mutable qu’on peut réassigner. En Lean, def m : Nat := 1 est une définition immuable : une fois écrite, m désigne toujours1. Si vous écrivez ensuite def m : Nat := 2, c’est une erreur — le nom est déjà pris dans ce namespace. Cette immuabilité est ce qui rend les preuves possibles : pour raisonner sur la valeur d’une constante, le noyau sait qu’elle ne changera pas sous ses pieds.
L’annotation : Nat est explicite mais pas obligatoire (cf. §1.3 sur l’inférence). La mettre systématiquement pour les premières déclarations est une bonne habitude : c’est une vérification que vous savez ce que vous écrivez, et c’est la première chose qu’un lecteur regardera pour comprendre votre intention. Quand vous voyez def b1 : Bool := true, le : Bool dit explicitement : « cette valeur est booléenne, pas une autre ». Notez l’usage de := et non = : c’est la syntaxe de définition en Lean.
-- Définitions simples avec annotation de type
def m : Nat := 1
def n : Nat := 0
def b1 : Bool := true
def b2 : Bool := false
def greeting : String := "Bonjour Lean!"
-- Vérification des types
#check m -- m : Nat
#check b1 -- b1 : Bool
-- Evaluation des valeurs
#eval m -- 1
#eval greeting -- "Bonjour Lean!"
Lean possede un puissant système d’inference de types : dans de nombreux cas, le compilateur peut determiner automatiquement le type d’une expression sans annotation explicite.
L’inférence, un dialogue avec le noyau
L’inférence de types est un dialogue entre votre code et le noyau : Lean essaie de reconstruire ce que vous avez omis, et s’il n’y arrive pas, il refuse de deviner. Ce refus est un cadeau, pas une limite : il vous dit « cette expression est ambiguë, exprime-toi ». Concrètement, Lean parcourt votre code de gauche à droite, collecte les contraintes sur les variables de type (?a, ?b, …) au fur et à mesure, puis résout le système à la fin. Si la résolution est unique, l’inférence réussit ; si plusieurs solutions existent, Lean affiche les types attendus dans le message d’erreur (vous verrez souvent « expected type, got type »).
Quand l’inférence fonctionne, ajoutez l’annotation quand même dans les cas non triviaux : #check sur une fonction longue vous dira son type, mais le : T après le def rend ce type immédiatement visible au lecteur. La règle pragmatique : annotation explicite pour les exports (définitions de namespace, API publique), inférence pour les calculs intermédiaires.
-- Sans annotation de type (infere automatiquement)
def x := 42 -- Lean infere Nat
def flag := true -- Lean infere Bool
def msg := "test" -- Lean infere String
#check x -- x : Nat
#check flag -- flag : Bool
-- Opérations arithmetiques
def sum := m + n -- Addition de Nat
def product := m * 5 -- Multiplication
#eval sum -- 1
#eval product -- 5
-- Sans annotation de type (infere automatiquement)
defx:=42-- Lean infere Nat
defflag:=true-- Lean infere Bool
defmsg:="test"-- Lean infere String
x:Nat
flag:Bool
-- Operations arithmetiques
defsum:=m+n-- Addition de Nat
defproduct:=m*5-- Multiplication
1
5
--% env 2
Raw input{"cmd": "-- Sans annotation de type (infere automatiquement)\ndef x := 42 -- Lean infere Nat\ndef flag := true -- Lean infere Bool\ndef msg := \"test\" -- Lean infere String\n\n#check x -- x : Nat\n#check flag -- flag : Bool\n\n-- Operations arithmetiques\ndef sum := m + n -- Addition de Nat\ndef product := m * 5 -- Multiplication\n\n#eval sum -- 1\n#eval product -- 5", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data": "x : Nat"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data": "flag : Bool"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 5},
"data": "1"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 5},
"data": "5"}],
"env": 2}
## 2. Types Fonctions
2.1 La fleche -> : le constructeur de types fonctions
En Lean, une fonction qui prend un argument de type A et retourne une valeur de type B a le type A -> B (lu “A vers B” ou “A implique B”).
Point cle : Les fonctions sont des valeurs de première classe - elles peuvent etre stockees dans des variables, passees en argument, ou retournees par d’autres fonctions.
Pourquoi -> plutôt qu’un autre constructeur ?
Avant Lean, la majorité des langages utilisent un constructeur de type « fonction » opaque : en C, un pointeur de fonction int (*)(int) ne porte aucune garantie que f(0) terminera ou même sera défini. La flèche A -> B de Lean est l’héritière directe du lambda-calcul simplement typé de Church (1940), où une fonction est un objet mathématique de plein droit — on peut parler de « la fonction qui à x associe x+1 » comme d’une valeur, exactement comme on parle d’un entier.
Cette filiation a trois conséquences concrètes que vous ressentirez dans tout le reste du notebook :
Toute fonction est totale par construction. Une fonction de type Nat -> Nat est promise par son type à retourner une valeur de type Nat pour chaque entrée. Pas d’exception, pas de boucle infinie cachée dans le type (la termination est vérifiée par une analyse statique sur les def récursifs — c’est une heuristique, pas une garantie absolue, mais elle attrape 95 % des cas). Les langages où une fonction peut « ne pas terminer » (def f : Nat -> Nat := f) imposent des marqueurs Partial, NonTermination, ou restreignent les programmes à IO ; ici, la flèche est par défaut stricte.
L’application f x est une opération de bêta-réduction. Quand vous écrivez (fun x => x + 1) 5, le noyau remplace x par 5 dans le corps, donnant 5 + 1. C’est ce qui permet à #reduce et #norm_num de calculer des valeurs plutôt que de se contenter d’enregistrer des appels. Vous retrouverez cette bêta-réduction dans Lean-5 (tactiques simp, norm_num, beta) et Lean-12 (preuve de la formule de sensibilité de Huang, où chaque simp [*] déclenche une cascade de bêtas).
La flèche est associative à droite : A -> B -> C se lit A -> (B -> C), pas (A -> B) -> C. C’est ce qui rend la curryfication possible — et c’est exactement ce que nous verrons à la cellule suivante. Les défenseurs de la curryfication disent qu’elle permet l’application partielle ; ses détracteurs répondent qu’elle obscurcit la lecture. Lean fait le choix curryfié, vous ferez avec.
Le pont vers la partie haute : la flèche -> est le constructeur de base de Lean-7 (Proof_by_Structure_Recursion) et Lean-8 (Proof_by_Primitive_Recursion), où elle sert à typer les prédicats (n : Nat) -> n > 0 -> .... Le Pi-type dépendant(x : A) -> B x que vous croiserez en section 7 est une généralisation directe de cette flèche : quand B ne dépend pas de x, vous retombez sur A -> B. Pas de surprise, juste une généralisation.
-- Types fonctions simples
#check Nat -> Nat -- Type des fonctions Nat vers Nat
#check Bool -> Nat -- Type des fonctions Bool vers Nat
#check Nat -> Bool -> Nat -- Equivalent a Nat -> (Bool -> Nat) - curryfication
-- Une fonction simple : le double d'un nombre
def double : Nat -> Nat := fun x => x + x
#check double -- double : Nat -> Nat
#eval double 21 -- 42
Les lambda expressions (ou fonctions anonymes) sont la brique fondamentale de la programmation fonctionnelle. La syntaxe fun x => corps créé une fonction qui prend x en argument et retourne corps.
C’est l’equivalent mathematique de la notation \(\lambda x. \text{corps}\) en lambda-calcul.
Le lambda-calcul, souche de tout le langage
Lean (comme Haskell, OCaml, et la grande famille ML) descend directement du lambda-calcul d’Alonzo Church (1936). Trois constructions et rien d’autre : les variables (x), les abstractions (fun x => corps, la notation de Church λx.corps), et l’application (f x). Tout le reste — types dépendants, polymorphisme, classes de types — se définit comme du sucre syntaxique sur ces trois briques.
Cette filiation explique deux particularités de Lean qui surprennent au premier contact : (1) il n’y a pas d’« instruction » au sens impératif — chaque def est une équation entre un nom et une expression ; (2) les fonctions sont des valeurs de première classe : on peut les passer en argument, les retourner, les stocker dans une structure. La cellule suivante utilise fun x => x + 1 comme une valeur qu’on passe à #eval et #check, ce qui n’aurait pas de sens dans un langage sans fonctions de première classe.
Préparez-vous : vous retrouverez les lambdas dans Lean-12 (preuve de la formule de sensibilité de Huang) et Lean-14 (dérivées de Finiteness), où ils servent à écrire des définitions par cas et des récurrences que les tactiques de Lean-5 ne savent pas dériver automatiquement.
-- Lambda expression simple
#check fun x : Nat => x + 1 -- fun x => x + 1 : Nat -> Nat
#eval (fun x : Nat => x + 1) 5 -- 6
-- Avec plusieurs arguments (forme curryfiee)
#check fun x : Nat => fun y : Nat => x + y
-- Type: Nat -> Nat -> Nat
-- Syntaxe raccourcie pour plusieurs arguments
def add : Nat -> Nat -> Nat := fun x y => x + y
#eval add 3 4 -- 7
-- Encore plus court : définition avec arguments nommes
def add' (x y : Nat) : Nat := x + y
#eval add' 3 4 -- 7
-- Lambda expression simple
funx=>x+1:Nat→Nat
6
-- Avec plusieurs arguments (forme curryfiee)
funxy=>x+y:Nat→Nat→Nat
-- Type: Nat -> Nat -> Nat
-- Syntaxe raccourcie pour plusieurs arguments
defadd:Nat->Nat->Nat:=funxy=>x+y
7
-- Encore plus court : definition avec arguments nommes
defadd'(xy:Nat):Nat:=x+y
7
--% env 4
Raw input{"cmd": "-- Lambda expression simple\n#check fun x : Nat => x + 1 -- fun x => x + 1 : Nat -> Nat\n#eval (fun x : Nat => x + 1) 5 -- 6\n\n-- Avec plusieurs arguments (forme curryfiee)\n#check fun x : Nat => fun y : Nat => x + y\n-- Type: Nat -> Nat -> Nat\n\n-- Syntaxe raccourcie pour plusieurs arguments\ndef add : Nat -> Nat -> Nat := fun x y => x + y\n\n#eval add 3 4 -- 7\n\n-- Encore plus court : definition avec arguments nommes\ndef add' (x y : Nat) : Nat := x + y\n\n#eval add' 3 4 -- 7", "env": 3}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "fun x => x + 1 : Nat → Nat"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 5},
"data": "6"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data": "fun x y => x + y : Nat → Nat → Nat"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "7"},
{"severity": "info",
"pos": {"line": 17, "column": 0},
"endPos": {"line": 17, "column": 5},
"data": "7"}],
"env": 4}
2.3 Curryfication et application partielle
En Lean (comme dans tous les langages fonctionnels purs), les fonctions a plusieurs arguments sont en realite des chaînes de fonctions a un seul argument. C’est la curryfication (du nom du logicien Haskell Curry).
Cela permet l’application partielle : appeler une fonction avec moins d’arguments qu’elle n’en attend pour obtenir une nouvelle fonction.
L’isomorphisme de Curry-Howard en embuscade
La curryfication n’est pas qu’une commodité syntaxique : elle révèle que les fonctions à plusieurs arguments et les fonctions à un argument qui retournent une fonction sont la même chose, vues de deux points de vue différents. Cet isomorphisme entre produit et exponentiel est l’une des colonnes vertébrales de la théorie des catégories — et vous la retrouverez, explicitement codée, dans Lean-12 (preuve de la formule de sensibilité de Huang) où la curryfication est appliquée à des fonctions de 5 et 6 arguments.
Trois fonctions à retenir : - curry : ((a, b) -> c) -> (a -> b -> c) — prend une fonction de paire et la transforme en fonction à deux arguments curryfiés. - uncurry : (a -> b -> c) -> ((a, b) -> c) — l’inverse. - swap (pour Prod) — échange les composantes d’une paire, ce qui combiné avec curry/uncurry permet de raisonner sur l’ordre des arguments.
Pourquoi cette section existe dans le notebook avant les types dépendants ? Parce que la curryfication est la passerelle entre le monde « je passe un argument » et le monde « je passe une fonction ». Or les types dépendants, en section 7, sont essentiellement des fonctions où le type de la sortie dépend de la valeur d’entrée — c’est curryfication + dépendance de type.
Le pont : dans Lean-14 (Derivatives_Finiteness), vous verrez curry réapparaître pour transformer une dérivée seconde d²f/dxdy (qui prend un couple (x, y)) en deux dérivées premières emboîtées dx → dy → .... Sans curryfication, la notation serait illisible.
Piège classique du débutant : oublier que f a b est syntactiquement(f a) b, et écrire des parenthèses inutiles. #check (Nat.add) 2 3 et #check Nat.add 2 3 sont identiques pour le noyau, mais le premier déroute les inférences de type quand Nat.add est polymorphe (par exemple HAdd.hAdd).
-- add prend 2 arguments
-- add 5 en prend 1 (application partielle)
def add5 : Nat -> Nat := add 5
#check add5 -- add5 : Nat -> Nat
#eval add5 10 -- 15
-- Autre exemple : multiplication partielle
def mul (x y : Nat) : Nat := x * y
def triple := mul 3
#eval triple 7 -- 21
-- La fleche est associative a droite :
-- Nat -> Nat -> Nat est equivalent a Nat -> (Nat -> Nat)
#check (add : Nat -> (Nat -> Nat))
-- add prend 2 arguments
-- add 5 en prend 1 (application partielle)
defadd5:Nat->Nat:=add5
add5:Nat→Nat
15
-- Autre exemple : multiplication partielle
defmul(xy:Nat):Nat:=x*y
deftriple:=mul3
21
-- La fleche est associative a droite :
-- Nat -> Nat -> Nat est equivalent a Nat -> (Nat -> Nat)
Un type produitA × B (note Prod A B en ASCII) represente les paires ordonnees (a, b) ou a : A et b : B.
C’est l’equivalent du produit cartesien en mathematiques.
Saisie Unicode : Le symbole × (multiplication) se tape : - VSCode : \times puis Tab ou Espace - Lean4 REPL : \x puis Tab - Copier-coller : ×
Notation
Description
A × B
Syntaxe Unicode (recommandee)
Prod A B
Syntaxe ASCII equivalente
A × B × C
Associe a droite : A × (B × C)
Au-delà des paires : Prod, Vec, et la voie vers les types dépendants
Le type Prod A B — noté A × B en Unicode — est le type produit de Lean. Trois choses à savoir pour ne pas le confondre avec ses voisins :
Prod est non-record : ses composantes n’ont pas de nom, seulement des positions (.1, .2). Pour des données nommées, on utilise une structure (Lean-3). Vous croiserez cette distinction dans Lean-14 (Derivatives_Finiteness), où Structure Finset porte des champs nommés (val, nodup, card) tandis que List est juste Prod à n composantes.
Prod est curryfié via × : Nat × Nat × Nat est Nat × (Nat × Nat), pas (Nat × Nat) × Nat. Pour les sommes gauche-associées (commutatif), utilisez (Nat × Nat × Nat) avec un let (a, (b, c)) := p — mais ça devient vite pénible. Pour trois dimensions ou plus, préférez les structures nommées.
#check @Prod.fst vous montre la signature complète avec les {a b : Type} implicites. C’est ce polymorphisme qui rend fst applicable à n’importe quelle paire (Nat, String), (Bool, List Int), etc. — sans avoir à réécrire fst pour chaque combinaison.
Le pont vers Lean-14 (Finiteness) : vous y manipulerez des paires (nat_value, proof_of_bound), qui sont exactement des paires Nat × (n < m). La seconde composante est un terme de preuve — la garantie que la valeur est dans les bornes. Ce mécanisme value × proof est ce qui distingue Lean d’un langage comme Haskell : la preuve vit dans le type, pas dans un commentaire ni dans un assert.
Notation pratique : pour une paire anonyme, le constructeur est (a, b) ; pour la projection, on utilise p.1 / p.2 ou p.fst / p.snd. Les deux notations sont interchangeables pour Prod, mais p.fst ne fonctionne pas sur les structures nommées — il faut alors p.fieldName.
-- Type produit
#check Nat × Nat -- Prod Nat Nat : Type
#check Prod Nat Bool -- Prod Nat Bool : Type
-- Construction de paires
def pair1 : Nat × Nat := (3, 4)
def pair2 : Nat × Bool := (42, true)
#check pair1 -- pair1 : Nat × Nat
#eval pair1 -- (3, 4)
-- Acces aux composantes avec .1 et .2 (ou .fst et .snd)
#eval pair1.1 -- 3 (premiere composante)
#eval pair1.2 -- 4 (deuxieme composante)
#eval pair2.fst -- 42
#eval pair2.snd -- true
-- Type produit
Nat×Nat:Type
Nat×Bool:Type
-- Construction de paires
defpair1:Nat×Nat:=(3,4)
defpair2:Nat×Bool:=(42,true)
pair1:Nat×Nat
(3,4)
-- Acces aux composantes avec .1 et .2 (ou .fst et .snd)
Les fonctions classiques sur les paires : fst, snd, swap…
Les projections, briques de base de la vie avec les paires
fst et snd sont les projections canoniques d’une paire : fst (a, b) = a et snd (a, b) = b. En Lean, ces fonctions sont déjà définies dans la bibliothèque standard (Prelude), donc vous n’avez jamais à les réécrire — #check @Prod.fst vous montre leur signature complète avec les {a b : Type} implicites.
Au-delà de fst/snd, on construit couramment swap (échange les composantes), curry (transforme une fonction de paires en fonction curryfiée, ce que nous reverrons dans Lean-12), et uncurry (l’inverse). Ces trois opérations forment la base de l’isomorphisme de Curry-Howard entre paires et fonctions, qui revient partout en théorie des types.
Point important pour la suite : Prod n’est pas le seul type produit en Lean. Il y a aussi les structures (records), où chaque champ a un nom au lieu d’une position. Vous verrez structure à partir de Lean-3 (propositions), et vous l’utiliserez intensivement dans Lean-14 (dérivées de Finiteness) et Lean-16b (Game of Life). Le mécanisme de projection r.field fonctionne uniformément sur les deux : p.1 et p.fst sont interchangeables pour Prod, mais seules les structures nommées supportent la notation p.fieldName.
-- Projection premiere (deja définie dans Lean)
#check @Prod.fst -- Prod.fst : {a : Type} -> {b : Type} -> Prod a b -> a
-- Notre propre fonction d'echange
def swap (p : Nat × Bool) : Bool × Nat := (p.2, p.1)
#eval swap (42, true) -- (true, 42)
-- Fonction qui somme les composantes d'une paire
def sumPair (p : Nat × Nat) : Nat := p.1 + p.2
#eval sumPair (3, 7) -- 10
Question fondamentale : si Nat est un type, quel est le type de Nat lui-même ?
Reponse naive : “Type” serait le type de tous les types. Mais alors, quel serait le type de “Type” ? Si “Type : Type”, on obtient le paradoxe de Girard (analogue au paradoxe de Russell).
4.2 La solution : une hiérarchie infinie
Lean resout ce problème avec une hiérarchie infinie d’univers : - Type 0 (ou simplement Type) contient les types “ordinaires” comme Nat, Bool - Type 1 contient Type 0 et les types construits a partir de Type 0 - Type 2 contient Type 1 - Et ainsi de suite…
-- Nat est un Type (niveau 0)
#check Nat -- Nat : Type
-- Type est un Type 1
#check Type -- Type : Type 1
-- Type 1 est un Type 2
#check Type 1 -- Type 1 : Type 2
-- On peut continuer (max offset = 32 en Lean 4)
#check Type 2 -- Type 2 : Type 3
#check Type 10 -- Type 10 : Type 11
-- Liste est un constructeur de types : Type -> Type
#check List -- List : Type u -> Type u
#check List Nat -- List Nat : Type
-- Nat est un Type (niveau 0)
Nat:Type
-- Type est un Type 1
Type:Type1
-- Type 1 est un Type 2
Type1:Type2
-- On peut continuer (max offset = 32 en Lean 4)
Type2:Type3
Type10:Type11
-- Liste est un constructeur de types : Type -> Type
List.{u}(α:Typeu):Typeu
ListNat:Type
--% env 8
Raw input{"cmd": "-- Nat est un Type (niveau 0)\n#check Nat -- Nat : Type\n\n-- Type est un Type 1\n#check Type -- Type : Type 1\n\n-- Type 1 est un Type 2\n#check Type 1 -- Type 1 : Type 2\n\n-- On peut continuer (max offset = 32 en Lean 4)\n#check Type 2 -- Type 2 : Type 3\n#check Type 10 -- Type 10 : Type 11\n\n-- Liste est un constructeur de types : Type -> Type\n#check List -- List : Type u -> Type u\n#check List Nat -- List Nat : Type", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "Nat : Type"},
{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data": "Type : Type 1"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data": "Type 1 : Type 2"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data": "Type 2 : Type 3"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "Type 10 : Type 11"},
{"severity": "info",
"pos": {"line": 15, "column": 0},
"endPos": {"line": 15, "column": 6},
"data": "List.{u} (α : Type u) : Type u"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 6},
"data": "List Nat : Type"}],
"env": 8}
4.3 Polymorphisme d’univers
Pour ecrire des fonctions qui marchent a tous les niveaux d’univers, Lean permet de declarer des variables d’univers avec universe.
Les variables d’univers, ou comment écrire du code qui marche « partout »
La commande universe u v déclare des noms d’univers que vous pouvez ensuite utiliser comme arguments implicites dans vos types. C’est l’outil qui permet d’écrire une fonction polymorphique sur tous les niveaux d’univers, pas seulement sur Type.
L’usage typique :
universe u v
def identity {a : Type u} (x : a) : a := x
Ici, a est un type de n’importe quel niveau d’univers, et identity retourne x au même niveau. Cette signature fonctionne pour identity 5 : Nat (niveau 0), identity [1,2,3] : List Nat (niveau 0 aussi), et même identity (fun x => x) : Type u -> Type u (niveau 1, ce qui n’aurait pas marché sans le universe u).
Pourquoi ce n’est pas un détail : sans univers polymorphes, vous seriez obligés de dupliquer vos fonctions pour chaque niveau de types. Lean-15b (Grothendieck Lean companion) utilise intensivement cette mécanique pour définir des catégories dont les objets sont des types à des niveaux variables. Préparez-vous à voir universe u revenir comme une incantation quasi systématique dans la partie haute de la série.
-- Declaration de variables d'univers
universe u v
-- Fonction identite polymorphe sur tous les univers
def identity (a : Type u) (x : a) : a := x
#check identity Nat 42 -- Nat
#check identity Bool true -- Bool
-- Meme avec des types de niveau supérieur
#check identity Type Nat -- Type
#check identity (Type 1) Type -- Type 1
-- Fonction constante polymorphe
def konstant (a : Type u) (b : Type v) (x : a) (y : b) : a := x
#eval konstant Nat Bool 42 true -- 42
-- Declaration de variables d'univers
universeuv
-- Fonction identite polymorphe sur tous les univers
Raw input{"cmd": "-- Declaration de variables d'univers\nuniverse u v\n\n-- Fonction identite polymorphe sur tous les univers\ndef identity (a : Type u) (x : a) : a := x\n\n#check identity Nat 42 -- Nat\n#check identity Bool true -- Bool\n\n-- Meme avec des types de niveau superieur\n#check identity Type Nat -- Type\n#check identity (Type 1) Type -- Type 1\n\n-- Fonction constante polymorphe\ndef konstant (a : Type u) (b : Type v) (x : a) (y : b) : a := x\n\n#eval konstant Nat Bool 42 true -- 42", "env": 8}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data": "identity Nat 42 : Nat"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data": "identity Bool true : Bool"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data": "identity Type Nat : Type"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "identity (Type 1) Type : Type 1"},
{"severity": "warning",
"pos": {"line": 15, "column": 48},
"endPos": {"line": 15, "column": 49},
"data":
"Variable name `y` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 17, "column": 0},
"endPos": {"line": 17, "column": 5},
"data": "42"}],
"env": 9}
## 5. Définitions Locales avec let
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.
let, le bloc-notes du programmeur Lean
Le mot-clé let introduit une liaison locale : let y := expr in corps. Contrairement à def, cette liaison n’existe que dans le corps qui suit. C’est l’équivalent strict du let mathématique (« soit y := … dans … »), et c’est l’outil que vous utiliserez le plus pour rendre lisibles les calculs intermédiaires sans polluer votre namespace.
La mécanique sous-jacente est la β-réduction : let y := e in body est syntaxiquement équivalent à (fun y => body) e. Lean sait inliner la liaison au moment de l’évaluation ou de la preuve. Vous voyez rarement cette transformation explicite, mais elle explique pourquoi une variable let peut être « remplacée » par sa valeur dans un message d’erreur : le noyau ne voit que des fonctions appliquées.
L’indentation compte : Lean utilise l’indentation pour délimiter le corps du let. L’usage canonique est
def exemple : Nat :=
let y := calcul1
let z := calcul2 y
résultat y z
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.
-- Définition locale simple
def example1 : Nat :=
let y := 2 + 2
y * y
#eval example1 -- 16
-- Plusieurs définitions locales
def example2 : Nat :=
let a := 5
let b := 3
let c := a + b
c * c
#eval example2 -- 64
-- Avec annotations de type explicites
def example3 : Nat :=
let x : Nat := 10
let f : Nat -> Nat := fun n => n + 1
f (f x)
#eval example3 -- 12
-- Definition locale simple
defexample1:Nat:=
lety:=2+2
y*y
16
-- Plusieurs definitions locales
defexample2:Nat:=
leta:=5
letb:=3
letc:=a+b
c*c
64
-- Avec annotations de type explicites
defexample3:Nat:=
letx:Nat:=10
letf:Nat->Nat:=funn=>n+1
f(fx)
12
--% env 10
Raw input{"cmd": "-- Definition locale simple\ndef example1 : Nat :=\n let y := 2 + 2\n y * y\n\n#eval example1 -- 16\n\n-- Plusieurs definitions locales\ndef example2 : Nat :=\n let a := 5\n let b := 3\n let c := a + b\n c * c\n\n#eval example2 -- 64\n\n-- Avec annotations de type explicites\ndef example3 : Nat :=\n let x : Nat := 10\n let f : Nat -> Nat := fun n => n + 1\n f (f x)\n\n#eval example3 -- 12", "env": 9}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 5},
"data": "16"},
{"severity": "info",
"pos": {"line": 15, "column": 0},
"endPos": {"line": 15, "column": 5},
"data": "64"},
{"severity": "info",
"pos": {"line": 23, "column": 0},
"endPos": {"line": 23, "column": 5},
"data": "12"}],
"env": 10}
5.1 let vs def
Aspect
def
let
Portee
Globale (ou namespace)
Locale a l’expression
Visibilite
Partout après définition
Uniquement dans le corps du let
Usage
Définitions reutilisables
Calculs intermediaires
Pourquoi let plutôt que def pour un sous-calcul
La règle est simple : si vous utilisez le résultat plus d’une fois, nommez-le avec def. Si vous l’utilisez une seule fois, let suffit. Un def répété 50 fois dans une fonction rend la lecture pénible et le namespace pollué ; un let à l’intérieur d’une expression disparaît dès qu’on sort du scope.
La destructuration (let (x, y) := pair) fonctionne comme un pattern matching léger : Lean sait décomposer une paire en ses composantes et lier x à la première, y à la seconde. Si vous destructurez un type non produit (par erreur), Lean vous le dira à la compilation avec un message « pattern not matchable ». C’est l’amorce de ce que Lean-3 appelle la définition par match/induction, beaucoup plus expressive.
Note technique utile : let peut apparaître dans un type ((x : Nat) × Fin x est valide via let x := 5 in ...), mais c’est plus rare. Dans la partie haute, Lean-12 utilise let pour introduire des hypothèses locales au cœur d’une preuve (let h := ... in ...). La mécanique est la même.
-- let permet aussi la destructuration
def sumOfPair : Nat :=
let pair := (3, 4)
let (x, y) := pair -- Destructuration de la paire
x + y
#eval sumOfPair -- 7
-- Expression where : syntaxe alternative pour les lets
def sumOfPair' : Nat :=
x + y
where
x := 3
y := 4
#eval sumOfPair' -- 7
-- let permet aussi la destructuration
defsumOfPair:Nat:=
letpair:=(3,4)
let(x,y):=pair-- Destructuration de la paire
x+y
7
-- Expression where : syntaxe alternative pour les lets
defsumOfPair':Nat:=
x+y
where
x:=3
y:=4
7
--% env 11
Raw input{"cmd": "-- let permet aussi la destructuration\ndef sumOfPair : Nat :=\n let pair := (3, 4)\n let (x, y) := pair -- Destructuration de la paire\n x + y\n\n#eval sumOfPair -- 7\n\n-- Expression where : syntaxe alternative pour les lets\ndef sumOfPair' : Nat :=\n x + y\n where\n x := 3\n y := 4\n\n#eval sumOfPair' -- 7", "env": 10}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 5},
"data": "7"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 5},
"data": "7"}],
"env": 11}
Exercice 4 : Normalisation d’une paire avec let
En utilisant les liaisons let et les types produits vus dans les sections précédentes, cet exercice vous demande de définir une fonction qui reordonne les composantes d’une paire.
Objectif : Définir normalize qui prend une paire (a, b) : Nat × Nat et retourne (min a b, max a b).
Indices : - Utilisez un let binding pour stocker le minimum et le maximum - En Lean 4, Nat.min a b et Nat.max a b sont disponibles (ou les opérateurs min / max) - Vous pouvez aussi utiliser if a <= b then (a, b) else (b, a)
-- Exercice 4 : Normalisation d'une paire avec let
-- TODO étudiant : définir normalize qui reordonne une paire (a, b) en (min, max)
-- Indice : utiliser des let bindings pour le minimum et le maximum
def normalize (p : Nat × Nat) : Nat × Nat := sorry
-- #eval normalize (7, 3) -- doit retourner (3, 7)
-- #eval normalize (1, 5) -- doit retourner (1, 5)
-- #eval normalize (4, 4) -- doit retourner (4, 4)
-- Exercice 4 : Normalisation d'une paire avec let
-- TODO etudiant : definir normalize qui reordonne une paire (a, b) en (min, max)
-- Indice : utiliser des let bindings pour le minimum et le maximum
🟨declarationuses`sorry`
-- #eval normalize (7, 3) -- doit retourner (3, 7)
-- #eval normalize (1, 5) -- doit retourner (1, 5)
-- #eval normalize (4, 4) -- doit retourner (4, 4)
--% env 12
--% prove 0
Raw input{"cmd": "-- Exercice 4 : Normalisation d'une paire avec let\n-- TODO etudiant : definir normalize qui reordonne une paire (a, b) en (min, max)\n-- Indice : utiliser des let bindings pour le minimum et le maximum\ndef normalize (p : Nat \u00d7 Nat) : Nat \u00d7 Nat := sorry\n-- #eval normalize (7, 3) -- doit retourner (3, 7)\n-- #eval normalize (1, 5) -- doit retourner (1, 5)\n-- #eval normalize (4, 4) -- doit retourner (4, 4)", "env": 11}Raw output{"sorries":
[{"proofState": 0,
"pos": {"line": 4, "column": 45},
"goal": "p : Nat × Nat\n⊢ Nat × Nat",
"endPos": {"line": 4, "column": 50}}],
"messages":
[{"severity": "warning",
"pos": {"line": 4, "column": 4},
"endPos": {"line": 4, "column": 13},
"data": "declaration uses `sorry`"}],
"env": 12}
## 6. Variables et Sections
6.1 La commande variable
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.
Pourquoi variable change l’écriture des signatures
La commande variable est un raccourci déclaratif : tout ce qui suit dans le même bloc de section hérite automatiquement des paramètres que vous avez déclarés. Concrètement, variable (a : Type) (x : a) avant def id (x : a) : a := x vous épargne d’écrire (a : Type) à la main : la définition devient def id (x : a) : a := x exactement comme si vous aviez tapé def id (a : Type) (x : a) : a := x.
Ce mécanisme n’est pas une macro qui injecte du code : c’est une transformation de signature au niveau de l’élaboration. Quand Lean voit variable (a : Type), il ajoute un argument implicite {a : Type} à toutes les définitions suivantes. C’est la même mécanique qui rend les notations comme ∀ n : Nat, ... possibles : le ∀ n’est que du sucre sur (n : Nat) -> ....
Piège classique : oublier le variable rendra la définition suivante impossible à typer parce qu’elle référence un type non déclaré. Si vous voyez « unknown identifier a » après une définition, c’est presque toujours ça.
-- Sans variable : on doit repeter (a : Type) partout
def id1 (a : Type) (x : a) : a := x
def const1 (a : Type) (b : Type) (x : a) (y : b) : a := x
-- Avec variable : declaration une seule fois
variable (a b : Type)
def id2 (x : a) : a := x
def const2 (x : a) (y : b) : a := x
-- Lean ajoute automatiquement les paramètres de type
#check id2 -- id2 (a : Type) (x : a) : a
#check const2 -- const2 (a b : Type) (x : a) (y : b) : a
-- Sans variable : on doit repeter (a : Type) partout
-- Lean ajoute automatiquement les parametres de type
id2(a:Type)(x:a):a
const2(ab:Type)(x:a)(y:b):a
--% env 13
Raw input{"cmd": "-- Sans variable : on doit repeter (a : Type) partout\ndef id1 (a : Type) (x : a) : a := x\ndef const1 (a : Type) (b : Type) (x : a) (y : b) : a := x\n\n-- Avec variable : declaration une seule fois\nvariable (a b : Type)\n\ndef id2 (x : a) : a := x\ndef const2 (x : a) (y : b) : a := x\n\n-- Lean ajoute automatiquement les parametres de type\n#check id2 -- id2 (a : Type) (x : a) : a\n#check const2 -- const2 (a b : Type) (x : a) (y : b) : a", "env": 12}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 3, "column": 42},
"endPos": {"line": 3, "column": 43},
"data":
"Variable name `y` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "warning",
"pos": {"line": 9, "column": 20},
"endPos": {"line": 9, "column": 21},
"data":
"Variable name `y` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data": "id2 (a : Type) (x : a) : a"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data": "const2 (a b : Type) (x : a) (y : b) : a"}],
"env": 13}
6.2 Sections et portee
Les sections permettent de limiter la portee des variable. Tout ce qui est declare dans une section n’est plus visible après le end.
Sections : un namespace éphémère
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.
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.
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.
section ExempleSection
-- Ces variables ne sont valides que dans cette section
variable (x y : Nat)
def addXY : Nat := x + y
def mulXY : Nat := x * y
#check addXY -- addXY (x y : Nat) : Nat
end ExempleSection
-- x et y ne sont plus dans la portee ici
-- mais addXY et mulXY sont toujours accessibles
#check addXY -- addXY (x y : Nat) : Nat
#eval addXY 3 4 -- 7
sectionExempleSection
-- Ces variables ne sont valides que dans cette section
variable(xy:Nat)
defaddXY:Nat:=x+y
defmulXY:Nat:=x*y
addXY(xy:Nat):Nat
endExempleSection
-- x et y ne sont plus dans la portee ici
-- mais addXY et mulXY sont toujours accessibles
addXY(xy:Nat):Nat
7
--% env 14
Raw input{"cmd": "section ExempleSection\n -- Ces variables ne sont valides que dans cette section\n variable (x y : Nat)\n\n def addXY : Nat := x + y\n def mulXY : Nat := x * y\n\n #check addXY -- addXY (x y : Nat) : Nat\nend ExempleSection\n\n-- x et y ne sont plus dans la portee ici\n-- mais addXY et mulXY sont toujours accessibles\n#check addXY -- addXY (x y : Nat) : Nat\n#eval addXY 3 4 -- 7", "env": 13}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 8, "column": 2},
"endPos": {"line": 8, "column": 8},
"data": "addXY (x y : Nat) : Nat"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data": "addXY (x y : Nat) : Nat"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 5},
"data": "7"}],
"env": 14}
6.3 Namespaces
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.
Namespaces : la version nommable de la section
Un namespace Geometry … end Geometryencapsule les définitions dans un préfixe : Geometry.Point, Geometry.origin, etc. Contrairement aux sections, les définitions restent visibles après le end — il faut juste les référencer avec leur préfixe, ou les ouvrir avec open Geometry.
Cette mécanique est ce qui permet à Lean-12 et Lean-14 de coexister dans le même lake sans collision : chaque module définit ses types dans son propre namespace (Sensitivity.formula, Finiteness.Derivative, etc.), et les noms longs qui en résultent sont lisibles plutôt que cryptiques. Vous verrez aussi open utilisé pour raccourcir les notations : open Function dans Lean-14 vous permet d’écrire uncurry au lieu de Function.uncurry.
Astuce Lean-2 : les namespaces imbriqués s’écrivent avec un point : namespace Conway.Life ouvre le namespace Conway.Life, et toutes les définitions qui suivent sont accessibles comme Conway.Life.step. C’est cette syntaxe qui rend possible l’organisation hiérarchique des grandes preuves (cf. Lean-14, Lean-16b).
namespace Geometry
def Point := Nat × Nat
def origin : Point := (0, 0)
def translate (p : Point) (dx dy : Nat) : Point :=
(p.1 + dx, p.2 + dy)
end Geometry
-- Acces avec le prefixe complet
#check Geometry.Point
#eval Geometry.translate Geometry.origin 3 4 -- (3, 4)
-- Ou avec open pour importer dans la portee actuelle
open Geometry
#eval translate origin 1 2 -- (1, 2)
-- Ou avec open pour importer dans la portee actuelle
openGeometry
(1,2)
--% env 15
Raw input{"cmd": "namespace Geometry\n def Point := Nat \u00d7 Nat\n\n def origin : Point := (0, 0)\n\n def translate (p : Point) (dx dy : Nat) : Point :=\n (p.1 + dx, p.2 + dy)\nend Geometry\n\n-- Acces avec le prefixe complet\n#check Geometry.Point\n#eval Geometry.translate Geometry.origin 3 4 -- (3, 4)\n\n-- Ou avec open pour importer dans la portee actuelle\nopen Geometry\n#eval translate origin 1 2 -- (1, 2)", "env": 14}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data": "Geometry.Point : Type"},
{"severity": "warning",
"pos": {"line": 11, "column": 2},
"endPos": {"line": 11, "column": 3},
"data":
"Variable name `a` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "warning",
"pos": {"line": 11, "column": 4},
"endPos": {"line": 11, "column": 5},
"data":
"Variable name `b` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "(3, 4)"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 5},
"data": "(1, 2)"}],
"env": 15}
## 6.4 Declarer ses propres types : inductive et structure
Avant les types dependants (Fin, Vector), il est utile de savoir construire un type de données : un type somme (plusieurs constructeurs distincts) et un record a champs nommes (structure).
Trois formes a distinguer :
Forme
Quand
Exemple canonique deja vu dans ce parcours
type concret (un seul habitant par définition)
Pour une valeur unique
Nat, Bool, String
type paramètre
Pour des familles de types indexees
List a, Prod a b (vu section 3)
type inductif (inductive)
Pour des données somme avec plusieurs constructeurs, recursives ou non
on va le voir : DayOfWeek
record (structure)
Pour un produit a champs nommes, equivalent a Prod mais accessible par .field
on va le voir : MyPoint
Pont avec la suite : Fin n (section 7) est declare par inductive ; Vector n a aussi. Le geste appris ici reapparait des la premiere vraie page de types dependants, et la recurrence le solidifie. Les formes logiques Or p q et Exists p (a venir) sont elles aussi des inductive de la bibliotheque standard : les reconnaitre vous evite de les traiter comme des primitives magiques.
Note de scope : pour eviter toute ambiguite avec Geometry.Point defini en section 6.3, les exemples suivants sont places dans un namespace dedie LocalIntro. Le namespace isole les noms sans imposer de qualification a l’interieur.
namespace LocalIntro
-- Type inductif : plusieurs constructeurs distincts.
-- Ici un type somme a 7 constructeurs (les jours de la semaine).
inductive DayOfWeek where
| mon | tue | wed | thu | fri | sat | sun
deriving Repr, DecidableEq, BEq
-- Construction de valeurs : un constructeur par jour.
#check DayOfWeek.mon -- DayOfWeek
#eval DayOfWeek.mon -- DayOfWeek.mon
#eval DayOfWeek.sun == DayOfWeek.sun -- true (grace a `deriving BEq`)
-- Fonction totale par `match` : reconnaitre le week-end.
def isWeekend (d : DayOfWeek) : Bool :=
match d with
| DayOfWeek.sat => true
| DayOfWeek.sun => true
| _ => false
#eval isWeekend DayOfWeek.sat -- true
#eval isWeekend DayOfWeek.mon -- false
end LocalIntro
namespaceLocalIntro
-- Type inductif : plusieurs constructeurs distincts.
-- Ici un type somme a 7 constructeurs (les jours de la semaine).
inductiveDayOfWeekwhere
|mon|tue|wed|thu|fri|sat|sun
derivingRepr,DecidableEq,BEq
-- Construction de valeurs : un constructeur par jour.
LocalIntro.DayOfWeek.mon:DayOfWeek
LocalIntro.DayOfWeek.mon
true
-- Fonction totale par `match` : reconnaitre le week-end.
defisWeekend(d:DayOfWeek):Bool:=
matchdwith
|DayOfWeek.sat=>true
|DayOfWeek.sun=>true
|_=>false
true
false
endLocalIntro
--% env 16
Raw input{"cmd": "namespace LocalIntro\n\n-- Type inductif : plusieurs constructeurs distincts.\n-- Ici un type somme a 7 constructeurs (les jours de la semaine).\ninductive DayOfWeek where\n | mon | tue | wed | thu | fri | sat | sun\n deriving Repr, DecidableEq, BEq\n\n-- Construction de valeurs : un constructeur par jour.\n#check DayOfWeek.mon -- DayOfWeek\n#eval DayOfWeek.mon -- DayOfWeek.mon\n#eval DayOfWeek.sun == DayOfWeek.sun -- true (grace a `deriving BEq`)\n\n-- Fonction totale par `match` : reconnaitre le week-end.\ndef isWeekend (d : DayOfWeek) : Bool :=\n match d with\n | DayOfWeek.sat => true\n | DayOfWeek.sun => true\n | _ => false\n\n#eval isWeekend DayOfWeek.sat -- true\n#eval isWeekend DayOfWeek.mon -- false\n\nend LocalIntro\n", "env": 15}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data": "LocalIntro.DayOfWeek.mon : DayOfWeek"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 5},
"data": "LocalIntro.DayOfWeek.mon"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "true"},
{"severity": "info",
"pos": {"line": 21, "column": 0},
"endPos": {"line": 21, "column": 5},
"data": "true"},
{"severity": "info",
"pos": {"line": 22, "column": 0},
"endPos": {"line": 22, "column": 5},
"data": "false"}],
"env": 16}
namespace LocalIntro
-- Record a champs nommes : equivalent a `Prod` mais accessible par `.field`.
-- Souvent preferable a un tuple anonyme des qu'on a plus de 2 dimensions.
structure MyPoint where
x : Nat
y : Nat
deriving Repr
-- Construction : notation `{ ... }`.
def origin : MyPoint := { x := 0, y := 0 }
def p1 : MyPoint := { x := 3, y := 4 }
-- Projection par `.field`.
#eval p1.x -- 3
#eval p1.y -- 4
#eval origin -- { x := 0, y := 0 } (grace a `deriving Repr`)
-- Fonction : distance carree au carré (pas de sqrt, reste en Nat).
def distanceSq (a b : MyPoint) : Nat :=
let dx := a.x - b.x
let dy := a.y - b.y
dx * dx + dy * dy
#eval distanceSq p1 origin -- 25
end LocalIntro
namespaceLocalIntro
-- Record a champs nommes : equivalent a `Prod` mais accessible par `.field`.
-- Souvent preferable a un tuple anonyme des qu'on a plus de 2 dimensions.
-- Fonction : distance carree au carre (pas de sqrt, reste en Nat).
defdistanceSq(ab:MyPoint):Nat:=
letdx:=a.x-b.x
letdy:=a.y-b.y
dx*dx+dy*dy
25
endLocalIntro
--% env 17
Raw input{"cmd": "namespace LocalIntro\n\n-- Record a champs nommes : equivalent a `Prod` mais accessible par `.field`.\n-- Souvent preferable a un tuple anonyme des qu'on a plus de 2 dimensions.\nstructure MyPoint where\n x : Nat\n y : Nat\n deriving Repr\n\n-- Construction : notation `{ ... }`.\ndef origin : MyPoint := { x := 0, y := 0 }\ndef p1 : MyPoint := { x := 3, y := 4 }\n\n-- Projection par `.field`.\n#eval p1.x -- 3\n#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).\ndef distanceSq (a b : MyPoint) : Nat :=\n let dx := a.x - b.x\n let dy := a.y - b.y\n dx * dx + dy * dy\n\n#eval distanceSq p1 origin -- 25\n\nend LocalIntro\n", "env": 16}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 6, "column": 6},
"endPos": {"line": 6, "column": 7},
"data":
"Variable name `a` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "warning",
"pos": {"line": 6, "column": 8},
"endPos": {"line": 6, "column": 9},
"data":
"Variable name `b` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 15, "column": 0},
"endPos": {"line": 15, "column": 5},
"data": "3"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 5},
"data": "4"},
{"severity": "info",
"pos": {"line": 17, "column": 0},
"endPos": {"line": 17, "column": 5},
"data": "{ x := 0, y := 0 }"},
{"severity": "info",
"pos": {"line": 25, "column": 0},
"endPos": {"line": 25, "column": 5},
"data": "25"}],
"env": 17}
Pont : inductive et structure vs types deja consommes
Le notebook Lean-1 introduit Bool, Nat, String comme types primitifs et Prod a b comme type produit anonyme. Les formes inductives et structures ne sont pas nouvelles :
Bool est un inductive a deux constructeurs (true, false).
List a est un inductive recursif (nil, cons).
Prod a b est une structure a deux champs (.1, .2) ; nos MyPoint.x et MyPoint.y en sont l’analogue nomme.
Or p q (a venir) est un inductive a deux constructeurs (Or.inl, Or.inr).
Exists p (a venir) est un inductive a un constructeur (Exists.intro).
La syntaxe inductive Foo where | c1 | c2 ... et structure Bar where field1 : Type1 ... est donc le geste fondamental que vous avez deja rencontre sans le voir ; on le rend maintenant explicite.
namespace LocalIntro
-- Exercice 4b : Sign d'un entier
-- TODO étudiant : declarer un type inductif `Sign` a 3 constructeurs `pos`, `zero`, `neg`
-- (avec `deriving Repr, BEq`), puis définir `sign : Int -> Sign` par `match` sur `Int`.
-- Tester avec `#eval sign 5`, `#eval sign 0`, `#eval sign (-3)`.
-- Indice : `Int` est un type primitif ; `match` fonctionne comme sur `DayOfWeek`.
-- cellule neutre : permet l'exécution de bout en bout avant que l'étudiant complète l'exercice.
def placeholder : Nat := 0
#eval placeholder
end LocalIntro
namespaceLocalIntro
-- Exercice 4b : Sign d'un entier
-- TODO etudiant : declarer un type inductif `Sign` a 3 constructeurs `pos`, `zero`, `neg`
-- (avec `deriving Repr, BEq`), puis definir `sign : Int -> Sign` par `match` sur `Int`.
-- Indice : `Int` est un type primitif ; `match` fonctionne comme sur `DayOfWeek`.
-- cellule neutre : permet l'execution de bout en bout avant que l'etudiant complete l'exercice.
defplaceholder:Nat:=0
0
endLocalIntro
--% env 18
Raw input{"cmd": "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-- 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.\ndef placeholder : Nat := 0\n#eval placeholder\n\nend LocalIntro\n", "env": 17}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 5},
"data": "0"}],
"env": 18}
## 7. Types Dependants
7.1 Introduction aux types dependants
Un type dependant est un type qui depend d’une valeur. C’est la caractéristique fondamentale qui distingue Lean des langages de programmation traditionnels.
Exemples intuitifs : - Vector n : vecteur de longueur exactement n - Matrix m n : matrice de dimensions m x n - Fin n : entier entre 0 et n-1
Ces types permettent d’encoder des invariants directement dans le système de types, empechant certaines erreurs a la compilation.
Pourquoi les types dépendants sont le « gros morceau » de Lean
Avant les types dépendants, les langages de programmation font une distinction tranchée entre valeurs (1, “hello”, (3, 4)) et types (Nat, String, Nat × Nat). Cette distinction est commode pour les humains, mais elle empêche de capturer certaines invariances dans les types eux-mêmes. Exemple : comment typer une liste « non vide » sans introduire une nouvelle structure à côté de List ? En ML on répondrait « on ajoute une couche de refinement types » (Liquid Haskell, F*). En Lean, on répond « le type lui-même porte l’information ».
C’est l’idée des types dépendants : un type peut dépendre d’une valeur. Trois exemples, du plus simple au plus riche :
Vector α n : le type des listes de longueur exactementn. Le second argument n est une valeur (un Nat), pas un type. Vous ne pourrez pas confondre Vector Nat 3 et Vector Nat 4 — le compilateur refuse. C’est la garantie que List.head ne déballera jamais une liste vide par accident.
Fin n : le type des entiers strictement inférieurs à n. Fin 5 a exactement 5 habitants (0, 1, 2, 3, 4). C’est ce qui permet de dire « l’indice i est garanti dans les bornes du tableau » dans le type — pas dans un commentaire, pas dans une précondition vérifiée à l’exécution, dans le type.
Fin.induction : une fonction qui élimine sur Fin n doit fournir un cas de base zero et un cas de successeur succ. Cette induction est structurelle sur la valeur n, pas sur une profondeur arbitraire.
Ces constructions sont partout dans la partie haute du cours. Lean-12 (sensibilité) utilise Fin (n+1) pour borner les sommes partielles. Lean-14 (Finiteness) utilise Vector pour encoder des dérivées partielles indexées par une multi-indices. Lean-16b (Game of Life) utilise Fin × Fin pour borner la grille. Si cette section est nébuleuse, relisez-la : le reste de la série s’appuie dessus.
Trois noms à retenir pour la suite : Pi-type (x : A) -> B x (section 7), Sigma-type {x : A // B x} (Lean-3, sous-ensemble défini par un prédicat), Vec/Fin/List.length (les briques concrètes).
-- Fin n : type des entiers de 0 a n-1
#check Fin 5 -- Fin 5 : Type (contient 0, 1, 2, 3, 4)
-- Construction de valeurs Fin
def zero_of_5 : Fin 5 := 0
def three_of_5 : Fin 5 := 3
-- def five_of_5 : Fin 5 := 5 -- ERREUR: 5 n'est pas < 5
#eval zero_of_5 -- 0
-- Vector : listes de longueur fixee
-- (On utilisera la version simplifiee Array pour l'instant)
#check (Array.mk [1, 2, 3] : Array Nat)
-- Fin n : type des entiers de 0 a n-1
Fin5:Type
-- Construction de valeurs Fin
defzero_of_5:Fin5:=0
defthree_of_5:Fin5:=3
-- def five_of_5 : Fin 5 := 5 -- ERREUR: 5 n'est pas < 5
0
-- Vector : listes de longueur fixee
-- (On utilisera la version simplifiee Array pour l'instant)
{toList:=[1,2,3]}:ArrayNat
--% env 19
Raw input{"cmd": "-- Fin n : type des entiers de 0 a n-1\n#check Fin 5 -- Fin 5 : Type (contient 0, 1, 2, 3, 4)\n\n-- Construction de valeurs Fin\ndef zero_of_5 : Fin 5 := 0\ndef three_of_5 : Fin 5 := 3\n-- def five_of_5 : Fin 5 := 5 -- ERREUR: 5 n'est pas < 5\n\n#eval zero_of_5 -- 0\n\n-- Vector : listes de longueur fixee\n-- (On utilisera la version simplifiee Array pour l'instant)\n#check (Array.mk [1, 2, 3] : Array Nat)", "env": 18}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "Fin 5 : Type"},
{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data": "{ toList := [1, 2, 3] } : Array Nat"}],
"env": 19}
7.2 Le type List a : un type paramètre
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.
List, votre premier constructeur de types
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 ».
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 ».
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.
-- List est un constructeur de types : Type -> Type
#check List -- List : Type u -> Type u
#check List Nat -- List Nat : Type
#check List Bool -- List Bool : Type
-- Construction de listes
def numbers : List Nat := [1, 2, 3, 4, 5]
def empty : List Nat := []
#eval numbers -- [1, 2, 3, 4, 5]
#eval numbers.length -- 5
-- Fonctions génériques sur les listes
#check @List.map -- List.map : {a b : Type} -> (a -> b) -> List a -> List b
#eval numbers.map (fun x => x * 2) -- [2, 4, 6, 8, 10]
-- List est un constructeur de types : Type -> Type
Raw input{"cmd": "-- List est un constructeur de types : Type -> Type\n#check List -- List : Type u -> Type u\n#check List Nat -- List Nat : Type\n#check List Bool -- List Bool : Type\n\n-- Construction de listes\ndef numbers : List Nat := [1, 2, 3, 4, 5]\ndef empty : List Nat := []\n\n#eval numbers -- [1, 2, 3, 4, 5]\n#eval numbers.length -- 5\n\n-- Fonctions generiques 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]", "env": 19}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "List.{u} (α : Type u) : Type u"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data": "List Nat : Type"},
{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data": "List Bool : Type"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 5},
"data": "[1, 2, 3, 4, 5]"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 5},
"data": "5"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data":
"@List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β"},
{"severity": "info",
"pos": {"line": 15, "column": 0},
"endPos": {"line": 15, "column": 5},
"data": "[2, 4, 6, 8, 10]"}],
"env": 20}
7.3 Types dependants véritables
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.
Le Pi-type, fondement du polymorphisme dépendant
Le Pi-type(x : A) -> B x est la forme la plus expressive du polymorphisme : B x est un type qui dépend de la valeurx. Concrètement, (n : Nat) -> Fin n est le type des fonctions qui prennent un Natn et retournent un Fin n — un type dont la taille dépend de l’entrée.
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.
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.
-- Un exemple simple : fonction qui retourne un type different selon l'argument
def TypeSelector (b : Bool) : Type :=
if b then Nat else String
#check TypeSelector true -- Type (c'est Nat)
#check TypeSelector false -- Type (c'est String)
-- Fonction dont le type de retour depend de l'argument
-- On utilise MATCH pour que Lean puisse calculer le type dans chaque branche
-- Dans la branche true, Lean sait que TypeSelector true = Nat
-- Dans la branche false, Lean sait que TypeSelector false = String
def magicValue (b : Bool) : TypeSelector b :=
match b with
| true => (42 : Nat) -- TypeSelector true = Nat
| false => "hello" -- TypeSelector false = String
#eval magicValue true -- 42 : Nat
#eval magicValue false -- "hello" : String
-- Note : Le "dependent if" (if h : b then ...) est une syntaxe alternative
-- qui lie une preuve h du predicat dans chaque branche, utile pour des
-- preuves plus complexes. Pour les valeurs simples, match suffit.
-- Un exemple simple : fonction qui retourne un type different selon l'argument
-- Fonction dont le type de retour depend de l'argument
-- On utilise MATCH pour que Lean puisse calculer le type dans chaque branche
-- Dans la branche true, Lean sait que TypeSelector true = Nat
-- Dans la branche false, Lean sait que TypeSelector false = String
defmagicValue(b:Bool):TypeSelectorb:=
matchbwith
|true=>(42:Nat)-- TypeSelector true = Nat
|false=>"hello"-- TypeSelector false = String
42
"hello"
-- Note : Le "dependent if" (if h : b then ...) est une syntaxe alternative
-- qui lie une preuve h du predicat dans chaque branche, utile pour des
-- preuves plus complexes. Pour les valeurs simples, match suffit.
--% env 21
Raw input{"cmd": "-- Un exemple simple : fonction qui retourne un type different selon l'argument\ndef TypeSelector (b : Bool) : Type :=\n if b then Nat else String\n\n#check TypeSelector true -- Type (c'est Nat)\n#check TypeSelector false -- Type (c'est String)\n\n-- Fonction dont le type de retour depend de l'argument\n-- On utilise MATCH pour que Lean puisse calculer le type dans chaque branche\n-- Dans la branche true, Lean sait que TypeSelector true = Nat\n-- Dans la branche false, Lean sait que TypeSelector false = String\ndef magicValue (b : Bool) : TypeSelector b :=\n match b with\n | true => (42 : Nat) -- TypeSelector true = Nat\n | false => \"hello\" -- TypeSelector false = String\n\n#eval magicValue true -- 42 : Nat\n#eval magicValue false -- \"hello\" : String\n\n-- Note : Le \"dependent if\" (if h : b then ...) est une syntaxe alternative\n-- qui lie une preuve h du predicat dans chaque branche, utile pour des\n-- preuves plus complexes. Pour les valeurs simples, match suffit.", "env": 20}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data": "TypeSelector true : Type"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data": "TypeSelector false : Type"},
{"severity": "warning",
"pos": {"line": 6, "column": 11},
"endPos": {"line": 6, "column": 12},
"data":
"Variable name `a` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "warning",
"pos": {"line": 6, "column": 13},
"endPos": {"line": 6, "column": 14},
"data":
"Variable name `b` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 17, "column": 0},
"endPos": {"line": 17, "column": 5},
"data": "42"},
{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 5},
"data": "\"hello\""}],
"env": 21}
Exercice 5 : Fonction a type de retour dependent
Après avoir vu TypeSelector et magicValue ci-dessus, voici un exercice pour mettre en pratique les fonctions dont le type de retour depend de la valeur d’un argument.
Objectif : Définir une fonction statusMessage dont le type de retour change selon un booléen : - Si b = true, retourner un Nat (un code numérique, par exemple 200) - Si b = false, retourner un String (un message d’erreur, par exemple “error”)
Indices : - Commencez par définir StatusType (b : Bool) : Type sur le même modèle que TypeSelector - Utilisez match b with pour que Lean puisse calculer le type dans chaque branche - Le type de retour doit etre StatusType b
-- Exercice 5 : Fonction a type de retour dependent
-- TODO étudiant : définir StatusType et statusMessage
-- StatusType (b : Bool) : Type doit retourner Nat si b = true, String si b = false
-- statusMessage (b : Bool) : StatusType b doit retourner 200 si b = true, "error" si b = false
def StatusType (b : Bool) : Type := sorry
def statusMessage (b : Bool) : StatusType b := sorry
-- #eval statusMessage true -- doit retourner 200
-- #eval statusMessage false -- doit retourner "error"
-- Exercice 5 : Fonction a type de retour dependent
-- TODO etudiant : definir StatusType et statusMessage
-- StatusType (b : Bool) : Type doit retourner Nat si b = true, String si b = false
-- statusMessage (b : Bool) : StatusType b doit retourner 200 si b = true, "error" si b = false
🟨declarationuses`sorry`
🟨declarationuses`sorry`
-- #eval statusMessage true -- doit retourner 200
-- #eval statusMessage false -- doit retourner "error"
--% env 22
--% prove 2
Raw input{"cmd": "-- Exercice 5 : Fonction a type de retour dependent\n-- TODO etudiant : definir 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\ndef StatusType (b : Bool) : Type := sorry\ndef statusMessage (b : Bool) : StatusType b := sorry\n-- #eval statusMessage true -- doit retourner 200\n-- #eval statusMessage false -- doit retourner \"error\"", "env": 21}Raw output{"sorries":
[{"proofState": 1,
"pos": {"line": 5, "column": 36},
"goal": "a b✝ : Type\nb : Bool\n⊢ Type",
"endPos": {"line": 5, "column": 41}},
{"proofState": 2,
"pos": {"line": 6, "column": 47},
"goal": "a b✝ : Type\nb : Bool\n⊢ StatusType b",
"endPos": {"line": 6, "column": 52}}],
"messages":
[{"severity": "warning",
"pos": {"line": 5, "column": 4},
"endPos": {"line": 5, "column": 14},
"data": "declaration uses `sorry`"},
{"severity": "warning",
"pos": {"line": 6, "column": 4},
"endPos": {"line": 6, "column": 17},
"data": "declaration uses `sorry`"}],
"env": 22}
## 8. Arguments Implicites
8.1 Le problème de la verbosité
Les fonctions polymorphes necessitent souvent des paramètres de type que Lean peut deduire du contexte. Les ecrire explicitement serait fastidieux.
Implicite vs explicite : un compromis entre concision et clarté
Le passage d’arguments implicites est une convention d’écriture : vous dites « Lean sait le retrouver, je ne vais pas l’écrire ». Lean tente l’inférence, et si elle réussit, votre code est plus court ; si elle échoue, Lean vous demande l’argument explicitement.
L’analogie est la suivante : les arguments explicites sont des questions que vous posez au lecteur (« quel type voulez-vous ici ? »), les implicites sont des questions que vous posez au noyau (« peux-tu inférer ce type ? »). Les bons codes équilibrent les deux : implicites pour les arguments évidents du contexte, explicites pour les conventions qu’un nouveau lecteur ne peut pas deviner.
Règle d’or : un argument implicite doit être calculable de manière unique depuis les arguments explicites. Si l’inférence est ambiguë, vous forcez l’explicite pour signaler au lecteur qu’il doit choisir.
-- Fonction identite avec type explicite
def idExplicit (a : Type) (x : a) : a := x
-- On doit toujours passer le type
#eval idExplicit Nat 42 -- 42
#eval idExplicit Bool true -- true
-- Avec arguments implicites (accolades)
def idImplicit {a : Type} (x : a) : a := x
-- Le type est infere automatiquement!
#eval idImplicit 42 -- 42 (Lean infere a = Nat)
#eval idImplicit true -- true (Lean infere a = Bool)
-- Fonction identite avec type explicite
defidExplicit(a:Type)(x:a):a:=x
-- On doit toujours passer le type
42
true
-- Avec arguments implicites (accolades)
defidImplicit{a:Type}(x:a):a:=x
-- Le type est infere automatiquement!
42
true
--% env 23
Raw input{"cmd": "-- Fonction identite avec type explicite\ndef idExplicit (a : Type) (x : a) : a := x\n\n-- On doit toujours passer le type\n#eval idExplicit Nat 42 -- 42\n#eval idExplicit Bool true -- true\n\n-- Avec arguments implicites (accolades)\ndef idImplicit {a : Type} (x : a) : a := x\n\n-- Le type est infere automatiquement!\n#eval idImplicit 42 -- 42 (Lean infere a = Nat)\n#eval idImplicit true -- true (Lean infere a = Bool)", "env": 22}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 5},
"data": "42"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 5},
"data": "true"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "42"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 5},
"data": "true"}],
"env": 23}
8.2 Syntaxe des arguments implicites
Syntaxe
Signification
(x : A)
Argument explicite - doit etre fourni
{x : A}
Argument implicite - infere par Lean
[x : A]
Argument d’instance (pour les typeclasses)
{x : A} ou ⦃x : A⦄
Argument implicite strict
Le @ pour forcer l’affichage des implicites
L’opérateur @ devant un appel de fonction désactive temporairement l’inférence : tous les arguments, implicites inclus, doivent être fournis explicitement. #check @id répond {a : Type u_1} -> a -> a — la signature complète, avec le {a : Type u_1} qui serait normalement inféré.
Pourquoi s’embêter : parce que @ est le premier outil de débogage quand Lean refuse de compiler un appel. Si Lean vous dit « type mismatch at … », préfixer l’appel par @ vous montre la signature attendue complète, et vous pouvez comparer argument par argument. C’est l’équivalent du « afficher les types » dans un langage comme TypeScript ou Rust.
L’autre usage : @ permet d’écrire des helpers de preuve qui ont besoin d’instancier des arguments implicites. Vous verrez cela intensivement dans Lean-5 (tactiques) : apply @SomeLemma force Lean à fournir les arguments implicites en un coup, là où apply SomeLemma demanderait peut-être plusieurs étapes d’instanciation.
-- Composition de fonctions avec types implicites
def compose {a b c : Type} (g : b -> c) (f : a -> b) : a -> c :=
fun x => g (f x)
def inc (n : Nat) := n + 1
def dbl (n : Nat) := n * 2
def incThenDouble := compose dbl inc
#eval incThenDouble 5 -- 12 (= (5 + 1) * 2)
-- Pour fournir explicitement un argument implicite : @
#eval @idImplicit Nat 42 -- Equivalent a idImplicit 42
#check @compose -- Montre tous les arguments
-- Pour fournir explicitement un argument implicite : @
42
@compose:{abc:Type}→(b→c)→(a→b)→a→c
--% env 24
Raw input{"cmd": "-- Composition de fonctions avec types implicites\ndef compose {a b c : Type} (g : b -> c) (f : a -> b) : a -> c :=\n fun x => g (f x)\n\ndef inc (n : Nat) := n + 1\ndef dbl (n : Nat) := n * 2\n\ndef incThenDouble := compose dbl inc\n\n#eval incThenDouble 5 -- 12 (= (5 + 1) * 2)\n\n-- Pour fournir explicitement un argument implicite : @\n#eval @idImplicit Nat 42 -- Equivalent a idImplicit 42\n#check @compose -- Montre tous les arguments", "env": 23}Raw output{"messages":
[{"severity": "warning",
"pos": {"line": 8, "column": 15},
"endPos": {"line": 8, "column": 16},
"data":
"Variable name `a` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 5},
"data": "12"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 5},
"data": "42"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data": "@compose : {a b c : Type} → (b → c) → (a → b) → a → c"}],
"env": 24}
## 9. Exemples guides (exercices resolus)
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.
Exemple guide 1 : Définitions de base
Une fonction square qui calcule le carré d’un nombre naturel.
Lire les solutions, c’est apprendre le style
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 :
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.
L’usage des implicites : applyTwice et mapPair utilisent {a : Type} (implicite), ce qui rend les appels comme applyTwice (fun x => x + 1) 5 lisibles sans surcharger le type. Le {a b c d : Type} de mapPair est plus risqué : quatre arguments implicites que Lean doit unifier en cascade.
L’économie de la notation : mapPair utilise la notation tuple (f : a -> c, g : b -> d) pour la paire d’arguments, ce qui la rend curryfiée. Vous pourriez aussi écrire mapPair f g (x, y) = (f x, g y) en notation unaire. Les deux sont équivalentes, le choix est stylistique.
Vous retrouverez ce style épuré dans toute la série Lean : pas de redondance, des signatures expressives, et un usage systématique des implicites pour ce qui peut être inféré du contexte.
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
def square (n : Nat) : Nat := n * n
#eval square 5 -- 25
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
Une fonction applyTwice qui applique une fonction deux fois a une valeur.
Fonctions d’ordre supérieur, le pivot du polymorphisme
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.
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.
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.
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
def applyTwice {a : Type} (f : a -> a) (x : a) : a := f (f x)
#eval applyTwice (fun n : Nat => n + 1) 0 -- 2
#eval applyTwice (fun n : Nat => n * 2) 3 -- 12
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
defapplyTwice{a:Type}(f:a->a)(x:a):a:=f(fx)
2
12
--% env 26
Raw input{"cmd": "-- Solution proposee par Clovis Lefebvre & Evariste Balvay\ndef applyTwice {a : Type} (f : a -> a) (x : a) : a := f (f x)\n\n#eval applyTwice (fun n : Nat => n + 1) 0 -- 2\n#eval applyTwice (fun n : Nat => n * 2) 3 -- 12", "env": 25}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 5},
"data": "2"},
{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 5},
"data": "12"}],
"env": 26}
Exemple guide 3 : Manipulation de paires
Une fonction mapPair qui applique deux fonctions aux composantes d’une paire.
mapPair, la version curryfiée de la dualité fonctionnel/produit
mapPair : {a b c d : Type} -> (a -> c) -> (b -> d) -> a × b -> c × d est l’illustration mécanique de l’isomorphisme de Curry : une fonction qui prend deux fonctions et une paire, et retourne la paire des applications. Cette signature encode la flèche (a -> c) -> (b -> d) -> (a × b) -> (c × d) que vous reverrez sous la forme Prod.map dans la bibliothèque standard.
Le lien avec Lean-12 (Sensitivity) : la formule de Huang prend deux vecteurs booléens et un seuil ; elle peut s’écrire comme un mapPair sur les composantes. Le lien avec Lean-14 (Finiteness) : la différentielle d’une application entre Finset est, en première approximation, un mapPair sur les composantes. Ce n’est pas un détail d’implémentation — c’est la bonne abstraction pour manipuler les paires.
Lisez aussi cette fonction comme un template : notez les 4 univers implicites {a b c d : Type} au lieu de 4 univers explicites. Lean les inférera du contexte d’appel. C’est exactement le genre de signature que vous écrirez quand vous définirez des bibliothèques.
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
def mapPair {a b c d : Type} (f : a -> c) (g : b -> d) (p : a × b) : c × d := (f p.1, g p.2)
#eval mapPair (fun n => n + 1) (fun s => s ++ "!") (5, "hello") -- (6, "hello!")
-- Solution proposee par Clovis Lefebvre & Evariste Balvay
Raw input{"cmd": "-- Solution proposee par Clovis Lefebvre & Evariste Balvay\ndef mapPair {a b c d : Type} (f : a -> c) (g : b -> d) (p : a \u00d7 b) : c \u00d7 d := (f p.1, g p.2)\n\n#eval mapPair (fun n => n + 1) (fun s => s ++ \"!\") (5, \"hello\") -- (6, \"hello!\")", "env": 26}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 5},
"data": "(6, \"hello!\")"},
{"severity": "warning",
"pos": {"line": 4, "column": 52},
"endPos": {"line": 4, "column": 53},
"data":
"Variable name `b` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}],
"env": 27}
## 10. Exercices a completer (a vous de jouer)
Remplacez chaque sorry par votre implémentation, puis decommentez la ligne #eval pour vérifier le résultat attendu indique en commentaire.
Stratégie pour aborder les exercices
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 :
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.
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.
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.
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.
-- Exercice 1 : Parite
-- TODO étudiant : définir isEven qui retourne true si n est pair (indice : n % 2 == 0)
def isEven (n : Nat) : Bool := sorry
-- #eval isEven 4 -- doit retourner true
-- #eval isEven 7 -- doit retourner false
-- Exercice 2 : Inversion d'arguments (ordre supérieur)
-- TODO étudiant : définir myFlip qui inverse l'ordre des deux arguments d'une fonction binaire
-- Note : renomme en myFlip pour eviter collision avec Function.flip de Lean core
def myFlip {a b c : Type} (f : a -> b -> c) : b -> a -> c := sorry
-- #eval myFlip (fun a b : Nat => a - b) 3 10 -- doit retourner 7 (= 10 - 3)
-- Exercice 3 : Echange des composantes d'une paire
-- TODO étudiant : définir mySwap qui echange les deux composantes d'une paire
-- Note : renomme en mySwap pour eviter collision avec swap defini en section 3.2
def mySwap {a b : Type} (p : a × b) : b × a := sorry
-- #eval mySwap (1, "x") -- doit retourner ("x", 1)
-- Exercice 1 : Parite
-- TODO etudiant : definir isEven qui retourne true si n est pair (indice : n % 2 == 0)
-- TODO etudiant : definir myFlip qui inverse l'ordre des deux arguments d'une fonction binaire
-- Note : renomme en myFlip pour eviter collision avec Function.flip de Lean core
🟨declarationuses`sorry`
-- #eval myFlip (fun a b : Nat => a - b) 3 10 -- doit retourner 7 (= 10 - 3)
-- Exercice 3 : Echange des composantes d'une paire
-- TODO etudiant : definir mySwap qui echange les deux composantes d'une paire
-- Note : renomme en mySwap pour eviter collision avec swap defini en section 3.2
🟨declarationuses`sorry`
-- #eval mySwap (1, "x") -- doit retourner ("x", 1)
--% env 28
--% prove 5
Raw input{"cmd": "-- Exercice 1 : Parite\n-- TODO etudiant : definir isEven qui retourne true si n est pair (indice : n % 2 == 0)\ndef 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-- Note : renomme en myFlip pour eviter collision avec Function.flip de Lean core\ndef 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-- Note : renomme en mySwap pour eviter collision avec swap defini en section 3.2\ndef mySwap {a b : Type} (p : a \u00d7 b) : b \u00d7 a := sorry\n-- #eval mySwap (1, \"x\") -- doit retourner (\"x\", 1)", "env": 27}Raw output{"sorries":
[{"proofState": 3,
"pos": {"line": 3, "column": 31},
"goal": "a b : Type\nn : Nat\n⊢ Bool",
"endPos": {"line": 3, "column": 36}},
{"proofState": 4,
"pos": {"line": 10, "column": 61},
"goal": "a✝ b✝ a b c : Type\nf : a → b → c\n⊢ b → a → c",
"endPos": {"line": 10, "column": 66}},
{"proofState": 5,
"pos": {"line": 16, "column": 47},
"goal": "a✝ b✝ a b : Type\np : a × b\n⊢ b × a",
"endPos": {"line": 16, "column": 52}}],
"messages":
[{"severity": "warning",
"pos": {"line": 3, "column": 4},
"endPos": {"line": 3, "column": 10},
"data": "declaration uses `sorry`"},
{"severity": "warning",
"pos": {"line": 10, "column": 4},
"endPos": {"line": 10, "column": 10},
"data": "declaration uses `sorry`"},
{"severity": "warning",
"pos": {"line": 16, "column": 4},
"endPos": {"line": 16, "column": 10},
"data": "declaration uses `sorry`"}],
"env": 28}
Resume
Dans ce notebook, nous avons explore :
Concept
Description
Types de base
Nat, Bool, String, etc.
Types fonctions
A -> B - fonctions de A vers B
Types produits
A × B - paires ordonnees (Unicode: \times + Tab)
Hiérarchie d’univers
Type 0, Type 1, … pour eviter les paradoxes
Lambda expressions
fun x => corps - fonctions anonymes
Curryfication
Fonctions a un argument retournant des fonctions
let bindings
Définitions locales
Sections/Namespaces
Organisation et portee du code
inductive / structure
Declarer ses propres types sommes et records (DayOfWeek, MyPoint)
deriving (Repr, BEq, DecidableEq)
Generation automatique d’instances standard
Types dependants
Types qui dependent de valeurs
Arguments implicites
{a : Type} - inferes par Lean
Prochaine étape
Dans le notebook Lean-03-Propositions-Proofs-Lean, nous verrons comment ce système de types permet de representer des propositions logiques et de construire des preuves mathematiques grace a l’isomorphisme de Curry-Howard.
Notebook base sur “TP - Z3 - Tweety - Lean.pdf” Section VI.B.1 et adapte pour Lean 4