Bug#855564: O: coq-highschoolgeometry -- coq library for high school geometry proofs/formalisation
Package: wnpp
Severity: normal
I'm orphaning all of my packages in Debian because I have decided to
move onto other endevours and I don't think that I will have the time
to give my packages the attention they deserve.
It's been great being part of Debian and I still remain an enthusiastic
user.
The description reads:
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", theorems about
these things are proven:
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
trigonometry
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", these are proven:
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
Reply to: