Algebraic numbers in Isabelle/HOL. (English) Zbl 1478.68443

Thiemann, René; Yamada, Akihisa

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 391-408 (2016).

Summary: We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, and a faster but approximative version.
To this end, we mechanize several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain. We moreover formalize algorithms for factorization of integer polynomials: Newton interpolation, factorization over the integers, and Kronecker’s factorization algorithm, as well as a factorization oracle via Berlekamp’s algorithm with the Hensel lifting.
For the entire collection see [Zbl 1343.68004].

MSC:

68V20	Formalization of mathematics in connection with theorem provers
03B35	Mechanization of proofs and logical operations
11R04	Algebraic numbers; rings of algebraic integers
13P15	Solving polynomial systems; resultants
68W30	Symbolic computation and algebraic computation

Software:

Transfer; Isabelle/HOL; HOL; Lifting; Isabelle

References:

[1]	Brown, W.S.: The subresultant PRS algorithm. ACM Trans. Math. Softw. 4(3), 237–249 (1978) · Zbl 0385.68044
[2]	Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 67–82. Springer, Heidelberg (2012) · Zbl 1360.68744
[3]	Cohen, C., Djalal, B.: Formalization of a Newton series representation of polynomials. In: CPP 2016, pp. 100–109. ACM (2016)
[4]	Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1:02), 1–40 (2012) · Zbl 1241.68096
[5]	Collins, G.E.: Subresultants and reduced polynomial remainder sequences. J. ACM 14, 128–142 (1967) · Zbl 0152.35403
[6]	Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: CPP 2015, pp. 75–83. ACM (2015)
[7]	Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013) · Zbl 1317.68212
[8]	Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013) · Zbl 1426.68284
[9]	Knuth, D.E.: The Art of Computer Programming. Seminumerical Algorithms, vol. 2, 2nd edn. Addison-Wesley, Boston (1981) · Zbl 0477.65002
[10]	Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1–13 (2010)
[11]	Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP 2016, pp. 66–75. ACM (2016)
[12]	Mahboubi, A.: Proving formally the implementation of an efficient gcd algorithm for polynomials. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 438–452. Springer, Heidelberg (2006) · Zbl 1222.68369
[13]	Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)
[14]	Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[15]	Prasolov, V.V.: Polynomials. Springer, Heidelberg (2004) · Zbl 1272.12001
[16]	Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: CPP 2016, pp. 88–99. ACM (2016)