# Décomposition Algébrique Cylindrique en Coq/Rocq

Quentin Vermande

► To cite this version:

Quentin Vermande. Décomposition Algébrique Cylindrique en Coq/Rocq. 2024. hal-04760627

HAL Id: hal-04760627

https://hal.science/hal-04760627v1

Preprint submitted on 30 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Décomposition Algébrique Cylindrique en Coq/Rocq

Quentin VERMANDE

Université Côte d'Azur, INRIA

La Décomposition Algébrique Cylindrique (ou CAD) est un outil fondamental de la géométrie semi-algébrique. C'est un algorithme doublement exponentiel dont l'application phare est l'élimination des quantificateurs dans les formules de la théorie des corps réels clos. En particulier, il permet de décider si des systèmes d'inéquations polynomiales sont satisfiables. Cet article décrit une formalisation de la correction de cet algorithme dans l'assistant de preuve Coq/Rocq. Si l'algorithme n'est pas implémenté de façon à être exécuté, il s'agit d'une étape vers une implémentation vérifiée de la CAD, où les seuls éléments manquant sont des implémentations efficaces des structures de données et des algorithmes requis.

## 1 Introduction

Une Décomposition Algébrique Cylindrique (ou CAD) est une partition de l'espace $\mathbb{R}^n$ en cellules sur lesquelles une famille donnée de polynômes à $n$ variables a un signe constant. Cette notion a été introduite par Collins [Col75] en 1975 dans le but de décider rapidement de la satisfiabilité de formules de la théorie des corps réels clos. Il a été le premier à obtenir un algorithme doublement exponentiel en le nombre de variables et polynomial en les autres paramètres. Depuis son introduction, il y a eu beaucoup d'optimisations de l'algorithme de calcul de la CAD, qui a eu un large champ d'applications incluant des problèmes de robotique [SS83], des problèmes d'optimisation [HJX16] et la vérification de systèmes dynamiques [ST11] et de systèmes hybrides [Pla22]. En tant qu'outil fondamental de la géométrie semi-algébrique, il est omniprésent dans les systèmes de calcul formel. Cet algorithme est connu pour la complexité de sa preuve de correction et a par conséquent été évité dans d'autres travaux de formalisation, comme l'implémentation de l'élimination des quantificateurs en Isabelle [KTP23].

Nous présentons ici une formalisation de la version originelle de l'algorithme par Collins dans l'assistant de preuve Coq/Rocq et une preuve formalisée de la preuve de sa correction, en suivant essentiellement la présentation donnée dans [BPR06]. L'implémentation n'est pas faite pour être exécutée, notamment car elle utilise des structures de données inefficaces. De plus, la procédure d'isolation des racines que nous utilisons ne calcule pas. Pour obtenir un programme exécutable, il faudrait implémenter des structures de données et des algorithmes efficaces et prouver leur équivalence avec ceux que nous utilisons. Nous utilisons la bibliothèque *MathComp*, et plus précisément son extension à la géométrie semi-algébrique [MC12, Dja18]. Certaines des primitives que nous utilisons, comme l'isolation des racines d'un polynôme réel ont déjà été formalisée, tandis que d'autres, comme l'obtention de points entre deux racines d'un polynôme, ne le sont pas.
En quelques mots, l'algorithmme fonctionne par récurrence sur la dimension $n$, le cas de base $n = 0$ étant trivial. En dimension $n + 1$, étant donnée une famille finie de polynômes $\mathcal{P} \subset \mathbb{R}[X_0, ..., X_n]$, on calcule une famille finie $\mathcal{Q}$ de polynômes à $n$ variables et on obtient récursivement une CAD pour $\mathcal{Q}$. Puis, pour chaque cellule $C$ de cette décomposition, le fait que les polynômes de $\mathcal{Q}$ aient un signe constant sur $C$ implique que les $P(x_0, ..., x_{n-1}, X)$, $P \in \mathcal{P}$ ont collectivement un nombre de racines réelles distinctes constant pour $x \in C$. On décrit ces racines par une séquence $f_1, ..., f_d : C \to \mathbb{R}$ de fonctions continues et on obtient alors des cellules de dimensions $n + 1$ en partitionnant le cylindre $C \times \mathbb{R}$ le long des graphes de $f_1, ..., f_d$.

La section 2 décrit les algorithmes dont nous prouvons la correction dans la section 3. Certaines preuves ne seront pas retranscrites, toutes sont consultables dans le projet github concerné. Dans tout le reste de cet article, on considère $R$ un corps réel clos et on appelle $R[i]$ le corps des complexes. On note $\deg'(P)$ le degré d'un polynôme, avec la convention de $\mathit{MathComp}$ selon laquelle $\deg'(0) = 0$, de sorte que $\deg'(0)$ soit un entier naturel.

## 2 Algorithmes

Nous définissons tout d'abord l'objet que l'algorithmme de calcul de la CAD produit. Une décomposition cylindrique est définie par récurrence sur la dimension de l'espace ambiant. Cette définition repose sur la notion de fonction semi-algébrique. On dit qu'une partie $S$ de $R^n$ est semi-algébrique lorsque $S$ est l'ensemble des points de $R^n$ satisfaisant une formule donnée du langage des anneaux ordonnés. Ensuite, une fonction de $R^n$ dans $R^m$ est semi-algébrique lorsque son graphe est semi-algébrique. Les cellules en dimension $n + 1$ sont obtenues en découpant un cylindre $C \times R$ le long de graphes de fonctions $f_1, ..., f_d : C \to R$. On note $\mathit{partition\_along}(C, f)$ l'ensemble des cellules obtenues ainsi à partir de $C$ et $f$.

**Définition 1.** Une partition finie $S$ de $R^n$ est une décomposition cylindrique lorsque $n = 0$ ou, avec $\pi : R^n \to R^{n-1}$ la projection canonique et $T = \{\pi(C), C \in S\}$, $T$ est une décomposition cylindrique de $R^{n-1}$ et, pour tout $C \in T$, il existe une suite $f_1, ..., f_d$ strictement croissant de fonctions semi-algébriques continues de $R^{n-1}$ dans $R^1$ telles que les éléments de $S$ qui se projettent sur $C$ soient les cellules de $\mathit{partition\_along}(C, f)$.

En Coq/Rocq et avec quelques simplifications mineures, cela donne :

```coq
Fixpoint isCylindricalDecomposition n (S : {fset {SAset R^n}}) :=
  SAset_partition S
  /
  match n with | 0 => True | n.+1 =>
    let S' := [fset (s : {SAset R^n}) | s in S] in
    isCylindricalDecomposition S'
    /
   forall (s' : S'),
    exists m, exists xi : m.-tuple {SAfun R^n -> R^1},
      (forall i, {within [set ` val s'], continuous (tnth xi i)})
    /
    sorted <%SA xi
    /
    [fset s in S | (s : {SAset R^n}) == val s']
    = partitionAlong (val s') xi
  end.
```

Il y a deux différences mineures avec la définition donnée dans [BPR06]. Cette dernière commence avec la dimension 1, mais commencer avec la dimension 0 ne change pas les cas récursif des algorithmes et rend les initialisations triviales. De plus, iels définissent une décomposition cylindrique comme une séquence $S_1, ..., S_n$ de partitions, tandis que nous n'introduisons que $S_n$, puisque les autres s'en déduisent par projection. Les décompositions qui nous intéressent sont celles qui respectent une famille de polynômes, au sens suivant :

**Définition 2.** Soit $\mathcal{P}$ une famille de polynômes à $n$ variables. Une partition $S$ de $R^n$ est adaptée à $\mathcal{P}$ lorsque, pour tous $C \in S$ et $P \in \mathcal{P}$, $P$ a un signe constant sur $C$.
**Input:** $n \in \mathbb{N}$ et un ensemble fini $\mathcal{P}$ de $R[X_0, ..., X_{n-1}]$

**Output:** Une décomposition cylindrique $S$ adaptée à $\mathcal{P}$

1 if $n = 0$ then

2 $S = \{R^0\}$

3 else

4 Soit $T = \text{CAD}(\text{elim}(\mathcal{P}))$

5 $S = \emptyset$

6 for $C \in T$ do

7 Soit $x \in C$

8 Soit $\mathcal{P}_* = \{P \in \mathcal{P}, \vec{P}(x) \neq 0\}$

9 Soit $Q = \prod_{P \in \mathcal{P}_*} \vec{P}$

10 Soit $d = |Q^{-1}(\{0\})|$

11 Soit, pour $i \in [0, d-1]$, $f_i : R^{n-1} \to R$ qui envoie $y \in C$ sur la $i$-ième racine de $Q(y)$ et $y \in R^{n-1} \setminus C$ sur $i$

12 $S = S \cup \text{partition\_along}(C, f)$

13 end

14 end

15 return $S$

**Algorithm 1:** Algorithme CAD

77

78

79

80

Les fonctions utilisées pour faire le découpage des cellules sont obtenus en calculant des racines de polynômes. Cependant, en dimension $n$ nous manipulons des polynômes à $n$ variables. Nous définissons donc l'évaluation partielle, qui permet d'évaluer un tel polynôme en ses $n-1$ premières variables.

81

82

**Définition 3.** Soit $P \in R[X_0, ..., X_n]$. L'évaluation partielle de $P$ est la fonction $\vec{P} : R^n \to R[X]$ définie par :

83

$$ \forall x \in R^n, \vec{P}(x) = P(x_0, ..., x_{n-1}, X) $$

84

85

86

87

88

89

90

91

92

93

94

Étant donnée un ensemble fini $\mathcal{P}$ de polynômes à $n$ variables, nous décrivons deux algorithmes. Le premier calcule une décomposition cylindrique adaptée à $\mathcal{P}$ et le second calcule une partie finie $S$ de $R^n$ telle qu'il existe une décomposition cylindrique adaptée à $\mathcal{P}$ dont toutes les cellules contiennent au moins un point de $S$. Ces algorithmes fonctionnent par récurrence sur la dimension de l'espace ambiant. Chaque étape récursive contient une phase de projection, où l'on calcule un ensemble fini de polynômes à $n-1$ variables et une phase de remontée, où l'on utilise le résultat du calcul récursif sur cet ensemble de polynômes pour obtenir le résultat final. Décrire précisément la phase de projection requiert l'introduction des sous-résultants et de leurs propriétés, ce qui sort du cadre de cet article. Par conséquent nous noterons elim l'opération sous-jacente, appelée élimination, et donnerons sans preuve les conséquence de la correction de l'algorithme de calcul de la CAD sur elim($\mathcal{P}$).

95

96

97

98

99

100

101

102

103

104

105

Le simple énoncé de l'Algorithmme 1 requiert des justifications non-triviales. Elles seront données avec la preuve de correction. Dans l'Algorithmhe 2, la formalisation construit $S'$ en utilisant des opérations algébriques simples sur les éléments de $r$, e.g. en prenant la moyenne de deux racines consécutives. C'est très peu efficace dans le cas des nombres algébriques. Nous laissons à de futurs travaux le soin de prouver une implémentation rapide de cette opération (e.g. Algorithme 10.109 dans [BPR06]). Les lecteurs les plus observateurs auront remarqué que, à la ligne 11 de l'Algorithmhe 1, $f_i$ envoie $y \in R^{n-1} \setminus C$ sur $i$ et non pas sur 0 comme on pourrait s'y attendre. Nous ne rentrerons pas suffisamment dans les détails pour expliquer pourquoi nous en avons besoin, mais nous devons prouver que $f_0 < ..., f_{d-1}$. Les $f_i$ doivent être définis sur $R$ tout entier car $C$ n'est actuellement pas un bon modèle de sous-ensemble de $R^{n-1}$.
**Input:** $n \in \mathbb{N}$ et une partie finie $\mathcal{P}$ de $R[X_0, \dots, X_{n-1}]$

**Output:** Un échantillon $S$ d'une decomposition cylindrique adaptée à $\mathcal{P}$

1 if $n = 0$ then

2 $|S = R^0|$

3 else

4 Soit $T = \text{échantillon}(\text{elim}(\mathcal{P}))$

5 $S = \emptyset$

6 for $x \in T$ do

7 Soit $\mathcal{P}_* = \{P \in \mathcal{P}, \vec{P}(x) \neq 0\}$

8 Soit $Q = \prod_{P \in \mathcal{P}_*} \vec{P}(x)$

9 Soit $r$ la suite des racines réelles de $Q$

10 if $r$ est vide then

11 $|S = S \cup \{(x, 0)\}|$

12 else

13 Soit $d = |Q^{-1}(\{0\})|$ la longueur de $r$

14 Soit $S'$ obtenue à partir de $\{r_i, i \in [0, d-1]\}$ en ajoutant un élément plus petit que tous les éléments de $S'$, un élément plus grand que tous les éléments de $S'$, et un élément entre toutes les paires de racines consécutives de $Q$. $S = S \cup S'$

15 end

16 end

17 end

18 return $S$

**Algorithm 2:** Algorithme échantillon

106

## 3 Correction

107

108

109

110

111

112

113

114

115

La correction de l'Algorithmhe 2 est obtenue en montrant qu'il renvoie au moins un point de chaque cellule du résultat de l'Algorithmhe 1. Nous ne prouverons pas que l'Algorithmhe 2 est optimal au sens où il renvoie exactement un point par cellule, bien que ce soit le cas. L'initialisation est triviale pour les deux algorithmes, donc nous nous concentrons sur le cas récursif. Soit donc $n \in \mathbb{N}$ tel que les Algorithmes 1 et 2 soient corrects en dimension $n$. Soit $\mathcal{P}$ une famille de polynômes de $R[X_0, \dots, X_n]$ et soit $T$ le résultat de l'Algorithmhe 1 sur $\text{elim}(\mathcal{P})$. $T$ est une décomposition cylindrique adaptée à $\text{elim}(\mathcal{P})$ d'après l'hypothèse de récurrence, ce qui a un certain nombre de conséquences que nous énonçons ici sans preuve. Soit $C$ une cellule de $T$.

116

**Proposition 1.** Soient $P, Q \in \mathcal{P}$.

117

1. $C \neq \emptyset$, i.e. nous disposons de $\text{pick}(C) \in C$.

118

2. Pour tout $i \in \mathbb{N}$, le i-ième coefficient de $\vec{P}(x)$ a un signe constant pour $x \in C$.

119

3. $x \mapsto \text{deg}'(\vec{P}(x))$ est constante sur $C$.

120

4. Le nombre de racines réelles distinctes de $\vec{P}(x)$ est constant pour $x \in C$.

121

5. $x \mapsto \text{deg}'(\text{gcd}(\vec{P}(x), \vec{Q}(x)))$ est constante sur $C$.

122

6. $x \mapsto \text{deg}'(\text{gcd}(\vec{P}(x), \vec{P}(x)'))$ est constante sur $C$.

123

7. Le nombre de racines complexes distinctes de $\vec{P}(x)$ est constant pour $x \in C$.

124

125

Partant de là, nous avons besoin de tels résultats pour le produit des polynômes non nuls de la forme $\vec{P}(\text{pick}(C))$ pour un certain $P \in \mathcal{P}$. C'est la partie centrale de l'argument.
Soient $\mathcal{P}_* = \{P \in \mathcal{P}, \vec{P}(\text{pick}(C)) \neq 0\}$, $\vec{\mathcal{P}} = \{\vec{P}, P \in \mathcal{P}_*\}$ et $\tilde{P} : \prod_{P \in \mathcal{P}_0} \vec{P}$. Pour commencer, nous allons montrer que, pour $x, y \in C$ assez proches, $\tilde{P}(x)$ et $\tilde{P}(y)$ ont le même nombre de racines distinctes réelles et complexes en montrant qu'il y a des bijections entre leurs ensembles de racines réelles et complexes. Cela repose sur le théorème de continuité des racines d'un polynôme [NR24], qui dans notre cas s'énonce comme suit.

**Lemme 1.** Soient $\vec{\mathcal{P}} : \mathbb{R}^{n-1} \to \mathbb{R}[i][X]$ continue de degré constant, $x \in \mathbb{R}^{n-1}$ et $\delta > 0$. Alors il existe $\varepsilon > 0$ tel que, pour tout $y \in B(x, \varepsilon)$ et pour toute racine $u$ de $\vec{\mathcal{P}}(x)$ de multiplicité $m \in \mathbb{N}$, la somme des multiplicités des racines de $\vec{\mathcal{P}}(y)$ dans $B(u, \delta)$ soit au moins $m$.

Grâce à cela, nous pouvons maintenant établir l'existence d'une bijection entre les racines de $\tilde{P}(x)$ et celles de $\tilde{P}(y)$ pour $x, y \in C$ assez proches. La preuve donnée dans [BPR06], pour la Proposition 5.13, ne traite que le cas où $\mathcal{P}$ contient 2 éléments sans expliquer comment traiter le cas général. Le piège est de tenter une récurrence, ce qui ne fonctionne pas (à notre connaissance). Cependant, la preuve se généralise très bien directement.

**Lemme 2.** Soient $x \in C$ et $\delta > 0$. Il existe $\varepsilon > 0$ tel que, pour tout $y \in C \cap B(x, \varepsilon)$, il existe une bijection $f$ entre l'ensemble des racines complexes de $\tilde{P}(x)$ et l'ensemble des racines complexes de $\tilde{P}(y)$ telle que pour toute racine complexe $u$ de $\tilde{P}(x)$, on ait $|u - f(u)| < \delta$.

**Démonstration** Sans perte de généralité, on peut supposer que $\delta$ est plus petit que la moitié de la distance entre deux racines complexes distinctes de $\tilde{P}(x)$, de sorte que deux racines complexes distinctes de $\tilde{P}(x)$ à distance au plus $2\delta$ soient égales. Le Lemme 1 appliqué à chaque $\vec{P} \in \vec{\mathcal{P}}$ fournit un ensemble de réels strictement positifs dont on note $\varepsilon$ le minimum. Soit $y \in B(x, \varepsilon)$.

Soit $\vec{\mathcal{P}} \in \vec{\mathcal{P}}$. Pour toute racine $u$ de $\vec{\mathcal{P}}(x)$, la définition de $\varepsilon$ venant du Lemme 1 fournit une racine $f_{\vec{\mathcal{P}}}(u)$ de $\vec{\mathcal{P}}(y)$ telle que $|u - f_{\vec{\mathcal{P}}}(u)| < \delta$. Comme les racines de $\vec{\mathcal{P}}(x)$ (qui sont racines de $\tilde{P}(x)$) sont distantes d'au moins $2\delta$, $f_{\vec{\mathcal{P}}}$ est injective. Donc, vu que le nombre de racines distinctes de $\vec{\mathcal{P}}(z)$ ne dépend pas de $z \in C$, $f_{\vec{\mathcal{P}}}$ est bijective.

En notant que, pour $z \in C$, l'ensemble des racines de $\tilde{P}(z)$ est l'union des racines des $\vec{\mathcal{P}}(z)$, $\vec{\mathcal{P}} \in \vec{\mathcal{P}}$, on obtient une fonction $g$ de l'ensemble des racines de $\tilde{P}(x)$ vers l'ensemble des racines de $\tilde{P}(y)$ telle que, pour toute racine $u$ de $\tilde{P}(x)$, on a $g(u) = f_{\vec{\mathcal{P}}}(u)$ pour un certain $\vec{P} \in \vec{\mathcal{P}}$. On obtient de même une fonction $g'$ de l'ensemble des racines de $\tilde{P}(y)$ vers l'ensemble de $\tilde{P}(x)$ telle que pour toute racine $v$ de $\tilde{P}(y)$, il existe $\vec{P} \in \vec{\mathcal{P}}$ tel que $g'(v) = f_{\vec{\mathcal{P}}}^{-1}(v)$. Nous allons montrer que $g$ et $g'$ sont inverses l'une de l'autre.

Notons déjà que, pour toute racine $u$ de $\tilde{P}(x)$, on a $|u - g(u)| < \delta$ et, pour toute racine $v$ de $\tilde{P}(y)$, on a $|v - g'(v)| < \delta$. Comme les racines de $\tilde{P}(x)$ sont distantes d'au moins $2\delta$, $g' \circ g$ est l'identité.

$$f_{\vec{\mathcal{P}}}(u) = f_{\vec{\mathcal{P}}}(u')$$

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

On remarque que, pour $\vec{\mathcal{P}} \in \vec{\mathcal{P}}$ et $v$ une racine de $\vec{\mathcal{P}}(y)$, $v$ est la seule racine de $\vec{\mathcal{P}}(y)$ à distance au plus $\delta$ de $\vec{\mathcal{P}}(y)$. En effet, si $v'$ est une telle racine, alors $g'(v)$ et $f_{\vec{\mathcal{P}}}^{-1}(v')$ sont deux racines de $\tilde{P}(x)$ à distance au plus $2\delta$, donc sont égaux. Pour $v' = v$, on obtient aussi $g'(v) = f_{\vec{\mathcal{P}}}^{-1}(v)$ et l'injectivité de $f_{\vec{\mathcal{P}}}^{-1}$ permet de conclure $v' = v$.
Montrons que $g'$ conserve la multiplicité, au sens où, pour tous $\vec{P} \in \vec{\mathcal{P}}$ et $v$ une racine de $\vec{P}(y)$, la multiplicité de $g'(v)$ comme racine de $\vec{P}(x)$ est la même que la multiplicité de $v$ comme racine de $\vec{P}(y)$. Soient donc $\vec{P} \in \vec{\mathcal{P}}$ et $v$ une racine de $\vec{P}(y)$. $v$ est la seule racine de $\vec{P}(y)$ à distance au plus $\delta$ de $g'(v)$. D'après le Lemme 1, la multiplicité de $v$ comme racine de $\vec{P}(y)$ est au moins la multiplicité de $g'(v)$ comme racine de $\vec{P}(x)$. Ceci est valable pour toute racine $v$ de $\vec{P}(y)$ et $g'$ est surjective. Or $\vec{P}(x)$ et $\vec{P}(y)$ ont le même degré, et donc le même nombre de racines comptées avec multiplicités, donc l'égalité précédente est une égalité.

Montrons à présent que $g \circ g'$ est l'identité. Soit $v$ une racine de $\tilde{P}(y)$. Soient $\vec{P}, \vec{Q} \in \vec{\mathcal{P}}$ tels que $v$ est une racine de $\vec{P}(y)$ et $g(g'(v))$ est une racine de $\vec{Q}(y)$. On a vu que $g' \circ g$ est l'identité, d'où l'on tire que $g'(g(g'(v))) = g'(v)$ est une racine à la fois de $\vec{P}(x)$ et $\vec{Q}(x)$. Or, $g'$ conserve la multiplicité, donc $v$ est aussi une racine de $\vec{Q}(y)$. Comme il n'y a qu'une seule racine de $\vec{Q}(y)$ à distance au plus $\delta$ de $g'(v)$, on obtient $g(g'(v))) = v$.

Passons maintenant au cas réel : il reste à montrer que $g$ induit une bijection entre les racines réelles de $\tilde{P}(x)$ et les racines réelles de $\tilde{P}(y)$. Soit $u$ une racine réelle de $\tilde{P}(x)$. Comme $\tilde{P}(y)$ est à coefficients réels, $g(u)$ est une racine de $\tilde{P}(y)$, et donc $g^{-1}(g(u))$ est une racine de $\tilde{P}(x)$. De $|u - g(u)|$ et du fait que $u$ est réel, on tire $|u - \overline{g(u)}| < \delta$, puis $|u - g^{-1}(\overline{g(u)})| < 2\delta$. D'où $g^{-1}(g(u)) = u$, ou encore $\overline{g(u)} = g(u)$. On obtient que $g(u)$ est réel. Soit maintenant $v$ une racine de $\tilde{P}(y)$. $g^{-1}(v)$ est une racine de $\tilde{P}(x)$, qui est à coefficients réels, donc $g^{-1}(v)$ est aussi une racine de $\tilde{P}(x)$. Comme $v$ est réel et $|v - g^{-1}(v)| < \delta$, on a $|v - \overline{g^{-1}(v)}| < \delta$, d'où l'on tire $|g^{-1}(v) - \overline{g^{-1}(v)}| < 2\delta$, puis $\overline{g^{-1}(v)} = g^{-1}(v)$. Ceci montre que $g^{-1}(v)$ est réel. En conclusion, $g$ induit bien une bijection entre les racines réelles de $\tilde{P}(x)$ et les racines réelles de $\tilde{P}(y)$. $\square$

En particulier, le nombre de racines réelles et complexes distinctes de $\tilde{P}(x)$ est localement constant. Cependant, nous n'avons pas supposé que le corps réel clos sur lequel nous travaillons est connexe. Par exemple, $\pi$ n'est pas dans le corps $\mathbb{R}_{\text{alg}}$ des nombres réels algébriques, donc $] -\infty, \pi[ \text{ et } ]\pi, +\infty[ \text{ sont ouverts, disjoints et recouvrent } \mathbb{R}_{\text{alg}}, \text{ qui n'est donc pas connexe. Ceci pose problème car la connexité des } C \text{ donnerait gratuitement le fait que le nombre de racines distinctes de } \tilde{P}(x) \text{ est constant pour } x \in C. \text{ Il existe une variante de la notion de connexité, appelée connexité semi-algébrique, où l'on demande que le recouvrement soit fait par des parties semi-algébriques. Cette propriété est suffisante pour retrouver que les fonctions localement constantes sont constantes, mais seulement pour les fonctions semi-algébriques. Le fait que le découpage soit fait par des fonctions semi-algébriques dans la définition de cellule implique que } C \text{ est semi-algébrique. Le résultat dont nous avons besoin devient :}$

**Lemme 3.** Soient $m \in \mathbb{N}$ et $f : C \to \mathbb{R}^m$ semi-algébrique. Si $f$ est localement constante sur $C$, alors $f$ est constante sur $C$.

Il ne reste plus qu'à prouver que les fonctions donnant le nombre de racines réelles et complexes distinctes d'un polynôme sont semi-algébrique. Cela ne fait a priori pas sens puisque ces fonctions vont de $R[X]$ dans $R$, mais on peut encoder un polynôme de degré $d$ dans $R^{d+1}$ avec la fonction $P \mapsto (P_0, ..., P_d)$, d'inverse $(x_0, ..., x_d) \mapsto \sum_{i=0}^{d} x_i X^i$. Ensuite, la clé du résultat est le schéma de formules suivant, indexé par $n$ et $m \in \mathbb{N}$, qui décrit les racines réelles d'un polynôme. Dans cette formule, $X_0, ..., X_{n-1}$ encode un polynôme de degré au plus $n$, $m$ est le nombre de racines et $X_n, ..., X_{n+m-1}$ les racines auxquelles on s'attend, et $\text{eval}_n$ est une formule décrivant l'évaluation d'un polynôme en un point, où $X_0, ..., X_{n-1}$ décrit le polynôme, $X_n$ décrit le point d'évaluation et $X_{n+1}$ la valeur de retour. En d'autres
termes, eval_n représente le graphe de la fonction d’évaluation.

$$ (\bigwedge_{i=0}^{n-1} X_i = 0) \wedge m = 0) \lor (\bigwedge_{i=n}^{n+m-1} \text{eval}_n[X_n \leftarrow X_i, X_{n+1} \leftarrow 0]) \land (\bigwedge_{i=n}^{n+m-2} X_i < X_{i+1}) \land (\forall X_{n+m}, \text{eval}_n[X_n \leftarrow X_{n+m}, X_{n+1} \leftarrow 0] \rightarrow \bigvee_{i=n}^{n+m-1} X_{n+m} = X_i). $$

Le degré d de $\tilde{P}(x)$ étant constant sur $C$, on peut l’encoder dans $R^{d+1}$ et on obtient :

**Corollaire 1.** Le nombre de racines réelles et complexes distinctes de $\tilde{P}(x)$ est constant pour $x \in C$.

Nous avons maintenant les fonctions dont nous avons besoin pour découper le cylindre $C \times R$. Ces fonctions sont semi-algébriques en vertu de la formule décrivant les racines d'un polynôme décrite ci-dessus. Il ne reste qu'à montrer qu'elles sont continues.

**Lemme 4.** Soit $P: C \to R[X]$ continue, de degré d constant et de nombre de racines réelles et complexes distinctes constant. Soient $f_1, ..., f_k$ les fonctions décrivant les racines de $P$. Alors, pour tout $i \in [1, k]$, $f_i$ est continue.

**Démonstration** Soient $x \in C$ et $\varepsilon > 0$. Sans perte de généralité, on peut supposer que $\varepsilon$ est inférieur à la moitié de la distance entre deux racines complexes distinctes de $P(x)$. Le lemme 1 fournit $\delta > 0$ tel que pour tout $y \in C \cap B(x, \delta)$ et pour toute racine $u$ de $P(x)$, il existe une racine de $P(y)$ dans $B(u, \varepsilon)$. Soit $y \in C \cap B(\delta, x)$. Pour toute racine $u$ de $P(x)$, on a une racine $f(u)$ de $P(y)$ telle que $|u - f(u)| < \varepsilon$. Comme deux racines de $P(x)$ sont distantes d'au moins $2\varepsilon$, $f$ est injective. Or $P(x)$ et $P(y)$ ont le même nombre de racines complexes distinctes, donc $f$ est bijective. Si $v$ est une racine réelle de $P(y)$, alors, comme $P(x)$ est à coefficients réels, $f^{-1}(v)$ et $\bar{f}^{-1}(v)$ sont deux racines de $P(x)$ à distance inférieure à $2\delta$, donc sont égaux. Ceci montre que $f^{-1}$ induit une fonction injective de l'ensemble des racines réelles de $P(y)$ dans l'ensemble des racines réelles de $P(x)$. Comme $P(x)$ et $P(y)$ ont le même nombre de racines réelles distinctes, $f^{-1}$ induit même une bijection. Comme les $f_i(x)$, $i \in [1, k]$ sont distants d'au moins $2\varepsilon$, $f$ est croissante : les inégalités $f_1(x) < ... < f_k(x)$ impliquent $f(f_1(x)) < ... < f(f_k(x))$. Alors, pour tout $i \in [1, k]$, on a $|f_i(y) - f_i(x)| = |f(f_i(x)) - f_i(x)| < \varepsilon$, ce qui conclut la preuve.

229

230

231

232

233

234

235

236

237

□

Nous pouvons faire le découpage de $C \times R$. Pour montrer qu'on obtient une décomposition cylindrique, il reste à montrer que les découpages des cellules de $T$ produisent bien une partition de $R^{n+1}$. Notons $S$ l'ensemble des cellules de $R^{n+1}$ obtenues. Montrer qu'elles sont non-vides et qu'elles recouvrent $R^n$ ne pose pas de problème. Montrer que $S$ possède la propriété de l'intersection triviale est plus difficile. En effet, il y a $O(|S|^2)$ contraintes à vérifier. Dans le contexte abstrait où nous sommes, on traite ensemble les cellules qui ont été construites de la même manière, mais cela laisse tout de même 16 cas à traiter.
Une première astuce consiste à utiliser le fait que $T$ est lui-même une partition. Ainsi, avec $\pi : R^{n+1} \to R^n$ la projection canonique, si $C, D \in S$ vérifient $\pi(C) \neq \pi(D)$, on a tout de suite $\pi(C) \cap \pi(D) = \emptyset$, puis $C \cap D = \emptyset$. Une deuxième astuce consiste à ordonner les cellules avec l'ordre suivant. Pour $X, Y \subset R^{n+1}$, on définit $X < Y$ par :

$$X < Y \Leftrightarrow Y \neq \emptyset \wedge \forall x \in R^n, \forall y, z \in R, (x, y) \in X \Rightarrow (x, z) \in Y \Rightarrow y < z$$

Montrer que le découpage de $C \times R$ produit des cellules ordonnées revient à montrer que deux cellules consécutives le sont, ce qui réduit le nombre de contraintes à $O(|S|)$. Plus précisément, il y 4 cas à traiter. En conclusion, on obtient le Lemme suivant.

**Lemme 5.** $S$ est une décomposition cylindrique de $R^{n+1}$.

Tout ce qui précède montre que l'Algorithme 1 est bien défini. Pour montrer la correction, il suffit de montrer que la partition produite est bien adaptée à $\mathcal{P}$.

**Proposition 2.** $S$ est adaptée à $\mathcal{P}$.

**Démonstration** Soient $P \in \mathcal{P}$, $C \in S$ et $D = \pi(C)$. On souhaite montrer que $P$ est de signe constant sur $C$. Si $\vec{P}(\text{pick}(D)) = 0$, alors $\vec{P}$ envoie tous les points de $D$ sur 0 et le résultat est clair. Supposons donc que $\vec{P}(\text{pick}(D)) \neq 0$. On distingue deux cas, selon que $P$ s'annule ou non sur $C$.

— Supposons que, pour tout $x \in C$, on a $P(x) \neq 0$. On sait montrer que $P(C)$ est semi-algébriquement connexe grâce au fait que $C$ l'est et que $P$ induit une fonction semi-algébrique continue de $C$ dans $R$. Comme $P(C)$ ne contient pas 0, il est inclus dans $] -\infty, 0[ \text{ ou } ]0, +\infty[$, ce qui conclut la preuve.

— Supposons qu'on dispose de $x \in C$ tel que $P(x) = 0$. Alors $x_n$ est une racine de $\vec{P}(\pi(x))$, donc de $\tilde{P}(\pi(x))$, disons la $i$-ième. Alors, avec $f_1 < \dots < f_k : D \to R$ décrivant les racines de $\vec{P}$ sur $D$, le graphe de $f_i$ est une cellule de $S$ contenant $x$, et est donc $C$. Soient $g_1 < \dots < g_l : D \to R$ décrivant les racines de $\vec{P}$. On sait montrer que $(g_j)_{j \in \llbracket 1, l \rrbracket}$ est une sous-suite de $(f_j)_{j \in \llbracket 1, l \rrbracket}$, de sorte qu'il existe $j \in \llbracket 1, l \rrbracket$ tel que $f_i = g_j$. P s'annule sur tout le graphe de $g_j$, c'est-à-dire sur tout le graphe de $f_i$, ou encore sur $C$, ce qui conclut la preuve.

On obtient la correction de l'Algorithme 1. En ce qui concerne l'Algorithme 2, si on note $T'$ et $S'$ ses résultats sur $\text{elim}(\mathcal{P})$ et $\mathcal{P}$, sa correction en dimension $n$ implique que $T'$ contient au moins un point de chaque cellule de $T$. Vu la façon dont on a construit $S$ et dont on choisit les points de $S'$, $S'$ contient au moins un point par cellule de $S$, ce qui est sa correction sur l'entrée $\mathcal{P}$.

**Théorème 1.** *Les Algorithmes 1 et 2 sont corrects.*

*Exemple 1.* Pour $\mathcal{P} = \{X^2 + Y^2 - 1\}$, on obtient la décomposition suivante avec 13 cellules, où $X^2 + Y^2 - 1$ est strictement positif en dehors du disque unité fermé, nul sur le cercle unité et strictement négatif dans le disque unité ouvert :

<figure><img src="image_4.png" /></figure>
276

# 4 Conclusion

277

278

279

280

281

282

283

284

Cet article décrit la première (au mieux de nos connaissances) formalisation d'un algorithme de calcul de Décomposition Algébrique Cylindrique. Il repose sur la bibliothèque *MathComp* pour les définitions et théories des objets mathématiques sous-jacents. La preuve de correction est supposément constructive, mais nous utilisons la bibliothèque *MathComp-Analysis* pour la notion de continuité et cette bibliothèque impose l'utilisation d'axiome classiques. Cependant, nous n'utilisons essentiellement que la définition de continuité, donc nous pensons que ces axiomes ne sont pas réellement nécessaires, au sens où nous pourrions réécrire la partie de la bibliothèque dont nous avons besoin sans ces axiomes.

285

286

**Remerciements.** Merci à Yves Bertot et Cyril Cohen pour leur soutien et les nombreuses discussions que nous avons eues.

287

# Références

288

289

290

[BPR06] Saugata BASU, Richard POLLACK et Marie-Françoise ROY : *Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)*. Springer-Verlag, Berlin, Heidelberg, 2006.

291

292

293

[Col75] George E. COLLINS : Quantifier elimination for real closed fields by cylindrical algebraic decompostion. *In* H. BRAKHAGE, éditeur : *Automata Theory and Formal Languages*, pages 134–183, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg.

294

295

296

297

[Dja18] Boris DJALAL : A Constructive Formalisation of Semi-algebraic Sets and Functions. *In* June ANDRONICK et Amy FELTY, éditeurs : *CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs*, pages 240–251, Los Angeles, California, United States, janvier 2018. ACM.

298

299

300

[HJX16] Jingjun HAN, Zhi JIN et Bican XIA : Proving inequalities and solving global optimization problems via simplified cad projection. *Journal of Symbolic Computation*, 72:206–230, 2016.

301

302

303

304

305

[KTP23] Katherine Kosaian, Yong Kiam Tan et André Platzer : A first complete algorithm for real quantifier elimination in isabelle/hol. *In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs*, CPP 2023, page 211–224, New York, NY, USA, 2023. Association for Computing Machinery.

306

307

308

[MC12] Assia MahBOUBI et Cyril Cohen : Formal proofs in real algebraic geometry : from ordered fields to quantifier elimination. *Logical Methods in Computer Science*, Volume 8, Issue 1, février 2012.

309

310

[NR24] Melvyn B. NATHANSON et David A. Ross : Continuity of the roots of a polynomial. *Communications in Algebra*, 52(6):2509–2518, 2024.

311

312

[Pla22] André Platzer : Correction to : Differential dynamic logic for hybrid systems. *J. Autom. Reason.*, 66(1):173, 2022.

313

314

315

[SS83] Jacob T SCHWARTZ et Micha Sharir : On the “piano movers” problem. ii. general techniques for computing topological properties of real algebraic manifolds. *Advances in Applied Mathematics*, 4(3):298–351, 1983.

316

317

318

319

[ST11] Thomas STURM et Ashish Tiwari : Verification and synthesis using real quantifier elimination. *In Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation*, ISSAC ’11, page 329–336, New York, NY, USA, 2011. Association for Computing Machinery.