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 :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072232
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:10:45 PM
Last modification on : Saturday, January 27, 2018 - 1:31:27 AM
Long-term archiving on: Sunday, April 4, 2010 - 10:59:31 PM

Identifiers

  • HAL Id : inria-00072232, version 1

Collections

Citation

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

Share

Metrics

Record views

106

Files downloads

113