coq-projective-geometry

Projective Geometry. This contributions contains elements of formalization of projective geometry. In the plane: Two axiom systems are shown equivalent. We prove some results about the decidability of the the incidence and equality predicates. The classic notion of duality between points and lines is formalized thanks to a functor. The notion of 'flat' is defined and flats are characterized. Fano's plane, the smallest projective plane is defined. We show that Fano's plane is desarguesian. In the space: We prove Desargues' theorem.

opam install coq-projective-geometry.8.5.0
homepage
https://github.com/coq-contribs/projective-geometry
license
Proprietary
bugs tracker
https://github.com/coq-contribs/projective-geometry/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/propcalc/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-projective-geometry/coq-projective-geometry.8.5.0