*To*: Julien Narboux <jnarboux at narboux.fr>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 29 Apr 2012 16:18:05 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com> (message from Julien Narboux on Sun, 29 Apr 2012 14:15:00 +0200)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com>

they have built a large Coq library about high school geometry. [...] But this [ Coq declarative proof] language is not used much by the Coq community so you may encounter bugs. Julien, I think that you and your coauthors in http://hal.inria.fr/docs/00/58/49/18/PDF/iccsaConf.pdf are using Coq to figure out how to teach the course, and not asking the students to write Coq code proofs. This sentence in your paper concerns me: The work closest to ours is the one by P. Scott and J. Fleuriot [17]. http://www.springerlink.com/content/b715100716u1t347/?MUD=MP I know I just got here, and I'm not trying to fight with anyone, but I think this paper shows I have some value to the group already. Scott and Fleuriot took on a challenging and interesting HOL Light project, to fill in the gaps of Hilbert's book FoG. That will show the power of HOL Light and their programming skill. But their paper doesn't seem helpful in teaching a rigorous Hilbert geometry course. Reading Greenberg's & Hartshorne's books (or my paper http://www.math.northwestern.edu/~richter/hilbert.pdf) would much more helpful. The authors don't seem to understand the gaps in Euclid's work which were fixed by Hilbert's axioms. Euclid messed up every single result that involved angle addition, including the triangle sum theorem (sum 3 angles = 180). That's a result kids taking a Hilbert geometry course need to know! The authors study instead possible deficiencies of Hilbert's book FoG, and there may be plenty, but you can't teach a geometry course out of FoG, as there isn't enough interesting material. Euclid's errors are much more interesting, as Euclid was often used as a textbook (for centuries?). Scott and Fleuriot say something misleading in their intro: Indeed, it is sufficient to note that Hilbert followed Euclid in one pervasive omission: they both give proofs on an ambient plane when the axioms characterise solid geometry [8]. First, they're citing Heath (a valuable Euclid resource), who mentions Hilbert quite often but shows absolutely no understanding of how Hilbert's work fixes Euclid's pervasive angle-addition errors. Second, is there even an error, as Scott and Fleuriot quote Heath as saying? I don't see any plane/solid-geometry error in Hilbert's axioms listed http://en.wikipedia.org/wiki/Hilbert%27s_axioms In my paper I explain (following Moise's rigorous book) how to handle this solid geometry biz. Basically, for all the 2-dim stuff you have to say "in a plane" and in the 3-dim part you then use the planar stuff plus extra incidence axioms. Euclid's book XI is a fantastic treatment of solid geometry, which Moise simplifies. -- Best, Bill

**References**:**[isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list