[isabelle] New in the AFP: a port of GeoCoq



I’m happy to announce a substantial new contribution to the AFP, by Roland Coghetto:

> Tarski's postulate of parallels implies the 5th postulate of Euclid, the postulate of Playfair and the original postulate of Euclid.
> 
> The GeoCoq library (Main autors: Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux) contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school. Some theorems also inspired by W. Schwabhaüser, W. Szmielew and A. Tarski are also formalized with others ITP (Metamath, Mizar) or ATP. We port a part of the GeoCoq 2.4.0 library within the Isabelle/Hol proof assistant: more precisely, the files Chap02.v to Chap13_3.v, suma.v as well as the associated definitions and some useful files for the demonstration of certain parallel postulates. While the demonstrations in Coq are written in procedural language, the transcript is done in declarative language Isar. The synthetic approach of the demonstrations are directly inspired by those contained in GeoCoq. 


You will find it online at https://www.isa-afp.org/entries/IsaGeoCoq.html

Larry





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.