Skip to Main content Skip to Navigation

Proofs with Coq of theorems in plane geometry using oriented angles

Frédérique Guilhot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Formalization of the theory of oriented angles of non zero vectors using Coq is reported. Using this theory, some classical plane geometry theorems are proved, among them : the theorem which gives a necessary and sufficient condition so that four points are cocyclic, the one which shows that the reflected points with respect to the sides of a triangle orthocenter are on its circumscribed circle, the Simson's theorem and the Napoleon's theorem. Elaboration of proofs using Coq that followed the traditional proofs in geometry, and the difficulties encountered are described. Use of the interface Pcoq allows notations close to mathematical ones.
Document type :
Complete list of metadatas
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:09:45 PM
Last modification on : Saturday, January 27, 2018 - 1:31:32 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:59:21 PM


  • HAL Id : inria-00072226, version 1



Frédérique Guilhot. Proofs with Coq of theorems in plane geometry using oriented angles. RR-4362, INRIA. 2002. ⟨inria-00072226⟩



Record views


Files downloads