Le théorème de Thalès pour les cercles et sa réciproque qui est plus connue sous le nom de théorème du cercle circonscrit à un triangle rectangle sont des propriétés de géométrie élémentaire enseignées dans les collèges français. Nous nous intéressons non seulement à différentes descriptions possibles de ces propriétés en Coq mais aussi aux preuves correspondantes. Nous étudions notamment comment le choix d'une représentation des objets géométriques contenus dans l'énoncé influencent les arguments de preuve. Nous présentons plusieurs approches, une basée sur des calculs d'angles, une autre basée sur la géométrie analytique et finalement deux démonstrations différentes dans l'axiomatique de Tarski en utilisant dans un cas le théorème de la droite des milieux et dans l'autre la notion de symétrie centrale et ses propriétés.

This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on previous work by Chollet, Fuchs et al. where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. Laugwitz-Schmieden numbers are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated. In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.

Keywords: formal proofs, discrete geometry, non-standard arithmetic, arithmetisation scheme, exact computations, Coq

La droite d'Harthong-Reeb est un modèle numérique du continu basé sur les entiers. La construction de cette droite en utilisant les Ω-entiers permet de décrire les objets mathématiques réels de manière discrète et constructive. En informatique graphique on est souvent amené à transformer des objets (images) par des applications affines réelles (rotations, translations, similitudes,...). Des discrétisés (à une échelle donnée) de ces applications, appelées applications quasi-affines ont été définies et étudiées. Dans ce papier, nous rappelons les définitions et propriétés de base des Ω-entiers, de la droite de Harthong-Reeb et des applications quasi-affines. Nous montrons ensuite comment définir des Ω-AQAs qui sont les discrétisés multi-échelle des applications affines suivant la théorie des Ω-entiers et la définition initiale des AQAs. Enfin nous donnons les premières propriétés de ces Ω-AQAs.

The polyhedral model provides techniques to optimize Static Control Programs (SCoP) using some complex transformations which improve data-locality and which can exhibit parallelism. These advanced transformations are now available in both GCC and LLVM. In this paper, we focus on the correctness of these transformations and in particular on the problem of integer overflows. Indeed, the strength of the polyhedral model is to produce an abstract mathematical representation of a loop nest which allows high-level transformations. But this abstract representation is valid only when we ignore the fact that our integers are only machine integers. In this paper, we present a method to deal with this problem of mismatch between the mathematical and concrete representations of loop nests. We assume the existence of polyhedral optimization transformations which are proved to be correct in a world without overflows and we provide a self-verifying compilation function. Rather than verifying the correctness of this function, we use an approach based on a validator, which is a tool that is run by the compiler after the transformation itself and which confirms that the code produced is equivalent to the original code. As we aim at the formal proof of the validator we implement this validator using the Coq proof assistant as a programming language.

This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.

This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on a previous work by some of the authors where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. A formalization of a first attempt for a model of the Hartong-Reeb line based on the work of Laugwitz and Schmieden is also presented and analyzed. We hope that this work could help reasoning and implementation of numeric computations in geometric systems.

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to formalize fairly easily Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.

Keywords: formalization, projective geometry, Coq, rank, desargues, hessenberg, hexamy

This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml-program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions leads to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this paper, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. It allows to carry out proofs in a more systematic way. To validate this approach, we formalize in Coq (using only ranks) one of the fundamental theorems of the projective space, namely Desargues' theorem.

We investigate how projective plane geometry can be formalized in a proof assistant such as Coq. Such a formalization increases the reliability of textbook proofs whose details and particular cases are often overlooked and left to the reader as exercises. Projective plane geometry is described through two different axiom systems which are formally proved equivalent. Usual properties such as decidability of equality of points (and lines) are then proved in a constructive way. The duality principle as well as formal models of projective plane geometry are then studied and implemented in Coq. Finally, notions of flats and ranks are introduced and their basic properties are proved. This would allow to develop a more algebraic approach to proofs of alignment properties such as Desargues' theorem.

Code certification is usually investigated for architecture-dependent assembly or machine code, where the trusted computing base (TCB) is minimised at the expense of portability. Work that departs from that scheme typically focuses on a comparatively high-level abstract machine code, such as that of the Java Virtual machine. In contrast, the aim of this work is machine-independent certified code on a level that is just above that of an architecture-dependent code. In other words, we aim to minimise the TCB under the over- ruling aim of portability. We represent computations as terms of a polymorphic lambda calculus in administrative normal form, which essentially is a low- level intermediate language. The type structure of these terms is embedded in the dependently-typed LF type theory, which serves to represent certificates. We study how to show the resulting type system is sound and that the operational semantics of the calculus does not depend on (dependent) type information. Moreover, we have implemented a prototype compiler that compiles a small functional language into certified code as well as a prototype certificate checker based on Twelf.

The Coq proof system allows users to write (functional) programs and to reason about them in a formal way. We study how to program using dependently typed data structures in such a setting. Using dependently typed data structures enables programmers to have more precise specifications for their programs before starting proving any significant properties (e.g. total correctness) about these programs. We particularly focus on an operational description of square matrices and their operations. Matrices are represented using dependent types. A matrix is a vector of rows, which are themselves vectors indexed by natural numbers. We also take advantage of Coq modules system to have matrices parametrised by a carrier set. Finally, this operational description of square matrices can be extracted into a mainstream functional programming language like Ocaml.

Nous étudions comment faciliter la réutilisation des preuves formelles en théorie des types. Nous traitons cette question lors de l'étude de la correction du programme de calcul de la racine carrée de GMP. A partir d'une description formelle, nous construisons un programme impératif avec l'outil Correctness. Cette description prend en compte tous les détails de l'implantation, y compris l'arithmétique de pointeurs utilisée et la gestion de la mémoire.
Nous étudions aussi comment réutiliser des preuves formelles lorsque l'on change la représentation concrète des données. Nous proposons un outil qui permet d'abstraire les propriétés calculatoires associées à un type inductif dans les termes de preuve. Nous proposons également des outils pour simuler ces propriétés dans un type isomorphe. Nous pouvons ainsi passer, systématiquement, d'une représentation des données à une autre dans un développement formel.

In a theorem prover like Coq, mathematical concepts can be implemented in several ways. Their different representations can be either efficient for computing or well-suited to carry out proofs easily. In this paper, we present improved techniques to deal with changes of data representation within Coq. We propose a smart handling of case analysis and definitions together with some general methods to transfer recursion operators and their reduction rules from one setting to another. Once we have built a formal correspondence between two settings, we can translate automatically properties obtained in the initial setting into new properties in the target setting. We successfully experiment with changing Peano's numbers into binary numbers for the whole 'Arith' library of Coq as well as with changing polymorphic lists into reversed (snoc) lists.

We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP), is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program. The formalization is rather large (more than 13000 lines) and requires some advanced techniques for proof management and reuse.

In type-theory based proof systems that provide inductive structures, computation tools are automatically associated to inductive definitions. Choosing a particular representation for a given concept has a strong influence on proof structure. We propose a method to make the change from one representation to another easier, by systematically translating proofs from one context to another. We show how this method works by using it on natural numbers, for which a unary representation (based on Peano axioms) and a binary representation are available. This method leads to an automatic translation tool that we have implemented in Coq and successfully applied to several arithmetical theorems.

Dans le calcul des constructions inductives, des outils de calcul et de preuve sont associés à chaque type de données concret défini inductivement. Par conséquent, le choix d'une structure de données influence fortement le contenu des preuves. Nous proposons dans ce document une méthode pour passer facilement d'une représentation à une autre, en effectuant des traductions partiellement automatisées des preuves. Nous mettons cette méthode en œuvre sur les entiers naturels, pour lesquels il existe une représentation unaire (à la Peano) et une représentation binaire. Un prototype d'outil de traduction est développé dans le système Coq et a été expérimenté avec succès sur une dizaine de théorèmes d'arithmétique.

We present the formal proofs of total correctness of three sorting algorithms in the Coq system, namely insertion sort, quicksort and heapsort. The implementations are imperative programs working in-place on a given array. Those developments demonstrate the usefulness of inductive types and higher-order logic in the process of software certification. They also show that the proof of rather complex algorithms may be done in a small amount of time --- only a few days for each development --- and without great difficulty.