[isabelle] 5 proofs of concept satisfied and awesomeness revisited



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




Attachment: 120712_structured_proof_found.png
Description: PNG image

Attachment: 120712_axiom_setup.png
Description: PNG image



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