docs(notebooks,#16638): reaccent Lean-4 Quantifiers (filtre print C.2)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-4-Quantifiers.ipynb

@@ -24,13 +24,13 @@
     "\n",
     "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\").\n",
     "\n",
-    "Ces quantificateurs permettent d'exprimer des proprietes sur des **ensembles infinis** d'objets, ce qui est essentiel pour les mathematiques.\n",
+    "Ces quantificateurs permettent d'exprimer des propriétés sur des **ensembles infinis** d'objets, ce qui est essentiel pour les mathematiques.\n",
     "\n",
     "### Objectifs d'apprentissage\n",
     "\n",
     "1. Maitriser le quantificateur universel `forall` et son utilisation\n",
     "2. Maitriser le quantificateur existentiel `Exists` et la construction de temoins\n",
-    "3. Manipuler les proprietes arithmetiques sur `Nat`\n",
+    "3. Manipuler les propriétés arithmetiques sur `Nat`\n",
     "4. Utiliser les hypotheses anonymes et les references\n",
     "5. Comprendre l'interaction entre quantificateurs\n",
     "\n",
@@ -39,15 +39,15 @@
     "- Notebooks **Lean-1**, **Lean-2** et **Lean-3** completes\n",
     "- Familiarite avec les concepts de base de la logique du premier ordre\n",
     "\n",
-    "### Duree estimee : 40-45 minutes\n",
+    "### Duree estimée : 40-45 minutes\n",
     "\n",
     "\n",
     "## Plan de ce Notebook\n",
     "\n",
     "- **1** [Quantificateur Universel forall](#1-forall)\n",
     "- **2** [Quantificateur Existentiel exists](#2-exists)\n",
     "- **3** [Combinaison de Quantificateurs](#3-combinaison)\n",
-    "- **4** [Egalite et Substitution](#4-egalite)\n",
+    "- **4** [Égalité et Substitution](#4-égalité)\n",
     "- **5** [Arithmetique sur Nat](#5-arithmetique)\n",
     "- **6** [Techniques Avancees](#6-techniques-avancees)\n",
     "- **7** [Exercices](#7-exercices)\n",
@@ -79,9 +79,9 @@
     "<a id=\"1-forall\"></a>\n",
     "## 1. Le Quantificateur Universel `forall`\n",
     "\n",
-    "### 1.1 Definition et syntaxe\n",
+    "### 1.1 Définition et syntaxe\n",
     "\n",
-    "Le quantificateur universel `forall x : A, P x` (note aussi `\\forall x : A, P x` ou avec le symbole Unicode `∀`) exprime que la propriete `P` est vraie pour **tout** élément `x` du type `A`.\n",
+    "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`.\n",
     "\n",
     "En Lean, `forall` est simplement un alias pour le Pi-type dans `Prop`.\n",
     "\n",
@@ -276,7 +276,7 @@
    "source": [
     "### 1.2 Introduction du forall\n",
     "\n",
-    "Pour prouver `forall x : A, P x`, on doit fournir une **fonction** qui, etant donne un `x : A` arbitraire, produit une preuve de `P x`.\n",
+    "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`.\n",
     "\n",
     "C'est exactement comme programmer une fonction!\n",
     "\n",
@@ -409,7 +409,7 @@
     "tags": []
    },
    "source": [
-    "### 1.3 Elimination du forall\n",
+    "### 1.3 Élimination du forall\n",
     "\n",
     "Pour utiliser `forall x : A, P x`, on l'**applique** a une valeur concrete `a : A` pour obtenir `P a`.\n",
     "\n",
@@ -539,17 +539,17 @@
     }
    ],
    "source": [
-    "-- Definition rappel (pour execution isolee)\n",
+    "-- Définition rappel (pour exécution isolee)\n",
     "theorem 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\n",
     "theorem use_forall : 5 + 0 = 5 :=\n",
-    "  add_zero_forall_copy 5   -- Appliquer le theoreme a 5\n",
+    "  add_zero_forall_copy 5   -- Appliquer le théorème a 5\n",
     "\n",
     "#eval 5 + 0  -- 5 (Lean calcule)\n",
     "\n",
-    "-- Exemple avec une propriete quelconque\n",
+    "-- Exemple avec une propriété quelconque\n",
     "-- On peut en deduire P 42 a partir de forall n, P n\n",
     "theorem instance_of_forall (P : Nat -> Prop)\n",
     "    (h : forall n : Nat, P n) : P 42 := h 42"
@@ -569,7 +569,7 @@
     "tags": []
    },
    "source": [
-    "### 1.4 Proprietes avec plusieurs quantificateurs\n",
+    "### 1.4 Propriétés avec plusieurs quantificateurs\n",
     "\n",
     "Quand on a plusieurs variables quantifiees, on peut les introduire une par une ou en groupe. Les hypotheses intermediaires (`have`) permettent de structurer les preuves complexes.\n",
     "\n",
@@ -700,7 +700,7 @@
     "#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\n",
+    "-- Prouver une propriété avec deux quantificateurs\n",
     "theorem 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",
@@ -724,7 +724,7 @@
     "<a id=\"2-exists\"></a>\n",
     "## 2. Le Quantificateur Existentiel `Exists`\n",
     "\n",
-    "### 2.1 Definition et syntaxe\n",
+    "### 2.1 Définition et syntaxe\n",
     "\n",
     "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.\n",
     "\n",
@@ -1090,7 +1090,7 @@
     "tags": []
    },
    "source": [
-    "### 2.3 Elimination du Exists\n",
+    "### 2.3 Élimination du Exists\n",
     "\n",
     "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.\n",
     "\n",
@@ -1224,12 +1224,12 @@
     "-- Si il existe n pair, alors il existe m tel que 2 * m existe\n",
     "-- (exemple simplifie)\n",
     "\n",
-    "-- Elimination avec Exists.elim\n",
+    "-- Élimination avec Exists.elim\n",
     "theorem exists_elim_example\n",
     "  (h : ∃ n : Nat, n > 0) : True :=\n",
     "  Exists.elim h (fun _n _hn => True.intro)\n",
     "\n",
-    "-- Elimination avec match (plus lisible)\n",
+    "-- Élimination avec match (plus lisible)\n",
     "theorem exists_elim_match\n",
     "  (h : ∃ n : Nat, n > 0) : ∃ m : Nat, m >= 0 :=\n",
     "  match h with\n",
@@ -1257,7 +1257,7 @@
    },
    "source": [
     "<a id=\"3-combinaison\"></a>\n",
-    "## 3. Proprietes Arithmetiques sur Nat\n",
+    "## 3. Propriétés Arithmetiques sur Nat\n",
     "\n",
     "### 3.1 Lemmes de base\n",
     "\n",
@@ -1637,7 +1637,7 @@
     "tags": []
    },
    "source": [
-    "<a id=\"4-egalite\"></a>\n",
+    "<a id=\"4-égalité\"></a>\n",
     "## 4. Combinaison de Quantificateurs\n",
     "\n",
     "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).\n",
@@ -1901,7 +1901,7 @@
     "  fun x => match h with\n",
     "    | ⟨y, hy⟩ => ⟨y, hy x⟩\n",
     "\n",
-    "-- L'inverse n'est pas vrai en general!\n",
+    "-- L'inverse n'est pas vrai en général!\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"
@@ -2384,7 +2384,7 @@
    },
    "source": [
     "<a id=\"6-techniques-avancees\"></a>\n",
-    "## 6. Egalite et Quantificateurs\n",
+    "## 6. Égalité et Quantificateurs\n",
     "\n",
     "### 6.1 Réécriture avec l'égalité\n",
     "\n",
@@ -2526,7 +2526,7 @@
     "tags": []
    },
    "source": [
-    "Cette preuve illustre la **substitution sous un quantificateur** : de l'egalite `a = b` et de l'hypothese universelle `∀ n, P n`, on derive `P b` (appliquer `hp`, puis reecrire par l'egalite). C'est le patron standard `intro` puis `rw` pour faire traverser une egalite sous un binder -- technique omnipresente dans les preuves sur les structures parametrees.\n",
+    "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.\n",
     "\n",
     "### L'extension de l'égalité sous quantificateur — le transport `▸`\n",
     "\n",
@@ -2553,7 +2553,7 @@
     "tags": []
    },
    "source": [
-    "### 6.2 Egalite fonctionnelle### Pourquoi l'extensionnalité fonctionnelle est un axiome\n",
+    "### 6.2 Égalité fonctionnelle### Pourquoi l'extensionnalité fonctionnelle est un axiome\n",
     "\n",
     "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.\n",
     "\n",
@@ -2703,7 +2703,7 @@
     "<a id=\"7-exercices\"></a>\n",
     "## 7. Exemples Complets\n",
     "\n",
-    "### 7.1 Proprietes de divisibilite\n",
+    "### 7.1 Propriétés de divisibilite\n",
     "\n",
     "### Divisibilité — la définition existentielle\n",
     "\n",
@@ -2824,7 +2824,7 @@
     }
    ],
    "source": [
-    "-- Definition : a divise b\n",
+    "-- Définition : a divise b\n",
     "def divides (a b : Nat) : Prop := ∃ k : Nat, b = a * k\n",
     "\n",
     "notation:50 a \" | \" b => divides a b\n",
@@ -2849,7 +2849,7 @@
     "tags": []
    },
    "source": [
-    "La divisibilite est encodee **existentiellement** : `a ∣ b` signifie « il existe un entier `k` tel que `b = a * k` ». Cette definition 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.\n",
+    "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.\n",
     "\n",
     "### Utilisation de `divides` — extraction de témoin et projection\n",
     "\n",
@@ -2998,7 +2998,7 @@
     }
    ],
    "source": [
-    "-- Definition rappel (necessaire si cellule executee isolement)\n",
+    "-- Définition rappel (necessaire si cellule executee isolement)\n",
     "def mydivides (a b : Nat) : Prop := ∃ k : Nat, b = a * k\n",
     "infix:50 \" mydiv \" => mydivides\n",
     "\n",
@@ -3019,7 +3019,7 @@
     "tags": []
    },
    "source": [
-    "La **transitivite** (`a ∣ b -> b ∣ c -> a ∣ c`) se prouve en deroulant la definition 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.\n",
+    "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.\n",
     "\n",
     "### `divides` — clôture par composition multiplicative\n",
     "\n",
@@ -4265,26 +4265,26 @@
     }
    ],
    "source": [
-    "-- Definition rappel pour execution isolee\n",
+    "-- Définition rappel pour exécution isolee\n",
     "def mydivides' (a b : Nat) : Prop := exists k : Nat, b = a * k\n",
     "infix: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",
+    "-- TODO étudiant : prouver qu'il existe n tel que 2 mydiv' n\n",
     "-- Indice : utiliser le temoin 4\n",
     "theorem exists_even_practice : exists n : Nat, 2 mydiv' n := by\n",
     "  sorry\n",
     "\n",
     "-- Exercice 2 : Distribution du forall sur la conjonction\n",
     "variable (A : Type) (P Q : A -> Prop)\n",
-    "-- TODO etudiant : prouver la distribution\n",
+    "-- TODO étudiant : prouver la distribution\n",
     "-- Indice : utiliser fun hp hq x => <hp x, hq x>\n",
     "theorem 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",
+    "-- TODO étudiant : prouver la contraposition\n",
     "-- Indice : utiliser byContradiction\n",
     "open Classical in\n",
     "theorem not_forall_exists_not_practice\n",
@@ -4327,7 +4327,7 @@
    "source": [
     "## Resume\n",
     "\n",
-    "| Concept | Syntaxe | Introduction | Elimination |\n",
+    "| Concept | Syntaxe | Introduction | Élimination |\n",
     "|---------|---------|--------------|-------------|\n",
     "| **forall** | `\\forall x : A, P x` | `fun x => ...` | Application `h a` |\n",
     "| **exists** | `\\exists x : A, P x` | `⟨temoin, preuve⟩` | `match h with \\| ⟨x, hx⟩ => ...` |\n",
@@ -4391,4 +4391,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}