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



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":

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





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