bination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs.pdf.pdf

Available online at
Electronic Notes in puter Science 285 (2012) 43–55
ate/entcs
bination of a Dynamic Geometry
Software With a Proof Assistant for
Interactive Formal Proofs
Tuan Minh Pham1 Yves Bertot2
Inria Sophia Antipolis
Abstract
This paper presents an interface for geometry proving. It is bination of a dynamic geometry software,
Geogebra[11] with a proof assistant, Coq[8]. Thanks to the features of Geogebra, users can create and
manipulate geometric constructions, they discover conjectures and interactively build formal proofs with
the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the
ones in high school. For each step of proving, we provide a set of applicable rules verified in Coq for users,
we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Keywords: interactive geometric proofs, Coq, proof assistant, dynamic geometry
1 Introduction
Nowadays, dynamic geometry software (DGS) plays an important role and has
highly influenced mathematics education. Students can use it to construct geomet-
ric objects, observe how these objects change when moving free points or applying
euclidian transformations, and they can discover conjectures. There are numerous
applications for interactive geometry on the market with a variety of features, many
of them are really used in classroom in many countries. However, these uses are usu-
ally limited at the level of discovering conjectures. Some DGS provide proof feature
bining with automated geometry theorem proving (GTP) and allow users to
verify conjectures. They rely on several efficient automatic proof methods, such as
Gr¨obner bases method[13], Wu’s method[4], the area method[5] and the full-angles
method[6]. The first two methods are algebraic methods which use polynomials to
solve problems, they do not give us human-readable proofs. The last two ones can
1 Email: tuan-minh.******@
2 Email