Email Gateway (Aug 18 2022 at 20:29): Email Gateway (Aug 18 2022 at 20:29):From: Makarius <makarius@sketis.net>
Note that concerning the prover backend, both \<II> \<RR> are allowed
within identifiers; the prover gets these ASCII sequences only. You don't
see the corresponding unicode glyph in Isabelle/jEdit, though. (The
traditional dropout is \<lambda>, which is still not possible in
identifiers as \<lambda>' etc.)
The problem of \<II> and \<RR> is an overlap with the Unicode rendering of
\<Re> and \<Im>. Unlike TeX, the second copy of fraktur I and R is
missing from the Unicode 6.1 standard, cf.
http://unicode.org/charts/PDF/U1D400.pdf
"Fraktur symbols
This style is sometimes known as black-letter. Black-letter symbols
already encoded in the Letterlike Symbols block are omitted here to
avoid duplicate encoding."
Donald Knuth and the AMS knew better, and provided separate copies, with
slightly different shape.
Our IsabelleText font happens to have I and R glyphs in the Fraktur slot
unofficially, but I did not use them in the default mapping of
Isabelle2012/etc/symbols. Instead of stretching unicode too far, I am
considering to remove the default rendering for \<Re> and \<Im> instead,
to make the fraktur alphabet more uniform.
(And yes, Unicode is notorious to require long explanations and
considerations for seemingly trivial things.)
Makarius
Email Gateway (Aug 18 2022 at 20:29):From: Makarius <makarius@sketis.net>
There is indeed a big difference of sledgehammer in Isabelle2011-1 vs.
Isabelle2012. The current release might still have some drop-outs,
though. If you spot anything specific, keep telling us (either the
mailing list, or Jasmin Blanchette, or me).
In particular, I suspect that E prover 1.4/1.5 still has too much shell
scripting built-in to work smoothly on Cygwin. It might also help to
point out such observations to Stephan Schulz from eprover.org, to
motivate him to improve it further.
Makarius
Email Gateway (Aug 19 2022 at 08:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I don't like making this mailing list my personal playground, and after
this email, I'll make a belated New Year's resolution to make a
concerted effort to use this list for what it's best used for, showing
experts a piece a code with a problem, which the experts are good at
analyzing fast and can reply to fast.
If I had a blog, which I do, I could turn this email into a preliminary
product review for Isabelle, which I won't at this time. If there's any
value in this, it could be that a potential user out there has some of
the same questions I had.
You can also consider me an early representative of the new wave of
users who will come here and either complain about the product and
disrespect the product, because they don't know what they're looking at,
or tell you how awesome it is, because they've figured out what they're
looking at.
[I interrupt this email for an important message. I don't know if I
would have been excited enough to write this email if I wouldn't have
gotten a structured proof out of sledgehammer on my first try. My
current run of sledgehammer failed on the structured proof. I'll try to
set the timeout longer. However, I did get a couple of lines that say
something like "Found proof (284 ms)", but I don't know which ATP proved
it. Anyway, I got a screenshot of the first results. Getting any proof
could be considered exciting, but the structured proof gives more visual
excitement.]
Not trying anymore to make this into a polished review, I throw out some
ideas.
I dropped Isabelle for about 6 months, up until about May 2012, but in a
period of about 4 to 5 months, I satisfied at least 5 "proof of concept"
questions I had, where there was and always will be the ongoing question
of how powerful Isabelle's logic engine is.
(1) Can proofs in Isabelle be made to look and flow like traditional
mathematical proofs?
I answered that fairly quickly after working through
http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf. Many
people don't take the time and make the choices to make their proofs
look great, but formatting a document to look good takes time.
(2) Can I become an advanced user of Isabelle with minimal help?
It took me a while to get confidence about that, because I knew I would
have a need to understand some of the distribution source, and the style
of proofs in the distribution source is all over the place; the theories
have been, after all, produced over many years. After reading Makarius's
twenty ways to prove (A /\ B) --> (B /\ A) in his PhD thesis, along with
all the documentation that I've collected, I got the confidence that I'm
not going to hit a brick learning wall I can't get over.
(3) Can the syntax of Isabelle be made to look very, very mathematical?
I already knew about the available math symbols, and the structured
proofs, which was part of the initial attraction. I showed in a recent
email that Isar identifiers can be made to look mathematical. Let no man
or woman say that single, subscripted Latin, Greek, mathcal, or mathfrak
alphabet characters do not meet the requirements of looking mathematical.
For those who don't know, an Isar identifier can use 0-9, ', and _,
though it can't start with those characters. In addition, it can use
a-z, A-Z, \<a> - \<z>, \<A> - \<Z>, \<aa> - \<zz>, \<AA> - \<ZZ> (but
not II and RR) , and the lower and upper case Greek alphabet, such as
\<alpha>. You can use \<^isub> and \<^isup> followed by the
aforementioned characters anywhere you want, and as many times as you
want. That's some major naming options, compared to most programming
languages.
(4) Can I get axiomatic ZF sets in HOL?
This whole thing of axiomatic sets in Isabelle is a big subject. I make
sure here that I don't go off telling you all my thoughts and opinions
on this subject. I only say that there are many practical reasons why I
choose Isabelle/HOL over Isabelle/ZF, and I have a sufficient interest
in sets to want to try my hand at reinventing the wheel.
Also, what has evolved is my understanding of the concept of
meta-languages and object languages. I leave it at that. Sort of. I'll
actually be working through Jech and Hrbacek's "Introduction to Set
Theory, 3rd", which is one of the standard texts on axiomatic sets. My
intent is to try to imitate their development of sets. Got to have goals
in life, even if the goals don't always work out.
(5) Does Isabelle allow me to choose between proving a proof step
automatically and explicitly specifying how to prove the step?
Yes. For this, I'm already starting to forget that this was a "big
question issue". I assure you, if Isabelle only had the ability to
provide "mysterious proof results" by auto, I wouldn't be trying to
learn it. On the other hand, if I knew I was never ever going to have
the option to not prove every little detail, then I would be buckling
down for some major brainwave pain in the future.
A TALE TO TELL
The above questions were some of my questions. It's not that they've set
things in stone, but up to this point, the answers to my big questions
have been positive.
Last year, I started looking at HOL.thy very early in the game to try
and figure out if "I can learn this". From November to May, I did
nothing and was simply waiting on the next release. Recently, when I got
to "type_synonym" on page 12, the light bulb came on for a way to try
and set up sets. I put down a little bit of code just to try my hand at
using some of the keywords.
I layed down some type commands, a few axioms, defined the first theorem
to be proved (that the empty set is unique), and tried my hand at using
"apply(auto)", which requires, of course, knowing how to type on the
keyboard.
It was a no go, which was okay because I wasn't trying to be in "serious
prover mode". A few days passed, and it occurred to me, "How about that
axiom of extension, bro? Defining set equality would be a good thing,
don't you think?"
So I put in the axiom of extension and tried auto again. No go. But,
hey, doing the easy stuff can count for a lot, because last year I put
quite a bit of effort into looking at sledgehammer's options. The idea
is, if sledgehammer gives you the option to try something, then make it
try it. It turns out that I end up using fairly simple options for
sledgehammer.
Last year, I had viper installed, but I only have the default setup now,
so I give it these options:
sledgehammer_params [provers = "e cvc3 spass z3 z3_tptp metis",
verbose=true, isar_proof=true]
What you should know is that with Isabelle2011-1, sledgehammer running
under Cygwin was useless. It wouldn't ever come back, or it would
timeout. I knew sledgehammer worked because I tried it out under Linux.
I tried sledgehammer, not expecting any results. I got results. In
particular, the structured proof stood out because it's not a one-line
statement telling you, "Found proof".
Having a healthy amount of paranoia, and preferring to think like a
lawyer, I wouldn't consider an auto proof meaningful without trying to
figure out any details it gives me, checking my code setup, and, in
general, trying to decide whether I gave sledgehammer meaningful
information.
However, I took out the axiom of extension, and sledgehammer found no
solution. I put it back in, and sledghammer finds a solution.
Conclusive? No. But not bad news either. The easy part is done, I
assume. Using the axiom of separation and the power set? I don't know
about that. Oh yea, and replacing the auto proof with a non-auto proof.
Okay. I completed this to partly get this type of thing out of my
system. I could have waited months, or a year, and said, "Hey, this
Jech's set theory thing worked out." It may not work out. It's no big
deal if it doesn't, since there would probably be a good reason why it
didn't work out.
It's also to say, "Hey, I like that magic". And to say, "Dude, how do
you do that? But please, don't even try to tell me."
Two screen shots are attached. One shows the structured proof that it
found that it doesn't find anymore. I assume it's because CPU resources
got sucked up by Windows for something else. I'll try setting the
options later.
Regards,
GB
120712_structured_proof_found.png
120712_axiom_setup.png
Last updated: Nov 21 2024 at 12:39 UTC