Hello! I was really excited to see that Cylindrical Algebraic Decomposition has been formalised in Coq, with an attached procedure for it, but I have two possibly ignorant questions:

a) Is there some documentation in the style of say ring, that explains how to use it in practice (alternatively, maybe one of the papers about it were it is explained? The ones I’ve seen seem all to focus on the formalisation aspects)

b) How did it work in practice? I can’t seem to find instances in mathcomp / other Coq repos. Was it too slow?

Is this about this repo? https://github.com/math-comp/cad

Last updated: Jun 23 2024 at 04:03 UTC