Formalization of the Area Method in the Coq proof assistant.

Julien Narboux

We present here the formalization within the Coq proof assistant of the area method described in the book Machine Proofs in Geometry by Chou, Gao and Zhang.

This an implementation of a decision procedure for constructive theorems in euclidean plane geometry.
This procedure is a mix of algebraic and synthetic methods. The idea of the method is to express the theorem as a sequence of geometric constructions and treat the points in the reverse order of their construction.
The treatment of each constructed point consists in eliminating every occurrence of the point in the goal. This can be done thanks to some elimination lemmas (for areas, for ratios and for pythagoras differences).

When all the constructed points have been eliminated, we get an arithmetic expression involving only free points. Thanks to some other lemmas, this expression can be transformed into an expression involving only independent quantities (the coordinates of the free points).
The equality between two arithmetic expressions involving independent quantities can then be proved using either the standard Coq tactic called field or our own implementation.

Shang-Ching Chou
Xiao-Shan Gao
Jing-Zhong Zhang

Machine Proofs in  Geometry

Automated Production of Readable Proofs for Geometry Theorems

World Scientific, 1994

To be in the language of the procedure, the goal to be proved must verify two conditions:
  1. The hypotheses of the theorem have to be stated as a sequence of constructions.
    The construction available are the following: The definition of these constructions can be found here and here.
  2. The goal must be expressed as an arithmetic expression using only three geometric quantities: the ratio of two oriented distances (AB/CD) with AB parallel to CD, the signed area of a triangle (noted SABC), the pythagoras difference.
    The geometric quantities are noted as:
    1. A ** I is the notation for the signed distance AI.
    2. S A B C means the signed area of ABC.
    3. Py A B C means the pythagoras difference (AB*AB+BC*BC-AC*AC).
    Using these three quantities some predicates can be defined: collinearparallel, midpoint, perpendicular...
  3. The predicates which are allowed to state the goal are:
All the proof are based on this axiom system plus these axioms for euclidean geometry.
The example files contain more than 100 examples. Here are some of theorems which are proved automatically:
The files containing the examples are the following:
You can browse the Coq files from the index, or have a look at the dependency graph of the modules or download the whole development as a .tar.gz file (to be compiled with Coq V8.3). These file are also distributed as a user contribution of Coq here.

References :
  1. A Decision Procedure for Geometry in Coq [.ps.gz | .pdf | Slides.pdf], published in TPHOL'04 proceedings
  2. Formalisation et automatisation du raisonnement géométrique  en Coq.
  3. The Area Method: a recapitulation [.pdf] with Predrag Janicic and Pedro Quaresma, in revision at JAR 2010.