Re: [isabelle] Proof by analogy and proof stability in Isabelle

Dear Professir Nipkov
Dear Isabelle Users

Thank you for the intensive discussion of the suggestions. Here I want to clarify some issues.

1.Proof stability

1.1  Feasibility
Yes, of course,  the “proof certificate” should include the proof s of required lemmas 
only once, as described by Pater Lammich. Writing “the proofs of intermediate lemmas will also be unpacked”,  I mean that proof certificate should include such a proofs, not just refer to Isabelle library.  What I want, it should be independent from the library,  and every line should be a simple corollary from previous lines (in other words, previous lemmas), and thus the proof can be checked by verifier which is 1) simple 2) independent from version of Isabelle, ideally independent from Isabelle itself.

1.2  Readability
>> And you would have lost the readable version.
Clearly, I am not proposing to delete all usual readable proofs in Isabelle after implementing “proof certificates”, so the readable non-stable version will not be lost. But may be in the future we will have so many theorems in Isabelle, that it will be just impossible to fix all the broken proof scripts. In this case we would at least have proof certificates which guarantee correctness. Moreover, may be it will be possible to create a readable tactic-based proof back from proof certificate. But for now, I would like to have usual readable proof in Isabelle, and in parallel I want to have a possibility to get a stable universal proof certificate for any theorem I have proved.

1.3. Stability
>>  And if one day the format for primitive proofs changes...
First, in this case I will have proof certificate and verifier for the old format, which is already a good guaranty for correctness. Second, there is a hope that fully automatic importer from the old format to a new one will be developed (in contrast, I do not believe that fully automated corrector for fixing broken proof scripts with methods like auto will ever be developed). Third, I see no reasons to change (at least often change)  the primitive Isabelle-independent logic-based format.

1.4 Usability
But the main concern is – do we actually need such “proof certificates”.
>> It is like packaging every library your program needs with that program (in binary) and freezing the program at that point. It may have its uses, but it is not recommended as a general
program development  method.
Proof certificates will not be used as some “general development method”. I would imagine some “export” button which would allow me to get it for any of my theorems, check (with simple Isabelle-independent verifier), and save on disk. Now:
1.4.1. I have “proof” of my result which is valid “ones and forever”.
1.4.2. I can convince other mathematicians, which do not know Isabelle. Imagine that Flyspeck project is finished – what we will have? Extremely long proof, which is impossible to understand and check for human, which uses tactics like “auto”, and some complicated provers like Isabelle claim that it is correct. Is this absolutely convincing? In contrast, imagine the “proof certificate” which is even much longer, but every line is a direct corollary from the previous ones, and there exist a very simple verifier for it. For me, now it is absolutely convincing. 
1.4.3. It can be huge amount of other applications in proof analysis, proof simplification, importing proofs from one provers to another ones, etc.

1.5. Is it realistic for realization?
I hope so. As I understand, many similar work was done for other provers, in Isabelle there are “proof  terms” which is an important step. Finally,  I just have a feeling that such “unpacking” should not be too hard for realization. Am I wrong?

2.Proof by analogy

2.1. Affine dimension vs dimension
>> Since this was not just a general hypothetical question, but a very concrete one, and since Bogdan is in contact with the author of the (ported) library, I was suggesting that they might generalize that part of the library.
This was a very concrete example, when the suggested new proof method would be extremely useful. In this particular case, if we would want to rewrite the existing library, would be better not to use locale to generalize both theories, but just replace existing “dimension” by affine one, which is just more general and correct definition. But I have already succeed  to derive main results about affine dimension using existing results without too much repetition, so this is not necessary anymore. On the other hand, it was not easy, and any alternative variant (for example, with locale) also would  be not easy. The suggested method would solve the problem in one line.  

2.2. Proof by analogy vs locale (is it always relevant?) 
In general, there are huge amount of proofs “by analogy” in any book. Sometimes this means that we indeed deal with two special cases of some general concept, and in this case using locales is relevant. But sometimes there is no abstract concept in mathematics such that generalizes two cases, and introducing it is somewhat artificial. Also, very often we just consider two similar cases like “a>b” and “a<b” (see “Without loss of generality”, John Harrison). Moreover, sometimes we intentionally consider some special case because its proof  is easier to understand, and then generalize it “by analogy”. The point is that using locales is not always appropriate and corresponds to mathematical intuition.   

2.3. Proof by analogy vs locale (is it always possible?)
But even if it is relevant, the user usually cannot change Isabelle library,  and does not want to do this, he (she) wants just use it to derive some lemma, spending not too much time and efforts. If user spend a month to formalize something big and interesting, this is ok, but if a mathematician spend a month do derive an intuitively easy result, may be he (she) will not want to use Isabelle anymore. In many cases the result is “intuitively easy” namely because it is analogous to one which is already proved. The suggested method  allow us to derive such results in one line. 

2.4. Proof by analogy – what if it is not completely analogous
If we have a feeling  that proof is 90% similar, but not exactly the same, but do not know exactly where is the difference, it is hard to use locale. “Analogy” method should tell us what exactly the problem is, we should be able to prove this part “by hand” and then finish the proof by analogy.

2.5. Proof by analogy – what if it does not work at all.
Imagine that we had an impression that the result is completely analogous, but it is not. Imagine that we tried to use locale, spend a week to rewrite everything, and then at the very last stage discover that it does not work. Having “analogy” method,  we would try to use it, and in one minute would see that it does not work and why.      

2.6. Again, is it realistic for realization?
In my original letter, I describe an algorithm for realization. Also,  the realization may be similar to "theory morphism". This gives a hope that it may be realistic.

Bogdan Grechuk.

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