# Formalization of the Area Method in the Coq proof assistant.

 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:
• 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 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:
• 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
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.