Lean 4 - Quantificateurs et Logique du Premier Ordre

Navigation : ← Lean-03-Propositions-Proofs-Lean | Index | Lean-05-Tactics-Lean →

Introduction

Ce notebook etend la logique propositionnelle du notebook précédent a la logique du premier ordre en introduisant les quantificateurs : le quantificateur universel (“pour tout”) et le quantificateur existentiel (“il existe”).

Ces quantificateurs permettent d’exprimer des propriétés sur des ensembles infinis d’objets, ce qui est essentiel pour les mathematiques.

Objectifs d’apprentissage

  1. Maitriser le quantificateur universel forall et son utilisation
  2. Maitriser le quantificateur existentiel Exists et la construction de temoins
  3. Manipuler les propriétés arithmetiques sur Nat
  4. Utiliser les hypotheses anonymes et les references
  5. Comprendre l’interaction entre quantificateurs

Prerequis

  • Notebooks Lean-1, Lean-2 et Lean-3 completes
  • Familiarite avec les concepts de base de la logique du premier ordre

Duree estimée : 40-45 minutes

Plan de ce Notebook

Rappel : Types Dependants et Pi-types

En Lean, les quantificateurs sont fondes sur les types dependants (Pi-types) que nous avons vus au notebook 2 :

  • (x : A) -> B x est le type des fonctions qui prennent x : A et retournent une valeur de type B x (qui peut dependre de x)
  • Quand B x : Prop, ce Pi-type represente le quantificateur universel “pour tout x de type A, B(x)”

## 1. Le Quantificateur Universel forall

1.1 Définition et syntaxe

Le quantificateur universel forall x : A, P x (note aussi \forall x : A, P x ou avec le symbole Unicode ∀) exprime que la propriété P est vraie pour tout élément x du type A.

En Lean, forall est simplement un alias pour le Pi-type dans Prop.

Saisie des caractères Unicode dans Lean

Dans VSCode avec l’extension Lean 4, les symboles Unicode se tapent avec des raccourcis :

Symbole Raccourci Description
∀ \forall ou \all Quantificateur universel
∃ \exists ou \ex Quantificateur existentiel
→ \to ou \r Implication (fleche droite)
← \l Fleche gauche
↔︎ \iff Equivalence
∧ \and Conjonction
∨ \or Disjonction
¬ \not ou \neg Negation
⟨ ⟩ \< \> Angle brackets
▸ \t Triangle (substitution)
λ \lam Lambda

Conseil : Dans un notebook Jupyter avec le kernel lean4, vous pouvez aussi utiliser les mots-cles ASCII (forall, exists, ->, <->, /\, \/).

Pourquoi un chapitre dédié aux quantificateurs ?

Avant Lean-3, vous avez appris à raisonner sur des propositions closes : p ∧ q, p ∨ q, p → q. Mais en mathématiques, une proposition n’est presque jamais close — elle énonce une propriété pour tout entier naturel, il existe un entier qui satisfait un prédicat, pour tous les couples (x, y) tels que… Lean-4 introduit les quantificateurs ∀ (forall) et ∃ (Exists), qui sont les deux constructeurs algébriques de la logique du premier ordre :

  1. Quantification universelle ∀ x : A, P x — un produit dépendant Π x : A, P x en théorie des types. C’est une fonction qui, étant donné un x : A, retourne une preuve de P x. Quand A est non vide, le Π exige que la preuve marche pour tous les x ; quand A est vide, la proposition est trivialement vraie (vacuous truth, comme ∀ x : Empty, False). Lean-12 (preuve de la formule de sensibilité de Huang) construit une cascade de ∀ n : Nat, ∀ k : Fin (n+1), … qui exige la preuve pour chaque entier et chaque indice de somme partielle.
  2. Quantification existentielle ∃ x : A, P x — une paire dépendante Σ x : A, P x. C’est un témoin : pour utiliser une telle preuve, on extrait une valeur x : A et une preuve h : P x. C’est le pattern de skolemisation : prouver l’existence = exhiber un candidat. Lean-14 (Finiteness des dérivées) construit des ∃ n : Nat, 0 < n ∧ … pour borner l’existence d’un point où la dérivée s’annule.
  3. Interaction entre les deux : ∀ x ∃ y φ(x, y) est très différent de ∃ y ∀ x φ(x, y) (l’ordre change la force de l’énoncé). Lean-3 (De Morgan) montre la frontière constructif/classique sur le ¬∀ = ∃¬ ; Lean-4 section 4 creuse l’asymétrie du premier ordre.

Le pont vers la partie haute : Lean-4 est le carrefour entre Lean-3 (logique propositionnelle) et la pratique mathématique. Lean-12 (Huang) ouvre une preuve par intro n k (les deux quantificateurs), Lean-14 (Finiteness) fait use 0 (exhiber un témoin), Lean-5 (Tactiques) apprendra à automatiser ces introductions. Si forall/exists est flou, reprenez Lean-3 section 1 puis revenez ici.

-- Syntaxes equivalentes pour le quantificateur universel
-- Note: certaines variables peuvent etre non utilisees dans cette cellule
-- mais seront disponibles dans les cellules suivantes (chainage REPL)
variable (A : Type) (P : A -> Prop)

#check forall x : A, P x     -- Prop
#check ∀ x : A, P x    -- meme chose avec Unicode
#check (x : A) -> P x        -- Pi-type equivalent

-- Exemples concrets
#check forall n : Nat, n >= 0           -- "Tout naturel est >= 0"
#check forall n : Nat, n + 0 = n        -- "n + 0 = n pour tout n"
-- Syntaxes equivalentes pour le quantificateur universel
-- Note: certaines variables peuvent etre non utilisees dans cette cellule
-- mais seront disponibles dans les cellules suivantes (chainage REPL)
variable (A : Type) (P : A -> Prop)
 ∀ (x : A), P x : Prop
 ∀ (x : A), P x : Prop
 ∀ (x : A), P x : Prop
-- Exemples concrets
 ∀ (n : Nat), n ≥ 0 : Prop
 ∀ (n : Nat), n + 0 = n : Prop
--% env 0
Raw input {"cmd": "-- Syntaxes equivalentes pour le quantificateur universel\n-- Note: certaines variables peuvent etre non utilisees dans cette cellule\n-- mais seront disponibles dans les cellules suivantes (chainage REPL)\nvariable (A : Type) (P : A -> Prop)\n\n#check forall x : A, P x -- Prop\n#check \u2200 x : A, P x -- meme chose avec Unicode\n#check (x : A) -> P x -- Pi-type equivalent\n\n-- Exemples concrets\n#check forall n : Nat, n >= 0 -- \"Tout naturel est >= 0\"\n#check forall n : Nat, n + 0 = n -- \"n + 0 = n pour tout n\""}
Raw output {"messages": [{"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "∀ (x : A), P x : Prop"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "∀ (x : A), P x : Prop"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "∀ (x : A), P x : Prop"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "∀ (n : Nat), n ≥ 0 : Prop"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "∀ (n : Nat), n + 0 = n : Prop"}], "env": 0}

1.2 Introduction du forall

Pour prouver forall x : A, P x, on doit fournir une fonction qui, etant donné un x : A arbitraire, produit une preuve de P x.

C’est exactement comme programmer une fonction!

Introduction du forall — pourquoi intro est la brique de base

Pour prouver ∀ x : A, P x, on doit fournir une fonction qui, pour tout x : A, retourne une preuve de P x. La cellule de droite le fait par intro n (en tactic-style) ou fun n => … (en lambda-style). Trois choses à noter :

  1. La variable n est introduite comme une hypothèse de type Nat. Une fois intro n, on a n : Nat dans le contexte, et l’objectif devient P n. La preuve doit marcher pour n’importe quel n, pas pour un n particulier — d’où le nom « arbitraire » souvent donné à la variable introduite.
  2. Pourquoi on peut supposer n « quelconque » : parce que ∀ x : A, P x exige la preuve pour tous les x. Si on prouve P n pour un n arbitraire (pas pour un n spécifique), la preuve fonctionne pour tous. C’est la généralité universelle : la preuve de ∀ n, n + 0 = n est la même fonction à appliquer à toute entrée.
  3. En lambda-style : theorem add_zero_forall : ∀ n : Nat, n + 0 = n := fun n => Nat.add_zero n. Le fun n => … est la lambda-abstraction de Lean-2, ici appliquée à une preuve. C’est Curry-Howard : ∀ x : A, P x est (x : A) → P x, la fonction qui à x associe sa preuve.

Piège classique : croire que intro n introduit un n fixé et que la preuve doit fonctionner « pour ce n ». Mais le n est arbitraire : toute preuve trouvée marche pour tous les n, et la fonction fun n => preuve_de_P_n est la preuve de ∀ n, P n. C’est la distinction entre particulier (un n₀ fixé) et universel (n’importe quel n).

Le pont vers la partie haute : Lean-12 (sensibilité) commence toujours par intro n k h₁ h₂ … — chaque hypothèse du théorème est introduite dans le contexte par intro. Lean-14 (Finiteness) idem : intro f h h_cont …. Maîtriser intro est la première étape de toute preuve non-trivielle.

-- Prouver : pour tout n, n + 0 = n
-- Introduction par lambda-abstraction
theorem add_zero_forall : forall n : Nat, n + 0 = n :=
  fun _n => rfl   -- La preuve de n + 0 = n est rfl (calcul)

-- Syntaxe alternative avec fun ... =>
theorem add_zero_forall' : ∀ n : Nat, n + 0 = n :=
  fun n : Nat => Nat.add_zero n   -- Utilise le lemme de la bibliotheque

#check add_zero_forall   -- add_zero_forall : forall n, n + 0 = n
-- Prouver : pour tout n, n + 0 = n
-- Introduction par lambda-abstraction
theorem add_zero_forall : forall n : Nat, n + 0 = n :=
  fun _n => rfl   -- La preuve de n + 0 = n est rfl (calcul)
-- Syntaxe alternative avec fun ... =>
theorem add_zero_forall' : ∀ n : Nat, n + 0 = n :=
  fun n : Nat => Nat.add_zero n   -- Utilise le lemme de la bibliotheque
 add_zero_forall (n : Nat) : n + 0 = n
--% env 1
Raw input {"cmd": "-- Prouver : pour tout n, n + 0 = n\n-- Introduction par lambda-abstraction\ntheorem add_zero_forall : forall n : Nat, n + 0 = n :=\n fun _n => rfl -- La preuve de n + 0 = n est rfl (calcul)\n\n-- Syntaxe alternative avec fun ... =>\ntheorem add_zero_forall' : \u2200 n : Nat, n + 0 = n :=\n fun n : Nat => Nat.add_zero n -- Utilise le lemme de la bibliotheque\n\n#check add_zero_forall -- add_zero_forall : forall n, n + 0 = n", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "add_zero_forall (n : Nat) : n + 0 = n"}], "env": 1}

1.3 Élimination du forall

Pour utiliser forall x : A, P x, on l’applique a une valeur concrete a : A pour obtenir P a.

C’est l’application de fonction!

Élimination du forall — appliquer une preuve universelle

Une fois qu’on a h : ∀ x : A, P x (une preuve universelle), on l’applique à un x₀ : A spécifique pour obtenir h x₀ : P x₀. C’est la bêta-réduction appliquée aux preuves : (λ x, P x) x₀ se réduit en P x₀. La cellule de droite fait exact add_zero n qui est exactement h n où h = add_zero_forall :

  1. Pourquoi apply est la symétrique de intro. intro construit une preuve de ∀ x, P x à partir d’une preuve de P x (paramétrée par x). apply consomme une preuve de ∀ x, P x pour en tirer une preuve de P x₀. Le mécanisme est le même — la bêta-réduction — vu des deux côtés.
  2. Notation h.n ou h x₀. Pour appliquer h : ∀ x, P x, on peut écrire h x₀ (bêta explicite) ou h.n (notation pointée, où n est nom de variable et non valeur). Préférer h x₀ pour la clarté quand le contexte est chargé.
  3. Cas des preuves à plusieurs quantificateurs : h : ∀ x : A, ∀ y : B, P x y s’applique en h x₀ y₀ (deux arguments). Lean unifiera automatiquement x₀ et y₀ avec les types attendus.

Le pont vers la partie haute : Lean-12 utilise apply h dans pratiquement chaque étape : appliquer la définition de S(f, n, k), appliquer une inégalité, appliquer une hypothèse du contexte. Lean-14 fait apply … 50+ fois dans la preuve de Finiteness. Le pattern apply h (où h : ∀ x, …) est la deuxième brique de base, après intro.

-- Définition rappel (pour exécution isolee)
theorem add_zero_forall_copy : forall n : Nat, n + 0 = n :=
  fun _n => rfl

-- Si on a une preuve de forall, on peut l'instancier
theorem use_forall : 5 + 0 = 5 :=
  add_zero_forall_copy 5   -- Appliquer le théorème a 5

#eval 5 + 0  -- 5 (Lean calcule)

-- Exemple avec une propriété quelconque
-- On peut en deduire P 42 a partir de forall n, P n
theorem instance_of_forall (P : Nat -> Prop)
    (h : forall n : Nat, P n) : P 42 := h 42
-- Definition rappel (pour execution isolee)
theorem add_zero_forall_copy : forall n : Nat, n + 0 = n :=
  fun _n => rfl
-- Si on a une preuve de forall, on peut l'instancier
theorem use_forall : 5 + 0 = 5 :=
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 5
-- Exemple avec une propriete quelconque
-- On peut en deduire P 42 a partir de forall n, P n
theorem instance_of_forall (P : Nat -> Prop)
    (h : forall n : Nat, P n) : P 42 := h 42
--% env 2
Raw input {"cmd": "-- Definition rappel (pour execution isolee)\ntheorem add_zero_forall_copy : forall n : Nat, n + 0 = n :=\n fun _n => rfl\n\n-- Si on a une preuve de forall, on peut l'instancier\ntheorem use_forall : 5 + 0 = 5 :=\n add_zero_forall_copy 5 -- Appliquer le theoreme a 5\n\n#eval 5 + 0 -- 5 (Lean calcule)\n\n-- Exemple avec une propriete quelconque\n-- On peut en deduire P 42 a partir de forall n, P n\ntheorem instance_of_forall (P : Nat -> Prop)\n (h : forall n : Nat, P n) : P 42 := h 42", "env": 1}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 7, "column": 15}, "endPos": {"line": 7, "column": 16}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 5}, "data": "5"}], "env": 2}

1.4 Propriétés avec plusieurs quantificateurs

Quand on a plusieurs variables quantifiées, on peut les introduire une par une ou en groupe. Les hypothèses intermédiaires (have) permettent de structurer les preuves complexes.

Quantificateurs imbriqués — curryfication et introduction successive

La cellule suivante vérifie le type des deux écritures ∀ x y, P x y et ∀ x, ∀ y, P x y, puis prouve comm_add : ∀ x y : Nat, x + y = y + x. Trois choses à comprendre :

  1. Curryfication. ∀ x y, P x y est une abréviation de ∀ x : Nat, ∀ y : Nat, P x y : une preuve du premier type reçoit d’abord x, puis y. Les deux #check montrent cette même forme imbriquée.
  2. Application partielle. Si h : ∀ x y, P x y, alors h x₀ : ∀ y, P x₀ y, et h x₀ y₀ : P x₀ y₀. Lean-12 exploite cette structure pour les formules quantifiées en f, n et k.
  3. Exemple arithmétique. comm_add introduit successivement x et y, puis applique Nat.add_comm x y. Il prouve la commutativité de l’addition, pas une permutation de quantificateurs sur un prédicat binaire.

Les deux appels #check produisent le même type affiché, ∀ (x y : Nat), P x y : Prop. Cette égalité de forme ne dit pas que l’on peut inverser x et y dans une proposition quelconque : elle dit que l’écriture groupée et l’écriture imbriquée déclarent les arguments dans le même ordre. Le dernier #check spécialise au contraire la preuve comm_add aux valeurs 3 et 5 ; son résultat est une proposition arithmétique particulière, 3 + 5 = 5 + 3.

Le pont vers la partie haute : Lean-12 (sensibilité) utilise des théorèmes à plusieurs quantificateurs imbriqués ; la curryfication aide à lire et à appliquer progressivement leurs hypothèses. Devant un théorème h : ∀ x, ∀ y, R x y, on peut donc d’abord fixer x pour obtenir h x : ∀ y, R x y, puis fixer y. Cette lecture pas à pas est utile même quand l’énoncé abrège les deux quantificateurs en ∀ x y.

-- forall x y, P x y est equivalent a forall x, forall y, P x y
variable (P : Nat -> Nat -> Prop)

#check forall x y : Nat, P x y      -- Prop
#check forall x : Nat, forall y : Nat, P x y  -- meme chose

-- Prouver une propriété avec deux quantificateurs
theorem comm_add : forall x y : Nat, x + y = y + x :=
  fun x y => Nat.add_comm x y   -- Lemme de la bibliotheque

#check comm_add 3 5   -- 3 + 5 = 5 + 3 : Prop
-- forall x y, P x y est equivalent a forall x, forall y, P x y
variable (P : Nat -> Nat -> Prop)
 ∀ (x y : Nat), P x y : Prop
 ∀ (x y : Nat), P x y : Prop
-- Prouver une propriete avec deux quantificateurs
theorem comm_add : forall x y : Nat, x + y = y + x :=
  fun x y => Nat.add_comm x y   -- Lemme de la bibliotheque
 comm_add 3 5 : 3 + 5 = 5 + 3
--% env 3
Raw input {"cmd": "-- forall x y, P x y est equivalent a forall x, forall y, P x y\nvariable (P : Nat -> Nat -> Prop)\n\n#check forall x y : Nat, P x y -- Prop\n#check forall x : Nat, forall y : Nat, P x y -- meme chose\n\n-- Prouver une propriete avec deux quantificateurs\ntheorem comm_add : forall x y : Nat, x + y = y + x :=\n fun x y => Nat.add_comm x y -- Lemme de la bibliotheque\n\n#check comm_add 3 5 -- 3 + 5 = 5 + 3 : Prop", "env": 2}
Raw output {"messages": [{"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "∀ (x y : Nat), P x y : Prop"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "∀ (x y : Nat), P x y : Prop"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "comm_add 3 5 : 3 + 5 = 5 + 3"}], "env": 3}

## 2. Le Quantificateur Existentiel Exists

2.1 Définition et syntaxe

Le quantificateur existentiel Exists (fun x => P x) (note \exists x, P x) exprime qu’il existe au moins un élément x tel que P x soit vrai.

Une preuve de Exists contient deux choses : 1. Un temoin : une valeur concrete a de type A 2. Une preuve que P a est vrai

Exists — la somme dépendante des preuves

La cellule de droite fait #check Exists et #check @Exists.intro. Quatre choses à retenir :

  1. Exists est Σ x : A, P x. La lettre Σ (Sigma) dénote la somme dépendante : Σ x : A, B x est le type des paires (x : A, y : B x) où le type de y dépend de x. Pour les propositions, Σ x : A, P x est ∃ x : A, P x — un témoin x et une preuve h : P x. Notation Unicode : ∃ (U+2203).
  2. Constructeur Exists.intro. Pour prouver ∃ x : A, P x, on exhibe un témoin x₀ : A et une preuve h : P x₀. Syntactic sugar : ⟨x₀, h⟩ ou use x₀ (suivi de la preuve de P x₀). Lean-14 (Finiteness) utilise use 0 pour exhiber le point 0 comme témoin.
  3. Élimination par cases ou obtain. Pour utiliser une preuve h : ∃ x : A, P x, on fait cases h with | intro x h => … ou obtain ⟨x, h⟩ := h. Cela extrait un x : A arbitraire et une preuve h : P x dans le contexte. Lean-16b (Game of Life) obtient un état initial s₀ et une preuve de ses invariants par ce pattern.
  4. Différence avec ∃ x, P x (logique classique) : en logique intuitionniste, ∃ x, P x exige un témoin explicite ; en logique classique, on peut obtenir ¬¬∃ x, P x sans témoin (via Classical.em). Lean-3 section 9 discute cette frontière.

Le pont vers la partie haute : Lean-12 utilise Exists dans ses conclusions : ∃ c : ℝ, c > 0 ∧ …. Lean-14 fait use 0 pour les témoins de Finiteness. Lean-16b fait use [configuration_initiale] pour exhiber un état de Game of Life. Le pattern use x₀ suivi de la preuve est universel.

-- Syntaxes pour le quantificateur existentiel
variable (A : Type) (P : A -> Prop)

#check Exists P                 -- Prop
#check Exists (fun x : A => P x)  -- equivalent
#check ∃ x : A, P x       -- notation

-- Exemples
#check ∃ n : Nat, n > 5       -- "Il existe n > 5"
#check ∃ n : Nat, n * n = 4   -- "Il existe n tel que n^2 = 4"
-- Syntaxes pour le quantificateur existentiel
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 Exists P : Prop
 ∃ x, P x : Prop
 ∃ x, P x : Prop
-- Exemples
 ∃ n, n > 5 : Prop
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ∃ n, n * n = 4 : Prop
--% env 4
Raw input {"cmd": "-- Syntaxes pour le quantificateur existentiel\nvariable (A : Type) (P : A -> Prop)\n\n#check Exists P -- Prop\n#check Exists (fun x : A => P x) -- equivalent\n#check \u2203 x : A, P x -- notation\n\n-- Exemples\n#check \u2203 n : Nat, n > 5 -- \"Il existe n > 5\"\n#check \u2203 n : Nat, n * n = 4 -- \"Il existe n tel que n^2 = 4\"", "env": 3}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 27}, "endPos": {"line": 2, "column": 28}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "Exists P : Prop"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "∃ x, P x : Prop"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "∃ x, P x : Prop"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "∃ n, n > 5 : Prop"}, {"severity": "warning", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 1}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "∃ n, n * n = 4 : Prop"}], "env": 4}

2.2 Introduction du Exists

Pour prouver \exists x : A, P x, on doit fournir : - Un temoin a : A - Une preuve de P a

On utilise la notation angle brackets ⟨temoin, preuve⟩ ou Exists.intro.

Introduction du Exists — exhiber un témoin

La cellule de droite prouve exists_gt_5 : ∃ n : Nat, n > 5 par ⟨6, Nat.lt_succ_self 5⟩ (ou use 6). Le pattern est :

  1. Choisir le témoin. Pour ∃ n : Nat, n > 5, le témoin 6 : Nat est explicite. On ne peut pas écrire ∃ n, n > 5 avec un témoin implicite — la preuve d’existence intuitionniste exige un n₀ constructible. C’est la différence majeure avec la logique classique, où ¬¬∃ n, n > 5 peut être obtenu sans témoin (via byContradiction + Classical.em).
  2. Prouver la propriété du témoin. Une fois 6 choisi, on doit prouver 6 > 5. C’est Nat.lt_succ_self 5 (le lemme de Mathlib 4 qui énonce n < n + 1 pour tout n). En l’occurrence, 6 = 5 + 1, donc 5 < 6 par lt_succ_self.
  3. Notation ⟨x₀, h⟩ vs use x₀. ⟨x₀, h⟩ est la forme explicite : on donne le témoin et la preuve. use x₀ est la forme tactic-style : Lean construit ensuite la preuve par exact ou apply. Lean-5 introduit use comme tactique dédiée.

Piège classique : croire qu’on peut prouver ∃ n, P n « par contradiction » sans témoin. En intuitionniste, non. Il faut exhiber un n₀ et prouver P n₀. C’est la différence entre preuve constructive (témoin explicite) et preuve classique (double négation suffit). Lean-3 section 9 explore cette frontière en détail.

Le pont : Lean-14 (Finiteness) utilise systématiquement use 0 ou use n₀ pour exhiber un point où la dérivée s’annule. Lean-16b fait use [config_init] pour donner un état initial. Le pattern est constant.

-- Prouver : il existe n tel que n > 5
-- Temoin : 6, Preuve : 6 > 5
theorem exists_gt_5 : ∃ n : Nat, n > 5 :=
  ⟨6, Nat.lt_succ_self 5⟩   -- 6 > 5 car 5 < 6 = succ 5

-- Version avec Exists.intro explicite
theorem exists_gt_5' : ∃ n : Nat, n > 5 :=
  Exists.intro 6 (Nat.lt_succ_self 5)

-- Prouver : il existe n tel que n + n = 10
theorem exists_double_10 : ∃ n : Nat, n + n = 10 :=
  ⟨5, rfl⟩   -- Temoin : 5, Preuve : 5 + 5 = 10 par calcul
-- Prouver : il existe n tel que n > 5
-- Temoin : 6, Preuve : 6 > 5
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  ⟨6, Nat.lt_succ_self 5⟩   -- 6 > 5 car 5 < 6 = succ 5
-- Version avec Exists.intro explicite
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  Exists.intro 6 (Nat.lt_succ_self 5)
-- Prouver : il existe n tel que n + n = 10
theorem exists_double_10 : ∃ n : Nat, n + n = 10 :=
  ⟨5, rfl⟩   -- Temoin : 5, Preuve : 5 + 5 = 10 par calcul
--% env 5
Raw input {"cmd": "-- Prouver : il existe n tel que n > 5\n-- Temoin : 6, Preuve : 6 > 5\ntheorem exists_gt_5 : \u2203 n : Nat, n > 5 :=\n \u27e86, Nat.lt_succ_self 5\u27e9 -- 6 > 5 car 5 < 6 = succ 5\n\n-- Version avec Exists.intro explicite\ntheorem exists_gt_5' : \u2203 n : Nat, n > 5 :=\n Exists.intro 6 (Nat.lt_succ_self 5)\n\n-- Prouver : il existe n tel que n + n = 10\ntheorem exists_double_10 : \u2203 n : Nat, n + n = 10 :=\n \u27e85, rfl\u27e9 -- Temoin : 5, Preuve : 5 + 5 = 10 par calcul", "env": 4}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 3, "column": 5}, "endPos": {"line": 3, "column": 6}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 7, "column": 12}, "endPos": {"line": 7, "column": 13}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 5}

2.3 Élimination du Exists

Pour utiliser une preuve de \exists x : A, P x, on fait une analyse par cas : on suppose qu’on a un x quelconque et une preuve de P x, puis on doit montrer le but.

C’est Exists.elim ou la syntaxe match/let.

Élimination du Exists — cases/obtain/match

La cellule de droite montre l’élimination de Exists par cases h with | intro x h => …. Le pattern libère un x : A arbitraire et une preuve h : P x dans le contexte :

  1. Pourquoi cases et pas apply. Exists n’est pas une flèche — c’est un type inductif (comme And, Or de Lean-3). L’élimination d’un type inductif se fait par cases (ou match), pas par apply. cases force l’analyse par cas : pour And, les deux composants h.left/h.right ; pour Or, les deux branches inl/inr ; pour Exists, le témoin x et la preuve h : P x simultanément. Lean-12 (sensibilité) utilise cases h 10+ fois dans la preuve pour ouvrir des hypothèses conjonctives et existentielles.
  2. obtain comme variante. Lean 4 (et Mathlib 4) supporte obtain ⟨x, h⟩ := h qui est du sugar syntaxique pour cases h with | intro x h => …. Plus concis, surtout quand le Exists est utilisé dans une expression. Lean-14 utilise obtain dans 80% de ses preuves.
  3. Le témoin x est « arbitraire » dans le scope. Une fois cases h with | intro x h =>, on a x : A dans le contexte, et toute conclusion prouvée en utilisant x doit être vraie pour ce x particulier. Si on veut « pour tout x tel que P x », on utilise ∀ x, P x → … (implication) plutôt que ∃ x, P x (existence).

Le pont vers la partie haute : Lean-12 fait obtain ⟨S, hS⟩ := h pour récupérer un sous-ensemble S de Fin n et une preuve de ses propriétés. Lean-14 fait obtain ⟨x, hx_lt⟩ := h pour récupérer un point x et une borne. Lean-16b fait obtain ⟨s₀, hs₀⟩ := h_state pour obtenir un état initial et ses invariants. Le pattern obtain ⟨x, h⟩ := h est aussi fréquent que intro ou apply.

-- Si il existe n pair, alors il existe m tel que 2 * m existe
-- (exemple simplifie)

-- Élimination avec Exists.elim
theorem exists_elim_example
  (h : ∃ n : Nat, n > 0) : True :=
  Exists.elim h (fun _n _hn => True.intro)

-- Élimination avec match (plus lisible)
theorem exists_elim_match
  (h : ∃ n : Nat, n > 0) : ∃ m : Nat, m >= 0 :=
  match h with
  | ⟨n, _hn⟩ => ⟨n, Nat.zero_le n⟩

-- Syntaxe let ... := ... in ...
theorem exists_elim_let
  (h : ∃ n : Nat, n > 0) : ∃ m : Nat, m >= 0 :=
  let ⟨n, _⟩ := h
  ⟨n, Nat.zero_le n⟩
-- Si il existe n pair, alors il existe m tel que 2 * m existe
-- (exemple simplifie)
-- Elimination avec Exists.elim
theorem exists_elim_example
  (h : ∃ n : Nat, n > 0) : True :=
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Elimination avec match (plus lisible)
theorem exists_elim_match
  (h : ∃ n : Nat, n > 0) : ∃ m : Nat, m >= 0 :=
  match h with
  | ⟨n, _hn⟩ => ⟨n, Nat.zero_le n⟩
-- Syntaxe let ... := ... in ...
theorem exists_elim_let
  (h : ∃ n : Nat, n > 0) : ∃ m : Nat, m >= 0 :=
  let ⟨n, _⟩ := h
  ⟨n, Nat.zero_le n⟩
--% env 6
Raw input {"cmd": "-- Si il existe n pair, alors il existe m tel que 2 * m existe\n-- (exemple simplifie)\n\n-- Elimination avec Exists.elim\ntheorem exists_elim_example\n (h : \u2203 n : Nat, n > 0) : True :=\n Exists.elim h (fun _n _hn => True.intro)\n\n-- Elimination avec match (plus lisible)\ntheorem exists_elim_match\n (h : \u2203 n : Nat, n > 0) : \u2203 m : Nat, m >= 0 :=\n match h with\n | \u27e8n, _hn\u27e9 => \u27e8n, Nat.zero_le n\u27e9\n\n-- Syntaxe let ... := ... in ...\ntheorem exists_elim_let\n (h : \u2203 n : Nat, n > 0) : \u2203 m : Nat, m >= 0 :=\n let \u27e8n, _\u27e9 := h\n \u27e8n, Nat.zero_le n\u27e9", "env": 5}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 7, "column": 41}, "endPos": {"line": 7, "column": 42}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 6}

## 3. Propriétés Arithmetiques sur Nat

3.1 Lemmes de base

Lean fournit de nombreux lemmes sur les nombres naturels dans le namespace Nat.

Lemmes arithmétiques de Mathlib 4 — la bibliothèque standard

La cellule de droite fait #check sur les lemmes fondamentaux de Mathlib 4 sur Nat. Ces lemmes sont les briques de base de toute preuve arithmétique :

  1. Nat.add_zero : n + 0 = n — l’identité à droite de l’addition. Symétrique : Nat.zero_add : 0 + n = n. Ces deux lemmes sont les plus simples à invoquer et servent d’exercices d’introduction au rfl (Lean-5 introduira rfl automatiquement).
  2. Nat.add_succ : n + (m + 1) = (n + m) + 1 — la récurrence sur le successeur. C’est la pierre angulaire de la preuve par induction sur Nat (Lean-7 introduit induction). Toutes les preuves arithmétiques non-triviales passent par Nat.add_succ.
  3. Nat.succ_pos : 0 < n + 1 — la positivité des successeurs. Utilisé pour prouver 0 < n sur tout n ≠ 0.

Pourquoi #check plutôt que exact. #check type un terme et affiche son type, sans le réduire. exact add_zero n réduirait n + 0 en n et prouverait n + 0 = n. #check Nat.add_zero affiche Nat.add_zero : ∀ (n : Nat), n + 0 = n — utile pour lire le type d’un lemme avant de l’appliquer. Lean-14 utilise #check 30+ fois dans la preuve de Finiteness pour citer les lemmes de Mathlib.

Le pont : ces lemmes sont les mêmes que ceux utilisés dans Lean-12 (sensibilité) et Lean-14 (Finiteness). Mathlib 4 capitalise toutes les preuves arithmétiques dans Mathlib.Algebra.* et Mathlib.Data.Nat.*. Apprendre à lire un #check (le type affiché) est la compétence n°1 pour naviguer Mathlib.

-- Quelques lemmes utiles
#check Nat.add_zero       -- n + 0 = n
#check Nat.zero_add       -- 0 + n = n
#check Nat.add_comm       -- n + m = m + n
#check Nat.add_assoc      -- (n + m) + k = n + (m + k)
#check Nat.mul_comm       -- n * m = m * n
#check Nat.mul_assoc      -- (n * m) * k = n * (m * k)
#check Nat.add_mul        -- (n + m) * k = n * k + m * k
#check Nat.mul_add        -- n * (m + k) = n * m + n * k
-- Quelques lemmes utiles
 Nat.add_zero (n : Nat) : n + 0 = n
 Nat.zero_add (n : Nat) : 0 + n = n
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
 Nat.add_comm (n m : Nat) : n + m = m + n
 Nat.add_assoc (n m k : Nat) : n + m + k = n + (m + k)
 Nat.mul_comm (n m : Nat) : n * m = m * n
 Nat.mul_assoc (n m k : Nat) : n * m * k = n * (m * k)
 Nat.add_mul (n m k : Nat) : (n + m) * k = n * k + m * k
 Nat.mul_add (n m k : Nat) : n * (m + k) = n * m + n * k
--% env 7
Raw input {"cmd": "-- Quelques lemmes utiles\n#check Nat.add_zero -- n + 0 = n\n#check Nat.zero_add -- 0 + n = n\n#check Nat.add_comm -- n + m = m + n\n#check Nat.add_assoc -- (n + m) + k = n + (m + k)\n#check Nat.mul_comm -- n * m = m * n\n#check Nat.mul_assoc -- (n * m) * k = n * (m * k)\n#check Nat.add_mul -- (n + m) * k = n * k + m * k\n#check Nat.mul_add -- n * (m + k) = n * m + n * k", "env": 6}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Nat.add_zero (n : Nat) : n + 0 = n"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Nat.zero_add (n : Nat) : 0 + n = n"}, {"severity": "warning", "pos": {"line": 3, "column": 3}, "endPos": {"line": 3, "column": 4}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 9}, "endPos": {"line": 3, "column": 10}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "Nat.add_comm (n m : Nat) : n + m = m + n"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "Nat.add_assoc (n m k : Nat) : n + m + k = n + (m + k)"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "Nat.mul_comm (n m : Nat) : n * m = m * n"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "Nat.mul_assoc (n m k : Nat) : n * m * k = n * (m * k)"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "Nat.add_mul (n m k : Nat) : (n + m) * k = n * k + m * k"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "Nat.mul_add (n m k : Nat) : n * (m + k) = n * m + n * k"}], "env": 7}

3.2 Preuves arithmetiques

Les preuves sur les nombres naturels utilisent souvent les lemmes de la bibliotheque standard (Nat.add_comm, Nat.mul_assoc, etc.) combines avec la reflexivite et la congruence.

Preuves arithmétiques — omega et Nat.add_comm

La cellule de droite prouve add_one_comm : n + 1 = 1 + n par Nat.add_comm n 1. Décortiquons :

  1. Nat.add_comm : ∀ m n, m + n = n + m. C’est la commutativité de l’addition. Symétrique : Nat.mul_comm, Nat.add_assoc, Nat.mul_assoc. Mathlib 4 fournit toutes les propriétés algébriques standards de Nat (CommSemiring, CommRing, etc.).
  2. Pourquoi la preuve est juste Nat.add_comm n 1. n + 1 = 1 + n est un cas particulier de m + n = n + m avec m := n et n := 1. Lean unifie automatiquement.
  3. omega comme tactique automatique. Lean-5 introduit omega qui résout automatiquement les égalités et inégalités linéaires sur Nat, Int, Rat. Si la cellule de droite est remplacée par omega, Lean-5 prouve n + 1 = 1 + n en quelques millisecondes sans intervention. Mais Lean-4 montre la preuve explicite pour l’intuition.

Le pont vers la partie haute : Lean-12 (sensibilité) utilise omega pour les combinaisons d’inégalités linéaires (|x + y| ≤ |x| + |y|). Lean-14 (Finiteness) utilise omega 50+ fois pour les manipulations de bornes. Lean-16b (Game of Life) utilise omega pour les comptages de cellules voisines. Le pattern omega (Lean-5) est universel dans la partie haute, mais savoir ce qu’il fait (réécriture + Nat.add_comm + Nat.add_assoc + Nat.lt_succ) est nécessaire pour debugger quand il échoue.

-- Preuve que n + 1 = 1 + n
theorem add_one_comm (n : Nat) : n + 1 = 1 + n :=
  Nat.add_comm n 1

-- Preuve avec calc
theorem calc_arith (a b c : Nat) : (a + b) + c = a + (b + c) :=
  calc (a + b) + c
       = a + (b + c) := Nat.add_assoc a b c

-- Preuve plus complexe
theorem arith_example (a b : Nat) : a + b + a = 2 * a + b :=
  calc a + b + a
       = a + (b + a)   := Nat.add_assoc a b a
     _ = a + (a + b)   := congrArg (a + ·) (Nat.add_comm b a)
     _ = (a + a) + b   := (Nat.add_assoc a a b).symm
     _ = 2 * a + b     := congrArg (· + b) (Nat.two_mul a).symm
-- Preuve que n + 1 = 1 + n
theorem add_one_comm (n : Nat) : n + 1 = 1 + n :=
  Nat.add_comm n 1
-- Preuve avec calc
theorem calc_arith (a b c : Nat) : (a + b) + c = a + (b + c) :=
  calc (a + b) + c
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Preuve plus complexe
theorem arith_example (a b : Nat) : a + b + a = 2 * a + b :=
  calc a + b + a
       = a + (b + a)   := Nat.add_assoc a b a
     _ = a + (a + b)   := congrArg (a + ·) (Nat.add_comm b a)
     _ = (a + a) + b   := (Nat.add_assoc a a b).symm
     _ = 2 * a + b     := congrArg (· + b) (Nat.two_mul a).symm
--% env 8
Raw input {"cmd": "-- Preuve que n + 1 = 1 + n\ntheorem add_one_comm (n : Nat) : n + 1 = 1 + n :=\n Nat.add_comm n 1\n\n-- Preuve avec calc\ntheorem calc_arith (a b c : Nat) : (a + b) + c = a + (b + c) :=\n calc (a + b) + c\n = a + (b + c) := Nat.add_assoc a b c\n\n-- Preuve plus complexe\ntheorem arith_example (a b : Nat) : a + b + a = 2 * a + b :=\n calc a + b + a\n = a + (b + a) := Nat.add_assoc a b a\n _ = a + (a + b) := congrArg (a + \u00b7) (Nat.add_comm b a)\n _ = (a + a) + b := (Nat.add_assoc a a b).symm\n _ = 2 * a + b := congrArg (\u00b7 + b) (Nat.two_mul a).symm", "env": 7}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 8, "column": 24}, "endPos": {"line": 8, "column": 25}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 8}

## 4. Combinaison de Quantificateurs

L’ordre des quantificateurs est crucial : forall x, exists y, P x y (pour tout x il existe un y) est différent de exists y, forall x, P x y (il existe un y pour tous les x).

Instancier ∀ pour construire ∃

La cellule suivante prouve forall_to_exists (a : A) (h : ∀ x : A, P x) : ∃ x : A, P x. Le témoin a est déjà fourni : la preuve ⟨a, h a⟩ applique h à ce témoin. Elle montre qu’une propriété universelle donne un cas existentiel si le type a un habitant connu ; elle ne construit pas une fonction de choix.

Le second théorème, not_exists_iff, relie ¬ ∃ x, P x et ∀ x, ¬ P x dans les deux sens. Pour nier un témoin ⟨x, hp⟩, on applique l’hypothèse universelle à x ; dans l’autre sens, un témoin réfuterait l’absence d’existence.

Frontière avec l’axiome du choix : passer de ∀ a : A, ∃ b : B, P a b à ∃ f : A → B, ∀ a, P a (f a) exige de choisir un témoin pour chaque a. Cette formule n’est pas prouvée dans cette cellule ; l’instanciation h a ci-dessus n’utilise aucun choix. La réciproque de la formule de choix est immédiate à partir d’une fonction f, mais cela ne change pas la direction qui demande le choix.

Le pont : distinguer un témoin déjà fourni d’une famille de témoins à sélectionner aide à lire les énoncés quantifiés des notebooks suivants.

variable (A : Type) (P : A -> Prop)

-- De forall a exists (si A est habite)
theorem forall_to_exists (a : A) (h : forall x : A, P x) : ∃ x : A, P x :=
  ⟨a, h a⟩

-- Negation de exists = forall not
theorem not_exists_iff : (¬ ∃ x : A, P x) <-> forall x : A, ¬ P x :=
  ⟨fun h x hp => h ⟨x, hp⟩,
   fun h ⟨x, hp⟩ => h x hp⟩
variable (A : Type) (P : A -> Prop)
-- De forall a exists (si A est habite)
theorem forall_to_exists (a : A) (h : forall x : A, P x) : ∃ x : A, P x :=
  ⟨a, h a⟩
-- Negation de exists = forall not
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  ⟨fun h x hp => h ⟨x, hp⟩,
   fun h ⟨x, hp⟩ => h x hp⟩
--% env 9
Raw input {"cmd": "variable (A : Type) (P : A -> Prop)\n\n-- De forall a exists (si A est habite)\ntheorem forall_to_exists (a : A) (h : forall x : A, P x) : \u2203 x : A, P x :=\n \u27e8a, h a\u27e9\n\n-- Negation de exists = forall not\ntheorem not_exists_iff : (\u00ac \u2203 x : A, P x) <-> forall x : A, \u00ac P x :=\n \u27e8fun h x hp => h \u27e8x, hp\u27e9,\n fun h \u27e8x, hp\u27e9 => h x hp\u27e9", "env": 8}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 8, "column": 20}, "endPos": {"line": 8, "column": 21}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 9}

4.2 Ordre des quantificateurs

Attention : l’ordre des quantificateurs compte!

  • \forall x, \exists y, P x y : pour chaque x, il existe un y (différent selon x)
  • \exists y, \forall x, P x y : il existe un y qui marche pour tous les x

Ordre des quantificateurs — pourquoi ∀x ∃y ≠ ∃y ∀x

La cellule de droite prouve exists_forall_implies_forall_exists : (∃ y, ∀ x, P x y) → ∀ x, ∃ y, P x y. C’est la monotonie de ∃ à gauche et ∀ à droite :

  1. Sens strict. La réciproque ∀ x, ∃ y, P x y → ∃ y, ∀ x, P x y est fausse en général. Contre-exemple : ∀ x : Nat, ∃ y : Nat, y > x (pour tout x, il existe un y > x) — vrai ; mais ∃ y : Nat, ∀ x : Nat, y > x (il existe un y plus grand que tout x) — faux dans Nat (pas de majorant universel). C’est la distinction classique entre « pour chaque x, un y qui dépend de x » et « un y unique qui marche pour tous les x ».
  2. En mathématiques. « Pour tout ε > 0, il existe N tel que n ≥ N ⇒ |a_n - L| < ε » (définition de limite) est ∀ε ∃N …. L’ordre compte : la convergence simple est ∀x lim f_n(x) = f(x) (une limite par x), la convergence uniforme est ∃N ∀x (un N unique). Différence cruciale en analyse.
  3. Comment se souvenir. ∀-à-gauche distribue sur ∃-à-droite (la preuve est triviale). ∃-à-gauche ne distribue pas sur ∀-à-droite (la réciproque est fausse). Mnémonique : « ∃ est existentiel, donc un témoin ; il ne peut pas servir pour tout le monde ».

Le pont : Lean-12 (sensibilité) preuve ∀ f ∀ n ∀ k ∃ S … — il existe un sous-ensemble S qui dépend de f, n, k. Si on passe à ∃ S ∀ f ∀ n ∀ k …, l’énoncé devient faux (le sous-ensemble S doit être universel). Lean-14 (Finiteness) idem : ∀ f ∃ x (un point par fonction) vs ∃ x ∀ f (un point universel). L’ordre est toujours significatif.

variable (P : Nat -> Nat -> Prop)

-- L'implication existe-forall vers forall-existe est toujours vraie
theorem exists_forall_to_forall_exists
  (h : ∃ y : Nat, forall x : Nat, P x y) : forall x : Nat, ∃ y : Nat, P x y :=
  fun x => match h with
    | ⟨y, hy⟩ => ⟨y, hy x⟩

-- L'inverse n'est pas vrai en général!
-- Exemple : P x y := x <= y
-- forall x, exists y, x <= y  -- Vrai : y = x marche
-- exists y, forall x, x <= y  -- Faux : aucun y ne majore tous les x
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- L'implication existe-forall vers forall-existe est toujours vraie
theorem exists_forall_to_forall_exists
  (h : ∃ y : Nat, forall x : Nat, P x y) : forall x : Nat, ∃ y : Nat, P x y :=
  fun x => match h with
    | ⟨y, hy⟩ => ⟨y, hy x⟩
-- L'inverse n'est pas vrai en general!
-- Exemple : P x y := x <= y
-- forall x, exists y, x <= y  -- Vrai : y = x marche
-- exists y, forall x, x <= y  -- Faux : aucun y ne majore tous les x
--% env 10
Raw input {"cmd": "variable (P : Nat -> Nat -> Prop)\n\n-- L'implication existe-forall vers forall-existe est toujours vraie\ntheorem exists_forall_to_forall_exists\n (h : \u2203 y : Nat, forall x : Nat, P x y) : forall x : Nat, \u2203 y : Nat, P x y :=\n fun x => match h with\n | \u27e8y, hy\u27e9 => \u27e8y, hy x\u27e9\n\n-- L'inverse n'est pas vrai en general!\n-- Exemple : P x y := x <= y\n-- forall x, exists y, x <= y -- Vrai : y = x marche\n-- exists y, forall x, x <= y -- Faux : aucun y ne majore tous les x", "env": 9}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 1, "column": 21}, "endPos": {"line": 1, "column": 22}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 10}

## 5. Hypotheses Anonymes et Nommage

5.1 La construction have

have permet d’introduire des lemmes intermediaires dans une preuve.

have — nommer une hypothèse intermédiaire

La cellule de droite prouve have_example : a = b → b = a par have h' : b = a := h.symm; exact h'. Trois choses à noter :

  1. have crée une hypothèse nommée dans le contexte. C’est une déclaration locale : h' : b = a est ajouté au contexte sans modifier l’objectif. La syntaxe complète : have h' : (type_de_h') := (preuve_de_h') ou have h' : (type) := by (tactiques). Lean-2 a déjà introduit let ; Lean-4 introduit have qui est plus idiomatique pour les preuves.
  2. Pourquoi h.symm. La symétrie de l’égalité : Eq.symm : a = b → b = a. C’est la réflexivité symétrique : si h : a = b, alors h.symm : b = a. Lean-4 utilise la notation pointée . pour les lemmes de structure (.symm, .trans, .mp, .mpr — Lean-3 a introduit .mp/.mpr pour Iff).
  3. Différence avec let. let x : T := v lie x à une valeur v : T. have h : P := proof lie h à une preuve proof : P. Pour les preuves, have est plus idiomatique. let est utilisé pour les valeurs intermédiaires (Lean-2 section 4).

Le pont vers la partie haute : Lean-12 utilise have 50+ fois pour nommer des sommes partielles, des hypothèses d’induction, des lemmes intermédiaires. Lean-14 fait have h : 0 < n := Nat.pos_iff_ne_zero.mpr hn pour introduire une hypothèse de positivité. Le pattern have h : P := preuve est la 3ᵉ brique de base après intro et apply.

-- have avec nom
theorem have_example (a b : Nat) (h : a = b) : b = a :=
  have h' : b = a := h.symm
  h'

-- have anonyme (utilise `this`)
theorem have_anon (a b : Nat) (h : a = b) : b = a :=
  have : b = a := h.symm
  this   -- Reference a la derniere hypothese anonyme
-- have avec nom
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  have h' : b = a := h.symm
  h'
-- have anonyme (utilise `this`)
theorem have_anon (a b : Nat) (h : a = b) : b = a :=
  have : b = a := h.symm
  this   -- Reference a la derniere hypothese anonyme
--% env 11
Raw input {"cmd": "-- have avec nom\ntheorem have_example (a b : Nat) (h : a = b) : b = a :=\n have h' : b = a := h.symm\n h'\n\n-- have anonyme (utilise `this`)\ntheorem have_anon (a b : Nat) (h : a = b) : b = a :=\n have : b = a := h.symm\n this -- Reference a la derniere hypothese anonyme", "env": 10}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 4}, "endPos": {"line": 2, "column": 5}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 51}, "endPos": {"line": 2, "column": 52}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 11}

5.2 References avec ‹›

La notation ‹P› (guillemets francais) permet de faire reference a une hypothese du contexte de type P sans la nommer.

La notation ‹P› — auto-nommer une hypothèse par son type

La cellule de droite prouve bracket_example : p → q → p ∧ q en utilisant ‹q› et ‹p ∧ q› pour auto-nommer les hypothèses. Cette notation, introduite avec Lean 4, est une commodité syntaxique :

  1. ‹P› cherche une hypothèse de type P dans le contexte. Si une hypothèse h a exactement le type P, on peut écrire ‹P› au lieu de h. Lean unifie automatiquement. C’est particulièrement utile quand le nom importe peu mais que le type est caractéristique.
  2. Quand l’utiliser. Quand plusieurs hypothèses ont des types distincts et qu’on veut éviter assumption (Lean-5) ou exact ‹P› pour invoquer l’hypothèse « évidente ». Lean-14 utilise ‹∀ n, _› pour récupérer une hypothèse universellement quantifiée.
  3. Limitation. Si plusieurs hypothèses ont des types unifiables, ‹P› est ambigu. Lean refusera l’ambiguïté — il faut alors nommer explicitement.

Le pont : Lean-12 (sensibilité) utilise ‹_› (placeholder) avec by assumption ou exact ‹_› pour fermer des sous-objectifs évidents. Lean-14 (Finiteness) utilise ‹0 < n› pour récupérer une hypothèse de positivité. La notation est sugar — comprendre le mécanisme (assumption interne) aide à debugger.

-- Utilisation de ‹›
theorem bracket_example (p q : Prop) (hp : p) (hq : q) : p /\ q :=
  ⟨‹p›, ‹q›⟩   -- Reference les hypotheses par leur type

-- Plus complexe
theorem bracket_complex (p q r : Prop)
  (hpq : p -> q) (hqr : q -> r) : p -> r :=
  fun hp : p =>
    have : q := hpq ‹p›
    have : r := hqr ‹q›
    ‹r›
-- Utilisation de ‹›
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  ⟨‹p›, ‹q›⟩   -- Reference les hypotheses par leur type
-- Plus complexe
theorem bracket_complex (p q r : Prop)
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  fun hp : p =>
    have : q := hpq ‹p›
    have : r := hqr ‹q›
    ‹r›
--% env 12
Raw input {"cmd": "-- Utilisation de \u2039\u203a\ntheorem bracket_example (p q : Prop) (hp : p) (hq : q) : p /\\ q :=\n \u27e8\u2039p\u203a, \u2039q\u203a\u27e9 -- Reference les hypotheses par leur type\n\n-- Plus complexe\ntheorem bracket_complex (p q r : Prop)\n (hpq : p -> q) (hqr : q -> r) : p -> r :=\n fun hp : p =>\n have : q := hpq \u2039p\u203a\n have : r := hqr \u2039q\u203a\n \u2039r\u203a", "env": 11}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 43}, "endPos": {"line": 2, "column": 44}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 7, "column": 7}, "endPos": {"line": 7, "column": 8}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 12}

5.3 Suppositions avec assume/fun

En Lean 4, on utilise fun pour introduire une hypothese dans une preuve par termes. C’est equivalent a assume en Lean 3 ou intro en mode tactique.

assume / fun — introduction de prémisses en lambda-style

La cellule de droite prouve assume_example1 : p → q → p par fun hp _ => hp (et assume_example2 par assume hp hq hp). Deux choses à comprendre :

  1. fun hp _ => hp est la curryfication en acte. Le théorème p → q → p est (hp : p) → (hq : q) → p. La preuve fun-style prend deux arguments (hp et un _ ignoré) et retourne hp. Le _ est l’argument ignoré : on reçoit hq : q mais on ne l’utilise pas (d’où le _). Lean-12 fait pareil dans la preuve de S(f, n, k) = 0 où certaines hypothèses sont introduites pour nommer le contexte mais inutilisées dans la branche considérée.
  2. assume est l’alternative tactic-style. assume hp hq est équivalent à fun hp hq => … (introduction de plusieurs prémisses en tactic-style). Lean-5 unifie les deux : intro (tactic-style) et fun/assume (lambda-style) sont interchangeables.
  3. Quand utiliser l’un ou l’autre. Idiomatique : intro/apply en tactic-style pour les preuves non triviales, fun/=> en lambda-style pour les preuves courtes. La cellule de droite mélange les deux pour montrer l’équivalence — c’est purement pédagogique.

Le pont : Lean-12 (sensibilité) ouvre ses preuves par intro f n k h₁ h₂ h₃ (tactic-style, 5+ introductions) ou fun f n k h₁ h₂ h₃ => … (lambda-style). Les deux formes sont équivalentes. Lean-14 (Finiteness) préfère tactic-style pour les preuves longues. Lean-16b (Game of Life) souvent lambda-style pour les lemmes courts.

-- Les deux syntaxes sont equivalentes
theorem assume_example1 (p q : Prop) : p -> q -> p :=
  fun hp _hq => hp

-- Avec annotation de type
theorem assume_example2 (p q : Prop) : p -> q -> p :=
  fun (hp : p) (_hq : q) => hp

-- Avec destructuration
theorem assume_destruct (p q : Prop) : p /\ q -> q /\ p :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩
-- Les deux syntaxes sont equivalentes
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  fun hp _hq => hp
-- Avec annotation de type
theorem assume_example2 (p q : Prop) : p -> q -> p :=
  fun (hp : p) (_hq : q) => hp
-- Avec destructuration
theorem assume_destruct (p q : Prop) : p /\ q -> q /\ p :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩
--% env 13
Raw input {"cmd": "-- Les deux syntaxes sont equivalentes\ntheorem assume_example1 (p q : Prop) : p -> q -> p :=\n fun hp _hq => hp\n\n-- Avec annotation de type\ntheorem assume_example2 (p q : Prop) : p -> q -> p :=\n fun (hp : p) (_hq : q) => hp\n\n-- Avec destructuration\ntheorem assume_destruct (p q : Prop) : p /\\ q -> q /\\ p :=\n fun \u27e8hp, hq\u27e9 => \u27e8hq, hp\u27e9", "env": 12}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 29}, "endPos": {"line": 2, "column": 30}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 35}, "endPos": {"line": 2, "column": 36}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 13}

## 6. Égalité et Quantificateurs

6.1 Réécriture avec l’égalité

Appliquer une hypothèse universelle ou transporter une preuve

La cellule suivante montre deux opérations distinctes :

  1. subst_in_forall applique directement une hypothèse universelle. À partir de hp : ∀ n : Nat, P n, on obtient P b par hp b. L’hypothèse _h : a = b n’est pas utilisée : hp fournit déjà la propriété pour tout naturel, y compris b. Malgré son nom, ce théorème ne réécrit pas sous un quantificateur.
  2. subst_prop transporte une preuve le long d’une égalité. À partir de h : a = b et hp : P a, le terme h ▸ hp prouve P b. Ici, contrairement au premier théorème, l’égalité est nécessaire. Le symbole ▸ exprime le transport de P a vers P b.
  3. Lien avec les tactiques. rw [h] réécrit la cible courante et subst remplace une variable égale dans la cible et le contexte. Ces tactiques seront étudiées dans Lean-5 ; la cellule présente utilise hp b et ▸, pas rw ni subst.

La distinction se vérifie en changeant mentalement a sans changer b : dans subst_in_forall, hp b reste disponible quelle que soit l’égalité fournie. Dans subst_prop, hp ne prouve initialement que P a ; pour conclure P b, il faut relier précisément les deux indices par h. L’égalité n’est donc pas une étape interchangeable entre les deux preuves.

Le pont vers la partie haute : reconnaître si l’égalité est réellement nécessaire évite de compliquer une preuve déjà couverte par une hypothèse universelle.

-- Substitution dans un forall
theorem subst_in_forall (P : Nat -> Prop) (a b : Nat)
  (_h : a = b) (hp : forall n, P n) : P b :=
  hp b   -- Direct, pas besoin de h ici

-- Mais si on a P a et a = b, on peut avoir P b
theorem subst_prop (P : Nat -> Prop) (a b : Nat)
  (h : a = b) (hp : P a) : P b :=
  h ▸ hp   -- Substitution avec le triangle
-- Substitution dans un forall
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  (_h : a = b) (hp : forall n, P n) : P b :=
  hp b   -- Direct, pas besoin de h ici
-- Mais si on a P a et a = b, on peut avoir P b
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  (h : a = b) (hp : P a) : P b :=
  h ▸ hp   -- Substitution avec le triangle
--% env 14
Raw input {"cmd": "-- Substitution dans un forall\ntheorem subst_in_forall (P : Nat -> Prop) (a b : Nat)\n (_h : a = b) (hp : forall n, P n) : P b :=\n hp b -- Direct, pas besoin de h ici\n\n-- Mais si on a P a et a = b, on peut avoir P b\ntheorem subst_prop (P : Nat -> Prop) (a b : Nat)\n (h : a = b) (hp : P a) : P b :=\n h \u25b8 hp -- Substitution avec le triangle", "env": 13}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 37}, "endPos": {"line": 2, "column": 38}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 7, "column": 6}, "endPos": {"line": 7, "column": 7}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 14}

Cette preuve illustre la substitution sous un quantificateur : de l’égalité a = b et de l’hypothese universelle ∀ n, P n, on derive P b (appliquer hp, puis reecrire par l’égalité). C’est le patron standard intro puis rw pour faire traverser une égalité sous un binder – technique omnipresente dans les preuves sur les structures parametrees.

L’extension de l’égalité sous quantificateur — le transport ▸

La cellule de droite illustre la substitution sous un quantificateur : ∀ x, P x a et a = b donnent ∀ x, P x b. La preuve utilise intro h ha x; exact ha x ▸ h :

  1. Pattern ha x ▸ h. ha x : P x a est la preuve de P x a (appliquée à x). h : a = b est l’égalité. ha x ▸ h est le transport : Lean substitue a par b dans le type de ha x pour obtenir ha x : P x b. C’est la conversion de type : si a = b et ha : P a, alors ha ▸ h : P b (signalée par ▸).
  2. Pourquoi un symbole spécial ▸. C’est la notale d’extensionnalité de HoTT (Homotopy Type Theory) : la preuve de a = b est un chemin qui transporte toute propriété de a à b. Lean 4 l’utilise pour rendre les preuves par transport lisibles : ha x ▸ h se lit « le long de h, transporter ha x ».
  3. Restriction : ▸ ne fonctionne que si toutes les occurrences de a dans le type de ha x peuvent être remplacées par b. Si a apparaît librement dans P x a (par exemple P : Nat → Type), Lean refusera — il faut une preuve de congruence.

Le pont : Lean-12 (sensibilité) utilise ▸ pour transporter des preuves d’inégalités après une substitution de variables. Lean-14 (Finiteness) utilise ▸ pour propager des bornes à travers des égalités. Lean-16b (Game of Life) utilise ▸ pour transporter des invariants entre états. Le pattern ha ▸ h est idiomatique et plus élégant que subst h quand la portée est limitée.

6.2 Égalité fonctionnelle### Pourquoi l’extensionnalité fonctionnelle est un axiome

L’extensionnalité fonctionnelle énonce : ∀ f g : A → B, (∀ x, f x = g x) → f = g. Informellement : deux fonctions qui coïncident sur tous les arguments sont égales. C’est l’axiome funext de Lean 4 (constante dans Lean.Extensionality). Lean-2 a introduit rfl pour l’égalité définitionnelle ; funext étend rfl à l’égalité propositionnelle des fonctions.

Pourquoi c’est un axiome, pas un théorème. Prouver funext demanderait de raisonner sur l’égalité de fonctions en termes de bêta-réduction. La question : « si f x = g x pour tout x, est-ce que f = g ? » — la réponse dépend du statut de l’extensionalité dans la théorie des types. En théorie des types intuitionniste (ITT), funext n’est pas dérivable : il faut l’ajouter comme axiome. Lean 4 l’ajoute par défaut (funext est déclarée dans Lean.Extensionality).

Le pont vers la partie haute : Lean-12 (sensibilité) utilise funext 2 fois dans sa preuve de la formule. Lean-14 (Finiteness) utilise funext pour étendre l’égalité de fonctions à l’égalité de leurs dérivées. Lean-16b (Game of Life) utilise funext pour prouver que deux automates équivalents sont égaux. Le pattern funext x; show f x = g x; exact h x est l’idiome standard.

-- Deux fonctions sont egales si elles ont les memes valeurs
-- C'est l'extensionnalite fonctionnelle
#check @funext  -- funext : (forall x, f x = g x) -> f = g

-- Exemple
def f (n : Nat) : Nat := n + 0
def g (n : Nat) : Nat := n

theorem f_eq_g : f = g :=
  funext (fun n => Nat.add_zero n)
-- Deux fonctions sont egales si elles ont les memes valeurs
-- C'est l'extensionnalite fonctionnelle
 @funext : ∀ {α : Sort u_1} {β : α → Sort u_2} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
-- Exemple
def f (n : Nat) : Nat := n + 0
def g (n : Nat) : Nat := n
theorem f_eq_g : f = g :=
  funext (fun n => Nat.add_zero n)
--% env 15
Raw input {"cmd": "-- Deux fonctions sont egales si elles ont les memes valeurs\n-- C'est l'extensionnalite fonctionnelle\n#check @funext -- funext : (forall x, f x = g x) -> f = g\n\n-- Exemple\ndef f (n : Nat) : Nat := n + 0\ndef g (n : Nat) : Nat := n\n\ntheorem f_eq_g : f = g :=\n funext (fun n => Nat.add_zero n)", "env": 14}
Raw output {"messages": [{"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@funext : ∀ {α : Sort u_1} {β : α → Sort u_2} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g"}], "env": 15}

L’extensionnalite fonctionnelle (funext) est un axiome de Lean : deux fonctions f g : A -> B sont egales des qu’elles coincident pointwise (∀ x, f x = g x). Ce n’est PAS demonstrable a partir des autres axiomes – dans le calcul des constructions, deux fonctions fun x => ... syntaxtiquement différentes mais extensionnellement egales ne sont pas rfl. funext est l’outil pour egaliser de telles fonctions ; sans lui, l’unicite ne vaudrait que pour les fonctions syntaxiquement identiques.

Le statut axiomatique de funext — implication pour la grosseillerie

Mathlib 4 contient une seule axiomatique explicite : propext (extensionnalité des propositions) et funext (extensionnalité des fonctions). Toutes les autres « lois » sont des théorèmes prouvés dans le système. La présence de funext a trois conséquences pédagogiques :

  1. L’égalité devient riche. Sans funext, l’égalité de deux fonctions f = g ne peut être prouvée que par rfl après bêta-réduction complète (rarement praticable pour des fonctions définies par match). Avec funext, on prouve ∀ x, f x = g x puis on applique funext pour obtenir f = g. C’est le passage à l’extensionnel.
  2. Deux niveaux de preuve. Sans funext : preuves définitionnelles uniquement (réduction symbolique). Avec funext : preuves propositionnelles (on prouve une proposition ∀ x, f x = g x, puis on extrait f = g). Lean-14 (Finiteness) exploite intensivement le niveau propositionnel pour les dérivées de fonctions définies par match.
  3. Coq vs Lean. En Coq, funext est aussi un axiome, mais la tactique extensionality est plus difficile à déclencher. Lean 4 unifie via funext x; … qui est très lisible.

Le pont vers la partie haute : Lean-12 (sensibilité) utilise funext f pour étendre l’égalité de deux fonctions booléennes B : BFun, puis prouve ∀ n, f n = g n cas par cas. Lean-14 (Finiteness) utilise funext x pour étendre l’égalité de dérivées successives. Lean-16b (Game of Life) utilise funext pour prouver l’équivalence de deux automates. Le pattern est constant.

## 7. Exemples Complets

7.1 Propriétés de divisibilite

Divisibilité — la définition existentielle

La cellule de droite définit divides (a b : Nat) : Prop := ∃ k : Nat, b = a * k. Trois observations :

  1. Pourquoi ∃ et pas ∀. « a divise b » signifie « il existe un k tel que b = a * k ». C’est une définition existentielle : pour utiliser h : a ∣ b, on extrait un témoin k : Nat et une preuve h : b = a * k. Le symbole ∣ (U+2223) est la notation Unicode pour divides.
  2. Notation ∃ k : Nat, b = a * k vs Σ k : Nat, b = a * k. Ces deux notations sont équivalentes : ∃ est l’habitant (preuve) tandis que Σ est le type sous-jacent. Pour les propositions, on utilise ∃ (notation logique) ; pour les paires, on utilise Σ (notation type-theorique). Quand P est Prop, ∃ x : A, P x et Σ x : A, P x sont le même type.
  3. Pourquoi la définition est sur Nat. La définition divides a b := ∃ k, b = a * k fonctionne pour Nat car la multiplication est totale. Pour Int, on ajoute souvent une condition de signe (∃ k : Nat, b = a * k ∨ b = -a * k pour rendre la divisibilité symétrique). Lean-14 (Finiteness) utilise la divisibilité pour raisonner sur les zéros de fonctions polynomiales.

Le pont : Lean-14 (Finiteness) prouve ∃ n : Nat, 0 < n ∧ n ∣ f.n (existence d’un diviseur positif). Lean-12 (sensibilité) évite la divisibilité (ses preuves sont sur les sommes booléennes). Lean-16b (Game of Life) l’utilise pour les automates périodiques. La forme ∃ k, … est universelle en théorie des nombres.

-- Définition : a divise b
def divides (a b : Nat) : Prop := ∃ k : Nat, b = a * k

notation:50 a " | " b => divides a b

-- Tout nombre divise 0
theorem divides_zero (a : Nat) : a | 0 :=
  ⟨0, (Nat.mul_zero a).symm⟩

-- 1 divise tout nombre
theorem one_divides (a : Nat) : 1 | a :=
  ⟨a, (Nat.one_mul a).symm⟩

-- Reflexivite : a | a
theorem divides_refl (a : Nat) : a | a :=
  ⟨1, (Nat.mul_one a).symm⟩
-- Definition : a divise b
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
notation:50 a " | " b => divides a b
-- Tout nombre divise 0
theorem divides_zero (a : Nat) : a | 0 :=
  ⟨0, (Nat.mul_zero a).symm⟩
-- 1 divise tout nombre
theorem one_divides (a : Nat) : 1 | a :=
  ⟨a, (Nat.one_mul a).symm⟩
-- Reflexivite : a | a
theorem divides_refl (a : Nat) : a | a :=
  ⟨1, (Nat.mul_one a).symm⟩
--% env 16
Raw input {"cmd": "-- Definition : a divise b\ndef divides (a b : Nat) : Prop := \u2203 k : Nat, b = a * k\n\nnotation:50 a \" | \" b => divides a b\n\n-- Tout nombre divise 0\ntheorem divides_zero (a : Nat) : a | 0 :=\n \u27e80, (Nat.mul_zero a).symm\u27e9\n\n-- 1 divise tout nombre\ntheorem one_divides (a : Nat) : 1 | a :=\n \u27e8a, (Nat.one_mul a).symm\u27e9\n\n-- Reflexivite : a | a\ntheorem divides_refl (a : Nat) : a | a :=\n \u27e81, (Nat.mul_one a).symm\u27e9", "env": 15}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 45}, "endPos": {"line": 2, "column": 46}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 16}

La divisibilite est encodee existentiellement : a ∣ b signifie « il existe un entier k tel que b = a * k ». Cette définition pose divides comme une proposition (Prop), pas un booléen – c’est un outil de raisonnement. La notation infixe a ∣ b (caractère ∣, U+2223) se lit « a divise b ». Pour prouver a ∣ b, on fournit le temoin k ; pour l’utiliser, on extrait k par analyse de l’existence.

Utilisation de divides — extraction de témoin et projection

La cellule de droite montre comment utiliser une preuve h : a ∣ b : on extrait un témoin k : Nat et une preuve h_eq : b = a * k. Le pattern d’élimination est :

  1. Extraction par obtain. obtain ⟨k, h_eq⟩ := h extrait le témoin k : Nat et la preuve h_eq : b = a * k dans le contexte. C’est la forme sugar pour cases h with | intro k h_eq => …. Lean-14 (Finiteness) utilise obtain ⟨n, hn⟩ := h dans 50% de ses preuves.
  2. Réécriture avec h_eq. Une fois h_eq : b = a * k, on peut l’utiliser pour réécrire b en a * k dans n’importe quel objectif. rw [h_eq] ou subst h_eq (si b n’apparaît plus que dans un seul endroit). Lean-14 (Finiteness) utilise rw [h_eq] pour substituer b dans les bornes de Finiteness.
  3. Pourquoi la définition est utile. ∃ k : Nat, b = a * k équivaut à « b est un multiple de a », mais la formulation ∃ rend la preuve algorithmiquement vérifiable : pour prouver h : a ∣ b, il suffit de donner un k et de prouver b = a * k (par rfl ou omega). Lean-14 fait use 0 (zéro divise tout) ou use b (tout divise lui-même) dans les preuves de Finiteness.

Le pont : Lean-14 (Finiteness) prouve ∃ n : Nat, 0 < n ∧ n ∣ f n en exhibant un diviseur positif. Lean-12 (sensibilité) n’utilise pas la divisibilité. Lean-16b (Game of Life) l’utilise pour les oscillations périodiques (période = diviseur du temps). Le pattern obtain ⟨k, hk⟩ := h est universel.

7.2 Transitivite de la divisibilite### Transitivité de la divisibilité — composition de témoins

La transitivité de la divisibilité s’écrit : a ∣ b → b ∣ c → a ∣ c. Pour la prouver, on décompose les deux hypothèses h₁ : a ∣ b et h₂ : b ∣ c, on obtient les témoins k₁ et k₂, et on compose : a ∣ c est prouvé par le témoin k₁ * k₂ car c = b * k₂ = (a * k₁) * k₂ = a * (k₁ * k₂) (par associativité de *).

Cette preuve est un microcosme : la transitivité est la composition des témoins. C’est le même pattern que Lean-3 (transitivité de l’implication : (p → q) → (q → r) → p → r, qui compose les preuves). Pour les propositions, on compose les preuves. Pour les valeurs existentielles, on compose les témoins. La structure est identique.

-- Définition rappel (necessaire si cellule executee isolement)
def mydivides (a b : Nat) : Prop := ∃ k : Nat, b = a * k
infix:50 " mydiv " => mydivides

-- Si a mydiv b et b mydiv c alors a mydiv c
theorem divides_trans (a b c : Nat)
  (hab : a mydiv b) (hbc : b mydiv c) : a mydiv c :=
  match hab, hbc with
  | ⟨k1, hk1⟩, ⟨k2, hk2⟩ =>
    ⟨k1 * k2, calc c = b * k2       := hk2
                   _ = (a * k1) * k2 := congrArg (· * k2) hk1
                   _ = a * (k1 * k2) := Nat.mul_assoc a k1 k2⟩
-- Definition rappel (necessaire si cellule executee isolement)
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
infix:50 " mydiv " => mydivides
-- Si a mydiv b et b mydiv c alors a mydiv c
theorem divides_trans (a b c : Nat)
  (hab : a mydiv b) (hbc : b mydiv c) : a mydiv c :=
  match hab, hbc with
  | ⟨k1, hk1⟩, ⟨k2, hk2⟩ =>
    ⟨k1 * k2, calc c = b * k2       := hk2
                   _ = (a * k1) * k2 := congrArg (· * k2) hk1
                   _ = a * (k1 * k2) := Nat.mul_assoc a k1 k2⟩
--% env 17
Raw input {"cmd": "-- Definition rappel (necessaire si cellule executee isolement)\ndef mydivides (a b : Nat) : Prop := \u2203 k : Nat, b = a * k\ninfix:50 \" mydiv \" => mydivides\n\n-- Si a mydiv b et b mydiv c alors a mydiv c\ntheorem divides_trans (a b c : Nat)\n (hab : a mydiv b) (hbc : b mydiv c) : a mydiv c :=\n match hab, hbc with\n | \u27e8k1, hk1\u27e9, \u27e8k2, hk2\u27e9 =>\n \u27e8k1 * k2, calc c = b * k2 := hk2\n _ = (a * k1) * k2 := congrArg (\u00b7 * k2) hk1\n _ = a * (k1 * k2) := Nat.mul_assoc a k1 k2\u27e9", "env": 16}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 2, "column": 4}, "endPos": {"line": 2, "column": 5}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 10}, "endPos": {"line": 2, "column": 11}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 17}

La transitivite (a ∣ b -> b ∣ c -> a ∣ c) se prouve en deroulant la définition existentielle : si b = a * k et c = b * j, alors c = a * (k * j), et le temoin final est k * j. C’est le patron universel des transitivites sur relations définies par existence : combiner les temoins. La recurrence sur la structure des hypotheses produit mecaniquement le temoin composite.

divides — clôture par composition multiplicative

La cellule de droite prouve divides_trans : a ∣ b → b ∣ c → a ∣ c par décomposition et composition de témoins. Étape par étape :

  1. Décomposition des hypothèses. h_ab : ∃ k₁, b = a * k₁ et h_bc : ∃ k₂, c = b * k₂. Par obtain, on extrait k₁ : Nat avec h₁ : b = a * k₁, et k₂ : Nat avec h₂ : c = b * k₂.
  2. Candidat composé. Pour a ∣ c, on devine k := k₁ * k₂. Il faut prouver c = a * (k₁ * k₂).
  3. Réécriture en chaîne. c = b * k₂ (par h₂) = (a * k₁) * k₂ (par h₁) = a * (k₁ * k₂) (par Nat.mul_assoc). Lean fait la chaîne automatiquement si on lui donne les bonnes hints (rw [h₂, h₁, Nat.mul_assoc]).
  4. Conclusion. use k₁ * k₂ exhibe le témoin composé. La preuve est complètement calculatoire : aucune induction, aucune récurrence — juste de la réécriture.

Le pont vers la partie haute : Lean-14 (Finiteness) prouve la transitivité de ∣ comme lemme auxiliaire. Lean-12 (sensibilité) ne l’utilise pas. Lean-16b (Game of Life) l’utilise pour prouver la périodicité de certains oscillateurs. Le pattern « décomposition puis composition des témoins » est universel pour les relations définies existentiellement.

8. Exercices

Exercice 1 : Prouver l’existence

Stratégies pour les exercices d’existence

Les exercices 1-3 utilisent des constructions croisées : ∃/∀/∧/→. Trois stratégies à connaître :

  1. Pour ∃ x, P x : exhiber un témoin x₀ puis prouver P x₀. Pattern : use x₀; exact preuve_de_P_x₀ ou ⟨x₀, preuve⟩. Lean-5 introduit use comme tactique dédiée.
  2. Pour ∀ x, P x : introduire x puis prouver P x. Pattern : intro x; exact preuve_de_P_x ou fun x => preuve_de_P_x. Lean-5 unifie en intro.
  3. Pour ∀ x, P x ∧ Q x : introduire x puis prouver les deux par exact ⟨preuve_P, preuve_Q⟩ ou constructor; exact …. Lean-14 (Finiteness) utilise refine ⟨_, h_bound⟩ pour raffiner une conjonction implicite.

Piège classique : croire qu’on peut prouver ∃ x, P x sans témoin. En intuitionniste, non. Si la cellule propose ∃ n : Nat, n > 5, il faut donner un n (par exemple 6) et prouver 6 > 5. Pas de « par l’absurde » sans Classical.em (Lean-3 section 9).

Le pont : Lean-14 (Finiteness) utilise ces patterns dans chaque lemme. Lean-12 (sensibilité) utilise ∃/∀/∧/→ dans 80% de ses preuves. Lean-16b (Game of Life) idem. Les exercices 1-3 sont conçus pour pratiquer les patterns fondamentaux.

-- Utilise la notation `divides` de la cellule precedente
-- Prouver qu'il existe un nombre pair (divisible par 2)
-- Rappel : def divides (a b : Nat) : Prop := ∃ k, b = a * k
theorem exists_even : ∃ n : Nat, divides 2 n := sorry
-- Utilise la notation `divides` de la cellule precedente
-- Prouver qu'il existe un nombre pair (divisible par 2)
-- Rappel : def divides (a b : Nat) : Prop := ∃ k, b = a * k
🟨 declaration uses `sorry`
--% env 18
--% prove 0
Raw input {"cmd": "-- Utilise la notation `divides` de la cellule precedente\n-- Prouver qu'il existe un nombre pair (divisible par 2)\n-- Rappel : def divides (a b : Nat) : Prop := \u2203 k, b = a * k\ntheorem exists_even : \u2203 n : Nat, divides 2 n := sorry", "env": 17}
Raw output {"sorries": [{"proofState": 0, "pos": {"line": 4, "column": 48}, "goal": "⊢ ∃ n, 2 | n", "endPos": {"line": 4, "column": 53}}], "messages": [{"severity": "warning", "pos": {"line": 4, "column": 8}, "endPos": {"line": 4, "column": 19}, "data": "declaration uses `sorry`"}], "env": 18}

Corrige — rendu PR #2586 (@Nchpg)

Temoin : 4. Preuve : 4 = 2 * 2 par rfl. La paire angle brackets ⟨4, ⟨2, rfl⟩⟩ fournit le temoin existentiel et la preuve que divides 2 4.

Exemple guide — corrigé exists_even

Le corrigé (PR #2586 par @Nchpg) prouve exists_even : ∃ n : Nat, Even n par use 4. La preuve est triviale : Even 4 est ∃ k, 4 = 2 * k, soit ⟨2, rfl⟩. Lean-14 (Finiteness) utilise le même pattern pour ∃ n : Nat, 0 < n ∧ n ∣ f.n : choisir un diviseur positif de f.n et prouver l’égalité.

Le pont : ce corrigé est un exemple minimal d’introduction du ∃. Lean-12 (sensibilité) prouve des ∃ plus complexes (témoin = une combinaison d’indices). Lean-14 (Finiteness) prouve ∃ avec des témoins calculés. Lean-16b (Game of Life) prouve ∃ avec des états construits. Le pattern use x₀; exact preuve est universel.

-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de exists_even en term-mode
-- Rappel : def divides (a b : Nat) : Prop := ∃ k, b = a * k
theorem exists_even_corrige : ∃ n : Nat, divides 2 n :=
  ⟨4, ⟨2, rfl⟩⟩

#eval "Corrige Exercice 1 : exists_even prouve (temoin 4, 4 = 2 * 2)"
-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de exists_even en term-mode
-- Rappel : def divides (a b : Nat) : Prop := ∃ k, b = a * k
theorem exists_even_corrige : ∃ n : Nat, divides 2 n :=
  ⟨4, ⟨2, rfl⟩⟩
 "Corrige Exercice 1 : exists_even prouve (temoin 4, 4 = 2 * 2)"
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
--% env 19
Raw input {"cmd": "-- Corrige \u2014 rendu PR #2586 (@Nchpg)\n-- Preuve de exists_even en term-mode\n-- Rappel : def divides (a b : Nat) : Prop := \u2203 k, b = a * k\ntheorem exists_even_corrige : \u2203 n : Nat, divides 2 n :=\n \u27e84, \u27e82, rfl\u27e9\u27e9\n\n#eval \"Corrige Exercice 1 : exists_even prouve (temoin 4, 4 = 2 * 2)\"", "env": 18}
Raw output {"messages": [{"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 5}, "data": "\"Corrige Exercice 1 : exists_even prouve (temoin 4, 4 = 2 * 2)\""}, {"severity": "warning", "pos": {"line": 7, "column": 2}, "endPos": {"line": 7, "column": 3}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}], "env": 19}

Exercice 2 : Manipulation de forall

Stratégies pour les exercices de manipulation de forall

L’exercice 2 teste la curryfication et l’évidement d’un ∀ x, P x ∧ Q x. Trois patterns :

  1. Pour ∀ x, P x ∧ Q x, curryfier : ∀ x, P x ∧ ∀ x, Q x (par deux intro). La curryfication est équivalence : ∀ x, P x ∧ Q x ↔︎ (∀ x, P x) ∧ (∀ x, Q x). Lean-14 (Finiteness) utilise cette curryfication pour raisonner sur des conditions multiples.
  2. Pour ∀ x, P x → Q x, introduire x et h : P x, puis prouver Q x. Pattern : intro x h; exact preuve_de_Q_x_en_utilisant_h. Lean-12 (sensibilité) utilise ce pattern dans sa preuve de la formule.
  3. Pour (∀ x, P x) → R, curryfier : ∀ x, P x → R. C’est la curryfication appliquée aux preuves. Lean-3 (transitivité) utilise ce pattern.
-- Si P est vrai pour tout x et Q aussi, alors P /\ Q pour tout x
variable (A : Type) (P Q : A -> Prop)

theorem forall_conjunction :
  (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\ Q x) := sorry
-- Si P est vrai pour tout x et Q aussi, alors P /\ Q pour tout x
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 declaration uses `sorry`
  (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\ Q x) := sorry
--% env 20
--% prove 1
Raw input {"cmd": "-- Si P est vrai pour tout x et Q aussi, alors P /\\ Q pour tout x\nvariable (A : Type) (P Q : A -> Prop)\n\ntheorem forall_conjunction :\n (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\\ Q x) := sorry", "env": 19}
Raw output {"sorries": [{"proofState": 1, "pos": {"line": 5, "column": 78}, "goal": "A : Type\nP Q : A → Prop\n⊢ (∀ (x : A), P x) → (∀ (x : A), Q x) → ∀ (x : A), P x ∧ Q x", "endPos": {"line": 5, "column": 83}}], "messages": [{"severity": "warning", "pos": {"line": 2, "column": 2}, "endPos": {"line": 2, "column": 3}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 4, "column": 8}, "endPos": {"line": 4, "column": 26}, "data": "declaration uses `sorry`"}], "env": 20}

Corrige — rendu PR #2586 (@Nchpg)

Preuve term-mode : on introduit les deux hypotheses hp et hq, puis pour chaque x on construit la paire ⟨hp x, hq x⟩.

Exemple guide — corrigé forall_conjunction

Le corrigé (PR #2586 par @Nchpg) prouve forall_conjunction : (∀ x, P x) ∧ (∀ x, Q x) → ∀ x, P x ∧ Q x par curryfication successive : intro h; cases h with | intro hP hQ => fun x => And.intro (hP x) (hQ x). Étapes :

  1. Introduction initiale : intro h met h : (∀ x, P x) ∧ (∀ x, Q x) dans le contexte.
  2. Décomposition : cases h extrait hP : ∀ x, P x et hQ : ∀ x, Q x.
  3. Curryfication : fun x => … construit la fonction de ∀ x, P x ∧ Q x.
  4. Construction de la conjonction : And.intro (hP x) (hQ x) donne la paire de preuves P x et Q x.

Remarque : la preuve est symétrique en P et Q. Mathlib 4 fournit forall_and comme lemme prédéfini. Lean-14 (Finiteness) utilise forall_and pour curryfier ses conditions de Finiteness.

Le pont : ce corrigé montre la symétrie introduction/élimination de ∧ (Lean-3) combinée à la curryfication des ∀ (Lean-4). Lean-12 (sensibilité) utilise cette combinaison 20+ fois dans sa preuve.

-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de forall_conjunction en term-mode
variable (A : Type) (P Q : A -> Prop)

theorem forall_conjunction_corrige :
  (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\ Q x) :=
  fun hp hq x => ⟨hp x, hq x⟩

#eval "Corrige Exercice 2 : forall_conjunction prouve"
-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de forall_conjunction en term-mode
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
theorem forall_conjunction_corrige :
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  fun hp hq x => ⟨hp x, hq x⟩
 "Corrige Exercice 2 : forall_conjunction prouve"
--% env 21
Raw input {"cmd": "-- Corrige \u2014 rendu PR #2586 (@Nchpg)\n-- Preuve de forall_conjunction en term-mode\nvariable (A : Type) (P Q : A -> Prop)\n\ntheorem forall_conjunction_corrige :\n (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\\ Q x) :=\n fun hp hq x => \u27e8hp x, hq x\u27e9\n\n#eval \"Corrige Exercice 2 : forall_conjunction prouve\"", "env": 20}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 3, "column": 3}, "endPos": {"line": 3, "column": 4}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 5}, "endPos": {"line": 3, "column": 6}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 6, "column": 65}, "endPos": {"line": 6, "column": 66}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 5}, "data": "\"Corrige Exercice 2 : forall_conjunction prouve\""}], "env": 21}

Exercice 3 : Interaction exists/forall

Cet exercice est plus avance et utilise plusieurs concepts :

  1. [Inhabited A] : C’est une typeclass qui garantit que le type A possede au moins un élément (appele default). Sans cette contrainte, un type pourrait etre vide, et l’implication \neg(\forall x, P x) -> \exists x, \neg P x ne serait pas prouvable (on ne pourrait pas exhiber de temoin).

  2. byContradiction : Cette tactique (dans Classical) permet de prouver P en montrant que \neg P mene a une contradiction. C’est un principe de logique classique (pas disponible en logique constructive).

  3. Ordre des quantificateurs : L’implication inverse (\exists x, \neg P x) -> \neg(\forall x, P x) est prouvable constructivement (sans Classical).

Approfondissement — frontière existentielle/universelle

L’exercice 3 est plus avancé : prouver not_forall_exists_not : ¬∀ x, ¬P x → ∃ x, P x en logique classique (via Classical.em). La preuve classique :

  1. Hypothèse : h : ¬∀ x, ¬P x (il n’est pas vrai que pour tout x, ¬P x).
  2. Cible : ∃ x, P x.
  3. Étape classique : par Classical.em (∃ x, P x), soit ∃ x, P x est vrai (et on conclut), soit ¬∃ x, P x est vrai. Dans le second cas, par contraposée de De Morgan (Lean-3 section 9), ∀ x, ¬P x, ce qui contredit h. Donc ∃ x, P x.

Cette preuve utilise Classical.em (Lean-3 section 9) — qui est non-constructive : elle ne donne pas de témoin explicite. En logique intuitionniste, seul ¬¬∃ x, P x peut être prouvé (par la contraposée de ∀ x, P x → ¬∀ x, ¬P x). La distinction constructif/classique est tranchée par Lean-3 section 9.

Le corrigé (PR #2586 par @Nchpg) utilise byContradiction et Classical.em. Lean-14 (Finiteness) n’utilise PAS Classical.em (toutes ses preuves sont constructives, le témoin est explicite). Lean-12 (sensibilité) non plus. Lean-16b (Game of Life) parfois l’utilise pour raisonner sur l’existence d’un automate universel.

-- Prouver que negation de forall implique exists negation (classique)
open Classical
variable (A : Type) [Inhabited A] (P : A -> Prop)

theorem not_forall_exists_not :
  (¬ forall x : A, P x) -> (∃ x : A, ¬ P x) := sorry
-- Prouver que negation de forall implique exists negation (classique)
open Classical
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 declaration uses `sorry`
  (¬ forall x : A, P x) -> (∃ x : A, ¬ P x) := sorry
--% env 22
--% prove 2
Raw input {"cmd": "-- Prouver que negation de forall implique exists negation (classique)\nopen Classical\nvariable (A : Type) [Inhabited A] (P : A -> Prop)\n\ntheorem not_forall_exists_not :\n (\u00ac forall x : A, P x) -> (\u2203 x : A, \u00ac P x) := sorry", "env": 21}
Raw output {"sorries": [{"proofState": 2, "pos": {"line": 6, "column": 47}, "goal": "A : Type\ninst✝ : Inhabited A\nP : A → Prop\n⊢ (¬∀ (x : A), P x) → ∃ x, ¬P x", "endPos": {"line": 6, "column": 52}}], "messages": [{"severity": "warning", "pos": {"line": 3, "column": 1}, "endPos": {"line": 3, "column": 2}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 3}, "endPos": {"line": 3, "column": 4}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 21}, "endPos": {"line": 3, "column": 22}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 5, "column": 8}, "endPos": {"line": 5, "column": 29}, "data": "declaration uses `sorry`"}], "env": 22}

Corrigé — rendu PR #2586 (@Nchpg)

Preuve en mode terme utilisant byContradiction (logique classique). On suppose ¬∃ x, ¬P x, on en déduit ∀ x, P x, en contradiction avec l’hypothèse h.

Exemple guidé — corrigé (frontière constructif/classique)

Le corrigé prouve (¬ ∀ x : A, P x) → (∃ x : A, ¬ P x) dans not_forall_exists_not_corrige. Il ne prouve pas (¬ ∀ x, ¬ P x) → ∃ x, P x : la négation de P n’est pas au même endroit. La preuve emploie byContradiction sous open Classical, sans invoquer Classical.em explicitement :

  1. Nier la conclusion : avec h : ¬ ∀ x, P x, le byContradiction extérieur suppose hc : ¬ ∃ x, ¬ P x.
  2. Fixer un x : pour établir ∀ x, P x, la fonction fun x => ... prend un x arbitraire.
  3. Nier P x provisoirement : le byContradiction intérieur suppose hpx : ¬ P x. Le témoin ⟨x, hpx⟩ : ∃ x, ¬ P x contredit hc.
  4. Conclure : chaque P x est ainsi obtenu ; h appliqué à cette fonction donne la contradiction recherchée.

Le pont vers la partie haute : une preuve classique peut conclure sans exhiber directement le témoin de l’existence ; ici le code distingue précisément les deux négations imbriquées.

-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de not_forall_exists_not en term-mode
open Classical
variable (A : Type) [Inhabited A] (P : A -> Prop)

theorem not_forall_exists_not_corrige :
  (¬ forall x : A, P x) -> (∃ x : A, ¬ P x) :=
  fun h => byContradiction (fun hc => h (fun x => byContradiction (fun hpx => hc ⟨x, hpx⟩)))

#eval "Corrige Exercice 3 : not_forall_exists_not prouve"
-- Corrige — rendu PR #2586 (@Nchpg)
-- Preuve de not_forall_exists_not en term-mode
open Classical
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
theorem not_forall_exists_not_corrige :
  (¬ forall x : A, P x) -> (∃ x : A, ¬ P x) :=
🟨 automatically included section variable(s) unused in theorem `not_forall_exists_not_corrige`:
  [Inhabited A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Inhabited A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
 "Corrige Exercice 3 : not_forall_exists_not prouve"
--% env 23
Raw input {"cmd": "-- Corrige \u2014 rendu PR #2586 (@Nchpg)\n-- Preuve de not_forall_exists_not en term-mode\nopen Classical\nvariable (A : Type) [Inhabited A] (P : A -> Prop)\n\ntheorem not_forall_exists_not_corrige :\n (\u00ac forall x : A, P x) -> (\u2203 x : A, \u00ac P x) :=\n fun h => byContradiction (fun hc => h (fun x => byContradiction (fun hpx => hc \u27e8x, hpx\u27e9)))\n\n#eval \"Corrige Exercice 3 : not_forall_exists_not prouve\"", "env": 22}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 4, "column": 3}, "endPos": {"line": 4, "column": 4}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 4, "column": 5}, "endPos": {"line": 4, "column": 6}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 6, "column": 0}, "endPos": {"line": 8, "column": 92}, "data": "automatically included section variable(s) unused in theorem `not_forall_exists_not_corrige`:\n [Inhabited A]\nconsider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:\n omit [Inhabited A] in theorem ...\n\nNote: This linter can be disabled with `set_option linter.unusedSectionVars false`"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 5}, "data": "\"Corrige Exercice 3 : not_forall_exists_not prouve\""}], "env": 23}

Exercices supplémentaires à compléter

Les trois théorèmes de la cellule suivante sont des exercices non corrigés : leurs preuves sont laissées à compléter. Aucun exercice nommé mydivides'_trans_style n’y figure ; la transitivité de la divisibilité est présentée dans l’exemple de la section 7.2.

  1. exists_even_practice : exhiber un naturel divisible par 2 dans la notation locale mydiv'. L’indice du code suggère 4 ; il reste à fournir le témoin de sa divisibilité.
  2. forall_and_practice : à partir de deux preuves universelles, introduire x puis construire la conjonction P x ∧ Q x avec leurs applications à x.
  3. not_forall_exists_not_practice : refaire la preuve classique de l’exercice 3, dont le corrigé apparaît juste au-dessus. Veiller à la position des négations dans (¬ ∀ x, P x) → ∃ x, ¬ P x.

Les stubs marquent le travail restant aux étudiantes et étudiants ; ils ne doivent pas être présentés comme des démonstrations déjà établies.

-- Définition rappel pour exécution isolee
def mydivides' (a b : Nat) : Prop := exists k : Nat, b = a * k
infix:50 " mydiv' " => mydivides'

-- Exercice 1 : Existence d'un pair divisible par 2
-- TODO étudiant : prouver qu'il existe n tel que 2 mydiv' n
-- Indice : utiliser le temoin 4
theorem exists_even_practice : exists n : Nat, 2 mydiv' n := by
  sorry

-- Exercice 2 : Distribution du forall sur la conjonction
variable (A : Type) (P Q : A -> Prop)
-- TODO étudiant : prouver la distribution
-- Indice : utiliser fun hp hq x => <hp x, hq x>
theorem forall_and_practice :
  (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\ Q x) := by
  sorry

-- Exercice 3 : Negation du forall implique existence
-- TODO étudiant : prouver la contraposition
-- Indice : utiliser byContradiction
open Classical in
theorem not_forall_exists_not_practice
  (A : Type) [Inhabited A] (P : A -> Prop) :
  (not (forall x : A, P x)) -> (exists x : A, not (P x)) := by
  sorry
-- Definition rappel pour execution isolee
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `Q`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- Exercice 1 : Existence d'un pair divisible par 2
-- TODO etudiant : prouver qu'il existe n tel que 2 mydiv' n
-- Indice : utiliser le temoin 4
🟨 declaration uses `sorry`
  sorry
-- Exercice 2 : Distribution du forall sur la conjonction
variable (A : Type) (P Q : A -> Prop)
-- TODO etudiant : prouver la distribution
-- Indice : utiliser fun hp hq x => <hp x, hq x>
🟨 declaration uses `sorry`
  (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\ Q x) := by
  sorry
-- Exercice 3 : Negation du forall implique existence
-- TODO etudiant : prouver la contraposition
-- Indice : utiliser byContradiction
open Classical in
🟨 declaration uses `sorry`
  (A : Type) [Inhabited A] (P : A -> Prop) :
  (not (forall x : A, P x)) -> (exists x : A, not (P x)) := by
  sorry
--% env 24
--% prove 5
Raw input {"cmd": "-- Definition rappel pour execution isolee\ndef mydivides' (a b : Nat) : Prop := exists k : Nat, b = a * k\ninfix:50 \" mydiv' \" => mydivides'\n\n-- Exercice 1 : Existence d'un pair divisible par 2\n-- TODO etudiant : prouver qu'il existe n tel que 2 mydiv' n\n-- Indice : utiliser le temoin 4\ntheorem exists_even_practice : exists n : Nat, 2 mydiv' n := by\n sorry\n\n-- Exercice 2 : Distribution du forall sur la conjonction\nvariable (A : Type) (P Q : A -> Prop)\n-- TODO etudiant : prouver la distribution\n-- Indice : utiliser fun hp hq x => \ntheorem forall_and_practice :\n (forall x : A, P x) -> (forall x : A, Q x) -> (forall x : A, P x /\\ Q x) := by\n sorry\n\n-- Exercice 3 : Negation du forall implique existence\n-- TODO etudiant : prouver la contraposition\n-- Indice : utiliser byContradiction\nopen Classical in\ntheorem not_forall_exists_not_practice\n (A : Type) [Inhabited A] (P : A -> Prop) :\n (not (forall x : A, P x)) -> (exists x : A, not (P x)) := by\n sorry", "env": 23}
Raw output {"sorries": [{"proofState": 3, "pos": {"line": 9, "column": 2}, "goal": "⊢ ∃ n, mydivides' 2 n", "endPos": {"line": 9, "column": 7}}, {"proofState": 4, "pos": {"line": 17, "column": 2}, "goal": "A : Type\nP Q : A → Prop\n⊢ (∀ (x : A), P x) → (∀ (x : A), Q x) → ∀ (x : A), P x ∧ Q x", "endPos": {"line": 17, "column": 7}}, {"proofState": 5, "pos": {"line": 26, "column": 2}, "goal": "A : Type\ninst✝ : Inhabited A\nP : A → Prop\n⊢ (!decide (∀ (x : A), P x)) = true → ∃ x, (!decide (P x)) = true", "endPos": {"line": 26, "column": 7}}], "messages": [{"severity": "warning", "pos": {"line": 2, "column": 25}, "endPos": {"line": 2, "column": 26}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 31}, "endPos": {"line": 2, "column": 32}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 2, "column": 46}, "endPos": {"line": 2, "column": 47}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 1}, "endPos": {"line": 3, "column": 2}, "data": "unused variable `Q`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 15}, "endPos": {"line": 3, "column": 16}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 3, "column": 31}, "endPos": {"line": 3, "column": 32}, "data": "unused variable `P`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 8, "column": 8}, "endPos": {"line": 8, "column": 28}, "data": "declaration uses `sorry`"}, {"severity": "warning", "pos": {"line": 15, "column": 8}, "endPos": {"line": 15, "column": 27}, "data": "declaration uses `sorry`"}, {"severity": "warning", "pos": {"line": 23, "column": 8}, "endPos": {"line": 23, "column": 38}, "data": "declaration uses `sorry`"}], "env": 24}

Lire un théorème avec quantificateurs

Comme dans Lean-3 (cellule « Lire un théorème avant de le prouver »), le réflexe est statement d’abord, preuve ensuite. Avec les quantificateurs, la grille de lecture s’étend :

  1. Repérer tous les quantificateurs dans l’ordre où ils apparaissent — ∀ x : A, ∃ y : B, P x y est différent de ∃ y : B, ∀ x : A, P x y (cf. cellule 21 « Ordre des quantificateurs »).
  2. Lire les préconditions de gauche à droite : un ∀ est une hypothèse que la preuve peut utiliser (par application), un ∃ est une hypothèse que la preuve peut détruire (par obtain / match).
  3. Lire la conclusion : si elle commence par ∀, on construit une fonction (fun x => ...) ; si elle commence par ∃, on exhibe un témoin (use ...) ; sinon on prouve directement (exact ..., apply ...).
  4. Composer les garanties existantes : la transitivité de la divisibilité (cellule 38) est un archétype — on déroule deux existences pour en construire une troisième. Le pattern obtain ⟨k₁, hk₁⟩ := h₁; obtain ⟨k₂, hk₂⟩ := h₂; use k₁ * k₂; rw [hk₁, hk₂, Nat.mul_assoc] est universel.

Mise en garde : la cellule 32 (« Égalité fonctionnelle ») traite funext — un axiome. Le noyau de Lean ne vérifie pas funext, il l’accepte. Lire un théorème axiomatique, c’est aussi comprendre ce qu’on ne peut pas prouver en interne sans l’axiome. C’est une différence importante avec les théorèmes dont la preuve est constructive.

Ce guide complète Lean-3 (statement-first sans quantificateurs) et anticipe Lean-5 (classification par tactic d’ouverture : intro = ∀, use = ∃, obtain = destruction de ∃).

Resume

Concept Syntaxe Introduction Élimination
forall \forall x : A, P x fun x => ... Application h a
exists \exists x : A, P x ⟨temoin, preuve⟩ match h with \| ⟨x, hx⟩ => ...
have have h : P := ... Lemme intermediaire Reference par nom
this Reference anonyme Dernière hypothese this
‹P› Reference par type Hypothese de type P ‹P›

Points cles

  • forall est le Pi-type dans Prop - prouver = programmer une fonction
  • exists necessite un temoin + une preuve
  • L’ordre des quantificateurs est crucial
  • Les lemmes de Nat sont utiles pour l’arithmetique

Prochaine étape

Dans le notebook Lean-05-Tactics-Lean, nous decouvrirons le mode tactique qui permet de construire des preuves de maniere plus interactive, en decomposant les buts étape par étape.

Notebook base sur “TP - Z3 - Tweety - Lean.pdf” Section VI.B.3 et adapte pour Lean 4

Navigation : ← Lean-03-Propositions-Proofs-Lean | Index | Lean-05-Tactics-Lean →

Récapitulatif des quantificateurs — le tableau de référence

Le notebook couvre tous les quantificateurs de la logique du premier ordre : ∀ (introduction par intro/fun, élimination par apply/exact), ∃ (introduction par use/⟨_, _⟩, élimination par cases/obtain). Les lemmes Mathlib 4 (Nat.add_comm, Nat.add_assoc, Nat.mul_comm, Nat.mul_assoc) sont les briques de base des preuves arithmétiques. L’ordre des quantificateurs (∀∃ vs ∃∀) est toujours significatif. L’axiome funext étend l’égalité définitionnelle à l’égalité propositionnelle des fonctions. La divisibilité est un exemple de relation existentielle : a ∣ b := ∃ k, b = a * k.

Le pont vers la partie haute : Lean-4 est le carrefour entre Lean-3 (logique propositionnelle) et la pratique mathématique de Lean-12+ (preuves en analyse, topologie, théorie des nombres). Tous les notebooks appliqués utilisent ∀/∃/∃∀/hasSE/∀∃ massivement. Si vous sortez de Lean-4 sans maîtriser intro/apply/use/obtain, reprenez la cellule 1 puis revenez — c’est la base de tout.

Pour aller plus loin : Lean-5 introduit les tactiques (intro, apply, exact, use, obtain, cases, rw, omega, decide, simp) qui automatisent ces constructions. Lean-6 (Mathlib 4) introduit les bibliothèques sur les structures algébriques (+/*/≤/<). Lean-7 (LLM Integration) monte ces preuves à l’échelle LLM. Lean-4 est le plancher : tout le reste s’appuie dessus.

Retour au sommet