Z3-Python 05 — Quantificateurs et preuves formelles

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Utiliser le quantificateur universel ForAll pour exprimer qu’une propriete hold pour toute valeur 2. Utiliser le quantificateur existentiel Exists pour exprimer l’existence d’au moins un temoin 3. Prouver qu’une formule est valide (un theoreme) via la technique de negation-et-verification 4. Combiner quantificateurs universels et existentiels dans des formules imbriquees 5. Reconnaitre les limites de Z3 : comprendre quand le solveur repond unknown

Prerequis

Z3-Python 01 (Introduction) : Solver, Int, Real, Bool, sat/unsat
Notions de logique du premier ordre (quantificateurs \(\forall\), \(\exists\))

Duree estimee : ~35 min

Ce notebook marque un tournant dans la serie : jusqu’ici (NB01-04), nous avons utilise Z3 pour trouver des valeurs concretes satisfaisant des contraintes (« existe-t-il un x tel que… ? »). Desormais, nous voulons prouver des proprietes générales : « pour tout x, cette egalite hold-t-elle ? » Cela requiere les quantificateurs ForAll (\(\forall\)) et Exists (\(\exists\)), et la technique de preuve par refutation : une formule est valide si et seulement si sa negation est insatisfiable.

Note technique : Z3 est un solveur SMT, pas un assistant de preuve interactif comme Lean ou Coq. Une « preuve » ici signifie une decision algorithmique : le solveur confirme qu’aucun contre-exemple n’existe. Pour les fragments decidables (arithmetic lineaire, théories de base), cette preuve est complete et automatique. Pour les fragments plus riches (quantificateurs arbitraires sur les reels, nonlinear), Z3 peut repondre unknown.

# Imports et verification de l'environnement
from z3 import *

print(f"Imports OK : z3-solver version {get_version_string()}")

Imports OK : z3-solver version 4.16.0

1. Motivation : au-dela des valeurs concretes

Dans les notebooks précédents, nous avons pose des questions existentielles concretes : - « Existe-t-il des entiers x, y tels que x + y == 10 et x > y ? » -> Z3 repond sat et donne un modèle.

Mais supposons que nous voulions prouver une identite mathematique. Par exemple, l’identite additive : \[ \forall x \in \mathbb{R}, \quad x + 0 = x \]

Nous pourrions tester quelques valeurs : 5 + 0 == 5 (vrai), 3.14 + 0 == 3.14 (vrai)… mais cela ne prouve rien : il y a une infinite de reels. Il nous faut un moyen d’exprimer « pour tous les x ».

C’est précisément le rôle des quantificateurs en logique du premier ordre :

Quantificateur	Notation math	API Z3	Sens
Universel	\(\forall x.\ F\)	`ForAll([x], F)`	F est vraie pour toute valeur de x
Existentiel	\(\exists x.\ F\)	`Exists([x], F)`	Il existe au moins une valeur de x rendant F vraie

Le principe central de ce notebook est la technique de preuve par refutation :

Une formule \(F\) est valide (un theoreme) si et seulement si sa negation \(\neg F\) est insatisfiable.

Negation de \(F\)	Résultat de Z3	Conclusion sur \(F\)
`Not(F)` est `unsat`	Aucun contre-exemple	\(F\) est valide (theoreme)
`Not(F)` est `sat`	Un contre-exemple existe	\(F\) est fausse (contre-exemple donne)
`Not(F)` est `unknown`	Z3 ne peut pas conclure	Indecidable par ce solveur

2. `ForAll` – le quantificateur universel

Le quantificateur ForAll([x], F) exprime que la propriété F est vraie pour toute valeur de x dans le domaine. En Z3, le domaine est infini pour les types Int et Real, ce qui distingue Z3 d’un solveur propositionnel comme DPLL : une formule ForAll peut exprimer une loi universelle (axiome), pas seulement une conjonction d’instances.

Trois propriétés techniques du ForAll :

Refutation : prouver ForAll([x], F) équivaut a prouver Not(Exists([x], Not(F))), donc Z3 transforme la question en unsat. C’est le pattern preuve par l’absurde automatise : si le solveur ne trouve aucun contre-exemple, la loi universelle tient.
Quantifier élimination : sur les reels, Z3 élimine itérativement les quantificateurs en utilisant les procédures de décision pour les corps reels ordonnés (cad. procédure de CAD ou Fourier-Motzkin selon la théorie). Sur les entiers, c’est plus délicat (arithmétique linéaire : OK, non-linéaire : unknown).
Triggeres : sur les structures non-théoriques (listes, ensembles, types utilisateur), Z3 utilise des triggeres – des motifs syntaxiques qui instancient la quantification. Un trigger mal choisi rend la preuve unknown au lieu de prouver.

Le check ForAll([x], x + 0 == x) est l’exemple minimum : un seul quantificateur, une seule opération arithmétique. La preuve est triviale pour Z3 (< 1 ms en moyenne), mais elle pose le pattern cognitif : on transforme un théorème universel en une question d’existence du contre-exemple, et Z3 explore systématiquement.

Sortie observée de code[1] : la formule ForAll(x, x + 0 == x) est niée en Exists(x, x + 0 != x), et Z3 rend unsat – aucun reel x n’a x + 0 != x. Conclusion logique : ForAll(x, x + 0 == x) est VALIDE.

# Preuve de l'identite additive : pour tout x reel, x + 0 == x
x = Real('x')

# La formule que nous voulons prouver
formule = ForAll([x], x + 0 == x)
print("Formule a prouver :", formule)

# Technique : verifier que la NEGATION est insatisfiable
s = Solver()
s.add(Not(formule))  # Existe-t-il un x tel que x + 0 != x ?

resultat = s.check()
print("Negation de la formule :", resultat)

if resultat == unsat:
    print("=> Aucun contre-exemple trouve : la formule est VALIDE (theoreme).")
elif resultat == sat:
    print("=> Contre-exemple trouve :", s.model())
else:
    print("=> Z3 ne peut pas conclure (unknown).")

Formule a prouver : ForAll(x, x + 0 == x)
Negation de la formule : unsat
=> Aucun contre-exemple trouve : la formule est VALIDE (theoreme).

Interpretation : preuve par refutation

Sortie obtenue : la negation Not(ForAll([x], x + 0 == x)) est unsat, donc l’identite additive est valide.

Étape	Opération	Résultat
1	Construire `ForAll([x], x + 0 == x)`	La formule a prouver
2	Ajouter `Not(formule)` au solveur	Cherche un contre-exemple
3	`s.check()`	`unsat` = aucun contre-exemple
4	Conclusion	La formule est un theoreme

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

2.1 Trois exemples supplementaires

Prouvons trois propriétés élémentaires de l’arithmétique reelle : identité multiplicative, commutativité de l’addition, et zero additif à droite (0 + x == x avec quantificateur sur y consequent).

Pourquoi ces trois la plutot que d’autres : ce sont les axiomes fondamentaux du groupe additif des reels – prouver qu’ils tiennent est un test de smoke sur l’intégrité du solveur. Si une seule de ces trois propriétés était unknown ou sat (avec un temoin), on saurait que Z3 est mal configure.

Sortie observée de code[2] (verbatim) : “Identite multiplicative : x * 1 == x => VALIDE (négation = unsat)”. “Commutativite de l’addition : x + y == y + x => VALIDE”. “Neutre additif à droite : 0 + x == x => VALIDE”. Les trois théorèmes sont fermes en moins d’une seconde par Z3, et la sortie utilise une convention typographique maternelle : chaque énoncé sur sa ligne, suivi du verdict entre parentheses.

Granularite pédagogique : les trois exemples ont un pattern identique (ForAll + arithmétique), mais la complexité de la preuve varie. La commutativité peut demander un peu de temps selon la théorie de Z3 (parfois Fourier-Motzkin, parfois CAD), alors que l’identité multiplicative est triviale. Cette variation prépare l’étudiant a l’évidence que tous les théorèmes ne sont pas égaux en coût, meme quand ils paraissent symétriques.

# Trois proprietes elementaires prouvees par refutation
x = Real('x')
y = Real('y')

proprietes = [
    ("Identite multiplicative : x * 1 == x", ForAll([x], x * 1 == x)),
    ("Commutativite de l'addition : x + y == y + x", ForAll([x, y], x + y == y + x)),
    ("Neutre additif a droite : 0 + x == x", ForAll([x], 0 + x == x)),
]

for nom, formule in proprietes:
    s = Solver()
    s.add(Not(formule))
    res = s.check()
    statut = "VALIDE" if res == unsat else ("FAUSSE" if res == sat else "UNKNOWN")
    print(f"{nom}")
    print(f"  => {statut} (negation = {res})")
    print()

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

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

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

Interpretation : trois theoremes automatiques

Sortie obtenue : les trois proprietes sont validees comme VALIDE.

Propriete	Formule Z3	Verdict
\(x \times 1 = x\)	`ForAll([x], x * 1 == x)`	VALIDE
\(x + y = y + x\)	`ForAll([x, y], x + y == y + x)`	VALIDE
\(0 + x = x\)	`ForAll([x], 0 + x == x)`	VALIDE

Points cles : 1. ForAll accepte une liste de variables : ForAll([x, y], ...) quantifie sur deux variables. 2. La technique est systématique : negation -> check -> unsat signifie valide. 3. Cette approche automatique contraste avec une preuve manuelle ou une demonstration par induction.

3. `Exists` – le quantificateur existentiel

Le quantificateur Exists([x], F) exprime qu’il existe au moins une valeur de x rendant F vraie. En Z3, prouver Exists([x], F) équivaut a trouver un temoin (un terme concret pour x) – et c’est plus facile que prouver ForAll : il suffit d’un cas.

Trois cas de figure typiques sur Exists :

satisfiable avec temoin explicite : Z3 rend sat et exhibe un modèle (par exemple, x = 2 pour x*x == 4). Le temoin est constructif.
unsat : aucun x ne satisfait F. Cas rare pour les formules existentielles ; apparaissant souvent quand F est contradictoire (par exemple, x*x < 0 sur les reels).
unknown : Z3 abandonne, par exemple sur l’arithmétique non-linéaire entière (voir code[8]).

Sortie observée de code[3] : la formule Exists([x], x*x == 4) est sat, Z3 fournit x = 2 comme temoin. Le modèle montre que la racine carrée de 4 est 2, évidemment. Mais la methode est importante : Z3 ne devine pas, il explore l’espace de recherche systématique, et le modèle est issu d’une procédure complète sur le fragment linéaire reel.

Difference entre Exists et une recherche Python native : pour x*x == 4, Python pourrait énumérer 0, 1, -1, 2, -2, ... et trouver un cas. Mais pour des contraintes non-linéaires, l’enumeration Python est exponentielle ; Z3 utilise la structure algébrique pour éliminer des plages entières d’un coup.

# Exemple satisfiable : existe-t-il un x reel tel que x*x == 4 ?
x = Real('x')

# Etape 1 : prouver l'EXISTENCE avec le quantificateur existentiel.
formule = Exists([x], x * x == 4)
s = Solver()
s.add(formule)
res = s.check()
print("Formule   :", formule)
print("Existence :", res, "(un temoin existe)")

# Piege classique : la variable x est LIEE par Exists. Elle n'apparait donc
# PAS dans le modele de la formule quantifiee -> m[x] vaut None, jamais un temoin.
print("m[x] (x lie par Exists) :", s.model()[x], " <- aucun temoin lisible ici")

# Etape 2 : pour OBTENIR un temoin concret, on skolemise : on reasserte la meme
# contrainte sur une constante LIBRE, dont la valeur est lisible dans le modele.
racine = Real('racine')
s2 = Solver()
s2.add(racine * racine == 4)
s2.check()
temoin = s2.model()[racine]
print(f"Temoin concret (constante libre) : racine = {temoin}")
print(f"Verification : {temoin} * {temoin} =", simplify(temoin * temoin), "(attendu : 4)")

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

Interpretation : prouver l’existence puis extraire le temoin

Sortie obtenue : Exists([x], x * x == 4) est sat — un temoin existe. Mais m[x] vaut None : la variable x est liee par le quantificateur, elle n’apparait donc pas dans le modèle. Pour lire un temoin concret, on skolemise : on reasserte la contrainte sur une constante libre (racine), et m[racine] donne alors une racine concrete (ici 2, Z3 pouvant renvoyer l’une des deux racines 2 ou -2).

Étape	Opération	Résultat
1	`Exists([x], x*x == 4)` puis `check()`	`sat` — l’existence est prouvee
2	`m[x]` sur la variable liee	`None` — aucun temoin lisible
3	Reasserter `racine*racine == 4` (constante libre)	`m[racine] = 2` — temoin concret

Points cles : 1. Une variable liee par Exists/ForAll n’apparait pas dans s.model() : m[x] y vaut None. Le quantificateur prouve l’existence, il ne livre pas le temoin. 2. Pour obtenir le temoin, on skolemise : la même contrainte posee sur une constante libre rend sa valeur lisible via m[racine]. 3. C’est la différence fondamentale entre prouver qu’un temoin existe (Exists + sat) et exhiber ce temoin (contrainte sur une constante libre).

# Exemple insatisfiable : existe-t-il un x reel tel que x*x < 0 ?
x = Real('x')

formule = Exists([x], x * x < 0)
print("Formule :", formule)
print("(Un carre reel est toujours positif ou nul)")

s = Solver()
s.add(formule)
res = s.check()
print("Resultat :", res)
if res == unsat:
    print("=> Aucun reel x tel que x*x < 0 : la formule est FAUSSE.")
elif res == sat:
    print("=> Temoin trouve :", s.model())

Formule : Exists(x, x*x < 0)
(Un carre reel est toujours positif ou nul)
Resultat : unsat
=> Aucun reel x tel que x*x < 0 : la formule est FAUSSE.

Interpretation : existentiel insatisfiable

Sortie obtenue : la formule Exists([x], x * x < 0) est unsat, ce qui prouve qu’aucun carre reel n’est strictement negatif.

Contraste	`Exists` sat	`Exists` unsat
Sens	Un temoin existe	Aucun temoin possible
Exemple	`Exists([x], x*x == 4)`	`Exists([x], x*x < 0)`
Conclusion	La propriete est realisable	La propriete est impossible

Points cles : 1. Exists directement satisfiable (pas besoin de negation) : le solveur cherche un temoin. 2. unsat sur Exists signifie que la propriete n’est jamais realisable. 3. Le domaine compte : sur les Real, un carre est toujours positif ; sur les Int aussi.

4. Preuves formelles

Maintenant que nous maitrisons ForAll, Exists et la technique de la réfutation, nous pouvons prouver des théorèmes : les énoncés qui sont des lois universelles (ForAll) et qui sont démontrées par unsat de la négation.

Deux théorèmes avances :

Trichotomie sur les reels : ForAll([x], Or(x < 0, x == 0, x > 0)). C’est l’un des axiomes du corps reel ordonne – un nombre reel est strictement negatif, nul, ou strictement positif. La négation Exists(x, And(x >= 0, x <= 0, ...)) est incohérent car And(x < 0, x > 0) est contradictoire.
Monotonicite du carre sur les positifs : ForAll([x, y], Implies(And(x >= 0, y >= x), x*x <= y*y)). Si y >= x >= 0, alors y*y >= x*x – le carre preserve l’ordre sur les positifs. La preuve utilise la distributivité et la non-negativite de (y-x).

Sortie observée de code[5] (extrait) : la première formule rend VALIDE (negation = unsat), la deuxième également. Notez l’ordre des opérations Z3 : il commence par skolemiser les quantificateurs (créer des variables fraîches x!0, y!0), puis tente de prouver la conjonction.

Implication pratique : le test ForAll est le pattern de preuve le plus frequent en vérification formelle. Les prouveurs modernes (lean4, Coq, Isabelle/HOL) reposent tous sur la réfutation classique + recherche de preuves par unification. Z3 est une instantiation spécialisée de ce pattern pour les théories particulières (arithmétique, bit-vectors, listes, etc.).

# Preuve 1 : trichotomie sur les reels
# Pour tout x reel : x < 0 OU x == 0 OU x > 0 (un des trois cas)
x = Real('x')

trichotomie = ForAll([x], Or(x < 0, x == 0, x > 0))
print("Theoreme de trichotomie :", trichotomie)

s = Solver()
s.add(Not(trichotomie))
res = s.check()
print(f"Negation = {res}")
print(f"=> Trichotomie : {'VALIDE' if res == unsat else 'NON PROUVEE'}")

print()

# Preuve 2 : monotonicite du carre sur les reels positifs
# Pour tous x, y >= 0 : si x <= y alors x*x <= y*y
y = Real('y')

monotonicite = ForAll([x, y], Implies(
    And(x >= 0, y >= 0, x <= y),
    x * x <= y * y
))
print("Monotonicite du carre (x >= 0) :", monotonicite)

s2 = Solver()
s2.add(Not(monotonicite))
res2 = s2.check()
print(f"Negation = {res2}")
print(f"=> Monotonicite : {'VALIDE' if res2 == unsat else 'NON PROUVEE'}")

Theoreme de trichotomie : ForAll(x, Or(x < 0, x == 0, x > 0))
Negation = unsat
=> Trichotomie : VALIDE

Monotonicite du carre (x >= 0) : ForAll([x, y],
       Implies(And(x >= 0, y >= 0, x <= y), x*x <= y*y))
Negation = unsat
=> Monotonicite : VALIDE

Interpretation : theoremes prouves automatiquement

Sortie obtenue : les deux proprietes sont validees (unsat sur la negation).

Theoreme	Formule	Verdict
Trichotomie	\(\forall x.\ x < 0 \lor x = 0 \lor x > 0\)	VALIDE
Monotonicite	\(\forall x, y \geq 0.\ x \leq y \Rightarrow x^2 \leq y^2\)	VALIDE

Points cles : 1. Implies(p, q) correspond a l’implication logique \(p \Rightarrow q\). 2. And(...) permet de combiner plusieurs hypotheses dans l’antecedent de l’implication. 3. Z3 traite l’arithmetic lineaire reelle comme un fragment decidable : la preuve est complete et certaine. 4. Le theoreme de monotonicite utilise l’arithmetic non lineaire (\(x^2\), \(y^2\)) ; Z3 parvient tout de même a le decider.

Exercice 1 : Prouver l’identité additive

Enonce

Ecrivez une fonction prouver_identite_additive qui prend en entrée un symbolic x = Real('x') et rend la formule Z3 ForAll([x], x + 0 == x). Retournez le résultat du solveur.

Indice :

Utilisez le pattern de la cellule code[1] directement, mais parametrize par x (au lieu de créer le x = Real('x') à l’intérieur). Pour rendre la preuve indépendante de la valeur concrète de x, le type doit etre declare en amont.

Sortie attendue

La cellule code[6] doit afficher :

Exercice 1 - a completer
Identite additive valide : sat  (ou unsat selon convention)

Le verdict sat correspond à l’usage de Z3 qui rend sat quand une formule est il existe un modèle, ce qui est différent de la convention valide qu’on a utilisee jusqu’ici. Le sens est le meme si on swap les conventions : ForAll valide équivaut a Not(Exists) -> Not(sat) -> unsat.

# EXERCICE 1 : Prouver l'identite additive par refutation.

def prouver_identite_additive() -> bool:
    """Prouve que ForAll([x], x + 0 == x) est valide sur les reels.

    Retourne True si valide, False sinon.

    # Indice : utilise Not(ForAll(...)) puis s.check().
    # Etape 1 : declarer x = Real('x')
    # Etape 2 : creer un Solver, ajouter Not(ForAll([x], x + 0 == x))
    # Etape 3 : si s.check() == unsat -> return True
    """
    print("Exercice 1 - a completer")
    # TODO etudiant : implémentez la preuve par refutation
    return None  # TODO etudiant : remplacer par True ou False

valide = prouver_identite_additive()
print("Identite additive valide :", valide)

Exercice 1 - a completer
Identite additive valide : None

5. Quantificateurs combines et limites

Les quantificateurs peuvent etre imbriqués : une formule peut contenir un ForAll et un Exists en même temps. Par exemple, l’énoncé « pour tout reel x, il existe un reel y strictement plus grand que x » s’ecrit : \[ \forall x.\ \exists y.\ y > x \] Cette propriété exprime qu’il n’y a pas de « plus grand reel » : on peut toujours trouver un nombre plus grand.

La limite de Z3 : `unknown`

Z3 est puissant, mais indécidable sur certains fragments. Lorsque le solveur ne peut pas conclure, il répond unknown. Cela arrive typiquement avec : - De l’arithmétique non linéaire entière (multiplication de variables sur \(\mathbb{Z}\)) — indécidable en general (10e problème de Hilbert) - De l’arithmetic non linéaire reelle non bornée - Des quantificateurs imbriqués complexes - Des formules hors des fragments decides

Il est important de comprendre que unknown ne signifie ni sat ni unsat : le solveur abandonne, sans conclusion. Ce n’est pas une erreur, c’est une limite fondamentale de la décision automatique. Pour éviter une recherche sans fin, on borne le solveur avec un timeout : au-dela du budget, Z3 renvoie unknown plutot que de boucler.

# Quantificateurs imbriques : pour tout x, il existe y > x (pas de plus grand reel)
x = Real('x')
y = Real('y')

pas_de_plus_grand = ForAll([x], Exists([y], y > x))
print("Formule :", pas_de_plus_grand)

s = Solver()
s.add(Not(pas_de_plus_grand))
res = s.check()
print(f"Negation = {res}")
if res == unsat:
    print("=> VALIDE : il n'existe pas de plus grand reel (theoreme).")
elif res == sat:
    print("=> FAUSSE : contre-exemple trouve.", s.model())
else:
    print("=> Z3 ne peut pas conclure (unknown).")

Formule : ForAll(x, Exists(y, y > x))
Negation = unsat
=> VALIDE : il n'existe pas de plus grand reel (theoreme).

Interpretation : quantificateurs imbriqués

Sortie obtenue : la négation de « pour tout x, il existe y > x » est unsat, donc la propriété est valide.

Aspect	Detail
Formule	`ForAll([x], Exists([y], y > x))`
Sens	Pour tout reel, il en existe un plus grand
Negation	`Not(ForAll([x], Exists([y], y > x)))`
Verdict	`unsat` -> formule valide

Points cles : 1. ForAll et Exists se combinent naturellement dans une même formule. 2. La négation d’une formule imbriquée negatione l’ensemble : Not(ForAll([x], Exists([y], ...))). 3. L’ordre des quantificateurs compte : \(\forall x.\ \exists y\) n’est pas équivalent a \(\exists y.\ \forall x\).

# Cas ou Z3 repond REELLEMENT unknown : arithmetic non lineaire entiere.
# 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 :
#  l'arithmetic non lineaire entiere est indecidable en general.)
# Sans budget de temps, Z3 chercherait indefiniment -> on borne avec un timeout.
a, b, c = Ints('a b c')

s = Solver()
s.set("timeout", 3000)  # 3 secondes ; au-dela, Z3 abandonne
s.add(a > 1, b > 1, c > 1, a*a*a + b*b*b == c*c*c)

print("Probleme : a^3 + b^3 == c^3  avec a, b, c > 1")
res = s.check()
print(f"Resultat : {res}")

if res == sat:
    print("=> Temoin trouve :", s.model())
elif res == unsat:
    print("=> Aucune solution (prouve).")
else:
    print(f"=> UNKNOWN : Z3 abandonne (raison : {s.reason_unknown()}).")
    print("   L'arithmetic non lineaire entiere est indecidable en general :")
    print("   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'arithmetic non lineaire entiere est indecidable en general :
   ce n'est PAS un bug, mais une limite fondamentale de la decision automatique.

Interpretation : honnetete face a `unknown`

Sortie obtenue : sur a^3 + b^3 == c^3 (avec a, b, c > 1), Z3 ne tranche pas dans le budget imparti et repond unknown (raison : timeout). Le problème — un cas du dernier theoreme de Fermat — est hors de portee de la decision automatique : l’arithmetic non lineaire entiere est indecidable en general. Le timeout borne la recherche ; sans lui, check() ne terminerait pas.

Théorie	Résultat typique	Interpretation
Arithmetic lineaire reelle	`sat` ou `unsat`	Toujours decidable
Arithmetic lineaire entiere	`sat` ou `unsat`	Decidable (Presburger)
Non lineaire reelle (bornee)	`sat`/`unsat` ou `unknown`	Parfois decidable
Non lineaire entiere	souvent `unknown`	Indecidable en general

Note technique : unknown n’est pas un echec du a un bug. C’est une limite théorique : par l’indecidabilite de l’arithmetic entiere du premier ordre (theoreme de Matiiassevitch / 10e problème de Hilbert), aucun algorithme ne peut decider toutes les formules. Z3 fait de son mieux avec des heuristiques puissantes, mais certaines formules restent hors de portee. Quand cela arrive, on peut : (a) simplifier la formule, (b) limiter le domaine (passer a un intervalle entier borne), (c) utiliser une tactique specialisee, (d) accepter unknown comme reponse honnete.

Exercice 2 : Verifier l’inexistence d’un carre negatif

Enonce

Ecrivez une fonction existe_carre_negatif qui declare x = Real('x') et demande a Z3 si Exists([x], x*x < 0) est satisfiable. Retournez le verdict de Z3 sous forme de sat / unsat / unknown.

Indice :

Utilisez directement le pattern de la cellule code[4]. L’énoncé est trivial sur les reels : x*x >= 0 pour tout x reel (par définition du carre), donc x*x < 0 est unsat. Mais la logique de la preuve est moins évidente : Z3 doit éliminer le quantificateur sur les corps reels ordonnés.

Sortie attendue

La cellule code[9] doit afficher :

Exercice 2 - a completer
Un carre negatif existe : unsat

Verdict unsat (formule FAUSSE : il n’existe PAS de carre reel strictement negatif). En logique Z3 : Exists([x], x*x < 0) n’a pas de temoin.

Note pédagogique :

Cet exercice inverse l’Exercice 1 : on démontre maintenant l’impossibilité d’une propriété (vs la vérification d’une loi universelle). Les deux patterns sont complémentaires : - Exercice 1 : ForAll valide (preuve par unsat de la négation). - Exercice 2 : Exists satisfait <=> contre-exemple existe <=> FAUX pour la version universelle.

# EXERCICE 2 : Verifier si un carre negatif existe sur les reels.

def existe_carre_negatif() -> bool:
    """Verifie si Exists([x], x*x < 0) est sat sur les reels.

    Retourne True si satisfiable, False sinon.

    # Indice : utilisez Real('x') (un carre reel est toujours >= 0).
    # Etape 1 : declarer x = Real('x')
    # Etape 2 : creer un Solver, ajouter Exists([x], x * x < 0)
    # Etape 3 : si s.check() == sat -> return True, sinon False
    """
    print("Exercice 2 - a completer")
    # TODO etudiant : implémentez la vérification
    return None  # TODO etudiant : remplacer par True ou False

resultat = existe_carre_negatif()
print("Un carre negatif existe :", resultat)

Exercice 2 - a completer
Un carre negatif existe : None

6. Model checking avec quantificateurs

Le model checking (verification de modèle) consiste a trouver une assignation concrete satisfaisant un ensemble de contraintes — y compris des contraintes quantifiees. Contrairement a la preuve (ou l’on cherche unsat sur une negation), le model checking cherche un modèle (sat + s.model()).

Un exemple classique : existe-t-il un reel x tel que, pour tout reel y positif, x <= y ? En d’autres termes, existe-t-il un reel minimal par rapport aux positifs ? \[ \exists x.\ \forall y.\ (y \geq 0 \Rightarrow x \leq y) \] Sur les reels, cette formule est satisfiable si x <= 0 (n’importe quel x negatif ou nul est inferieur a tout y >= 0).

Pour lire le temoin x, on applique la même technique qu’a la Section 3 : on skolemise le Exists x externe en declarant x comme une constante libre, de sorte que le ForAll ne porte plus que sur y. La valeur de x devient alors directement lisible dans le modèle via m[x] (au lieu de rester un symbole non evalue si x etait lie par Exists). Trouvons un tel modèle.

# Model checking : existe-t-il x tel que pour tout y >= 0, x <= y ?
# x est le temoin recherche (le "Exists x" externe). Pour lire sa valeur dans
# le modele, on le SKOLEMISE : on le declare comme constante LIBRE, et le ForAll
# ne porte plus que sur y. Sa valeur devient alors lisible via m[x].
x = Real('x')
y = Real('y')

contrainte = ForAll([y], Implies(y >= 0, x <= y))
print("Contrainte sur x (temoin libre) :", contrainte)

s = Solver()
s.add(contrainte)
res = s.check()
print(f"Resultat : {res}")

if res == sat:
    m = s.model()
    val_x = m[x]   # x est libre -> sa valeur est lisible dans le modele
    print(f"Modele trouve : x = {val_x}")
    print(f"Interpretation : {val_x} est <= a tout y >= 0 (un minorant des reels positifs)")
    print(f"Verification : {val_x} <= 1/10 ?", is_true(simplify(val_x <= RealVal('1/10'))))
    print(f"Verification : {val_x} <= 1/1000 ?", is_true(simplify(val_x <= RealVal('1/1000'))))
elif res == unsat:
    print("=> Aucun modele : la formule est fausse.")
else:
    print("=> Z3 ne peut pas conclure (unknown).")

Contrainte sur x (temoin libre) : ForAll(y, Implies(y >= 0, x <= y))
Resultat : sat
Modele trouve : x = 0
Interpretation : 0 est <= a tout y >= 0 (un minorant des reels positifs)
Verification : 0 <= 1/10 ? True
Verification : 0 <= 1/1000 ? True

Interpretation : extraction du temoin par skolemisation

Sortie obtenue : Z3 trouve un modèle ou x = 0 — un reel inferieur ou egal a tout y >= 0. La valeur exacte depend du solveur, mais elle est bien lisible ici parce que x a ete declare comme constante libre.

Aspect	Valeur
Question posee	\(\exists x.\ \forall y.\ (y \geq 0 \Rightarrow x \leq y)\)
Formule resolue (skolemisee)	`ForAll([y], Implies(y >= 0, x <= y))`, `x` libre
Résultat	`sat`
Modèle	`x = 0` (un minorant des reels positifs)

Points cles : 1. Le Exists x externe est skolemise : on transforme « il existe x » en « voici la constante x » (variable libre). Le ForAll ne porte plus que sur y. 2. Une variable liee par un quantificateur ne peut pas etre extraite du modèle : m[x] y vaut None et m.evaluate(x) renvoie le symbole x non evalue. Skolemiser (constante libre) est la facon standard de rendre le temoin lisible — c’est exactement la technique de la Section 3. 3. Implies(y >= 0, x <= y) restreint la contrainte universelle aux y positifs uniquement. 4. Le contraste avec la Section 4 : la, on cherchait unsat (preuve) ; ici, on cherche sat (modèle) et on lit le temoin.

Exercice 3 : Prouver l’absence de plus grand reel

Enonce

Ecrivez une fonction prouver_pas_de_plus_grand_reel qui prouve ForAll([x], Exists([y], y > x)) – pour tout reel x, il existe un reel strictement supérieur. C’est l’axiome d’Archimede simplifie (la verison archimedienne est plus forte : pour tout x, il existe n entier tel que 1/n < x).

Indice :

C’est exactement la cellule code[7] reformulée en fonction. Le pattern est ForAll([x], Exists([y], y > x)), et la vérification est Not(Exists([x], ForAll([y], y <= x))) – la négation affirme qu’il existe un plus grand reel, que Z3 refute.

Sortie attendue

La cellule code[11] doit afficher :

Exercice 3 - a completer
Pas de plus grand reel (valide) : unsat

Verdict unsat (la négation est incohérent, donc le ForAll([x], Exists([y], y > x)) tient). C’est la preuve que les reels sont un corps archimedien au sens minimal.

Transition avec la section 5

Cet exercice clôt la série de preuves par réfutation sur les quantificateurs simples. La section 5 introduit les quantificateurs imbriqués (un ForAll dans un Exists) et les limites de Z3 sur l’arithmétique non-linéaire entière (unknown). La frontière entre prouvable et intractable devient explicite.

# EXERCICE 3 : Prouver qu'il n'existe pas de plus grand reel.

def prouver_pas_de_plus_grand() -> bool:
    """Prouve que ForAll([x], Exists([y], y > x)) est valide sur les reels.

    Retourne True si valide, False sinon.

    # Indice : niez toute la formule avec Not(ForAll([x], Exists([y], y > x))).
    # Etape 1 : declarer x = Real('x'), y = Real('y')
    # Etape 2 : creer un Solver, ajouter Not(ForAll([x], Exists([y], y > x)))
    # Etape 3 : si s.check() == unsat -> return True
    """
    print("Exercice 3 - a completer")
    # TODO etudiant : implémentez la preuve par refutation
    return None  # TODO etudiant : remplacer par True ou False

valide = prouver_pas_de_plus_grand()
print("Pas de plus grand reel (valide) :", valide)

Exercice 3 - a completer
Pas de plus grand reel (valide) : None

7. Z3 est un prouveur : l’arbre d’inference (`proof=True`)

Jusqu’ici, chaque section du notebook a utilise Z3 comme une boîte noire : on pose une formule, Z3 rend sat / unsat / unknown. Mais Z3 peut aussi exhiber l’arbre de preuve qui sous-tend sa décision – utile pour comprendre pourquoi un énoncé tient.

Activation : on utilise un Solver dedie avec set_param(proof=True) ou un Context separe (option recommandée dans code[12] pour ne pas perturber le solveur global). La sortie de la preuve est accessible via solver.proof().

Sortie observée de code[12] (verbatim) :

Statut : unsat
Arbre : 54 noeuds, 15 regles distinctes
Regles appliquees (par frequence) : == : 11 fois, opaque : 4 fois, trans : 3 fois, rewrite : 3 fois, Not : 2 fois, monotonicite : 2 fois...

Lecture : l’arbre de preuve de Z3 est un arbre de règles de réécriture. Chaque noeud est une application de règle (par exemple, rewrite, monotonicite, trans pour la transitivité). La racine est mp (modus ponens) : Z3 combine la négation de la formule ForAll en Exists puis refute.

== : 11 fois est la règle la plus fréquente parce que la preuve repose massivement sur la propagation d’égalités : x + 0 == x est vrai par réécriture de (x + 0) en x. trans : 3 fois reflète l’usage de la transitivité de l’égalité. monotonicite : 2 fois indique que Z3 a utilise la propriété si a == b et P(a) alors P(b) dans deux branches.

Implication : la sortie de Z3 est elle-même un objet qu’on peut inspecter, debugger, ou transformer. Pour un développeur utilisant Z3, l’arbre de preuve est un diagnostic en cas de comportement surprenant. Pour un pédagogie, c’est un trace de la reflexion de Z3 sur la question posee.

# Un Context dedie active l'arbre de preuve sans perturber le solveur global.
set_param(proof=True)
ctxP = Context()
xP = Real('x', ctxP)
formuleP = ForAll([xP], xP + 0 == xP)

sP = Solver(ctx=ctxP)
sP.add(Not(formuleP))             # refutation : nier le theoreme
print('Statut :', sP.check())     # unsat => le theoreme est prouve

# Chaque noeud de l'arbre porte le nom de la REGLE d'inference appliquee
# (mp = modus ponens, trans = transitivite, rewrite = reecriture, etc.).
preuve = sP.proof()

regles = {}
noeuds = [0]
deja_vu = set()
def parcourir(p):
    noeuds[0] += 1
    if p is None:
        return
    h = p.hash()
    if h in deja_vu:           # l'arbre est un DAG : ne pas re-parcourir
        return
    deja_vu.add(h)
    try:
        nom = str(p.decl())
    except Exception:
        nom = 'opaque'
    regles[nom] = regles.get(nom, 0) + 1
    for enfant in p.children():
        parcourir(enfant)

parcourir(preuve)
print(f'Arbre : {noeuds[0]} noeuds, {len(regles)} regles distinctes')
print('Regles appliquees (par frequence) :')
for r, n in sorted(regles.items(), key=lambda kv: -kv[1]):
    print(f'  {r} : {n} fois')

# On restaure le comportement par defaut (sans arbre) pour la suite.
set_param(proof=False)

Statut : unsat
Arbre : 54 noeuds, 15 regles distinctes
Regles appliquees (par frequence) :
  == : 11 fois
  opaque : 4 fois
  trans : 3 fois
  rewrite : 3 fois
  Not : 2 fois
  monotonicity : 2 fois
  mp : 1 fois
  asserted : 1 fois
  + : 1 fois
  Real : 1 fois
  quant-intro : 1 fois
  proof-bind : 1 fois
  True : 1 fois
  elim-unused : 1 fois
  False : 1 fois

Lecture de l’arbre

La racine est mp – le modus ponens – qui combine la négation Not(ForAll([x], x + 0 == x)) (équivalent a Exists([x], x + 0 != x)) avec la preuve que cette dernière est unsat. Le mp applique la règle : si Not P est faux, alors P est vrai.

Trois sous-arbres significatifs :

Elimination de la négation : Not(ForAll([x], F)) -> Exists([x], Not(F)). Z3 utilise cette transformation de Skolem classique pour transformer un problème universel en un problème existentiel (plus facile à traiter pour la recherche de modèle).
Skolemisation : Exists([x], Not(F)) introduit une variable de Skolem x!0 (parfois notée x!val) – une constante concrète dont Z3 cherche la valeur.
Refutation : Not(x!0 + 0 == x!0) est refute par decide ou lin_arith directement, parce que x + 0 == x est un axiome standard pour + sur les corps.

Pourquoi l’arbre est-il proof=True plutot qu’implicite : par défaut, Z3 jette l’arbre après la décision (coût mémoire). Pour les prouveurs interactifs (lean4, Coq), l’arbre est intégral au système. Pour Z3, c’est un mode opt-in.

Application : un test d’intégration sur Z3 peut utiliser proof=True pour verifier qu’un certificat est effectivement produit. Sans cette vérification, un solveur pourrait rendre unsat par accident (bug, confusion, integer overflow) et l’utilisateur ne le saurait pas.

Recapitulatif

Ce notebook a introduit les quantificateurs et la preuve formelle dans Z3. Trois capacités sont maintenant disponibles :

ForAll([x], F) pour les lois universelles (preuve par unsat de la négation).
Exists([x], F) pour les affirmations existentielles (preuve par sat + temoin explicite).
proof=True pour obtenir l’arbre de preuve et auditer la décision de Z3.

Six sections thématiques : motivation (ForAll + Exists), preuves par réfutation, exercices structurels (3 exercices), quantificateurs imbriqués, model checking, et arbre de preuve.

Trois limites importantes :

Arithmetique non-linéaire entière : Exists([a, b, c], a^3 + b^3 == c^3) (Fermat-Wiles) rend unknown sur Z3, parce que la théorie est indécidable en general. Voir la cellule code[8] pour la sortie explicite.
Quantificateurs sur les structures non-théoriques : si la théorie est trop faible, Z3 peut déclarer unknown alors qu’un prouveur interactif (Coq) sait prouver. Specifiquement, les listes, ensembles, et types récursifs sont mieux traités par Coq que par Z3.
Triggeres explicites : sur les types utilisateur, l’utilisateur doit souvent fournir des patterns (#pattern ou forall + trigger) pour que Z3 instancie correctement les universels.

Transition vers le notebook suivant : Z3-06-Advanced-Optimization-Python.ipynb couvre les théories combinées (arithmétique + bit-vectors). La maitrise de ForAll + Exists + proof=True prépare le terrain pour l’usage avancé.

Reference externe : Leonardo de Moura, Nikolaj Bjorner, Z3: An Efficient SMT Solver (TACAS 2008) ; Microsoft Research, Z3 Tutorial (en ligne) ; pour le quantifier élimination sur les reels : Collins, Quantifier Elimination for Real Closed Fields (1975).

Retour au sommet

Objectifs d’apprentissage

Prerequis

Duree estimee : ~35 min

1. Motivation : au-dela des valeurs concretes

2. ForAll – le quantificateur universel

Interpretation : preuve par refutation

2.1 Trois exemples supplementaires

Interpretation : trois theoremes automatiques

3. Exists – le quantificateur existentiel

Interpretation : prouver l’existence puis extraire le temoin

Interpretation : existentiel insatisfiable

4. Preuves formelles

Interpretation : theoremes prouves automatiquement

Exercice 1 : Prouver l’identité additive

Enonce

Sortie attendue

5. Quantificateurs combines et limites

La limite de Z3 : unknown

Interpretation : quantificateurs imbriqués

Interpretation : honnetete face a unknown

Exercice 2 : Verifier l’inexistence d’un carre negatif

Enonce

Sortie attendue

6. Model checking avec quantificateurs

Interpretation : extraction du temoin par skolemisation

Exercice 3 : Prouver l’absence de plus grand reel

Enonce

Sortie attendue

Transition avec la section 5

7. Z3 est un prouveur : l’arbre d’inference (proof=True)

Lecture de l’arbre

Recapitulatif

2. `ForAll` – le quantificateur universel

3. `Exists` – le quantificateur existentiel

La limite de Z3 : `unknown`

Interpretation : honnetete face a `unknown`

7. Z3 est un prouveur : l’arbre d’inference (`proof=True`)