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



Hi Brian,

Thank you very much for your letter.
I wanted to formulate suggestions which would make Isabelle much more attractive for mathematicians, and at the same time which would be realistic for realization. Your letter confirms my impression that these suggestions are indeed realistic.

 >       This process seems very similar to the idea of "theory morphism" that I learned about from Christoph Lüth a few years ago.... It seems that their tool is not *exactly* what you want, since it translates everything all the way down to the axioms.


Excellent. This "theory morphism" is indeed not what I want, in sense that it is hard (or impossible) to use it to prove my theorem and many similar results. But I have an impression that the realization should be similar, which confirms my hope that my “analogy” method is realistic for realization.

>        There is a potential limitation, though. I suppose your theorem mapping would map many abstract properties about "subspace" to lemmas about "affine". But this would not include the actual *definition* of "subspace". Any lemma about "subspace" or "dim" whose proof used only the abstract properties could be translated automatically, but if its proof mentioned the actual definition of "subspace", the translation wouldn't work.


Exactly! If a lemma uses actual definition of subspace, or any other specific properties of subspaces, which have no analogy for affine sets, it will not be translated automatically, because this would mean that the proof is not actually analogous! My point is that we should be able to prove in one line completely analogous facts. Another crucial point is that, if proof is not completely analogous, the analogous part should be done automatically, and only “interesting” part (often very small) should be left for the user.

>      Yes, it is troubling that Isabelle does not really provide any kind of backward compatibility for proof scripts. As someone who has spent a lot of time fixing broken proof scripts, this is an important concern for me.

Thank you for advice for writing robust proof scripts. But, again, the final goal is to make Isabelle attractive for the whole mathematical community. If thousands of mathematicians start to formalize their results in Isabelle, relatively small Isabelle team will not be able to fix all broken proof scripts. It is necessary to have absolutely stable low-level “proof certificate”, and it should do only very primitive steps, such that the proof can be verified by extremely simple Isabelle-independent checker. Again, I am glad to hear that the first step (Isabelle proof terms) is done already, and now it seems that the "external" representation of them should be the next step.

>       It would probably be straightforward to implement a tool for Isabelle to *import* theorems from OpenTheory files, but *exporting* would be much more difficult, since type classes would have to be translated away somehow.

Again, good news, I would be happy to see at least exporting program, which, together with the existing importing from HOL-Light, would help me to translate, say, convex analysis theory from HOL Light, and see how it looks. Meanwhile, I have found folder “import” among Isabelle src files, containing translated theory HOLLight.thy, which is probably based on the work of Steven Obua and Sebastian Skalberg (2006). But, first, I do not know how to get similar automatic translation for convex analysis theory, and second, HOLLight.thy contains no definitions, and some of lemmas are absolutely non-readable. Probably, it would be better to have a parallel tree of definitions (which would make lemmas simpler), and then prove equivalence of these definitions. May be, import from OpenTheory would help with the first step?

Sincerely,
Bogdan.


28.04.10, 09:45, "Brian Huffman" <brianh at cs.pdx.edu>:

> Hi Bogdan,
>  
>  You make some good points here. I will try to address a few of them.
>  
>  On Tue, Apr 27, 2010 at 10:39 AM, grechukbogdan  wrote:
>  > Next, I want to discuss proof by analogy and proof stability in Isabelle.
>  >
>  > Recently, I needed to prove the following lemma
>  >
>  > lemma 1:
>  > 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”
>  >
>  > lemma 2:
>  > 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.
>  
>  This process seems very similar to the idea of "theory morphism" that
>  I learned about from Christoph Lüth a few years ago. There is a 2006
>  paper about this called "Structured Formal Development in Isabelle":
>  
>  informatik.uni-bremen.de/~cxl/papers/njc06.ps.gz
>  
>  They also implemented a tool that implements theory morphisms for
>  Isabelle. To use it, you specify a mapping for types, a mapping for
>  terms, and a mapping from axioms in the original theory to theorems in
>  the new theory. It will then reconstruct proofs of derived lemmas by
>  transforming the recorded proof objects.
>  
>  It seems that their tool is not *exactly* what you want, since it
>  translates everything all the way down to the axioms. In your case,
>  "dim" is not defined axiomatically, so a mapping from axioms to
>  theorems doesn't help. You would want to give a mapping from
>  *theorems* about "dim" to analogous theorems about "aff_dim". Then any
>  proof about "dim" built up from those basic theorems could be
>  translated to "aff_dim".
>  
>  There is a potential limitation, though. I suppose your theorem
>  mapping would map many abstract properties about "subspace" to lemmas
>  about "affine". But this would not include the actual *definition* of
>  "subspace". Any lemma about "subspace" or "dim" whose proof used only
>  the abstract properties could be translated automatically, but if its
>  proof mentioned the actual definition of "subspace", the translation
>  wouldn't work.
>  
>  > 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.
>  
>  Yes, it is troubling that Isabelle does not really provide any kind of
>  backward compatibility for proof scripts. As someone who has spent a
>  lot of time fixing broken proof scripts, this is an important concern
>  for me.
>  
>  At the very least, it should be safe for you to assume that tactics
>  like auto are "monotonic" with respect to versions, i.e. any subgoal
>  that can be solved in one step by "auto" in Isabelle2008 should also
>  be solved in one step by "auto" in Isabelle2009. Of course, it is also
>  likely (and generally desirable!) that 2009's "auto" will solve some
>  subgoals that 2008's "auto" could not.
>  
>  Robust proof scripts need to keep this "monotonicity" property in
>  mind. Here's an example of a proof script that is NOT robust:
>  
>  apply (rule foo)
>  apply auto
>  apply (rule bar)
>  apply auto
>  apply (rule ...)
>  apply auto
>  ...
>  
>  Proof scripts like this are a nightmare to fix when they go wrong. The
>  problem is that there are applications of "auto" that don't solve
>  subgoals completely, but leave a bunch of leftover subgoals behind.
>  The rest of the proof script relies on the leftover junk being in a
>  very particular shape. If in a later version of Isabelle, auto leaves
>  a slightly smaller pile of leftovers, then the proof will break.
>  
>  So here is my advice for writing robust proof scripts:
>  
>  * One-step proofs like "by auto" should always be OK (You should be
>  able to rely on the developers to ensure "monotonicity" of future
>  versions.)
>  
>  * Tactics that leave other subgoals behind are OK if and only if they
>  have predictable behavior (this includes tactics like "rule",
>  "clarify", "intro", and "safe"; but NOT "auto".)
>  
>  > 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.
>  
>  Isabelle does have a notion of "proof terms" that (when enabled)
>  record all the low-level details of proofs, including all the steps
>  done by a tactic like "auto". Most of the work on this has been done
>  by Stefan Berghofer; you can find some publications about it on his
>  homepage:
>  
>  http://www.in.tum.de/~berghofe/
>  
>  When proof terms are enabled in Isabelle, they are available at
>  runtime as values on the ML heap. Thus they can be saved in heap
>  images, to be used for later sessions of the same version of Isabelle.
>  But as far as I know, there is no other "external" representation of
>  Isabelle proof terms, so I'm not sure how easy it would be to transfer
>  a proof term between different versions of Isabelle.
>  
>  > 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)?
>  
>  One bit of recent work in this area that I know about is the
>  OpenTheory project. Joe Hurd published a paper on this work last year;
>  you can find it at the project website:
>  
>  http://www.gilith.com/research/opentheory/
>  
>  The tools are currently targeting HOL4, ProofPower, and HOL Light.
>  Isabelle/HOL has not been included yet because its logic is actually
>  slightly different from the others: Isabelle supports type classes and
>  overloaded constant definitions, but none of the others do. It would
>  probably be straightforward to implement a tool for Isabelle to
>  *import* theorems from OpenTheory files, but *exporting* would be much
>  more difficult, since type classes would have to be translated away
>  somehow.
>  
>  >
>  > Sincerely,
>  > Bogdan.
>  >
>  >
>  
>  Hope this helps,
>  - Brian
>  
>  

-- 
Яндекс.Почта. Письма есть. Спама - нет. http://mail.yandex.ru/nospam/sign





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