Re: [isabelle] Proof by analogy and proof stability in Isabelle
Proof by analogy: I wondered if locales would have helped to generalize
the dim/aff_dim lemmas, obtaining both by an interpretation?
Brian Huffman schrieb:
> 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 <grechukbogdan at yandex.ru> 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":
> 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
> * 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
> 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:
> 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
> Hope this helps,
> - Brian
This archive was generated by a fusion of
Pipermail (Mailman edition) and