Abstract

In this project we wish to apply computerized theorem proving tools to two aspects of geometry. The first aspect concerns computational geometry, the second aspect concerns verifying geometric reasoning steps in usual constructions, such as constructions with rules and compass.

We mainly want to use the Coq theorem tool. Regarding computational geometry, we can describe algorithms in Coq's language, which is close to the language of mathematics and, using Coq's extraction tools, we can derive executable programs that are practically error-free. Regarding the verification of geometrical reasoning, we can use Coq's capabilities to define axiom systems that define the basic concepts, to experiment with the combination of these axioms to prove arbitrarily complex theorem, and to verify whether these axioms are entailed by other presentations of geometry (like the geometry of R^n).

In computational geometry, we first want to implement elementary data structures and abstract operations that are adapted to algorithms in geometry. An important data structure is the structure of combinatorial map. It makes it possible to observe and manipulate notions that occur often in geometric data, while abstracting away from numerical notions. Another approach to abstract away from details relies on geometry algebras, where the basic operations of a geometric algorithms are represented as the laws of an algebraic structure. This makes it possible to stay away from problems of numeric computation and to describe some algorithms independently from the dimension of geometrical space.

In computational geometry, we want to experiment on several well-known algorithms of the domain: convex hulls in two or three dimensions, Delaunay triangulation and the dual problem of Voronoï diagrams, and algorithms to compute arrangements. In each case, we will perform a first study in dimension two and then address dimension three or, when possible, look for formulations are independent from the dimension.

With respect to formalizing geometric constructions, we want to handle the usual constructions of geometry: constructing a straight line, a circle, the intersection of two figures, etcetera. Several approaches are possible and we want to study how to reconcile these approaches. A first approach is based on the formal description of axiom systems for geometry that were proposed in the history of mathematics. We will focus on the axioms proposed by Hilbert. A second approach is based on providing a new axiom system that is more adapted to formal verification with a theorem proving tool and to extend this axiom system to cover larger and larger fields of geometry. In this approach we want to extend our previous work on plane geometry to integrate notions of incidence, areas, angles, and inversions. We also wish to evolve to geometry in three dimension.

With respect to formalizing geometric constructions, we also want to reduce the tedious constraints on formal proofs by providing formally verified methods that make it possible to encode geometrical problems as algebraic problems and solve these problems using algebraic techniques. This study will be completed by a study of the relations between several presentations of geometry, based on several axiom systems. Thus, we will provide a variety of formalizations to handle geometric problems, making possible to decompose problems into sub-problems that can each be handled with the better adapted tool. We want to add to this work the implementation of an graphical and interactive tool, to help experimenting with geometric constructions, guide the proof process, and give access to automatic proving tools for some of the sub-proofs.

Our work on geometric constructions is not independent from the work on computational geometry. Reasoning on elementary constructions makes it possible to justify the elementary operations and some of the optimisations that can be found in geometric algorithms.