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:

**The hypotheses of the theorem have to be stated as a sequence of constructions.**

The construction available are the following:- on_line A B C means A is on line BC
- on_line_d A B C r means that A is on line BC such that BA=r*BC
- inter_ll I A B C D means that I is at intersection of AB and CD
- on_parallel A' A B C means that A' is on the parallel to BC going through A.
- on_parallel_d A' A B C r means that A' is on the parallel to BC going through A such that AA'=r*BC.
- on_inter_line_parallel Y R U V P Q means that Y is the intersection of UV and the parallel to PQ going through R.
- on_inter_parallel_parallel Y R U V W P Q means that Y is at the intersection of the parallel to PQ going through W and the parallel to U V going through R.
- is_midpoint I A B means that I is constructed as the midpoint of AB
- on_perp A' B C means that A' is on the perpendicular line to BC going through B.
- on_perp_d A' B C r means that A' is on the perpendicular to B C going through B and r*Py B C B = 4*S B C A'.
- on_inter_line_perp Y R U V P Q means that Y is at the intersection of UV and the perpendicular to PQ going through R.
- is_circumcenter O A B C
- is_orthocenter H A B C
- is_centroid I A B C

**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 S_{ABC}), the pythagoras difference.

The geometric quantities are noted as:- A ** I is the notation for the signed distance AI.
- S A B C means the signed area of ABC.
- Py A B C means the pythagoras difference (AB*AB+BC*BC-AC*AC).

The predicates which are allowed to state the goal are:
- Col A B C means that A,B and C are collinear
- parallel A B C D means that AB is parallel to CD or A=B or C=D
- perp A B C D means that AB is perpendicular to CD
- on_foot Y P U V mean that Y is on UV and YP is perpendicular to UV
- eq_distance A B C D means that AB=CD (unsigned distances)
- eq_angle A B C D E F means that the measure of the angle ABC is equal to the measure of the angle DEF

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:

- examples_1
- examples_2
- examples_3
- examples_4
- examples_5
- examples_6
- examples_centroid
- examples_circumcenter
- examples_interactive (this file contains examples which require some human interaction)

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 :

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