Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. (English) Zbl 1468.68299

Summary: In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
30E20 Integration, integrals of Cauchy type, integral representations of analytic functions in the complex plane
68W30 Symbolic computation and algebraic computation
Full Text: DOI arXiv


[1] Arnold, Vi, Ordinary Differential Equations (1992), Berlin: Springer, Berlin
[2] Basu, S.; Pollack, R.; Roy, Mf, Algorithms in Real Algebraic Geometry (2006), Berlin: Springer, Berlin
[3] Brunel, A.: Non-constructive complex analysis in Coq. In: Danielsson, N.A., Nordström, B. (eds.) 18th International Workshop on Types for Proofs and Programs (TYPES 2011), pp. 1-15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2013) · Zbl 1354.68231
[4] Collins, G.E., Krandick, W.: An efficient algorithm for infallible polynomial complex root isolation. In: Proceedings of International Symposium on Symbolic and Algebraic Computation, ISSAC ’92, pp. 189-194. ACM (1992) · Zbl 0964.68582
[5] Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: Conference on Certified Programs and Proofs, pp. 75-83. ACM Press (2015)
[6] Eisermann, M., The fundamental theorem of algebra made effective: an elementary real-algebraic proof via Sturm chains, Am. Math. Mon., 119, 9, 715 (2012) · Zbl 1267.26016
[7] Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol. 10, no. 23, pp. 151-165. University of Białystok (2007). http://mizar.org/trybulec65/. Accessed 2 Apr 2019
[8] Harrison, J., Formalizing an analytic proof of the prime number theorem (Dedicated to Mike Gordon on the occasion of his 60th birthday), J. Autom. Reason., 43, 243-261 (2009) · Zbl 1185.68624
[9] Hölzl, Johannes; Immler, Fabian; Huffman, Brian, Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, Interactive Theorem Proving, 279-294 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1317.68213
[10] Li, W.: The Sturm-Tarski theorem. In: Archive of Formal Proofs (2014). http://isa-afp.org/entries/Sturm_Tarski.html. Accessed 2 Apr 2019
[11] Li, W.: Count the number of complex roots. In: Archive of Formal Proofs (2017). http://isa-afp.org/entries/Count_Complex_Roots.html. Accessed 2 Apr 2019
[12] Li, W.: Evaluate winding numbers through cauchy indices. In: Archive of Formal Proofs (2017). http://isa-afp.org/entries/Winding_Number_Eval.html. Accessed 2 Apr 2019
[13] Li, W.; Passmore, Go; Paulson, Lc, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, J Autom Reason, 62, 69-91 (2017) · Zbl 1468.68298
[14] Li, W., Paulson, L.C.: A formal proof of Cauchy’s residue theorem. In: Blanchette, J.C., Merz, S., (eds.) 7th International Conference on Interactive Theorem Proving, pp. 235-251. Springer (2016) · Zbl 1478.68440
[15] Mahboubi, A.; Cohen, C., Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Log. Methods Comput. Sci., 8, 1, 1-40 (2012) · Zbl 1241.68096
[16] Marden, M., Geometry of Polynomials (1949), Providence: American Mathematical Society, Providence
[17] Mclaughlin, S.; Harrison, J.; Nieuwenhuis, R., A proof-producing decision procedure for real arithmetic, Automated Deduction - CADE-20. CADE 2005. Lecture Notes in Computer Science (2005), Berlin: Springer, Berlin · Zbl 1135.03329
[18] Narkawicz, A.; Muñoz, Ca; Dutle, A., Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems, J. Autom. Reason., 54, 4, 285-326 (2015) · Zbl 1356.68196
[19] Rahman, Qi; Schmeisser, G., Analytic Theory of Polynomials (2002) (2016), Oxford: Oxford University Press, Oxford
[20] Wilf, Hs, A global bisection algorithm for computing the zeros of polynomials in the complex plane, J. ACM, 25, 3, 415-420 (1978) · Zbl 0378.30003
[21] Yap, C.K., Sagraloff, M.: A simple but exact and efficient algorithm for complex root isolation. In: 36th International Symposium on Symbolic and Algebraic Computation, ISSAC ’11, pp. 353-360. ACM Press (2011) · Zbl 1323.65051
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.