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.
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.
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.
- For each direction in the plane an ideal point
is added serving as the point where all parallel lines of that
direction meet.
- To comply with the axiom that any two points are on a line an
ideal line is added through all the ideal points.
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:
- a point is a pair of antipodal points with all great circles
through them,
- a line is a great circle with all pairs of antipodal points
on it.
The statement of Hessenberg's Theorem is:
- In axiomatic plane projective geometry, Pappus' Axiom implies Desargues' Axiom.
We axiomatize plane projective geometry as follows:
- Any two points are incident with a line.
- Any two lines are incident with a point.
- If two points are both incident with two lines, then the points are equal or the lines are equal.
Pappus' Axiom:
- For collinear P,Q,R and collinear P',Q',R',
the intersections ((QR')(RQ')),
((RP')(PR')), and
((PQ')(QP'))
are collinear if they are determinate.
Desargues' Axiom:
-
Two triangles perspective from a point are perspective from a line.
See the
paper for more details.
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:
filename.in contains the inputfilename.out contains the outputfilename.prf contains an intermediate proof formatfilename.v contains a Coq (version 8.0pl3) script of the proof
- Hessenberg's classical argument
(case 1 of Cronheim's proof, see Section 5.1 of the paper)
- Reducing 8 gaps to 2 (see Section 5.2 of the paper)
- The special case: one triangle circumscribes the other
(case 2 of Cronheim's proof, see Section 5.3 of the paper)
- Assembling the parts (see Section 5.4 of the paper)
- In the main file ht.v
the stepping stones (see previous items in this list) are assembled
to obtain a proof of Hessenberg's Theorem.
- Desargues' Axiom by Skolem (see Appendix C of the paper)