Formalization of Hensel's lemma in Coq

Érik Martin-Dorel 1, 2, *
* Auteur correspondant
2 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : Suppose we want to find the integral simple roots of a univariate polynomial with integer coefficients. We can use Hensel's lifting, which can be viewed as the $p$-adic variant of the Newton--Raphson's iteration. It enables us to compute the roots modulo increasing powers of a prime $p$. As soon as the considered power of $p$ becomes greater than a known bound on the roots, we easily obtain the sought integral roots. The bivariate version of this root-finding algorithm is extensively used by the Stehlé--Lefèvre--Zimmermann algorithm, designed to solve the so-called Table Maker's Dilemma in an exact way. Consequently, the formal verification of Hensel's lemma (i.e., the correctness lemma of Hensel's lifting method) will contribute to the validation of this kind of algorithm. In this talk, we describe the various steps we met during the formalization of Hensel's lemma with the Coq proof assistant along with the SSReflect extension.
Type de document :
Communication dans un congrès
TYPES 2010: The 17th Workshop on Types for Proofs and Programs, Oct 2010, Warsaw, Poland
Liste complète des métadonnées
Contributeur : Érik Martin-Dorel <>
Soumis le : vendredi 28 janvier 2011 - 13:36:26
Dernière modification le : jeudi 17 janvier 2019 - 15:16:03


  • HAL Id : ensl-00560449, version 1



Érik Martin-Dorel. Formalization of Hensel's lemma in Coq. TYPES 2010: The 17th Workshop on Types for Proofs and Programs, Oct 2010, Warsaw, Poland. 〈ensl-00560449〉



Consultations de la notice