Cylindical Algbebraic Decomposition

This library contains a formal proof of Collins' Cylindical Aglebraic Decomposition, using the Mathematical Components Library.

Meta

• Author(s):
  • Cyril Cohen (initial)
  • Boris Djalal (initial)
  • Quentin Vermande (initial)
• License: GNU Lesser General Public License v3.0
• Compatible Coq versions: Coq 8.18 or later
• Additional dependencies:
  • Hierarchy Builder >= 1.4.0
  • MathComp ssreflect 2.2
  • MathComp algebra
  • MathComp fingroup
  • MathComp solvable
  • MathComp field
  • MathComp bigenough 1.0.1 or later
  • MathComp bigenough 1.0.1 or later
  • MathComp multinomials 2.2.0 or later
  • MathComp real-closed 2.0.1 or later
  • MathComp classical 1.1.0 or later
  • MathComp analysis 1.1.0 or later
• Coq namespace: SemiAlgebraic
• Related publication(s):
  • A Constructive Formalisation of Semi-algebraic Sets and Functions doi:10.1145/3167099

Building and installation instructions

The easiest way to install the latest released version of Cylindical Algbebraic Decomposition is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-cad

To instead build and install manually, do:

git clone https://github.com/math-comp/cad.git
cd cad
make   # or make -j <number-of-cores-on-your-machine> 
make install