Publications

My PhD thesis

Formalisation et automatisation du raisonnement géométrique en Coq, Septembre 2006.

Submitted papers

A formalization of diagrammatic proofs in abstract rewriting [.ps.gz | .pdf (40 pages)]
Diagrams are in common use in the rewriting community. In this paper, we present a formalization of this kind of diagrams. We give a formal definition for the diagrams used to state properties. We propose inference rules to formalize the reasoning depicted by some well known diagrammatic proofs : a transitivity property of some abstract rewriting systems and the Newman's lemma. We show that the system proposed is both correct and complete for a class of formulas called coherent logic.
Click here to access to the Coq files.
The Area Method : a Recapitulation (with Predrag Janicic and Pedro Quaresma [.pdf (55 pages)]
The area method for Euclidean constructive geometry was proposed by Chou et al. in the early 1990's. The method produces human-readable proofs and can efficiently prove many non-trivial geometry theorems. It is one of the most interesting and most successful methods for automated theorem proving in geometry and probably the most successful in the domain of automated production of readable proofs in geometry.
In this paper, we provide a first complete presentation of the method. We provide both algorithmic and implementation details that were omitted in the original presentations. We also give a variant of Chou, Gao and Zhang's axiom system. Based on this axiom system, we proved formally all the lemmas needed by the method and its soundness using the Coq proof assistant.
Click here to access to the Coq files.
A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem [.pdf (33 pages)]
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.

Refereed publications

Formal SOS-Proofs for the Lambda-Calculus (with Christian Urban) in ENTCS proceedings of LSFA'08, vol 247, pages 139-155, 2009 [.pdf (15 pages)]
We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termina- tion of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity allows us to show actual theorem-prover code of the formal proofs. The formalisations are done in Nominal Isabelle, a de?nitional extention of the theorem prover Isabelle/HOL. The point of these formalisations is to be as close as possible to the ?pencil-and-paper? proofs for these properties, but of course be completely rigorous. We describe where Nominal Isabelle is of great help with such formalisations and where one has to invest additional effort in order to obtain formal proofs.
Formalizing Desargues' theorem in Coq using ranks in Coq (with Nicolas Magaud and Pascal Schreck) [paper (6 pages), slides] accepted for publication in the proceedings of SAC 2009 (track Geometric Constraints and Reasoning) .
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.
Formalization of Projective Plane Geometry in Coq (with Nicolas Magaud and Pascal Schreck) [.pdf (20 pages)] accepted for presentation at ADG2008.
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.
A Formalisation of Logical Relation Proofs given by Crary for Completeness of Equivalence Checking (with Christian Urban) [.pdf (14 pages)], presented at LFMTP07, Electr. Notes Theor. Comput. Sci. (ENTCS) 196:3-18 (2008) .
In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning method of logical relations in a case study about equivalence checking. He presents a type-driven equivalence checking algorithm and verifies its completeness with respect to a definitional characterisation of equivalence. We present in this paper a formalisation of Crary's proof using Isabelle/HOL and the nominal datatype package.
The documented proofs (.pdf 25 pages).
An introduction to GeoProof [online paper], accepted for presentation at MathUI 2007

This paper presents the concrete use of the GeoProof software.
Mechanical Theorem Proving in Tarski's geometry [.ps.gz | .pdf | slides: .pdf], presented at ADG 2006, F. Botana and T. Recio (Eds.), LNAI 4869, pages 139-156, 2008.

This paper describes the mechanization of the proofs of the first height chapters of Schwabäuser, Szmielew and Tarski's book: Metamathematische Methoden in der Geometrie. The goal of this development is to provide foundations for other formalizations of geometry and implementations of decision procedures. We compare the mechanized proofs with the informal proofs. We also compare this piece of formalization with the previous work done about Hilbert's Gründlagen der Geometrie. We analyze the differences between the two axiom systems from the formalization point of view.
Click here to access to the Coq files.
A Graphical User Interface for Formal Proofs in Geometry [.ps.gz | .pdf | slides: .pdf | bibtex], presented at UITP 2006, published in the Journal of Automated Reasoning, Volume 39, Number 2, 2007.
We present in this paper the design of a graphical user interface to deal with proofs in geometry. The software developed combines three tools: a dynamic geometry software to explore, measure and invent conjectures, an automatic theorem prover to check facts and an interactive proof system (Coq) to mechanically check proofs built interactively by the user.
Click here to access to GeoProof web site.
A Decision Procedure for Geometry in Coq [.ps.gz | .pdf | slides: .pdf], published in TPHOL'04 proceedings, LNCS 3223, 2004.
We present in this paper the development of a decision procedure for affine plane geometry in the Coq proof assistant. Among the existing decision methods, we have chosen to implement one based on the area method developed by Chou, Gao and Zhang, which provides short and ``readable'' proofs for geometry theorems. The idea of the method is to express the goal to be proved using three geometric quantities and eliminate points in the reverse order of their construction thanks to some elimination lemmas.
Click here to access to the Coq files.
Toward the use of a proof assistant to teach mathematics, published in ICTMT7 proceedings, 2005

Other documents

Généricité dans le calcul des constructions, mémoire de DEA Sémantique, Preuves, programmation, septembre 2002.
The faq of Coq with Hugo Herbelin and Florent Kirchner.