Cylindrical Algebraic Decomposition in Coq/Rocq

Abstract

The Cylindrical Algebraic Decomposition (CAD in short) is a fundamental tool of semi-algebraic geometry. It is a doubly-exponential time algorithm that enables most famously to eliminate quantifiers from a formula in the theory of real closed fields. In particular, it allows to decide the satisfiability of problems involving sets of comparisons between polynomials. The present article describes the first formalization of a correctness proof of this algorithm in a proof assistant.