Tuan-Minh Pham

Yves Bertot

Julien Narboux

A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry

Keywords: formalization, automation, geometry, Coq, teaching

.

Introduction

Technological tools are widely used to teach mathematics in schools. Dynamic Geometry Software (DGS) and Computer Algebra Software (CAS) are the two families of software that are well represented. These tools are widely used to explore, experiment, visualize, calculate, measure, find counter examples, conjectures... but most of them can not be used directly to build or check a proof. Proof is a crucial aspect of mathematics and therefore should be integrated more into the mathematical tools. The exploration and proof activities are interlaced. We think that these two activities could be better interlaced if they were both conducted using the computer.

Dynamic geometry systems (DGS) are used more and more to teach geometry in school. They not only allow students to understand construction steps that lead to final drawings, but also provide access to geometric objects, allow students to move free points and see the influence on the rest. Then, students can find out new properties from the drawings. To justify conjectures, some among the numerous DGS provide proving features. These systems are almost This work is partially supported by the french ANR project Galapagos all based on algebraic (coordinate-based) methods or semi-algebraic (coordinatefree) methods. Most DGS do not allow users to interactively build traditional proofs. The few DGS which provide interactive theorem proving features are either based on databases of proofs known in advance or on adhoc theorem provers which can not be easily extended. In [START_REF] Narboux | Toward the use of a proof assistant to teach mathematics[END_REF], we give a more precise description of the different systems. We believe that deductive proofs should continue to be an essential part of the high-school curriculum for a geometry course. We also think that the use of a proof assistant to interactively build proofs could help students understand the concepts of deduction. This use has the following advantages:

-It gives clear logical view about the geometric problems. The system makes clear what are the hypotheses and the conclusions. Student can understand the logical inferences used in each reasoning step by observing the change of the proof environment. -Reasoning steps are verified by the proof assistant, thus constructed proofs have very high level of confidence. -It allows to combine purely geometric arguments with other kinds of proofs (using complex numbers for instance).

This leads to the necessity of developing a geometry proving tool for high school students which they can use to interactively construct traditional geometry proofs with the support of a proof assistant.

The first step in this direction was done by F. Guilhot, a high school teacher who developed a library in the Coq proof assistant for interactive theorem proving in geometry at the level of high-school [START_REF] Guilhot | Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée[END_REF]. This development is based on a specific axiom system which is adapted to the knowledge of high school students. It covers a large portion of basic notions of plane geometry, properties and theorems. Its proofs and its geometry reasoning are close to what students learn in high school. Some classical theorems are proved in this library, such as Menelaus, Ceva, Desargues, Pythagoras, Simsons' line etc. Then, a tool called GeoView was developped in order to visualize graphically geometry statements using a DGS [START_REF] Bertot | Visualizing geometrical statements with GeoView[END_REF].

Another tool using Coq that was developed by J. Narboux is GeoProof. This tool works in the opposite direction: the DGS is used to generate statements and tactics for Coq. Its proving feature is based on the automated deduction method -the area method. It is not an interactive proving tool [START_REF] Narboux | A graphical user interface for formal proofs in geometry[END_REF].

Recently, the first author developed a tool for interactive proof using GeoGebra [6] and Coq [START_REF] Pham | A combination of a dynamic geometry software with a proof assistant for interactive formal proofs[END_REF]. A proof window is added in GeoGebra, it allows to communicate with Coq. The user can draw figures and state conjectures, geometric constructions and conjectures are translated into relations between geometric objects and sent to Coq. A geometric problem is expressed by a set of hypotheses and conclusions. The reasoning steps are interactively built by mouse clicks over geometric objects and hypotheses using appropriate proving methods. The reasoning steps are translated into commands and executed by Coq. The new state is sent back to the user. The changes of hypotheses and conclusions allows the user to continue the proof. We refer readers to [START_REF] Pham | A combination of a dynamic geometry software with a proof assistant for interactive formal proofs[END_REF] for more information about the graphical user interface for this tool.

A crucial part of this tool lies in its library for synthetic geometry in Coq. The library contains formalizations of geometric notions, and of geometric theorems that allow the user to manipulate geometric objects and to produce proofs. Developing a library in the style of the synthetic geometry system is appropriate. In the synthetic geometry, we postulate the existence of geometric objects (e.g. points, lines,. . . ) and geometric relations as primitive notions and build up the geometry from an axiom system that deals with these primitive notions. The geometry proofs are constructed by making use of axioms, theorems and logical arguments. This approach is pedagogically suitable and satisfactory from a logical point of view. In this paper, we focus on this synthetic library and we present why and how we extended [START_REF] Guilhot | Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée[END_REF].

The development by F.Guilhot has three main drawbacks: first it is based on many axioms which are not really needed, second it lacks constructive definitions for the existence of geometric objects, third it lacks automation. Indeed, in this library, each geometric notion is defined by axioms that assert its properties. This leads to an explosion of the number of axioms. Moreover, the library does not provides functions to construct points and lines and compound geometric constructions, it only provides axioms which states the existence of the compound objects. We will detail these drawbacks in section 2. Finally, the library does not include any automatic theorem proving methods. We think that having an automatic theorem proving method is important because:

-During an interactive proof, students can meet minor proof obligations. It they need to solve these proof obligations interactively this can lead to very technical proofs. This is not adapted to their level of abstraction. -It may be useful to be able to check if a statement is correct in order to help the student or to give better error messages when the student make a mistake.

This motivates us to improve this library. We reduce the number of axioms by providing a more compact axiom system and constructively building up the geometric notions from this system. We also enrich the library with an automated deduction method -the area method [START_REF] Chou | Machine Proofs in Geometry[END_REF]. This method gives readable proofs, based on the notions: signed area, ratio of directed segment and Pythagoras difference which are also very close to high school knowledge. For that purpose, we integrate the formalization of the area method in Coq by J.Narboux [START_REF] Narboux | A decision procedure for geometry in Coq[END_REF][START_REF] Janicic | The Area Method : a Recapitulation[END_REF].

This article is organized as follows. After giving some discussion about the formalization of F. Guilhot in Section 2, we present in Section 3 our developments to eliminate its redundant axioms and to redefine geometric notions. Section 4 deals with the integration of the area method. The last section is for the conclusion and our perspectives.

Related works Several axiom systems for synthetic geometry were produced, Hilbert proposed his axiom system [START_REF] Hilbert | Les fondements de la géométrie[END_REF] with 20 axioms relating two primitive notions: point and line. Another was proposed by Tarski [START_REF] Tarski | What is Elementary Geometry?[END_REF] which is simpler, relies on first order logic, and contains only eleven axioms, two predicates, and one primitive notion: point. The axiom system of Hilbert was formalized in Coq by C. Dehlinger [START_REF] Dehlinger | Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry[END_REF] and in Isabelle/Isar by L. Meikle [START_REF] Meikle | Formalizing Hilbert's Grundlagen in Isabelle/Isar[END_REF]. The one of Tarski was formalized in Coq by J. Narboux [START_REF] Narboux | Mechanical theorem proving in Tarski's geometry[END_REF]. However, systems such as Hilbert's system or Tarski's system have starting points that are too low, hence they can not be used in a pedagogical context. The work closest to ours is the one by P. Scott and J. Fleuriot [START_REF] Scott | Idle time discovery in geometry theorem proving[END_REF]. This work present the integration of an automatic theorem proving tool in the user interface of a proof assistant. The difference with our work is that the automatic theorem proving tool they integrate is not specialized in geometry. Hence, it can be used in many contexts as for example a low level development about Hilbert axiom system but it may be less efficient for complex geometry theorems.

Formalization of High-school Geometry

In this section, we present the development of F.Guilhot and what can be improved. As mentioned, F. Guilhot does not try to provide a system with a minimal number of axioms, nor to provide an automated tool for theorem proving. She only tries to provide a system in which definitions of geometric notions, theorems and geometry reasonings are described as they are taught in high school. She does not build up the whole of Euclidean geometry from a fundamental axiomatic system (such as the systems mentioned above). She uses an alternative approach to the same geometrical results. She first constructs a vector space attached to the affine geometry, then she construct an Euclidean space by adding the notion of scalar product to the affine geometry.

We use small letters a, b, c. . . to denote real numbers; capital letters A, B, C. . . to denote points; pairs of a real number and a point in the form aA to denote mass points.

The key technique in her formalization lies in using the universal space proposed by M. Berger [START_REF] Berger | Problems in Geometry[END_REF]. The vector space is extended to the universal space which is a union of points with a given non-zero mass and the vectors in the vector space. The rule aB -aA = a --→ AB is used to convert vectors to the representation in mass points. The vector space property of the universal space is preserved and defined by the following axioms:

-Axiom 1 (Definition of addition) : With (m + n = 0), there is a unique point R (called barycenter) on

P Q such that nP + mQ = (m + n)R. -Axiom 2 (Definition of vector): With (m + n = 0), the sum of (nP + mQ) is a vector m --→ P Q. -Axiom 3 (Idempotent): nP + mP = (m + n)P . -Axiom 4 (Commutative): nP + mQ = mQ + nP . -Axiom 5 (Associative): nP + (mQ + kR) = (nP + mQ) + kR. -Axiom 6 (Definition of scalar multiplication): k(nP ) = (k * n)P . -Axiom 7 (Distributivity) k(nP + mQ) = knP + kmQ.
These properties form an extension of the theory of mass points (where mass is not limited to a positive real number). So we can completely perform calculations in mass points as we can do with problem-solving technique of mass point theory. Furthermore, these calculations are taught in high school courses and straightforward.

In Coq, the type of mass points is declared as a record composed of a real number and a point. A variable add MP which takes two arguments of type mass point and gives a mass point is declared for addition operator and a variable mult MP which takes a real number and a mass point as arguments and gives a mass point is declared for scalar multiplication operator.

Record MassPoint : Type := c o n s {number : R; p o i n t : P o i n t } . V a r i a b l e add MP :

MassPoint -> MassPoint -> MassPoint . V a r i a b l e mult MP : Real -> MassPoint -> MassPoint .
The system of axioms which defines the universal space is introduced. It allows us to manipulate mass points. A good idea for calculating mass points in Coq is mapping this space to an abstract field structure. This enables us to simplify equations of mass points using automated tactics in Coq library for field (such as ring simplify, field simplify. . . ). It makes calculations easier. Plane Euclidean geometry can be obtained by equipping affine geometry with the notion of scalar product. The other geometric notions are added step by step using existing formalized notions and their relations in the library.

However, the geometric objects are almost all declared as abstract functions that take points as input, and axioms allow to manipulate these notions. For example, the orthogonal projection of a point C onto the line AB is defined as follows. Where a variable expresses the orthogonal projection function. The axioms say that if we have collinearity of A, B and H and orthogonality of --→ AB and --→ CH then H is the orthogonal projection of C onto the line AB and vice versa.

Using axioms asserting properties of objects to define them is a usual manner in high school. However, this leads to an explosion of the number of axiom and makes the axiomatic system redundant. Moreover, for compound objects, this kind of definitions are not constructive. The existence of the compound objects is stated by axioms and constructing these objects from existing simpler objects is not clear.

In the next section, we introduce a more compact axiom system, we redefine geometric notions and build up a new geometry system. Redundant axioms in the older system are put in the form of theorems to be proved. Theorems and properties that are proved in the older system are maintained. New properties corresponding to new definition of notions are introduced.

3 From Affine to 2D-Euclidean Geometry : a Vector Approach

Axiomatic system

The use of mass points is a good approach for computation, similar to what students know. However, students may feel bored in these computations since they can not visualize objects that they are manipulating. So, we use the notion of vector as the key notion in our development. We will define other geometric notions by relations of vectors.

In the last section, the vector is defined as a sum of two mass points in the special case where the sum of mass equals zero. We use a sub-type of mass point to define it in Coq.

D e f i n i t i o n i s V e c t o r ( v : MassPoint ):= e x i s t s A, B : Point , v = add MP (( -1) A) ( 1 B ) . Record Vector : Type := vecCons { mpOf : MassPoint ; p r o o f : i s V e c t o r mpOf } .
The vector data type is constructed from an element mpOf having the mass point type with a proof showing that this element can be expressed by the sum of mass point of two certain points A and B with mass values (-1) and 1 respectively. After proving the fact that a linear combination of two mass points satisfying isVector predicate also satisfies this predicate, we can easily define the addition operator and the scalar multiplication operator for the vector type. It is clear that we can perform computation over vectors by reusing computations over mass points.

To build up the Euclidean space, we introduce a system of axioms for the scalar product (also called the dot product or the inner product).

Axiom 8 p o s i t i v i t y : ∀ -→ v : Vector , -→ v • -→ v 0 Axiom 9 p o s i t i v i t y 2 : ∀ -→ v : Vector , -→ v • -→ v = 0 -> -→ v = -→ 0 Axiom 10 symmetry : ∀ -→ u -→ v : Vector , -→ u • -→ v = -→ v • -→ u Axiom 11 d i s t r i b u t i v i t y : ∀ -→ v1 -→ v2 -→ v3 : Vector , ( -→ v1 + -→ v2)• -→ v3 = -→ v1 • -→ v3 + -→ v2 • -→ v3 Axiom 12 h o m o g e n e i t y : ∀ ( k : R) ( -→ u -→ v : Vector ) , (k × -→ u ) • -→ v = k × ( -→ u • -→ v )
To define the Euclidean plane, we introduce an axiom about the existence of three distinct and non-collinear points and another about co-planarity any fourth point with them. These axioms not only ensure that all given points lie on the same plane, but also allow us to define the orientation for planes. The concept of orientation is important because of its use in the definition of trigonometric functions.

V a r i a b l e O O1 O2 : P o i n t . Axiom 13 e x i s t 3 d i s t i n c t n o t c o l p o i n t s :

O = O1 ∧ O = O2 ∧ O = O3 ∧ ¬collinear OO1O2
. Axiom 14 c o p l a n a r i t y : ∀ (M : P o i n t ) , ∃ k1 k2 : R,

--→ OM = (k1 × --→ OO1) + (k2 × --→ OO2) .

Overview of the structure of the formalization

We construct geometric notions from our primitive notions and prove their properties using our axiom system. Properties and theorems in the library of F. Guilhot are either preserved or reformalized with new definitions of geometric notions. Let's take a look at the Fig. 1 and 2 to have a overview of our formalization.

Figure 1 shows the dependency between concepts in our formalization for affine geometry. Notions in affine geometry are easily formalized from vector. Alignment of three points A, B and C is defined by collinearity of -→ AC and --→ AB, parallelism of two vectors is defined by collinearity of them. The other ones are also covered such as midpoint, center of gravity of triangle, parallelogram, . . . Our formalization covers a large part of the geometry curriculum in French high school. Many notions are formalized, their properties are verified. They are considered as basic concepts to produce more complex geometric proofs.

A constructive geometry library

In this section and the following one, we use these notations:

-- → v 1 • - → v 2 for the scalar product of - → v 1 - → v 2 -|AB| for the Euclidean distance from A to B -- → v ⊥ for the orthogonal vector of - → v -AB for the signed distance from A to B -S ABC for the signed area of ABC -| - → v | for the measure of - → v
In GeoGebra or other DGS, the user can create and manipulate geometric constructions. The user starts with points and simple constructions, then constructs new geometric object from existing ones. So, to match our library with constructions in DGS, we try to provide primitive constructions which are elementary constructions by rules and compass and mentioned in [9]. They include: the point lying on a given line, the midpoint of two given points, the line passing through two given points, the line passing through a given point and perpendicular to a given line; the line passing through a given point and parallel to a given line, the intersection point of two lines, the circle with a given center passing through a given point, the circle with a given diameter,. . . These constructions one by one are defined by vector or by relations over existing notions. The line AB is formalized by A and --→ AB. The midpoint I of two points A and B is formalized by constructing -→ AI such that -→ AI = 1 2 × --→ AB. The circle with center O that passes through A is formalized as the set of points M which distance OM equals distance OA. . . One interesting formalization here is the one of line. We look for a data structure to express all sorts of line. In Coq, we use a record with a root point and a direction vector to define the line. To ensure existence of line, an element is added to record, this is a proof to show that this direction vector is not the null vector. The line passing through two points A and B is expressed by a null Line in the case A = B, and by the construction of A and --→ AB in the other case. The line which goes through a given point A and which is parallel to another line a (denoted lineP A a) is expressed by the construction of A and --→ AB where B is constructed such that --→ AB equals the direction vector of line a. The perpendicular line (denoted lineT ) is formalized in the same way.

We define also equality of lines by collinearity of their direction vectors for the case that two lines have the same root point, and by collinearity of their direction vector with the vector constructed by two root points for the case where these points are distinct. Properties concerning equality of lines are verified with this definition, such as: For compound constructions, we formalize them by the way that they are built from primitive constructions. For example, instead of defining the orthogonal projection with three given points by axioms as mentioned in Section 3, we define an orthogonal projection of a given point C onto a given line a. We construct the line that passes through C and which is perpendicular with a, we prove that this line and a are not parallel, then we get the intersection point of them.

D e f i n i t i o n o r t h o g o n a l P r o j e c t i o n (C : P o i n t ) ( a : L i n e ) :=

i n t e r s e c t i o n P o i n t ( l i n e T C a ) a .

As we said above, students are familiar with definition of geometric objects by axioms about their properties. So, to avoid losing the pedagogical meaning of the library and to verify if objects are well formalized, we keep the former axioms in the form of theorems, and prove them. Each object is accompanied by a pair of theorems. One allows us to get properties from its definition, the other is to get a definition from properties.

Lemma o r t h o g o n a l P r o j e c t i o n P r o p e r t i e s : f o r a l l A B C H : Point , A <> B-> H = o r t h o g o n a l P r o j e c t i o n C ( l i n e A B) -> c o l l i n e a r A B H /\ o r t h o g o n a l ( v e c t A B) ( v e c t H C ) . Lemma p r o p e r t i e s o r t h o g o n a l P r o j e c t i o n : f o r a l l A B C H : Point , A <> B -> c o l l i n e a r A B H -> o r t h o g o n a l ( v e c t A B) ( v e c t H C) -> H = o r t h o g o n a l P r o j e c t i o n C ( l i n e A B ) .

Proving theorems of the first kind is simpler than proving theorems of the second kind. The latter usually lead to the proof of uniqueness property of objects. Many compound constructions are introduced: the perpendicular bisector of two given points, orthogonal projection of a point onto a line, the circumcircle of three given points, the center of circumcircle, the orthocenter, the center of gravity,. . . Reformalizing the geometric objects allows us to eliminate a lot of redundant axioms. Remaining axioms are used to introduce other geometric notions such as: the parallelism of lines, the perpendicularity of lines, the signed area of vectors or of triangle, the vector angles, the trigonometric functions,. . . These notions are essential for the library manipulating geometric objects and stating geometric problems. Except for vector angles and the trigonometric functions, the rest are formalized without much effort, and many axioms are eliminated.

Integration with the Area Method

Our library contains a large number of geometric notions and propositions. This allows us to prove many geometry theorems. Constructing a traditional proof consists in finding a sequence in logical steps to the conclusion. But in the context of education, a drawback of constructing fully traditional proofs is that, as mentioned in the introduction section, there are minor goals in interactive proving which are necessary to complete the formal proof but which lead to tedious steps and are not adapted to the level of abstraction at which we usually work with students. Hence we integrate a coordinate-free automatic deduction method with a library for interactive proof. This improves the power and does not decrease pedagogical meaning of the library. The coordinate-free automatic deduction method we chose is the area method of Chou, Gao and Zhang. This method consists in expressing the goal to be proved using three geometric quantities (the signed area of a triangle, the signed distance and the Pythagoras difference), and eliminating the points from the goal in the reverse order of their construction using some elimination lemmas.

To integrate the area method in our development, we need first to ensure the correctness of all the elimination lemmas of the area method and second we need to create a mapping between the definitions of the geometric constructions of the two systems.

Correctness of the area method

The first work in the process of integration is to ensures the correctness of this method in our library. Because the area method is constructed based on its own axiom system mentioned in Table 1, we need only to verify these axioms. Before proving them, we have to make a mapping of primitive notions of this method into our library. In fact, this method only has two primitive notions, being the signed area and the signed distance. Others notions such as the Pythagoras difference, the parallelism, the perpendicularity, the collinearity. . . , as well as geometric constructions, are defined from these two primitive notions. The crucial thing in the formalization of these two basic notions is constructing three points O, I and J that form a Cartesian coordinate system. With the support of these points, we can define the two primitive notions of the area method in our system.

O, I and J form a Cartesian coordinate system, in other words, they satisfy

--→ OO 1 ⊥ ---→ O 1 O 2 , we first construct M such that --→ OM = 1 2 × --→ OO 2 , we then construct O 3 such that ---→ O 1 O 3 = 2 × ---→ O 1 M . M is the midpoint of OO 2 and O 1 O 3 , so --→ OO 3 ---→ O 1 O 2 . From the hypothesis --→ OO 1 ⊥ ---→ O 1 O 2 we have --→ OO 3 ⊥ --→ OO 1 . For the second case --→ OO 1 ⊥ ---→ O 1 O 2 , we construct H as the orthogonal projection of O 2 on OO 1 . O 3 is constructed from O 1 , O 2 by ---→ O 1 O 3 = |O1O| |O1H| × ---→ O 1 O 2 .
Thanks to an extension of the Thales theorem for parallel lines in our library, we can prove

--→ OO 3 ---→ HO 2 from |O1H| |O1O| = |O1O2| |O1O3| .
From the definition of H, we get

---→ O 2 H ⊥ --→ OO 1 , therefore --→ OO 3 ⊥ --→ OO 1 . O = O 3 in
               if --→ AB • -→ OI > 0 AB = |AB| if --→ AB • -→ OI < 0 AB = -|AB| if --→ AB • -→ OI = 0      if --→ AB • -→ OJ > 0 AB = |AB| if --→ AB • -→ OJ < 0 AB = -|AB| if --→ AB • -→ OJ = 0 AB = 0
On the other hand, the Cartesian coordinate system with the new points O, I, J enables us to construct the orthogonal vector for the given vector.

-

→ v ⊥ := (-- → v • -→ OJ) × -→ OI + ( - → v • -→ OI) × -→ OJ.
We can then formalize the trigonometric functions of two vectors and the signed area of a triangle as follows:

cos

- → v 1 - → v 2 = - → v1• - → v2 | - → v1|×| - → v2| and sin - → v 1 - → v 2 = - → v1 ⊥ • - → v2 | - → v1 ⊥ |×| - → v2| S ABC = 1 2 × |AB| × |AC| × sin --→ AB -→
AC Two primitive notions of the area method are formalized, many properties are also proved. They are properties of the signed distance

--→ AB = k × --→ CD ↔ AB = k × CD ∧ --→ AB --→ CD, col A B C → AB + BC = AC; properties of the orthogonal vector ( - → v 1 + - → v 2 ) ⊥ = - → v 1 ⊥ + - → v 2 ⊥ , (k × - → v ) ⊥ = k × - → v ⊥ , | - → v ⊥ | = | - → v |, - → v 1 • - → v 2 ⊥ = -- → v 1 ⊥ • - → v 2 ;
as well as properties of signed area S ABC = 1 2 × --→ AB ⊥ • -→ AC, S ABC = S BCA , S ABC = -S ACB . . . They serve as basic properties to prove the axiom system in Table 1. We do not intend to detail long proofs, we give only the following proof of the property 6: S DAB + S DBC + S DCA = S ABC presented with two column method as an example. The full Coq proofs consists of approximately 1500 lines of Coq tactics. Property Reasoning 1.

S DAB = S BDA = 1 2 × --→ BD ⊥ • --→ BA signed area props 2. S DBC = S BCD = 1 2 × --→ BC ⊥ • --→ BD signed area props 3. 1 2 × --→ BC ⊥ • --→ BD = -1 2 × --→ BC • --→ BD ⊥ orthor vect props 4. -1 2 × --→ BC • --→ BD ⊥ = 1 2 × --→ CB • --→ BD ⊥ orthor vect props 5. S DBC = 1 2 × --→ CB • --→ BD ⊥ from (2) (3) (4) 6. S DAB + S DBC = 1 2 × --→ BD ⊥ • --→ BA + 1 2 × --→ CB • --→ BD ⊥ from (1) (5) 6. S DAB + S DBC = 1 2 × --→ BD ⊥ • ( --→ BA + --→ CB) distrib prop 7. S DAB + S DBC = 1 2 × --→ BD ⊥ • -→ CA ( --→ BA + --→ CB) = -→ CA 8. S DAB + S DBC = 1 2 × ( --→ BC + --→ CD) ⊥ • -→ CA --→ BD ⊥ = --→ BC + --→ CD 9. S DAB + S DBC = 1 2 × ( --→ BC ⊥ • -→ CA + --→ CD ⊥ • -→ CA) --→ BD ⊥ = --→ BC + --→ CD 10. S DAB + S DBC = 1 2 × (- --→ CB ⊥ • -→ CA + --→ CD ⊥ • -→ CA) --→ BC ⊥ = - --→ CB ⊥ 11

Usability of the area method

This method consists in expressing the goal to be proved using three geometric quantities (the signed area of a triangle, the signed distance and the Pythagoras difference), and eliminating the points from the goal in the reverse order of their construction using some elimination lemmas. It deals with problems stated in terms of sequences of specific geometric construction steps. So to make it runnable in our library, we have to convert geometry statements in our library to its statements. Precisely, from sequences of geometric constructions of our library, we have to construct sequences in the area method.

The first step in this process is to normalize the constructions in our library. Compound constructions are unfolded and replaced by sequences of primitive constructions. These sequences are also reduced without loosing their semantics. For example, a line passing through A that is parallel with perpendicular bisector of BC is simplified to a line passing through A that is perpendicular to line BC.

In the second step, we try to extract constructions of the area method from the sequence of constructions we get in the first step. Let's consider constructions of the area method. In fact, each construction aims to create a geometric object with a precise semantics. For example, on inter line perp Y R U V P Q is a construction in the area method and defined by It means that Y is at the intersection of U V and the perpendicular to P Q going through R. With the semantics of construction, we can construct a sequence of primitive constructions of our library that produces this object. For each constructions, a lemma is introduced to ensure that sequences of primitive constructions give us exactly the object defined by this construction. In our example, the corresponding sequence of the construction on inter line perp Y R U V P Q is Y = intersectionPoint (lineT R (line P Q)) (line U V). The lemma that ensures exactness is as follows: To complete this step, we write tactics to automatically introduce constructions of the area method when their corresponding sequence of primitive constructions appears in hypotheses. The following tactic is for our example:

Ltac c o n v e r t t o A M C o n s t r u c t i o n s 1 2 := r e p e a t match g o a l with | H: ?Y = i n t e r s e c t i o n P o i n t ( l i n e T ?R ( l i n e ?P ?Q) ) ( l i n e ?U ?V)| -=> t r y ( a s s e r t ( o n i n t e r l i n e p e r p Y R U V P Q) by ( apply ( @ c o n s t r o n i n t e r l i n e p e r p Y R U V P Q) ; auto with geo ) ; r e v e r t H) end ; i n t r o s .

Conclusion

Our development provides a library in Coq for interactive and automated geometry theorem proving. As far as we know, this is the first system which integrate both interactive and automatic theorem proving in geometry in a formal setting. We give an axiom system, from which we build up Euclidean plane geometry. We then verify the axiom system of the area method and integrate this method into our library. In this library, geometric objects are formalized in a constructive manner. Proof of properties, lemmas, and theorems are formal and traditional proofs, they are adapted to student knowledge. The combination with the automated deduction method offers flexibility and power in proving geometry theorem. The integration of this library in a dynamic geometry tool offers advantages in education. It allows student to build proofs themselves. In addition, it highlights the structure of the proofs. Student have a logical view of geometry problems and understands what are the hypotheses and the goal. This work could also be used to study the combination of different automatic theorem proving methods in geometry.

V

  a r i a b l e o r t h o g o n a l P r o j e c t i o n : Point->Point->Point->P o i n t . Axiom d e f o r t h o g o n a l P r o j e c t i o n : f o r a l l A B C H : Point , A <> B -> c o l l i n e a r A B H -> o r t h o g o n a l ( v e c t A B) ( v e c t H C) -> H = o r t h o g o n a l P r o j e c t i o n A B C . Axiom d e f o r t h o g o n a l P r o j e c t i o n 2 : f o r a l l A B C H : Point , A <> B -> H = o r t h o g o n a l P r o j e c t i o n A B C -> c o l l i n e a r A B H /\ o r t h o g o n a l ( v e c t A B) ( v e c t H C ) .

Fig. 1 :

 1 Fig. 1: Formalization of notions in affine geometry

Fig. 2 :

 2 Fig. 2: Formalization of plane geometry

Record L i n

  e : Type := l i n e C o n s { r o o t O f : P o i n t ; vecOf : Vector ; p r o o f : i s N o t Z e r o V e c vecOf } .

  Lemma a l i g n l i n e : f o r a l l A B C : Point , A <> B -> A <> C -> c o l l i n e a r A B C -> l i n e A B = l i n e A C . Lemma l i e s O n L i n e e q L i n e : f o r a l l A B C D: Point , A <> B -> C <> D -> l i e s O n L i n e C ( l i n e A B) -> l i e s O n L i n e D ( l i n e A B) -> l i n e A B = l i n e C D.For example, to prove the first lemma, we start with the hypotheses A = B and A = C we have that the definition of line --→ AB and -→ AC are direction vectors of line AB and line AC respectively. By the definition of collinearity we have that --→ AB and -→ AC are collinear. So line AB = line AC by the definition of equality of lines for the case that lines have the same root point.

1 .

 1 AB = 0 if and only if the points A and B are identical 2. SABC = SCAB 3. SABC = -SBAC 4. If SABC = 0 then AB + BC = AC (Chasles' axiom) 5. There are points A, B, C such that SABC = 0 (dimension; not all points are collinear) 6. SABC = SDBC + SADC + SABD (dimension; all points are in the same plane) 7. For each element r of F , there exists a point P , such that SABP = 0 and AP = rAB (construction of a point on the line) 8. If A = B, SABP = 0, AP = rAB, S ABP = 0 and AP = rAB, then P = P (uniqueness) 9. If P Q CD and P Q CD = 1 then DQ P C (parallelogram) 10. If SP AC = 0 and SABC = 0 then AB AC = S P AB S P AC (proportions) 11. If C = D and AB ⊥ CD and EF ⊥ CD then AB EF 12. If A = B and AB ⊥ CD and AB EF then EF ⊥ CD 13. If F A ⊥ BC and SF BC = 0 then 4S 2 ABC = AF 2 BC 2 (area of a triangle)

  |OI| = 1 and |OJ| = 1. The axiom 13 gives us the existence of three non-collinear points O, O 1 and O 2 . The axiom system for mass point (the key here is axiom 1 for the barycenter) allows us to produce a new point C from two given points A, B and a real number k such that -→ AC = k× --→ AB. We explain how to construct O, I, J from O, O 1 , O 2 using this rule for producing new points. We first construct a point O 3 such that --→ OO 1 ⊥ --→ OO 3 and O = O 3 . Let's consider two configurations of O, O 1 , O 2 in Fig. 3. For the first case

  the two cases is easily verified thanks to distinctions of O, O 1 , O 2 in the axiom 13.

Fig. 3 Now

 3 Fig.3

  . S DAB + S DBC = -S CBA + S CDA signed area props 12. S DAB + S DBC = S CAB -S CAD signed area props 13. S DAB + S DBC + S CAD = S CAB signed area props 14. S DAB + S DBC + S DCA = S ABC signed area props Qed.

  Lemma c o n s t r o n i n t e r l i n e p e r p :f o r a l l Y R U V P Q : Point , P <> Q -> U <> V ->˜p e r p e n d i c u l a r ( l i n e P Q) ( l i n e U V) -> Y = i n t e r s e c t i o n P o i n t ( l i n e T R ( l i n e P Q) ) ( l i n e U V) -> o n i n t e r l i n e p e r p Y R U V P Q .

Table 1 :

 1 The axiom system for the area method

In the future, we will study the integration of algebraic approaches to automatic theorem proving in geometry such as Gröbner bases and Wu's method. To be useful in high-school, we will also need to extend our proof system to allow proofs which look less formal. For that purpose we will study how to deal automatically with degenerated cases.