Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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.