[isabelle] Proof by analogy and proof stability in Isabelle
Dear Isabelle Users,
I am working on project, which includes providing feedback about Isabelle, including comments and suggestions. Here is my second feedback letter, mostly about proof by analogy and proof stability in Isabelle.
First, I discuss my suggestions from the previous letter.
Suggestion 1. The message like “The current goal could be solved directly with...” should appear not only after I formulate the existing result as a lemma, but also when I formulate it inside the proof, say
Suggestion 2: It should be a possibility to run Sledgehammer in the background automatically, every time when I formulate a lemma or “have” statement .
As pointed out by Prof. Makarius, Sledgehammer and lemma suggestion mechanism temporarily works in the crude asynchronous mode, such that user has to wait for it. In this case I agree that Sledgehammer should not work at the background. But I would say that lemma suggestion mechanism works very fast, and I personally would found it very
helpful, if it works as described in Suggestion 1. In any case, it should be an option in the menu, so that if somebody does not like this, he could turn it off. And, of course, I will be very happy when this temporarily difficulties will be solved and I will be able to run Sledgehammer at the background (Suggestion 2).
Suggestion 4: There should be a simple way to see the definition of any object in Isabelle, even if I do not know in advance if it is a lemma, method, term, abbreviation, notation, or something else.
I was happy ho hear from Prof. Makarius that a universal markup mechanism already works internally, and only the front-ends are still lacking. Hope for more to come here soon.
Next, I want to discuss proof by analogy and proof stability in Isabelle.
Recently, I needed to prove the following lemma
fixes S :: "(real^'n) set"
assumes "aff_dim S = CARD('n)"
shows "affine hull S = (UNIV :: (real^'n) set)"
The definition of affine dimension is similar to the definition of dimension in Isabelle (“dim”), the difference is that “aff_dim” uses affine hull in the definition, while “dim” uses subspace hull. And the corresponding lemma is true for “dim”
fixes S :: "(real^'n) set"
assumes "dim S = CARD('n)"
shows "subspace hull S = (UNIV :: (real^'n) set)"
The proof of lemma 2 is very simple to proof, because a lot of machinery for “dim” is developed in Isabelle library. To prove lemma 1, I could just copy all these results (about 50 lemmas, some of them long!) about dim with proofs to my theory, search and replace dim by aff_dim, subspace by affine, span (which is subspace hull) by affine hull, add
“aff” to every lemma name and again search and replace for lemmas, etc. There is a lot of mechanical work here, and I would get 20 pages of theory which is basically a repetition of the existing one (which is looks very bed for me). So I just found a tricky way to derive lemma 1 from lemma 2 using some special connection between these dimensions, but it took me a long time to do this.
After this, I am thinking about some automatic method for proving by analogy, which would look something like
lemma 1 by analogy[ with lemma 2 replacing dim by aff_dim, subspace by affine, span by affine hull]
Here “analogy” is new automatic method, “with” and “replacing” are attributes of this method. First, the method should check if lemma 2
formally become lemma 1 after such replacing. If no, the error is given. If yes, it just tries to repeat the proof of lemma 2 for lemma 1
with such a replacing. If the proof uses some lemma, it should try to find the corresponding lemma for aff_dim, and if it exists, substitute it, and if it does not, try to prove such a lemma by analogy. The method is either successful, or should give an error like this “can not prove lemma aff_dim S >= 0, which is the analogy for lemma dim S >= 0”. After
this, the user can prove such a “hard” part by hand, and then repeat the attempt. If the analogy is complete (like in my case) the proof will be fully automated (as it should be in this case). If there are some lemmas whose analogy are not trivial, the user will need to prove them separately, I e will need to do only nontrivial, interesting work (again, as it should be).
Such a method would be extremely useful. For example, it would help to perform proofs by symmetry, discussed in the resent Hohn Harrison's paper “without loss of generality” (but it would give us much more – there is no symmetry in my example with dimensions). Also, user could avoid creation of a huge amount of analogous lemmas in copy-paste style. On the other hand, this method looks for me to be relatively straightforward for realization, because there is a clear and simple algorithm for it.
Next, I will discuss proof stability in Isabelle.
I was in USA recently, installed the same version of Isabelle there, and tried to compile my theory. In three places the compilation fails, because “auto” did not perform the job for some reason. I fix this by adding a little bit more explanation, but it may be not so simple next time. As a mathematician, I know that if I prove something, this is
proved forever. For this reason I would prefer to have a proof which is extremely stable, even if non-readable.
What is proof “by auto”? This is a sequence of some logical steps, which should be (I am sure) easy to unpack. Can I, after proving some lemma, get a fully unpacked version of proof, which is non-readable for human,
but will be compiled in any version of Isabelle? Moreover, if the proofs of intermediate lemmas will also be unpacked, this proof would remain correct even if some intermediate lemmas disappear in the new version! If I will spend 5-6 month to prove a major result, I want to have such a proof for it, save it on my computer, and this would be like
a “proof certificate”, extremely stable and valid forever (I know that if I submit the proof to Isabelle archive then somebody will take care, but this do not make me completely happy). Moreover, I need such a low-level proof for some other reasons, connected with proof analysis, and ideas about translation between different theorem provers. So, the question is, can I get somehow such a low-level stable proof of my lemmas? If yes, how? If no, the suggestion is to provide users with such a possibility.
Finally, I have one question. All the work about convex analysis which I am doing in Isabelle is already formalized in HOL-Light, and this is a very sad situation. It is extremely important to develop automatic translators, and I know that everybody understand this. My question is, what is the state of the art in this area? What are the main reasons for
such translators do not exists by now, even between Isabelle and HOL Light which uses the same logic (HOL)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and