Cylindrical Algebraic Decomposition in Coq/Rocq
summary
Formalizes correctness of Cylindrical Algebraic Decomposition in Coq/Rocq, proving: for any finite family of polynomials in n variables there exists a CAD where each polynomial has constant sign per cell. Implementation uses elimination via subresultants, formalizes continuity of root functions (week-long proof), and cylinder partitioning into semi‑algebraic cells. Code is about 10,000 lines, developed in ~5 months, builds on mathcomp, mathcomp real closed and mathcomp analysis, and is a non‑executable specification rather than an extracted, efficient program.
AI-written summary · about
chapters (11)
- 0:00Introduction to CAD in Coq/Rocq
- 1:08Definition of Cylindrical Algebraic Decomposition
- 3:56CAD for quantifier elimination
- 6:47CAD in robotics
- 7:51Recursive CAD algorithm
- 8:58Partitioning cylinders
- 10:48Polynomial roots in CAD
- 11:53Formalizing semi-algebraic functions
- 13:37Project scope
- 15:20CAD theorem statement
- 17:08Conclusion
related talks
46mMechanizing Abstract Interpretation
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
58mFast Cryptographic Code via Partial Evaluation
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
21mIntrinsically Correct Algorithms and Recursive Coalgebras
19mCertified Compilers à la Carte
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders