*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 15:51:14 -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>

I appreciate your work [...] Maybe we could join our efforts. Julien, I'd be thrilled to work with you and Gabriel Braun, especially as you & Makarius are on a committee studying Theorem Proving Components for Educational Software. So you & Makarius are people I want to talk to about teaching geometry, and not only vital programming resources. This is very interesting: I appreciate your work, your proofs seem to be really more readable than Coq proofs. Of course my LCF style proofs are not meant to be readable. In fact, I believe that these proofs about Tarski's axioms are really low level and it is hard to have intuition about the proofs because there are basic facts which are hard to prove (for instance existence of the midpoint arrives only at chapter 7 !) and therefore it is not really the kind of proof one wants to show in high-school, that is why I did not try to produce readable proofs. Surely no one should teach Tarski's axioms in high school, as the proofs are way too hard since his axioms are so weak. But the Tarski proofs are still worth understanding, for the same reason that high school kids (arguably) ought to learn Hilbert's axioms and not use the stronger axioms of Moise & Venema, based on Birkhoff's real line for distances and angles, and taking the plane separation axiom instead of Hilbert's weaker Pasch axiom. Moise proofs are a lot easier than Hilbert proofs. But only using Moise raises the question in the student's mind: am I smart enough to understand the supposedly harder Hilbert axioms? And if I'm not smart enough, maybe I shouldn't even be using the simpler Moise axioms! The only way to reassure the students is to write up nice Hilbert proofs, and I think I succeeded, or at least made a start, in http://www.math.northwestern.edu/~richter/hilbert.pdf The same remarks go for Tarksi, at least for me (the teacher). I know I couldn't figure out the Tarski proofs myself, I needed your Coq code, but am I even smart enough to understand the proofs? I think there is definitely is Tarski geometry intuition, although it's hard to come by. Gupta's amazing proof is definitely based on intuition, and you can see the intuition in the pictures you and the wikiproofs folks draw. Gupta's theorem a ≠ b ∧ Babc ∧ Babd → Bacd ∨ Badc would be easy if we could find two points p & q that are equidistant from a, b & c. We could easily do that if we had Hilbert's angle construction axiom, but we don't. So Gupta (as you explained to me in your Coq code) first finds a rhombus (which turns out to be flat), and then shows the diagonals of the rhombus bisect each other (that's generally true, and in our flat case it follows easily from the Inner Pasch axiom), and then we can do enough angle construction using this bisected rhombus to find the points p & q, which turn out to be on the same line after all. Isn't that an amazing proof? Your email from last week reactivated my interest in these proofs and I worked on the proof of Hilbert's Pasch axiom. Excellent! I noticed that your proof of the full Pasch axiom in your (in progress) http://dpt-info.u-strasbg.fr/~narboux/Tarski/Hilbert.html seems to be still in progress. Also, you didn't quite prove the midpoint theorem, but only Lemma l7_25 : forall A B C, Cong C A C B -> exists X, is_midpoint X A B. Your C should exist, by constructing an isosceles triangle, but I can't even do that. I don't know why my address from hol-info bounced, as I've gotten mail from other hol-info users. Can you check what my bad address was? About your questions about Isabelle, I think you could use the latest use interface based on Jedit. Thanks. Makarius told me this after I posted. I still don't know how to use Isabelle. Makarius stressed that I ought to try Coq. -- Best, Bill

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

- Previous by Date: Re: [isabelle] size_changes raises Option and Bind
- 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