On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic

Marc Bezem & Dimitri Hendriks

This page accompanies the paper On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic, that appeared in Journal of Automated Reasoning, January 2008, Volume 40(1): 61–85.

Here you find an abstract of the paper, an introduction to the real projective plane, and all Prolog input and Coq output files the paper refers to. SWI-Prolog has evolved over the years, so that the prover "CL.pl" mentioned in the paper only works with old versions of SWI-prolog. Please contact Marc Bezem for the latest version of the prover. The Coq files still type-check with Coq 8.4pl2 and constitute the certificate that the results in the paper are correct.

Abstract

State-of-the-art automated theorem provers are not yet able to prove difficult mathematical theorems. The formal verification of difficult theorems still requires human ingenuity, and this situation is not likely to change any time soon. In the combined effort of man and machine called interactive proof construction one would like to have as much automation as possible. It turns out that boosting automation in interactive proof construction is difficult. One reason is that the best automatic provers translate the problem and then work on the translated problem. The correctness of this procedure usually relies on difficult metatheory. Converting a proof of the translated problem into a proof of the original problem can be difficult. Also, navigating the ``automatic'' prover if it doesn't solve the problem can be obscured by the translation. The biggest step in the translation is usually Skolemization, the elimination of existential quantifiers by Skolem functions. We propose to combine interactive proof construction with proof automation for a fragment of first-order logic called Coherent Logic (CL). CL allows enough existential quantification to make Skolemization unnecessary and has a natural proof theory based on forward reasoning. Moreover, this proof theory is easy to automate and standardized proof terms can easily be obtained. We test our approach with a case study which is interesting in itself. Hessenberg's Theorem (1905) states that in axiomatic projective plane geometry Pappus' Axiom (see picture) implies Desargues' Axiom (see picture). Besides being a beautiful theorem, it has an interesting history in that the proof contained a gap for almost 50 years. This makes it worthwhile to formalize the proof by Cronheim (1953), which was claimed to be (and indeed is) complete. We use the proof assistant Coq in combination with our own prover for CL, which generates Coq proof objects. Our CL prover makes it possible to automate large parts of the proof, in particular taking care of the large number of degenerate cases. The proof is constructive in the sense of intuitionistic logic, the Law of the Excluded Middle has not been used.

The Real Projective Plane

As perceived by the human eye, the two parallel tracks of a railroad seem to meet each other at the horizon. This phenomenon is commonly called perspectivity and is caused by the fact that our visual system works through projection on the retina. Projective geometry tries to capture this phenomenon (and many others) by extending the ordinary x,y-plane in the following way.

Ideal points are also called points at infinity and likewise the ideal line is called the line at infinity. In order to fully comply with the axiom that any two points are on a line, we take the line through a normal point and an ideal point to be the line through the normal point in the direction corresponding to the ideal point. Observe that we now also have achieved that every two lines intersect, including parallel ones and a normal and the ideal line.

The above construction may be visualized as follows. Consider the unit sphere x2 + y2 + z2 = 1 and the (tangent) plane z=1. Through projection from the origin, the points in this plane are in one-to-one correspondence with pairs of antipodal points on the unit sphere. From the latter we must of course exclude the pairs with z=0. These pairs are a natural choice for points at infinity, since parallel lines in the plane z=1 are projected onto great circles on the unit sphere and the pair of antipodal points with z=0 depends only on the direction. (A great circle on a sphere is the intersection of the sphere with a plane through the center of the sphere. Two parallel lines in z=1 define two planes through the origin which intersect in a third parallel line in z=0.) The great circle with z=0 on the unit sphere finally forms a natural choice for the line at infinity.

The above model, where the `lines' are great circles on the unit sphere and the `points' are pairs of antipodal points on the same sphere, may be considered as the standard model of the real projective plane. There are many other projective planes, not necessarily based on the real numbers, even finite ones. In this paper we take the axiomatic approach, where we postulate a number of essential properties shared by all structures that one would like to call `projective planes'. These may or may not satisfy additional properties, such as those of Pappus and Desargues, whose interrelation we study.

A beautiful principle in projective geometry is that of duality. Duality in a projective plane P means that we can interchange the roles of points and lines while keeping the incidences. In this way one obtains another projective plane, namely the dual plane Pd. In any statement about incidences which is valid in P, the words point and line can be systematically interchanged to obtain a dual statement, which is valid in Pd. Duality carries over to derived concepts such as connecting line, collinear and intersection, concurrent, respectively. The duality principle follows from the observation that the axioms either are self-dual (i.e., they imply their own duals), or their duals are themselves listed as axioms. If a statement is valid in all projective planes, then its dual is also valid in all projective planes. Duality is also visible in the standard model:

Hessenberg's Theorem

The statement of Hessenberg's Theorem is:

We axiomatize plane projective geometry as follows: Pappus' Axiom: Desargues' Axiom: See the paper for more details.

The files referred to in the paper

Here we list the files of our case study of using the CL prover to automatically generate a proof of Hessenberg's theorem. The automatically generated files cro_case1.v, cro_8_2.v, cro_case2.v and the main file ht.v have been type checked with Coq version 8.4pl2.
For any experiment filename:

Marc Bezem
Dimitri Hendriks

created: 2005/12/05
last modified: 2016/09/07
Marc Bezem