[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#789432: ITP: coq-highschoolgeometry -- coq library for high school geometry proofs/formalisation

Package: wnpp
Severity: wishlist
Owner: Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>

* Package name    : coq-highschoolgeometry
  Version         : 8.4+20150620
  Upstream Author : Frédérique Guilhot <Frederique.Guilhot@sophia.inria.fr>
* URL             :
* License         : LGPL-2.1+
  Programming Lang: Coq
  Description     : coq library for high school geometry proofs/formalisation

Created by Frédérique Guilhot, this library consists of a collection of
"chapters" spanning most of the geometry taught in French high schools.

The first part "2-3 dimensional affine geometry" deals with formalising:
 points, vectors, barycenters, oriented lengths
 collinearity, coplanarity
 parallelism and incidence of straight lines
 proofs of Thales and Desargues theorems.

In the second part "3 dimensional affine geometry", we prove theorems about:
 relative positions of two straight lines in the space
 relative positions of a straight line and a plane
 relative positions of two planes
 parallelism and incidence properties for several planes and straight lines

The third part "2-3 dimensional euclidean geometry" deals with formalising:
 scalar product, orthogonal vectors, and unitary vectors
 Euclidean distance and orthogonal projection on a line
 proofs of Pythagorean theorem, median theorem

The fourth part "space orthogonality" deals with formalising:
 orthogonal line and plan

The fifth part "plane euclidean geometry" deals with formalising:
 affine coordinate system, orthogonal coordinate system, affine coordinates
 oriented angles
 proofs of Pythagorean theorem, median theorem, Al-Kashi and sine theorems
 perpendicular bisector, isocel triangle, orthocenter
 circle, cocyclicity, tangency (line or circle tangent)
 signed area, determinant
 equations for straight lines and circles in plane geometry

The sixth part "plane transformations", deals with formalising:
 translations, homothety
 rotations, reflexions
 composition of these transformations.
 conservation of tangency for these transformations.

In the seventh part "applications", we prove:
 Miquel's theorem, orthocenter theorem, Simson line
 circle power and plane inversion
 Euler line theorem and nine point circle theorem

The eighth part "complex numbers", deals with formalising:
 the field properties of complex numbers
 application to geometry of complex numbers

This package is a dependency of geoproof.

Reply to: