|
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 |