Coq 中的三圆定理

实代数几何中的三圆定理保证了单变量多项式实根隔离算法的终止性和正确性。其证明的主要思路是考虑根属于由直线界定的复平面特定区域的多项式。在应用包含反演的变换后，该区域被映射为由圆界定的区域。我们在 Ssreflect（证明助手 Coq 的一个扩展，提供多功能的代数工具）中形式化了这个相当几何化的证明。这些工具使我们能够从代数的角度形式化该证明。