Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Oops, of course I meant "Peirce" (but after three occurrences I can hardly claim this as a typo ;)).

On 05/02/2012 01:45 PM, Christian Sternagel wrote:
Dear Bill,

On 05/02/2012 01:09 PM, Bill Richter wrote:
Thanks, Chris, that's very helpful. I'll look for the red wavy error
lines in jedit. I'll look at /src/HOL/ex/. I've looked at
tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good.
Thanks for explaining simp, blast etc, although I don't really know
what you mean. Is there somewhere an FOL example, with a long
(perhaps indigestible) single step "rule" method proof, which is
shortened with simp, and then shortened even more with blast& auto?
Well, not really indigestible, but consider the following Isabelle/HOL
proof of Pierce's Law:

lemma Pierce1: "((P --> Q) --> P) --> P"
proof (rule impI)
assume 1: "(P --> Q) --> P"
have "(~ P) | P" by (rule excluded_middle)
thus P
proof (rule disjE)
assume "P" thus "P" by assumption
next
assume 2: "~ P"
have "P --> Q"
proof (rule impI)
assume "P"
with 2 show "Q" by (rule notE)
qed
with 1 show "P" by (rule mp)
qed
qed

Which just uses the existing lemmas

impI: (?P ==> ?Q) ==> ?P --> ?Q
excluded_middle: ~ ?P | ?P
disjE: ?P | ?Q ==> (?P ==> ?R) ==> (?Q ==> ?R) ==> ?R
notE: ~ ?P ==> ?P ==> ?R
mp: ?P --> ?Q ==> ?P ==> ?Q

where the question marks indicate that variables can be instantiated
arbitrarily (i.e., they are so called "schematic variables"). In this
proof every step (w.r.t. some given set of rules) is done explicitly. If
we use "blast" (or "auto" for that matter) it reduces to.

lemma Pierce2: "((P --> Q) --> P) --> P" by blast

But note that both proofs are equally rigorous, since blast just applies
existing lemmas that are setup as introduction and elimination rules for
logical symbols (besides others). (The whole idea of proof assistants
like Isabelle, is that internally everything is reducible to the initial
axioms, whether this is done by hand or left to the system is to some
extend the users choice [sometimes the automatic methods are just not
powerful enough to solve a goal and the user has to divide it in smaller
pieces manually].)


(In courses it is often done that students are only allowed to use
certain rules in order to proof a statement, since the automatic
tools would outright solve many typical examples.)

Wow! Can you point me to any of these courses? That sounds like what
I need to know. As I posted earlier, I'm mostly trying to cite some
good code for my geometry paper above (which I'll then submit). I
don't have to write the code myself, although I did
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
Examples of real classroom situations where students hand in Isabelle
proofs would be fantastic! Dunno about Europe, but US public schools
are really gungho about computer applications.
There is the Isabelle Community Wiki

https://isabelle.in.tum.de/community

(which has not yet really come to life). It contains pointers to some
courses that use or are about Isabelle

https://isabelle.in.tum.de/community/Course_Material

This could be interesting for you.

hope this helps

chris







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