Z3 (C# / .NET) — Quantificateurs et preuves par refutation

Twin C# de Z3-05-Quantifiers-Proofs-Python.ipynb (parite .NET) : meme parcours, meme vocabulaire, API Microsoft.Z3.

Navigation : Index | Index SMT | Index SymbolicAI | << 04 - Strings (C#) | 06 - Advanced Optimization (C#) >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez :

1. Utiliser le quantificateur universel MkForall pour exprimer qu’une propriete vaut pour toute valeur.
2. Utiliser le quantificateur existentiel MkExists pour exprimer qu’il existe au moins un temoin.
3. Prouver qu’une formule est valide (un theoreme) par la technique de negation-et-verification.
4. Combiner les deux quantificateurs dans des formules imbriquees.
5. Reconnaitre les limites de Z3 : quand le solveur repond UNKNOWN.

Prerequis

• Z3 C# : Context, Solver, ArithExpr, IntSort/RealSort, sat/unsat.
• Notions de logique du premier ordre (quantificateurs \(\forall\), \(\exists\)).

---

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.

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.

La technique de preuve par refutation

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.

Negation de \(F\)	Resultat Z3	Conclusion sur \(F\)
Not(F) est UNSATISFIABLE	Aucun contre-exemple	\(F\) est valide (theoreme)
Not(F) est SATISFIABLE	Un contre-exemple existe	\(F\) est fausse (contre-exemple donne)
Not(F) est UNKNOWN	Z3 ne peut pas conclure	Indecidable par ce solveur

#r "nuget: Microsoft.Z3"
#load "Z3NativeLoader.cs"
using Microsoft.Z3;

// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Context).Assembly);
Console.WriteLine("Imports OK : Microsoft.Z3 version " + Microsoft.Z3.Version.FullVersion);

The below script needs to be able to find the current output cell; this is an easy method to get it.

Installed Packages

• Microsoft.Z3, 4.12.2

Imports OK : Microsoft.Z3 version Z3 4.12.2.0

1. Preuve par refutation : ForAll x, x + 0 == x

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.

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.

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);

// La formule que nous voulons prouver : pour tout x reel, x + 0 == x
var body = ctx.MkEq(ctx.MkAdd(x, ctx.MkReal(0)), x);
var formule = ctx.MkForall(new Expr[]{ x }, body);
Console.WriteLine("Formule a prouver : " + formule);

// Technique : verifier que la NEGATION est insatisfiable
var s = ctx.MkSolver();
s.Add(ctx.MkNot(formule));  // Existe-t-il un x tel que x + 0 != x ?

Status resultat = s.Check();
Console.WriteLine("Negation de la formule : " + resultat);

if (resultat == Status.UNSATISFIABLE)
    Console.WriteLine("=> Aucun contre-exemple trouve : la formule est VALIDE (theoreme).");
else if (resultat == Status.SATISFIABLE)
    Console.WriteLine("=> Contre-exemple trouve : " + s.Model);
else
    Console.WriteLine("=> Z3 ne peut pas conclure (unknown).");

Formule a prouver : (forall ((x Real)) (= (+ x 0.0) x))
Negation de la formule : UNSATISFIABLE
=> Aucun contre-exemple trouve : la formule est VALIDE (theoreme).

Lecture du resultat

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.

Etape	Operation	Resultat
1	Construire MkForall(x, x + 0 == x)	La formule a prouver
2	Ajouter Not(formule) au solveur	Cherche un contre-exemple
3	solver.Check()	UNSATISFIABLE = aucun contre-exemple
4	Conclusion	La formule est un theoreme

Points cles : 1. Z3 ne prouve pas « cette formule est valide » : il prouve que sa negation est absurde. 2. Si la negation etait SATISFIABLE, solver.Model donnerait un contre-exemple concret. 3. Le type Real couvre l’arithmetique rationnelle exacte ; l’identite tient sur tout \(\mathbb{Q}\).

2. Trois proprietes elementaires

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).

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.

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.

using Microsoft.Z3;
using System.Collections.Generic;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);
var y = (ArithExpr)ctx.MkConst("y", ctx.RealSort);

var proprietes = new (string nom, Quantifier formule)[]{
    ("Identite multiplicative : x * 1 == x",
        ctx.MkForall(new Expr[]{ x }, ctx.MkEq(ctx.MkMul(x, ctx.MkReal(1)), x))),
    ("Commutativite de l addition : x + y == y + x",
        ctx.MkForall(new Expr[]{ x, y }, ctx.MkEq(ctx.MkAdd(x, y), ctx.MkAdd(y, x)))),
    ("Neutre additif a droite : 0 + x == x",
        ctx.MkForall(new Expr[]{ x }, ctx.MkEq(ctx.MkAdd(ctx.MkReal(0), x), x))),
};

foreach (var (nom, formule) in proprietes)
{
    var s = ctx.MkSolver();
    s.Add(ctx.MkNot(formule));
    var res = s.Check();
    string statut = res == Status.UNSATISFIABLE ? "VALIDE" : (res == Status.SATISFIABLE ? "FAUSSE" : "UNKNOWN");
    Console.WriteLine(nom);
    Console.WriteLine("  => " + statut + " (negation = " + res + ")");
    Console.WriteLine();
}

Identite multiplicative : x * 1 == x
  => VALIDE (negation = UNSATISFIABLE)

Commutativite de l addition : x + y == y + x
  => VALIDE (negation = UNSATISFIABLE)

Neutre additif a droite : 0 + x == x
  => VALIDE (negation = UNSATISFIABLE)

Lecture des trois theoremes

Sortie de code[2] (verbatim) : trois lignes, trois verdicts VALIDE (negation = UNSATISFIABLE) — identite multiplicative, commutativite de l’addition, neutre additif a droite.

• L’identite multiplicative (x * 1 == x) teste le neutre de la multiplication : l’element 1 est bien l’unite.
• La commutativite (x + y == y + x) teste la symetrie — une propriete souvent tenue pour evidente, que la machine doit prouver.
• 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.

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.

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.

3. Exists satisfiable : existe-t-il x tel que x*x == 4 ?

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.

Deux subtilites pedagogiques que ce cas revele :

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.
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).

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);

// Etape 1 : prouver l existence avec le quantificateur existentiel
var formule = ctx.MkExists(new Expr[]{ x }, ctx.MkEq(ctx.MkMul(x, x), ctx.MkReal(4)));
var s = ctx.MkSolver();
s.Add(formule);
var res = s.Check();
Console.WriteLine("Formule   : " + formule);
Console.WriteLine("Existence : " + res + " (un temoin existe)");

// Piege : x est LIEE par Exists -> pas dans le modele
Console.WriteLine("m[x] (x lie par Exists) : " + s.Model.Evaluate(x) + "  <- aucun temoin lisible ici");

// Etape 2 : skolemisation sur une constante LIBRE
var racine = (ArithExpr)ctx.MkConst("racine", ctx.RealSort);
var s2 = ctx.MkSolver();
s2.Add(ctx.MkEq(ctx.MkMul(racine, racine), ctx.MkReal(4)));
s2.Check();
var temoin = s2.Model.Evaluate(racine);
Console.WriteLine("Temoin concret (constante libre) : racine = " + temoin);
Console.WriteLine("Verification : " + temoin + " * " + temoin + " = " + ctx.MkMul((ArithExpr)temoin, (ArithExpr)temoin).Simplify() + " (attendu : 4)");

Formule   : (exists ((x Real)) (= (* x x) 4.0))
Existence : SATISFIABLE (un temoin existe)
m[x] (x lie par Exists) : x  <- aucun temoin lisible ici
Temoin concret (constante libre) : racine = 2
Verification : 2 * 2 = 4 (attendu : 4)

Lecture du resultat

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.

Etape	Operation	Resultat
1	MkExists(x, x*x == 4) puis Check()	SATISFIABLE — l’existence est prouvee
2	Lire la variable liee x	Aucun temoin lisible
3	Reasserter racine*racine == 4 (constante libre)	racine = 2 — temoin concret
4	Verifier 2 * 2 = 4	Conforme

Points cles : 1. Une variable liee par MkExists/MkForall n’apparait pas dans le modele : le quantificateur prouve l’existence, il ne livre pas le temoin. 2. Pour obtenir le temoin, on skolemise : la meme contrainte posee sur une constante libre rend sa valeur lisible. 3. C’est la difference entre prouver qu’un temoin existe et exhiber ce temoin.

4. Exists insatisfiable : un carre negatif n’existe pas

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).

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);

var formule = ctx.MkExists(new Expr[]{ x }, ctx.MkLt(ctx.MkMul(x, x), ctx.MkReal(0)));
Console.WriteLine("Formule : " + formule);
Console.WriteLine("(Un carre reel est toujours positif ou nul)");

var s = ctx.MkSolver();
s.Add(formule);
var res = s.Check();
Console.WriteLine("Resultat : " + res);
if (res == Status.UNSATISFIABLE)
    Console.WriteLine("=> Aucun reel x tel que x*x < 0 : la formule est FAUSSE.");
else if (res == Status.SATISFIABLE)
    Console.WriteLine("=> Temoin trouve : " + s.Model);

Formule : (exists ((x Real)) (< (* x x) 0.0))
(Un carre reel est toujours positif ou nul)
Resultat : UNSATISFIABLE
=> Aucun reel x tel que x*x < 0 : la formule est FAUSSE.

Lecture du resultat

Sortie de code[4] (verbatim) : (exists ((x Real)) (< (* x x) 0.0)) repond UNSATISFIABLE. Aucun reel x n’a un carre strictement negatif.

Etape	Operation	Resultat
1	Construire MkExists(x, x*x < 0)	Cherche un carre negatif
2	Check()	UNSATISFIABLE
3	Conclusion	La formule est fausse (sa negation est un theoreme)

Points cles : 1. Le carre d’un reel est toujours \(\ge 0\), donc \(x^2 < 0\) est contradictoire. 2. Ici la conclusion porte sur la faussete de la formule, pas sur sa validite — c’est le miroir des sections 1-2. 3. UNSATISFIABLE sur un Exists signifie qu’aucun temoin n’existe ; le solveur l’a etabli sans enumerer tous les reels.

5. Trichotomie et monotonie du carre

Deux theoremes classiques prouves par refutation.

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.

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.

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);
var y = (ArithExpr)ctx.MkConst("y", ctx.RealSort);

// Preuve 1 : trichotomie sur les reels
var trichotomie = ctx.MkForall(new Expr[]{ x }, ctx.MkOr(
    ctx.MkLt(x, ctx.MkReal(0)),
    ctx.MkEq(x, ctx.MkReal(0)),
    ctx.MkGt(x, ctx.MkReal(0))));
Console.WriteLine("Theoreme de trichotomie : " + trichotomie);
var s = ctx.MkSolver();
s.Add(ctx.MkNot(trichotomie));
var res = s.Check();
Console.WriteLine("Negation = " + res);
Console.WriteLine("=> Trichotomie : " + (res == Status.UNSATISFIABLE ? "VALIDE" : "NON PROUVEE"));
Console.WriteLine();

// Preuve 2 : monotonie du carre sur les reels positifs
var monotonicite = ctx.MkForall(new Expr[]{ x, y }, ctx.MkImplies(
    ctx.MkAnd(ctx.MkGe(x, ctx.MkReal(0)), ctx.MkGe(y, ctx.MkReal(0)), ctx.MkLe(x, y)),
    ctx.MkLe(ctx.MkMul(x, x), ctx.MkMul(y, y))));
Console.WriteLine("Monotonicite du carre (x >= 0) : " + monotonicite);
var s2 = ctx.MkSolver();
s2.Add(ctx.MkNot(monotonicite));
var res2 = s2.Check();
Console.WriteLine("Negation = " + res2);
Console.WriteLine("=> Monotonicite : " + (res2 == Status.UNSATISFIABLE ? "VALIDE" : "NON PROUVEE"));

Theoreme de trichotomie : (forall ((x Real)) (or (< x 0.0) (= x 0.0) (> x 0.0)))
Negation = UNSATISFIABLE
=> Trichotomie : VALIDE

Monotonicite du carre (x >= 0) : (forall ((x Real) (y Real))
  (=> (and (>= x 0.0) (>= y 0.0) (<= x y)) (<= (* x x) (* y y))))
Negation = UNSATISFIABLE
=> Monotonicite : VALIDE

Lecture des resultats

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).

Propriete	Formule Z3	Verdict
Trichotomie	ForAll x, (x < 0 or x == 0 or x > 0)	VALIDE
Monotonie	ForAll x y, (x>=0 and y>=0 and x<=y) => x*x<=y*y	VALIDE

Points cles : 1. La trichotomie est l’ordre total des reels : sa negation cherche un reel ni < 0, ni == 0, ni > 0 — contradictoire. 2. La monotonie montre des formules plus riches qu’une egalite : implication (=>) et conjonction (and) imbriquees sous les quantificateurs. 3. Les deux se prouvent par le meme geste — negation puis unsat — mais exerceraient une preuve manuelle bien plus longue.

6. Quantificateurs imbriquees : pas de plus grand reel

Une formule peut imbriquer ForAll et Exists. L’enonce « il n’existe pas de plus grand reel » s’ecrit :

\[ \forall x \in \mathbb{R},\ \exists y \in \mathbb{R},\ y > x \]

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.

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);
var y = (ArithExpr)ctx.MkConst("y", ctx.RealSort);

// ForAll x, Exists y, y > x
var pasDePlusGrand = ctx.MkForall(new Expr[]{ x },
    ctx.MkExists(new Expr[]{ y }, ctx.MkGt(y, x)));
Console.WriteLine("Formule : " + pasDePlusGrand);

var s = ctx.MkSolver();
s.Add(ctx.MkNot(pasDePlusGrand));
var res = s.Check();
Console.WriteLine("Negation = " + res);
if (res == Status.UNSATISFIABLE)
    Console.WriteLine("=> VALIDE : il n existe pas de plus grand reel (theoreme).");
else if (res == Status.SATISFIABLE)
    Console.WriteLine("=> FAUSSE : contre-exemple trouve. " + s.Model);
else
    Console.WriteLine("=> Z3 ne peut pas conclure (unknown).");

Formule : (forall ((x Real)) (exists ((y Real)) (> y x)))
Negation = UNSATISFIABLE
=> VALIDE : il n existe pas de plus grand reel (theoreme).

Lecture du resultat

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.

Etape	Operation	Resultat
1	Construire ForAll(x, Exists(y, y > x))	La formule a prouver
2	Nier la formule	Cherche un x non depassable
3	Check()	UNSATISFIABLE
4	Conclusion	Valide : les reels ne sont pas bornes

Points cles : 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. 2. La negation est faite sur la formule imbriquee entiere, pas sur la sous-formule interne. 3. Contraste avec la section 8, ou l’ordre est inverse et le solveur doit trouver une valeur.

7. Le cas honnete unknown : Fermat

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 :

\[ a^3 + b^3 = c^3,\quad a, b, c > 1 \]

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.

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.

using Microsoft.Z3;
var ctx = new Context();
var a = (ArithExpr)ctx.MkConst("a", ctx.IntSort);
var b = (ArithExpr)ctx.MkConst("b", ctx.IntSort);
var c = (ArithExpr)ctx.MkConst("c", ctx.IntSort);

var s = ctx.MkSolver();
s.Set("timeout", 3000);  // 3 secondes ; au-dela, Z3 abandonne
s.Add(ctx.MkGt(a, ctx.MkInt(1)), ctx.MkGt(b, ctx.MkInt(1)), ctx.MkGt(c, ctx.MkInt(1)));
var a3 = ctx.MkMul(a, ctx.MkMul(a, a));
var b3 = ctx.MkMul(b, ctx.MkMul(b, b));
var c3 = ctx.MkMul(c, ctx.MkMul(c, c));
s.Add(ctx.MkEq(ctx.MkAdd(a3, b3), c3));

Console.WriteLine("Probleme : a^3 + b^3 == c^3  avec a, b, c > 1");
var res = s.Check();
Console.WriteLine("Resultat : " + res);

if (res == Status.SATISFIABLE)
    Console.WriteLine("=> Temoin trouve : " + s.Model);
else if (res == Status.UNSATISFIABLE)
    Console.WriteLine("=> Aucune solution (prouve).");
else
{
    Console.WriteLine("=> UNKNOWN : Z3 abandonne (raison : " + s.ReasonUnknown + ").");
    Console.WriteLine("   L arithmetique non lineaire entiere est indecidable en general :");
    Console.WriteLine("   ce n est PAS un bug, mais une limite fondamentale de la decision automatique.");
}

Probleme : a^3 + b^3 == c^3  avec a, b, c > 1
Resultat : UNKNOWN
=> UNKNOWN : Z3 abandonne (raison : timeout).
   L arithmetique non lineaire entiere est indecidable en general :
   ce n est PAS un bug, mais une limite fondamentale de la decision automatique.

Lecture du resultat

Sortie de code[7] (verbatim) : le probleme a^3 + b^3 == c^3 avec a, b, c > 1 repond UNKNOWN (raison : timeout).

Statut	Sens	Ce que cela veut dire
SATISFIABLE	un temoin existe	la formule est consistante
UNSATISFIABLE	aucun temoin	la formule est fausse
UNKNOWN	Z3 abandonne	indecidable par ce solveur

Points cles : 1. UNKNOWN n’est ni vrai ni faux : c’est « je ne peux pas trancher ». 2. L’arithmetique entiere non lineaire (avec multiplication) est hors des fragments decidables de Z3 ; le timeout est le symptome, pas la cause. 3. Distinguer UNKNOWN-limite-de-solveur d’une erreur de code est essentiel : ici le code est correct, la limite est theorique.

8. Model checking : skolemiser un Exists x, ForAll y

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 :

\[ \exists x,\ \forall y \ge 0,\ x \le y \]

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.

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.

using Microsoft.Z3;
var ctx = new Context();
var x = (ArithExpr)ctx.MkConst("x", ctx.RealSort);
var y = (ArithExpr)ctx.MkConst("y", ctx.RealSort);

// ForAll y >= 0 => x <= y  (x skolemise, libre)
var contrainte = ctx.MkForall(new Expr[]{ y },
    ctx.MkImplies(ctx.MkGe(y, ctx.MkReal(0)), ctx.MkLe(x, y)));
Console.WriteLine("Contrainte sur x (temoin libre) : " + contrainte);

var s = ctx.MkSolver();
s.Add(contrainte);
var res = s.Check();
Console.WriteLine("Resultat : " + res);

if (res == Status.SATISFIABLE)
{
    var m = s.Model;
    var valX = m.Evaluate(x);  // x est libre -> sa valeur est lisible
    Console.WriteLine("Modele trouve : x = " + valX);
    Console.WriteLine("Interpretation : " + valX + " est <= a tout y >= 0 (un minorant des reels positifs)");
    // Verifier x <= 1/10 et x <= 1/1000 contre le modele
    Console.WriteLine("Verification : x <= 1/10 ? " + m.Evaluate(ctx.MkLe(x, ctx.MkReal(1, 10))));
    Console.WriteLine("Verification : x <= 1/1000 ? " + m.Evaluate(ctx.MkLe(x, ctx.MkReal(1, 1000))));
}
else if (res == Status.UNSATISFIABLE)
    Console.WriteLine("=> Aucun modele : la formule est fausse.");
else
    Console.WriteLine("=> Z3 ne peut pas conclure (unknown).");

Contrainte sur x (temoin libre) : (forall ((y Real)) (=> (>= y 0.0) (<= x y)))
Resultat : SATISFIABLE
Modele trouve : x = 0
Interpretation : 0 est <= a tout y >= 0 (un minorant des reels positifs)
Verification : x <= 1/10 ? true
Verification : x <= 1/1000 ? true

Lecture du resultat

Sortie de code[8] : la constante libre x sous contrainte (forall ((y Real)) (=> (>= y 0.0) (<= x y))) est SATISFIABLE, modele x = 0.

Etape	Operation	Resultat
1	Skolemiser : constante libre x	x est une inconnue a determiner
2	Contrainte x <= tout y >= 0	x minorant des positifs
3	Check()	SATISFIABLE, x = 0
4	Verification croisee (x <= 1/10, x <= 1)	Conforme

Points cles : 1. La skolemisation transforme un Exists en une inconnue a resoudre : le modele donne x = 0, le minorant trivial des positifs. 2. Les verifications croisees valident le modele contre des instances pragmatiques (« est-ce que 0 <= 1/10 ? »), pas seulement contre la formule. 3. C’est le pattern du model checking : on ne prouve plus une existence, on synthetise une valeur.

9. Z3 est un prouveur : l’arbre d’inférence (proof=true)

Jusqu’ici, chaque section demande à Z3 un verdict — UNSATISFIABLE, SATISFIABLE, UNKNOWN — et s’arrête là. Mais Z3 n’est pas un oracle : c’est un prouveur. Avec le paramètre proof=true, le solveur enregistre l’arbre d’inférence qui justifie son verdict — la chaîne des règles logiques (modus ponens, transitivité, rewrite…) menant de ses hypothèses à la contradiction.

Pourquoi cela change la lecture d’une preuve. Sans l’arbre, UNSATISFIABLE est une affirmation boîte noire. Avec l’arbre, on peut inspecter le raisonnement : quelles simplifications algébriques ont été appliquées, quelles instanciations de quantificateurs, quelles réécritures. C’est ce qui distingue un décideur (qui répond) d’un prouveur (qui justifie). Et c’est aussi ce qui explique le UNKNOWN de Fermat (section 7) : faute d’arbre de preuve, Z3 ne peut pas certifier le résultat.

using Microsoft.Z3;
using System.Collections.Generic;

// Active la production de l'arbre de preuve.
var ctxP = new Context(new Dictionary<string, string> { { "proof", "true" } });
var xP = (ArithExpr)ctxP.MkConst("x", ctxP.RealSort);
var corpsP = ctxP.MkEq(ctxP.MkAdd(xP, ctxP.MkReal(0)), xP);
var formuleP = ctxP.MkForall(new Expr[] { xP }, corpsP);

var sP = ctxP.MkSolver();
sP.Add(ctxP.MkNot(formuleP));
Console.WriteLine("Statut : " + sP.Check());

// Chaque nœud de l'arbre porte le nom de la RÈGLE d'inférence appliquée
// (mp = modus ponens, trans = transitivité, rewrite = réécriture, etc.).
Expr preuve = sP.Proof;
int noeuds = 0;
void Parcourir(Expr p, int prof)
{
    noeuds++;
    if (prof > 7) return;
    string etiquette = p.IsApp ? p.FuncDecl.Name.ToString() : p.ToString();
    Console.WriteLine(new string(' ', prof * 2) + "- [" + etiquette + "]");
    if (p.IsApp)
        foreach (Expr fils in p.Args) Parcourir(fils, prof + 1);
}
Console.WriteLine("\nArbre d'inférence (règles de Z3) :");
Parcourir(preuve, 0);

// Vocabulaire des règles : les briques du raisonnement de Z3
var regles = new HashSet<string>();
void Collecter(Expr p)
{
    if (p.IsApp) { regles.Add(p.FuncDecl.Name.ToString()); foreach (Expr a in p.Args) Collecter(a); }
}
Collecter(preuve);
Console.WriteLine($"\nNoeuds : {noeuds} | Règles : {string.Join(", ", regles)}");

Statut : UNSATISFIABLE

Arbre d'inférence (règles de Z3) :
- [mp]
  - [asserted]
    - [not]
      - [(forall ((x Real)) (= (+ x 0.0) x))]
  - [trans]
    - [monotonicity]
      - [trans]
        - [quant-intro]
          - [proof-bind]
            - [(lambda ((x Real))
  (let ((a!1 (monotonicity (rewrite (= (+ x 0.0) x))
                           (= (= (+ x 0.0) x) (= x x)))))
    (trans a!1 (rewrite (= (= x x) true)) (= (= (+ x 0.0) x) true))))]
          - [=]
            - [(forall ((x Real)) (= (+ x 0.0) x))]
            - [(forall ((x Real)) true)]
        - [elim-unused]
          - [=]
            - [(forall ((x Real)) true)]
            - [true]
        - [=]
          - [(forall ((x Real)) (= (+ x 0.0) x))]
          - [true]
      - [=]
        - [not]
          - [(forall ((x Real)) (= (+ x 0.0) x))]
        - [not]
          - [true]
    - [rewrite]
      - [=]
        - [not]
          - [true]
        - [false]
    - [=]
      - [not]
        - [(forall ((x Real)) (= (+ x 0.0) x))]
      - [false]
  - [false]

Noeuds : 35 | Règles : mp, asserted, not, trans, monotonicity, quant-intro, proof-bind, =, elim-unused, true, rewrite, false

Lecture de l’arbre. La racine est mp — le modus ponens — qui combine la négation de la formule (asserted) et une chaîne de réécritures (rewrite, trans) ramenant x + 0 == x à l’identité triviale. Chaque nœud nomme la règle appliquée : rewrite pour les simplifications algébriques, quant-intro pour l’introduction du quantificateur, monotonicity pour la propagation d’égalité.

Le pont avec le cas unknown. Sur Fermat (section 7), Z3 répond UNKNOWN : aucun arbre de preuve n’est produit, parce que la théorie des entiers avec exponentiation dépasse la classe décidable du solveur. La présence de l’arbre est donc elle-même une garantie : quand Z3 répond UNSATISFIABLE en mode proof=true, il peut en exhiber la justification — c’est ce qui fonde la confiance dans le verdict, par opposition au UNKNOWN qui reste une absence de conclusion.

Limite honnête. L’arbre de preuve de Z3 est une trace du raisonnement interne au solveur — précieuse pour l’audit et le débogage, mais pas une preuve au format que vérifierait un assistant de preuve comme Lean (section Lean de la série). Pour une preuve exportable et vérifiable de façon indépendante, il faudrait passer par un proof certifié (format Dedukti ou étapes Lean), ce qui dépasse le cadre de ce notebook d’introduction à l’API Z3.

Exercices

Trois exercices a completer. Les stubs retournent null.

// EXERCICE 1 : Prouver l identite multiplicative par refutation.
// Verifier que ForAll(x, x * 1 == x) est valide sur les reels.
// Indice : niez la formule et regardez le verdict.
// Etape 1 : declarer x = (ArithExpr)ctx.MkConst("x", ctx.RealSort)
// Etape 2 : formule = ctx.MkForall(new Expr[]{x}, ctx.MkEq(ctx.MkMul(x, ctx.MkReal(1)), x))
// Etape 3 : s.Add(ctx.MkNot(formule)), return s.Check() == Status.UNSATISFIABLE
bool? ProuverIdentiteMultiplicative(Context ctx)
{
    // TODO etudiant : implementez la preuve par refutation
    return null;  // TODO etudiant : remplacer par true (valide) ou false (fause)
}

var r1 = ProuverIdentiteMultiplicative(new Context());
Console.WriteLine("Exercice 1 (x * 1 == x valide ?) : " + (r1.HasValue ? r1.Value.ToString() : "(a completer)"));

Exercice 1 (x * 1 == x valide ?) : (a completer)

// EXERCICE 2 : Verifier si un carre negatif existe sur les reels.
// Existe-t-il x reel tel que x*x < 0 ? Retourne true si sat, false sinon.
// Indice : MkExists + MkLt(x*x, 0) + Check.
// Etape 1 : declarer x = (ArithExpr)ctx.MkConst("x", ctx.RealSort)
// Etape 2 : s.Add(ctx.MkExists(new Expr[]{x}, ctx.MkLt(ctx.MkMul(x,x), ctx.MkReal(0))))
// Etape 3 : return s.Check() == Status.SATISFIABLE
bool? ExisteCarreNegatif(Context ctx)
{
    // TODO etudiant : implementez la verification
    return null;  // TODO etudiant : remplacer par true ou false
}

var r2 = ExisteCarreNegatif(new Context());
Console.WriteLine("Exercice 2 (un carre negatif existe ?) : " + (r2.HasValue ? r2.Value.ToString() : "(a completer)"));

Exercice 2 (un carre negatif existe ?) : (a completer)

// EXERCICE 3 : Prouver qu il n existe pas de plus grand reel.
// Verifier que ForAll(x, Exists(y, y > x)) est valide sur les reels.
// Indice : niez toute la formule et regardez le verdict.
// Etape 1 : declarer x, y = (ArithExpr)ctx.MkConst(..., ctx.RealSort)
// Etape 2 : nest = ctx.MkForall(new Expr[]{x}, ctx.MkExists(new Expr[]{y}, ctx.MkGt(y, x)))
// Etape 3 : s.Add(ctx.MkNot(nest)), return s.Check() == Status.UNSATISFIABLE
bool? ProuverPasDePlusGrandReel(Context ctx)
{
    // TODO etudiant : implementez la preuve par refutation
    return null;  // TODO etudiant : remplacer par true ou false
}

var r3 = ProuverPasDePlusGrandReel(new Context());
Console.WriteLine("Exercice 3 (pas de plus grand reel, valide ?) : " + (r3.HasValue ? r3.Value.ToString() : "(a completer)"));

Exercice 3 (pas de plus grand reel, valide ?) : (a completer)

Conclusion

Ce twin C# couvre les quantificateurs (MkForall/MkExists sur new Expr[]{ constantes }) et la preuve par refutation (une formule universelle est valide ssi sa negation est insatisfiable) avec le moteur reel Microsoft.Z3. On a prouve l’identite additive/multiplicative, la commutativite, la trichotomie, la monotonie du carre, et l’absence de plus grand reel ; traite le piege de la variable liee par Exists (skolemisation) ; et affronte honnetement la limite UNKNOWN de l’arithmetique non lineaire entiere (Fermat, avec ReasonUnknown).

Complementarite : le twin Python utilise ForAll([x], ...) / Exists([x], ...) / is_true(simplify(...)) (API pythonique, unsat/sat/unknown litteraux) ; ce twin C# montre l’API .NET (MkForall(new Expr[]{x}, body) / Status.UNSATISFIABLE enum / ReasonUnknown propriete / Set("timeout", N)), avec le casting (ArithExpr) systématique des constantes reelles/entieres. Les deux executent le même moteur Z3 et demontrent les mêmes theoremes.