Commit d00d3e3e authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry IsaGeoCoq

parent f2bc278d8c6e
chapter AFP
session IsaGeoCoq (AFP) = HOL +
options [timeout = 300]
theories
Tarski_Neutral
document_files
"root.bib"
"root.tex"
This diff is collapsed.
%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/
%% Created for Larry Paulson at 2021-02-01 11:31:03 +0000
%% Saved with string encoding Unicode (UTF-8)
@article{Poincare_Disc-AFP,
author = {Danijela Simi{\'c} and Filip Mari{\'c} and Pierre Boutry},
date-added = {2021-02-01 11:30:15 +0000},
date-modified = {2021-02-01 11:30:15 +0000},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = dec,
note = {\url{https://isa-afp.org/entries/Poincare_Disc.html}, Formal proof development},
title = {Poincar{\'e} Disc Model},
year = 2019}
@article{Tarskis_Geometry-AFP,
author = {T. J. M. Makarios},
date-added = {2021-02-01 11:28:01 +0000},
date-modified = {2021-02-01 11:28:28 +0000},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = oct,
note = {\url{https://isa-afp.org/entries/Tarskis_Geometry.html}, Formal proof development},
title = {The Independence of {Tarski's Euclidean} Axiom},
year = 2012}
@book{tarski,
address = {Berlin},
author = {Wolfram Schwabh{\"a}user and Wanda Szmielew and Alfred Tarski},
publisher = {Springer-Verlag},
title = {{Metamathematische Methoden in der Geometrie}},
year = {1983}}
@mastersthesis{makarios,
author = {Makarios, Timothy James McKenzie},
note = {Master Thesis},
school = {Victoria University of Wellington},
title = {{A Mechanical Verification of the Independence of Tarski's Euclidean Axiom}},
year = {2012}}
@misc{beeson:hal-01912024,
author = {Beeson, Michael and Boutry, Pierre and Braun, Gabriel and Gries, Charly and Narboux, Julien},
hal_id = {hal-01912024},
hal_version = {v1},
keywords = {coordinates ; Triangle centers ; parallel postulates ; Euclidean geometry ; Formal proofs ; Coq Proof Assistant ; Foundations of geometry ; arithmetization ; Thales theorem ; pythagoras theorem ; neutral geometry ; Tarski's geometry ; Hilbert's geometry},
month = Jun,
title = {{GeoCoq}},
url = {https://hal.inria.fr/hal-01912024},
year = {2018},
Bdsk-Url-1 = {https://hal.inria.fr/hal-01912024}}
@article{wiedijk2012synthesis,
author = {Wiedijk, Freek},
journal = {Logical Methods in Computer Science},
publisher = {Episciences. org},
title = {A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving},
volume = {8},
year = {2012}}
@article{boutry:hal-01178236,
author = {Boutry, Pierre and Gries, Charly and Narboux, Julien and Schreck, Pascal},
doi = {10.1007/s10817-017-9422-8},
hal_id = {hal-01178236},
hal_version = {v2},
journal = {{Journal of Automated Reasoning}},
keywords = {Archimedes' axiom ; axiom ; Aristotle's ; Coq ; neutral geometry ; formalization ; decidability of intersection ; classification ; foundations of geometry ; Euclid ; parallel postulate ; Saccheri-Legendre theorem ; sum of angles},
note = {online first},
pages = {68},
pdf = {https://hal.inria.fr/hal-01178236/file/parallel_postulates_revised.pdf},
publisher = {{Springer Verlag}},
title = {{Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq}},
url = {https://hal.inria.fr/hal-01178236},
year = {2017},
Bdsk-Url-1 = {https://hal.inria.fr/hal-01178236},
Bdsk-Url-2 = {https://doi.org/10.1007/s10817-017-9422-8}}
@inproceedings{gries:hal-01228612,
address = {Saint Malo, France},
author = {Gries, Charly and Boutry, Pierre and Narboux, Julien},
booktitle = {{Les vingt-septi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2016)}},
hal_id = {hal-01228612},
hal_version = {v2},
keywords = {Euclid ; formalization ; Coq ; parallel postulate ; geometry ; formalisation},
month = Jan,
organization = {{Jade Algave and Julien Signoles}},
pages = {15},
pdf = {https://hal.inria.fr/hal-01228612/file/jfla2016-gries-boutry-narboux.pdf},
series = {Actes des Vingt-septi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2016)},
title = {{Somme des angles d'un triangle et unicit{\'e} de la parall{\`e}le : une preuve d'{\'e}quivalence formalis{\'e}e en Coq}},
url = {https://hal.inria.fr/hal-01228612},
year = {2016},
Bdsk-Url-1 = {https://hal.inria.fr/hal-01228612}}
@inproceedings{narboux:inria-00118812,
address = {Pontevedra, Spain},
author = {Narboux, Julien},
booktitle = {{Automated Deduction in Geometry 2006}},
doi = {10.1007/978-3-540-77356-6},
editor = {Eugenio Roanes Lozano, Francisco Botana},
hal_id = {inria-00118812},
hal_version = {v1},
keywords = {Tarski's axioms ; Coq ; Formal Proof ; geometry},
month = Aug,
organization = {{Francisco Botana}},
pages = {139-156},
pdf = {https://hal.inria.fr/inria-00118812/file/adg06-narboux.pdf},
publisher = {{Springer}},
series = {LNCS},
title = {{Mechanical Theorem Proving in Tarski's geometry.}},
url = {https://hal.inria.fr/inria-00118812},
volume = {4869},
year = {2006},
Bdsk-Url-1 = {https://hal.inria.fr/inria-00118812},
Bdsk-Url-2 = {https://doi.org/10.1007/978-3-540-77356-6}}
@article{boutry:hal-01483457,
author = {Boutry, Pierre and Braun, Gabriel and Narboux, Julien},
doi = {10.1016/j.jsc.2018.04.007},
hal_id = {hal-01483457},
hal_version = {v1},
journal = {{Journal of Symbolic Computation}},
keywords = {Pythagoras' theorem ; intercept theorem ; arithmetization ; Coq ; geometry ; Formalization ; area method},
pages = {149-168},
pdf = {https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf},
publisher = {{Elsevier}},
series = {Special Issue on Symbolic Computation in Software Science},
title = {{Formalization of the Arithmetization of Euclidean Plane Geometry and Applications}},
url = {https://hal.inria.fr/hal-01483457},
volume = {90},
year = {2019},
Bdsk-Url-1 = {https://hal.inria.fr/hal-01483457},
Bdsk-Url-2 = {https://doi.org/10.1016/j.jsc.2018.04.007}}
@incollection{narboux:hal-01779452,
author = {Narboux, Julien and Janicic, Predrag and Fleuriot, Jacques},
booktitle = {{Handbook of Geometric Constraint Systems Principles}},
editor = {Meera Sitharam and Audrey St. John and Jessica Sidman},
hal_id = {hal-01779452},
hal_version = {v1},
publisher = {{Chapman and Hall/CRC }},
series = {Discrete Mathematics and Its Applications},
title = {{Computer-assisted Theorem Proving in Synthetic Geometry}},
url = {https://hal.inria.fr/hal-01779452},
year = {2018},
Bdsk-Url-1 = {https://hal.inria.fr/hal-01779452}}
@article{dhurdjevic2015automated,
author = {{\DH}ur{\dj}evi{\'c}, Sana Stojanovi{\'c} and Narboux, Julien and Jani{\v{c}}i{\'c}, Predrag},
journal = {Annals of Mathematics and Artificial Intelligence},
number = {3-4},
pages = {249--269},
publisher = {Springer},
title = {Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry},
volume = {74},
year = {2015}}
@inproceedings{beeson2014otter,
author = {Beeson, Michael and Wos, Larry},
booktitle = {International Joint Conference on Automated Reasoning},
organization = {Springer},
pages = {495--510},
title = {OTTER proofs in Tarskian geometry},
year = {2014}}
@inproceedings{DBLP:conf/csedu/DoreB18a,
author = {Maximilian Dor{\'{e}} and Krysia Broda},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/csedu/DoreB18a.bib},
booktitle = {Computer Supported Education - 10th International Conference, {CSEDU} 2018, Funchal, Madeira, Portugal, March 15-17, 2018, Revised Selected Papers},
doi = {10.1007/978-3-030-21151-6\_26},
editor = {Bruce M. McLaren and Rob Reilly and Susan Zvacek and James Uhomoibhi},
pages = {549--571},
publisher = {Springer},
series = {Communications in Computer and Information Science},
timestamp = {Tue, 25 Jun 2019 19:08:13 +0200},
title = {Intuitive Reasoning in Formalized Mathematics with Elfe},
url = {https://doi.org/10.1007/978-3-030-21151-6\_26},
volume = {1022},
year = {2018},
Bdsk-Url-1 = {https://doi.org/10.1007/978-3-030-21151-6%5C_26}}
@article{DBLP:journals/fm/CoghettoG19,
author = {Roland Coghetto and Adam Grabowski},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/fm/CoghettoG19.bib},
doi = {10.2478/forma-2019-0008},
journal = {Formalized Mathematics},
number = {1},
pages = {75--85},
timestamp = {Mon, 17 Jun 2019 17:02:00 +0200},
title = {Tarski Geometry Axioms. Part {IV} - Right Angle},
url = {https://doi.org/10.2478/forma-2019-0008},
volume = {27},
year = {2019},
Bdsk-Url-1 = {https://doi.org/10.2478/forma-2019-0008}}
@article{DBLP:journals/fm/CoghettoG17,
author = {Roland Coghetto and Adam Grabowski},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/fm/CoghettoG17.bib},
doi = {10.1515/forma-2017-0028},
journal = {Formalized Mathematics},
number = {4},
pages = {289--313},
timestamp = {Sat, 19 Oct 2019 19:33:25 +0200},
title = {Tarski Geometry Axioms. Part {III}},
url = {https://doi.org/10.1515/forma-2017-0028},
volume = {25},
year = {2017},
Bdsk-Url-1 = {https://doi.org/10.1515/forma-2017-0028}}
@article{DBLP:journals/fm/CoghettoG16,
author = {Roland Coghetto and Adam Grabowski},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/fm/CoghettoG16.bib},
doi = {10.1515/forma-2016-0012},
journal = {Formalized Mathematics},
number = {2},
pages = {157--166},
timestamp = {Sat, 19 Oct 2019 19:33:25 +0200},
title = {Tarski Geometry Axioms - Part {II}},
url = {https://doi.org/10.1515/forma-2016-0012},
volume = {24},
year = {2016},
Bdsk-Url-1 = {https://doi.org/10.1515/forma-2016-0012}}
@article{DBLP:journals/fm/RichterGA14,
author = {William Richter and Adam Grabowski and Jesse Alama},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/fm/RichterGA14.bib},
journal = {Formalized Mathematics},
number = {2},
pages = {167--176},
timestamp = {Thu, 19 Feb 2015 15:03:13 +0100},
title = {Tarski Geometry Axioms},
url = {http://www.degruyter.com/view/j/forma.2014.22.issue-2/forma-2014-0017/forma-2014-0017.xml},
volume = {22},
year = {2014},
Bdsk-Url-1 = {http://www.degruyter.com/view/j/forma.2014.22.issue-2/forma-2014-0017/forma-2014-0017.xml}}
@article{sutcliffe1998tptp,
author = {Sutcliffe, Geoff and Suttner, Christian},
journal = {Journal of Automated Reasoning},
number = {2},
pages = {177--203},
publisher = {Springer},
title = {The TPTP problem library},
volume = {21},
year = {1998}}
@book{martin2012foundations,
author = {Martin, George Edward},
publisher = {Springer Science \& Business Media},
title = {The foundations of geometry and the non-Euclidean plane},
year = {2012}}
@inproceedings{nipkow2002structured,
author = {Nipkow, Tobias},
booktitle = {International Workshop on Types for Proofs and Programs},
organization = {Springer},
pages = {259--278},
title = {Structured proofs in Isar/HOL},
year = {2002}}
@article{PoincareDisc,
author = {Simic, Danijela and Maric, Filip and Boutry, Pierre},
doi = {10.1007/s10817-020-09551-2},
journal = {J. Autom. Reasoning},
number = {4},
title = {Formalization of the Poincar{\'e} Disc Model of Hyperbolic Geometry},
url = {https://doi.org/10.1007/s10817-020-09551-2},
volume = {64},
year = {2020},
Bdsk-Url-1 = {https://doi.org/10.1007/s10817-020-09551-2}}
@inproceedings{stojanovic2010coherent,
author = {Stojanovi{\'c}, Sana and Pavlovi{\'c}, Vesna and Jani{\v{c}}i{\'c}, Predrag},
booktitle = {International Workshop on Automated Deduction in Geometry},
organization = {Springer},
pages = {201--220},
title = {A coherent logic based geometry theorem prover capable of producing formal and readable proofs},
year = {2010}}
@article{beeson2017finding,
author = {Beeson, Michael and Wos, Larry},
journal = {Journal of Automated Reasoning},
number = {1},
pages = {181--207},
publisher = {Springer},
title = {Finding proofs in Tarskian geometry},
volume = {58},
year = {2017}}
@article{beeson2019proof,
author = {Beeson, Michael and Narboux, Julien and Wiedijk, Freek},
journal = {Annals of Mathematics and Artificial Intelligence},
number = {2},
pages = {213--257},
publisher = {Springer},
title = {Proof-checking Euclid},
volume = {85},
year = {2019}}
@article{narboux2018computer,
author = {Narboux, Julien and Janicic, Predrag and Fleuriot, Jacques},
journal = {Handbook of Geometric Constraint Systems Principles},
pages = {25--73},
publisher = {Chapman and Hall/CRC},
title = {Computer-assisted theorem proving in synthetic geometry},
year = {2018}}
@phdthesis{boutry2018formalization,
author = {Boutry, Pierre},
school = {Universit{\'e} de Strasbourg},
title = {On the formalization of foundations of geometry},
year = {2018}}
\documentclass[8pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=2cm]{geometry}
\usepackage{isabelle,isabellesym}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\usepackage{amsmath}
\begin{document}
\title{IsaGeoCoq: Partial porting of GeoCoq 2.4.0. Case studies:
Tarski's postulate of parallels implies the 5th postulate of Euclid,
the postulate of Playfair and
the original postulate of Euclid.}
\author{Roland Coghetto}
\maketitle
\begin{abstract}
The GeoCoq library contains a formalization of geometry using
the Coq proof assistant.
It contains both proofs about the foundations of geometry
\cite{tarski,narboux:inria-00118812,boutry:hal-01483457,narboux:hal-01779452}
and high-level proofs in the same style as in high-school.
\cite{beeson:hal-01912024}(Code Repository https://github.com/GeoCoq/GeoCoq).
Some theorems also inspired by \cite{tarski} are also formalized with others ITP(Metamath, Mizar) or ATP
\cite{sutcliffe1998tptp,dhurdjevic2015automated,beeson2014otter,
stojanovic2010coherent,beeson2017finding,beeson2019proof,
narboux2018computer,boutry2018formalization,
{DBLP:conf/csedu/DoreB18a},
{DBLP:journals/fm/RichterGA14},{DBLP:journals/fm/CoghettoG16},
{DBLP:journals/fm/CoghettoG17},{DBLP:journals/fm/CoghettoG19}}.
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
\cite{wiedijk2012synthesis}, the transcript
is done in declarative language Isar\cite{nipkow2002structured}.
The synthetic approach of the demonstrations are directly inspired by
those contained in GeoCoq.
Some demonstrations are credited to G.E Martin(<<lemma bet$\_$le$\_$lt:>> in Ch11$\_$angles.thy, proved by Martin as Theorem 18.17 in
\cite{martin2012foundations}) or
Gupta H.N (Krippen Lemma, proved by Gupta in its PhD in 1965 as Theorem 3.45).
(See \cite{gries:hal-01228612}).
In this work, the proofs are not contructive.
The sledeghammer tool being used to find some demonstrations.
The names of the lemmas and theorems used are kept as far as possible
as well as the definitions.
A different translation has been proposed when the name was already used in
Isabel/Hol ("Len" is translated as "TarskiLen") or that characters were not
allowed in Isabel/Hol ("anga'" in Ch13$\_$angles.v is translated as "angaP").
For some definitions the highlighting of a variable has changed the order or
the position of the variables (Midpoint, Out, Inter,...).
All the lemmas are valid in absolute/neutral space defined with Tarski's axioms.
It should be noted that T.J.M. Makarios \cite{Tarskis_Geometry-AFP} has
begun some demonstrations of certain proposals
mainly those corresponding to SST chapters 2 and 3.
It uses a definition that does not quite coincide with the definition
used in Geocoq and here. As an example, Makarios introduces
the axiom A11 (Axiom of continuity) in the definition of the locale
"Tarski$\_$absolute$\_$space".
Furthermore, the definition of the locale "TarskiAbsolute" \cite{PoincareDisc,Poincare_Disc-AFP} is not
not identical to the one defined in the "Tarski$\_$neutral$\_$dimensionless"
class of GeoCoq.
Indeed this one does not contain the axiom "upper$\_$dimension". In some cases
particular, it is nevertheless to use the axiom "upper$\_$dimension".
The addition of the word "$\_$2D" in the file indicates its presence.
In the last part, it is formalized that, in the neutral/absolute space, the axiom of the parallels of the system of Tarski
implies the Playfair axiom, the 5th postulate of euclide and the postulate
original from Euclid.
These proofs, which are not constructive, are directly inspired by
\cite{gries:hal-01228612,boutry:hal-01178236}.
\end{abstract}
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
\clearpage
% generated text of all theories
\input{session}
% optional bibliography
\clearpage
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
......@@ -252,6 +252,7 @@ Irrationality_J_Hancl
Isabelle_C
Isabelle_Marries_Dirac
Isabelle_Meta_Model
IsaGeoCoq
Jacobson_Basic_Algebra
Jinja
JinjaDCI
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment