diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-05-Quantifiers-Proofs-Csharp.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-05-Quantifiers-Proofs-Csharp.ipynb index 1934af8e84..ea0d17698a 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-05-Quantifiers-Proofs-Csharp.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-05-Quantifiers-Proofs-Csharp.ipynb @@ -16,23 +16,37 @@ "source": [ "# Z3 (C# / .NET) — Quantificateurs et preuves par refutation\n", "\n", - "**Twin C# de `Z3-Python-05-Quantifiers-Proofs.ipynb`** (parite .NET, marathon #4956, suite de `Z3-Python-04-Strings-Regex-Csharp`).\n", + "**Twin C# de `Z3-Python-05-Quantifiers-Proofs.ipynb`** (parite .NET) : meme parcours, meme vocabulaire, API `Microsoft.Z3`.\n", "\n", - "Ce notebook aborde les **quantificateurs** (`ForAll`, `Exists`) et la notion de **preuve formelle par refutation** avec le **moteur reel [Microsoft.Z3](https://github.com/Z3Prover/z3)** (NuGet, Z3 4.12.2.0). Une formule est *valide* (un theoreme) si sa **negation** est insatisfiable : on demande au solveur de trouver un contre-exemple, et s'il n'en existe aucun, la formule est demontree.\n", + "## Objectifs d'apprentissage\n", "\n", - "## Plan\n", + "A la fin de ce notebook, vous saurez :\n", "\n", - "1. Preuve de l'identite additive par refutation (`ForAll x, x+0 == x`).\n", - "2. Trois proprietes elementaires (multiplicatif, commutativite, neutre a droite).\n", - "3. `Exists` sat : existe-t-il un `x` tel que `x*x == 4` ? Piege de la variable liee.\n", - "4. `Exists` unsat : un carre reel est toujours positif (`x*x < 0` impossible).\n", - "5. Trichotomie et monotonie du carre sur les reels positifs.\n", - "6. Quantificateurs imbriques (`ForAll x, Exists y, y > x` = pas de plus grand reel).\n", - "7. Le cas honnete `unknown` : dernier theoreme de Fermat (`a^3 + b^3 == c^3`).\n", - "8. Model checking : skolemisation d'un `Exists x, ForAll y`.\n", - "9. Trois exercices.\n", + "1. **Utiliser** le quantificateur universel `MkForall` pour exprimer qu'une propriete vaut pour toute valeur.\n", + "2. **Utiliser** le quantificateur existentiel `MkExists` pour exprimer qu'il existe au moins un temoin.\n", + "3. **Prouver** qu'une formule est valide (un theoreme) par la technique de negation-et-verification.\n", + "4. **Combiner** les deux quantificateurs dans des formules imbriquees.\n", + "5. **Reconnaitre** les limites de Z3 : quand le solveur repond `UNKNOWN`.\n", "\n", - "> **API .NET** : `ctx.MkForall(new Expr[]{x}, body)` / `ctx.MkExists(new Expr[]{x}, body)` ou `x` est une constante créée via `ctx.MkConst(\"x\", sort)` (le *body* utilise `x` directement, pas de de-Bruijn). `ctx.MkImplies`, `MkOr`, `MkAnd`, `MkNot` pour les connecteurs. Le timeout se règle via `s.Set(\"timeout\", 3000)` ; la raison d'un `UNKNOWN` se lit via la propriete `s.ReasonUnknown`. Les constantes reelles/entieres retournees par `MkConst` sont statiquement `Expr` → a caster en `(ArithExpr)` pour `MkAdd`/`MkMul`/`MkLt`/etc.\n" + "### Prerequis\n", + "- Z3 C# : `Context`, `Solver`, `ArithExpr`, `IntSort`/`RealSort`, `sat`/`unsat`.\n", + "- Notions de logique du premier ordre (quantificateurs $\\forall$, $\\exists$).\n", + "\n", + "***\n", + "\n", + "**Ce notebook marque un tournant.** Jusqu'ici, Z3 servait a trouver des **valeurs concretes** satisfaisant des contraintes (« existe-t-il un `x` tel que... ? »). Ici, nous voulons **prouver des proprietes generales** : « pour tout `x`, cette egalite tient-elle ? ». Cela exige les **quantificateurs** et la technique de **preuve par refutation**.\n", + "\n", + "> **Note technique** : Z3 est un solveur SMT, pas un assistant de preuve interactif (Lean/Coq). Une « preuve » ici est une **decision algorithmique** : le solveur confirme qu'aucun contre-exemple n'existe. Sur les fragments decidables, cette decision est complete et automatique ; sur les fragments plus riches (quantificateurs arbitraires, arithmetique non lineaire), Z3 peut repondre `UNKNOWN`.\n", + "\n", + "### La technique de preuve par refutation\n", + "\n", + "Une formule $F$ est **valide** (un theoreme) si et seulement si sa negation $\\neg F$ est **insatisfiable**. On ne prouve pas $F$ directement : on ajoute $\\neg F$ au solveur et on regarde s'il trouve un contre-exemple.\n", + "\n", + "| Negation de $F$ | Resultat Z3 | Conclusion sur $F$ |\n", + "|-----------------|-------------|--------------------|\n", + "| `Not(F)` est `UNSATISFIABLE` | Aucun contre-exemple | $F$ est **valide** (theoreme) |\n", + "| `Not(F)` est `SATISFIABLE` | Un contre-exemple existe | $F$ est **fausse** (contre-exemple donne) |\n", + "| `Not(F)` est `UNKNOWN` | Z3 ne peut pas conclure | Indecidable par ce solveur |\n" ] }, { @@ -68,7 +82,6 @@ " The below script needs to be able to find the current output cell; this is an easy method to get it.\r\n", " \r\n", " \r\n", @@ -213,7 +218,11 @@ "source": [ "## 1. Preuve par refutation : `ForAll x, x + 0 == x`\n", "\n", - "Pour prouver qu'une formule universelle est valide, on ajoute sa **negation** au solveur. Si le solveur repond `UNSATISFIABLE`, c'est qu'il n'existe aucun contre-exemple : la formule est donc un theoreme. Ici `x + 0 == x` pour tout reel `x`.\n" + "Pour prouver qu'une formule universelle est valide, on ajoute sa **negation** au solveur. Si le solveur repond `UNSATISFIABLE`, c'est qu'aucun contre-exemple n'existe : la formule est un theoreme.\n", + "\n", + "L'identite additive est l'exemple le plus simple : elle ne porte qu'**un** quantificateur et **une** operation arithmetique. La preuve est triviale pour Z3, mais elle pose le **pattern cognitif** qui se repetera dans toutes les sections : transformer un theoreme universel en une recherche de contre-exemple, laisser Z3 explorer, conclure sur le statut.\n", + "\n", + "> Ce pattern vaut pour toute identite mathematique : tester quelques valeurs (`5+0==5`, `3.14+0==3.14`) ne **prouve** rien — il y a une infinite de reels. Seul le quantificateur exprime « pour tous les `x` », et seul le solveur decide sans enumeration.\n" ] }, { @@ -287,6 +296,28 @@ " Console.WriteLine(\"=> Z3 ne peut pas conclure (unknown).\");\n" ] }, + { + "cell_type": "markdown", + "id": "07df56fc", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[1]** (verbatim) : la formule `(forall ((x Real)) (= (+ x 0.0) x))`, mise sous negation, repond `UNSATISFIABLE`. Aucun contre-exemple : **l'identite additive est valide**.\n", + "\n", + "| Etape | Operation | Resultat |\n", + "|-------|-----------|----------|\n", + "| 1 | Construire `MkForall(x, x + 0 == x)` | La formule a prouver |\n", + "| 2 | Ajouter `Not(formule)` au solveur | Cherche un contre-exemple |\n", + "| 3 | `solver.Check()` | `UNSATISFIABLE` = aucun contre-exemple |\n", + "| 4 | Conclusion | La formule est un theoreme |\n", + "\n", + "**Points cles** :\n", + "1. Z3 ne prouve pas « cette formule est valide » : il prouve que sa negation est absurde.\n", + "2. Si la negation etait `SATISFIABLE`, `solver.Model` donnerait un **contre-exemple** concret.\n", + "3. Le type `Real` couvre l'arithmetique rationnelle exacte ; l'identite tient sur tout $\\mathbb{Q}$.\n" + ] + }, { "cell_type": "markdown", "id": "6a739626", @@ -303,7 +334,11 @@ "source": [ "## 2. Trois proprietes elementaires\n", "\n", - "On automatise la preuve par refutation sur trois proprietes : l'identite multiplicative (`x * 1 == x`), la commutativite de l'addition (`x + y == y + x`), et le neutre additif a droite (`0 + x == x`). Pour chacune, on nie la formule universelle et on regarde le verdict du solveur.\n" + "On automatise la preuve par refutation sur trois proprietes : l'identite multiplicative (`x * 1 == x`), la commutativite de l'addition (`x + y == y + x`), et le neutre additif a droite (`0 + x == x`).\n", + "\n", + "**Pourquoi ces trois-la** : ce sont des axiomes fondamentaux du groupe additif des reels. Les prouver est un **test de fumee** sur l'integrite du solveur — si l'une d'elles repondait `sat` ou `UNKNOWN` (avec un temoin), on saurait que Z3 est mal configure.\n", + "\n", + "**Granularite pedagogique** : les trois exemples partagent le meme motif (`MkForall` + arithmetique), mais le cout de preuve varie — la commutativite peut demander plus de travail a la theorie reelle que l'identite multiplicative. Cette variation prepare l'etudiant au fait que tous les theoremes ne sont pas egaux en cout, meme quand ils paraissent symetriques.\n" ] }, { @@ -422,6 +457,24 @@ "}\n" ] }, + { + "cell_type": "markdown", + "id": "88a425fd", + "metadata": {}, + "source": [ + "### Lecture des trois theoremes\n", + "\n", + "**Sortie de code[2]** (verbatim) : trois lignes, trois verdicts `VALIDE (negation = UNSATISFIABLE)` — identite multiplicative, commutativite de l'addition, neutre additif a droite.\n", + "\n", + "- L'**identite multiplicative** (`x * 1 == x`) teste le neutre de la multiplication : l'element `1` est bien l'unite.\n", + "- La **commutativite** (`x + y == y + x`) teste la symetrie — une propriete souvent tenue pour evidente, que la machine doit prouver.\n", + "- Le **neutre additif a droite** (`0 + x == x`) teste un chemin d'analyse different du `x + 0 == x` de la section 1 ; les deux sont equivalents mais eprouvent des branches distinctes de la theorie.\n", + "\n", + "**Pourquoi Z3 les ferme si vite** : les corps reels ont des algorithmes dedies (Fourier-Motzkin, simplex) pour l'arithmetique lineaire. Ces trois theoremes sont triviaux pour eux — aucun backtracking.\n", + "\n", + "**Implication** : ce sont des **tests canari**. Si une mise a jour de Z3 cassait l'un d'eux, on saurait immediatement que la theorie reelle est cassee.\n" + ] + }, { "cell_type": "markdown", "id": "c61e0c9f", @@ -438,7 +491,14 @@ "source": [ "## 3. `Exists` satisfiable : existe-t-il `x` tel que `x*x == 4` ?\n", "\n", - "Le quantificateur existentiel `MkExists` demontre l'existence d'un temoin. **Piege classique** : la variable liee par `Exists` n'apparait **pas** dans le modèle (elle est quantifiee) — `m.Evaluate(x)` ne donne pas de temoin lisible. Pour obtenir une valeur concrete, on **skolemise** : on reasserte la même contrainte sur une constante *libre*, dont la valeur est alors lisible dans le modèle.\n" + "Le quantificateur existentiel `MkExists` demontre l'existence d'un **temoin**. C'est en general plus facile que `ForAll` : il suffit d'un cas. La formule `x*x == 4` est `SATISFIABLE` — Z3 exhibe un modele.\n", + "\n", + "**Deux subtilites pedagogiques** que ce cas revele :\n", + "\n", + "1. **Une variable liee n'apparait pas dans le modele.** La variable `x` quantifiee par `Exists` est **liee** : `m[x]` (ou l'equivalent C#) ne donne pas de temoin lisible. Le quantificateur prouve l'existence, il ne livre pas la valeur.\n", + "2. **Pour exhiber un temoin, on skolemise.** On reasserte la meme contrainte sur une **constante libre** (`racine`), et sa valeur devient lisible (ici `2` — Z3 pouvant renvoyer l'une des deux racines `2` ou `-2`).\n", + "\n", + "> **`Exists` vs recherche naive** : pour `x*x == 4`, on pourrait enumener `0, 1, -1, 2, -2, ...` et trouver un cas. Mais pour des contraintes non lineaires, l'enumeration est exponentielle ; Z3 exploite la structure algebrique pour eliminer des plages entieres d'un coup.\n" ] }, { @@ -527,6 +587,28 @@ "Console.WriteLine(\"Verification : \" + temoin + \" * \" + temoin + \" = \" + ctx.MkMul((ArithExpr)temoin, (ArithExpr)temoin).Simplify() + \" (attendu : 4)\");\n" ] }, + { + "cell_type": "markdown", + "id": "96eb5291", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[3]** (verbatim) : la formule `(exists ((x Real)) (= (* x x) 4.0))` est `SATISFIABLE` — un temoin existe. Mais `m[x]` (variable liee) rend « aucun temoin lisible », et c'est la constante libre `racine` qui donne `racine = 2`.\n", + "\n", + "| Etape | Operation | Resultat |\n", + "|-------|-----------|----------|\n", + "| 1 | `MkExists(x, x*x == 4)` puis `Check()` | `SATISFIABLE` — l'existence est prouvee |\n", + "| 2 | Lire la variable liee `x` | Aucun temoin lisible |\n", + "| 3 | Reasserter `racine*racine == 4` (constante libre) | `racine = 2` — temoin concret |\n", + "| 4 | Verifier `2 * 2 = 4` | Conforme |\n", + "\n", + "**Points cles** :\n", + "1. Une variable **liee** par `MkExists`/`MkForall` n'apparait **pas** dans le modele : le quantificateur prouve l'existence, il ne livre pas le temoin.\n", + "2. Pour **obtenir** le temoin, on **skolemise** : la meme contrainte posee sur une constante libre rend sa valeur lisible.\n", + "3. C'est la difference entre *prouver qu'un temoin existe* et *exhiber ce temoin*.\n" + ] + }, { "cell_type": "markdown", "id": "613e9fef", @@ -543,7 +625,9 @@ "source": [ "## 4. `Exists` insatisfiable : un carre negatif n'existe pas\n", "\n", - "A l'inverse, `MkExists(new Expr[]{ x }, x*x < 0)` est insatisfiable sur les reels : un carre est toujours positif ou nul. Le solveur repond `UNSATISFIABLE`, demontrant que la formule existentielle est fausse.\n" + "A l'inverse, `MkExists(new Expr[]{ x }, x*x < 0)` est **insatisfiable** : aucun reel `x` n'a un carre strictement negatif. Le carre d'un reel est toujours positif ou nul, donc la formule est **fausse** (sa negation est un theoreme).\n", + "\n", + "Ce cas est le **miroir** du precedent : une formule existentielle peut etre `unsat` quand elle est contradictoire. C'est la **troisieme branche** du tableau de la refutation — ici on ne prouve pas qu'un temoin existe, on prouve qu'il n'en existe aucun, et la conclusion porte sur la **faussete** de la formule plutot que sur sa validite.\n" ] }, { @@ -618,6 +702,27 @@ " Console.WriteLine(\"=> Temoin trouve : \" + s.Model);\n" ] }, + { + "cell_type": "markdown", + "id": "fbac57d7", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[4]** (verbatim) : `(exists ((x Real)) (< (* x x) 0.0))` repond `UNSATISFIABLE`. Aucun reel `x` n'a un carre strictement negatif.\n", + "\n", + "| Etape | Operation | Resultat |\n", + "|-------|-----------|----------|\n", + "| 1 | Construire `MkExists(x, x*x < 0)` | Cherche un carre negatif |\n", + "| 2 | `Check()` | `UNSATISFIABLE` |\n", + "| 3 | Conclusion | La formule est **fausse** (sa negation est un theoreme) |\n", + "\n", + "**Points cles** :\n", + "1. Le carre d'un reel est toujours $\\ge 0$, donc $x^2 < 0$ est contradictoire.\n", + "2. Ici la conclusion porte sur la **faussete** de la formule, pas sur sa validite — c'est le miroir des sections 1-2.\n", + "3. `UNSATISFIABLE` sur un `Exists` signifie qu'aucun temoin n'existe ; le solveur l'a etabli sans enumerer tous les reels.\n" + ] + }, { "cell_type": "markdown", "id": "eb7c93c0", @@ -634,7 +739,13 @@ "source": [ "## 5. Trichotomie et monotonie du carre\n", "\n", - "Deux theoremes classiques prouves par refutation. **Trichotomie** : pour tout reel `x`, exactement un des trois cas `x < 0`, `x == 0`, `x > 0` est vrai. **Monotonie du carre** : pour tous `x, y >= 0`, si `x <= y` alors `x*x <= y*y`. On nie chaque formule universelle et on constate `UNSATISFIABLE`.\n" + "Deux theoremes classiques prouves par refutation.\n", + "\n", + "**Trichotomie** : pour tout reel `x`, ou bien `x < 0`, ou bien `x == 0`, ou bien `x > 0`. C'est l'axiome d'ordre total des reels, et sa negation — un reel qui ne serait ni negatif, ni nul, ni positif — est contradictoire, donc `UNSATISFIABLE`.\n", + "\n", + "**Monotonie du carre** : si `x >= 0` et `y >= 0` et `x <= y`, alors `x*x <= y*y`. C'est la croissance du carre sur les positifs. Sa negation chercherait deux positifs ranges mais dont les carres seraient mal ranges : contradiction.\n", + "\n", + "Ces deux theoremes illustrent comment Z3 manipule des **implications** (`=>`) et des **conjonctions** (`and`) a l'interieur des quantificateurs — des formules plus riches que l'egalite simple des sections 1-2.\n" ] }, { @@ -743,6 +854,26 @@ "Console.WriteLine(\"=> Monotonicite : \" + (res2 == Status.UNSATISFIABLE ? \"VALIDE\" : \"NON PROUVEE\"));\n" ] }, + { + "cell_type": "markdown", + "id": "e3790490", + "metadata": {}, + "source": [ + "### Lecture des resultats\n", + "\n", + "**Sortie de code[5]** : deux theoremes, deux verdicts. La **trichotomie** — `(forall ((x Real)) (or (< x 0.0) (= x 0.0) (> x 0.0)))` — est `VALIDE` (negation `UNSATISFIABLE`). La **monotonie du carre** — avec implication et conjonction — est `VALIDE` (tronquee dans l'affichage, la negation reste `UNSATISFIABLE`).\n", + "\n", + "| Propriete | Formule Z3 | Verdict |\n", + "|-----------|-----------|---------|\n", + "| Trichotomie | `ForAll x, (x < 0 or x == 0 or x > 0)` | VALIDE |\n", + "| Monotonie | `ForAll x y, (x>=0 and y>=0 and x<=y) => x*x<=y*y` | VALIDE |\n", + "\n", + "**Points cles** :\n", + "1. La trichotomie est l'**ordre total** des reels : sa negation cherche un reel `ni < 0, ni == 0, ni > 0` — contradictoire.\n", + "2. La monotonie montre des formules plus riches qu'une egalite : **implication** (`=>`) et **conjonction** (`and`) imbriquees sous les quantificateurs.\n", + "3. Les deux se prouvent par le meme geste — negation puis `unsat` — mais exerceraient une preuve manuelle bien plus longue.\n" + ] + }, { "cell_type": "markdown", "id": "e0e7ed77", @@ -757,9 +888,15 @@ "tags": [] }, "source": [ - "## 6. Quantificateurs imbriques : pas de plus grand reel\n", + "## 6. Quantificateurs imbriquees : pas de plus grand reel\n", "\n", - "Une formule peut imbriquer `ForAll` et `Exists`. L'enonce « il n'existe pas de plus grand reel » se formalise : `ForAll x, Exists y, y > x` — pour tout `x`, on peut toujours trouver un `y` strictement plus grand. On nie la formule entiere et le solveur repond `UNSATISFIABLE`.\n" + "Une formule peut **imbriquer** `ForAll` et `Exists`. L'enonce « il n'existe pas de plus grand reel » s'ecrit :\n", + "\n", + "$$ \\forall x \\in \\mathbb{R},\\ \\exists y \\in \\mathbb{R},\\ y > x $$\n", + "\n", + "Pour tout `x`, il existe un `y` strictement plus grand — c'est la **non-borne** des reels (archimedien). On prouve cet enonce par refutation : on nie la formule `ForAll(x, Exists(y, y > x))` et on montre que la negation est `UNSATISFIABLE`.\n", + "\n", + "**L'ordre des quantificateurs importe.** `ForAll x, Exists y` (pour chaque `x`, un `y` dependant) n'est pas equivalent a `Exists y, ForAll x` (un `y` unique qui dominerait tous les `x`). La premiere est vraie ici (les reels ne sont pas bornes) ; la seconde est fausse (il n'existe pas de reel unique au-dessus de tous les autres). Ce contraste se materialisera en section 8.\n" ] }, { @@ -831,6 +968,28 @@ " Console.WriteLine(\"=> Z3 ne peut pas conclure (unknown).\");\n" ] }, + { + "cell_type": "markdown", + "id": "0b381381", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[6]** : `(forall ((x Real)) (exists ((y Real)) (> y x)))` a pour negation `UNSATISFIABLE`. **Il n'existe pas de plus grand reel** : c'est un theoreme.\n", + "\n", + "| Etape | Operation | Resultat |\n", + "|-------|-----------|----------|\n", + "| 1 | Construire `ForAll(x, Exists(y, y > x))` | La formule a prouver |\n", + "| 2 | Nier la formule | Cherche un `x` non depassable |\n", + "| 3 | `Check()` | `UNSATISFIABLE` |\n", + "| 4 | Conclusion | Valide : les reels ne sont pas bornes |\n", + "\n", + "**Points cles** :\n", + "1. L'ordre des quantificateurs est **critique** : `ForAll x, Exists y` (chaque `x` a son `y`) est la **non-borne** ; `Exists y, ForAll x` (un `y` unique) serait faux.\n", + "2. La negation est faite sur la formule imbriquee entiere, pas sur la sous-formule interne.\n", + "3. Contraste avec la section 8, ou l'ordre est inverse et le solveur doit **trouver** une valeur.\n" + ] + }, { "cell_type": "markdown", "id": "b4aa7aae", @@ -847,7 +1006,13 @@ "source": [ "## 7. Le cas honnete `unknown` : Fermat\n", "\n", - "L'arithmetique non lineaire entiere est **indecidable en general** : Z3 ne peut pas toujours trancher. Existe-t-il des entiers `a, b, c > 1` tels que `a^3 + b^3 == c^3` ? Le dernier theoreme de Fermat dit non, mais cette preuve depasse Z3. Sans budget de temps, Z3 chercherait indefiniment ; on borne donc avec un timeout, et le solveur repond honnetement `UNKNOWN` avec une raison (`timeout`). Ce n'est **pas un bug** mais une limite fondamentale de la decision automatique.\n" + "L'arithmetique non lineaire entiere est **indecidable en general** : Z3 ne peut pas trancher toute formule. On le montre avec le dernier theoreme de Fermat pour l'exposant 3 :\n", + "\n", + "$$ a^3 + b^3 = c^3,\\quad a, b, c > 1 $$\n", + "\n", + "Z3 repond `UNKNOWN` (ici par **timeout**). **Ce n'est pas un bug, c'est une limite fondamentale** de la decision algorithmique — le fragment des entiers avec multiplication est justement hors des theories decidables que Z3 sait traiter.\n", + "\n", + "> Le `UNKNOWN` est une reponse **honnete** : elle dit « je ne sais pas », pas « c'est faux » ni « c'est vrai ». C'est le troisieme statut du tableau de la refutation. Savoir le lire — et savoir que sa presence est normalement une limite du solveur, pas une erreur de code — est une competence en soi.\n" ] }, { @@ -941,6 +1106,27 @@ "}\n" ] }, + { + "cell_type": "markdown", + "id": "bfb1eccf", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[7]** (verbatim) : le probleme `a^3 + b^3 == c^3` avec `a, b, c > 1` repond `UNKNOWN` (raison : timeout).\n", + "\n", + "| Statut | Sens | Ce que cela veut dire |\n", + "|--------|------|-----------------------|\n", + "| `SATISFIABLE` | un temoin existe | la formule est consistante |\n", + "| `UNSATISFIABLE` | aucun temoin | la formule est fausse |\n", + "| `UNKNOWN` | Z3 abandonne | **indecidable** par ce solveur |\n", + "\n", + "**Points cles** :\n", + "1. `UNKNOWN` n'est **ni** vrai **ni** faux : c'est « je ne peux pas trancher ».\n", + "2. L'arithmetique entiere non lineaire (avec multiplication) est hors des fragments decidables de Z3 ; le timeout est le symptome, pas la cause.\n", + "3. Distinguer `UNKNOWN`-limite-de-solveur d'une **erreur de code** est essentiel : ici le code est correct, la limite est theorique.\n" + ] + }, { "cell_type": "markdown", "id": "6525b475", @@ -957,7 +1143,13 @@ "source": [ "## 8. Model checking : skolemiser un `Exists x, ForAll y`\n", "\n", - "On cherche s'il existe un `x` tel que pour tout `y >= 0`, `x <= y`. Le `Exists x` externe est le temoin recherche. Pour lire sa valeur, on le **skolemise** : on declare `x` comme constante *libre* et le `ForAll` ne porte plus que sur `y`. Le solveur trouve alors un modèle (par exemple `x = 0`), dont la valeur devient lisible via `m.Evaluate(x)`.\n" + "On cherche s'il existe un `x` tel que pour tout `y >= 0`, `x <= y` — c'est-a-dire un **minorant** des reels positifs. La formule est :\n", + "\n", + "$$ \\exists x,\\ \\forall y \\ge 0,\\ x \\le y $$\n", + "\n", + "En reasserte la contrainte sur une **constante libre** `x` (skolemisation), on interroge le solveur : « quel `x` est `<=` a tout `y >= 0` ? ». Cette forme est celle du **model checking** : on ne quantifie plus `x`, on en fait une inconnue a determiner, et le modele retourne sa valeur.\n", + "\n", + "**Verification croisee** : le code verifie ensuite que le `x` trouve est bien `<= 1/10`, `<= 1`, etc. — on valide le modele contre des instances pragmatiques, pas seulement contre la formule.\n" ] }, { @@ -1059,6 +1251,28 @@ " Console.WriteLine(\"=> Z3 ne peut pas conclure (unknown).\");\n" ] }, + { + "cell_type": "markdown", + "id": "474ff68b", + "metadata": {}, + "source": [ + "### Lecture du resultat\n", + "\n", + "**Sortie de code[8]** : la constante libre `x` sous contrainte `(forall ((y Real)) (=> (>= y 0.0) (<= x y)))` est `SATISFIABLE`, modele `x = 0`.\n", + "\n", + "| Etape | Operation | Resultat |\n", + "|-------|-----------|----------|\n", + "| 1 | Skolemiser : constante libre `x` | `x` est une inconnue a determiner |\n", + "| 2 | Contrainte `x <= tout y >= 0` | `x` minorant des positifs |\n", + "| 3 | `Check()` | `SATISFIABLE`, `x = 0` |\n", + "| 4 | Verification croisee (`x <= 1/10`, `x <= 1`) | Conforme |\n", + "\n", + "**Points cles** :\n", + "1. La skolemisation transforme un `Exists` en une **inconnue a resoudre** : le modele donne `x = 0`, le minorant trivial des positifs.\n", + "2. Les verifications croisees valident le modele contre des **instances pragmatiques** (« est-ce que `0 <= 1/10` ? »), pas seulement contre la formule.\n", + "3. C'est le pattern du **model checking** : on ne prouve plus une existence, on **synthetise** une valeur.\n" + ] + }, { "cell_type": "markdown", "id": "1b24788f", @@ -1677,4 +1891,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-05-quantifiers-proofs.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-05-quantifiers-proofs.yaml index 3c93ff37a0..523c0c1926 100644 --- a/scripts/notebook_tools/twin_pairs.d/z3-python-05-quantifiers-proofs.yaml +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-05-quantifiers-proofs.yaml @@ -39,6 +39,13 @@ csharp_sha: 1934af8e843c3bc8359671b0f47f0614b2af126b content_python_sha: b80e45b44ea5b6a531a371716d7ab3c487f258d7ba0cd569691e5142cf84797b content_csharp_sha: 426c6c7837711d69d4c1d011a2a178d3e2234b5f0180094963c32192c40c5583 + - date: "2026-09-06" + by: myia-po-2026:CoursIA-2 + python_sha: 2ad0124c1141c5d26f8e0574184a3270e47fda3f + csharp_sha: ea0d17698a9a37051aaeb6d1ed1d5e42f62b8bc4 + content_python_sha: b80e45b44ea5b6a531a371716d7ab3c487f258d7ba0cd569691e5142cf84797b + content_csharp_sha: 97fab73a374aafda9ae3d00cf9e5d2dd71023a3ff195ae913981c35b4a798199 + reason: "Enrichissement densite (#13410) du twin C# (622 -> 1490 c/cell, markdown-only) : 8 cellules d'interpretation + intros. Les 13 cellules code et tous les outputs restent byte-identiques a main (verifie code_identity.py) ; le twin Python inchange. Parity native-both tenue : meme moteur Z3, memes concepts, seuls la prose d'interpretation et le numeroteur de cellules divergent. Rebaseline apres audit firsthand par la lane auteure." known_differences: - "Python : pyz3 (ForAll, Exists, prove() par refutation). C# : Microsoft.Z3 .NET (ctx.MkForall, MkExists, Solver+unsat)." - "Concept demontre (preuve par refutation, Exists sat/unsat, Fermat unknown) verifie cote Python (structure CLEAN c.20)."