Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and