Email Gateway (Aug 18 2022 at 15:01): Email Gateway (Aug 18 2022 at 15:01):From: grechukbogdan <grechukbogdan@yandex.ru>
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.
Sincerely,
Bogdan Grechuk.
Email Gateway (Aug 18 2022 at 15:01):From: "steven@obua.de" <steven@obua.de>
Actually I have been thinking about these kinds of problems for a while. IMHO,
you can choose between two options here:
a) Do it how Isabelle (and the AFP) does it currently: When the Isabelle system
changes, change all proofs and theorems and so on to become up-to-date.
b) Develop a versioning system that not only manages source code (like it is
currently done) but also content (theories, theorems, proofs, and so on). Part
of this versioning system is also a mechanism on how to transfer content from
one version to another (most of the time nothing has to be done here; for
example for a minimal implementation of such a versioning system there is most
of the time no need to transfer proofs, but only theorems). And yes, this means
that at least a part of the versioning system becomes part of the trusted kernel
of the proof assistant.
I think of those two options only option b) scales to hundreds of thousands of
concurrent users. A working versioning system like proposed in b) does not
exclude a): You can still do refactoring, to use newer proof methods for
example. But you don't have to.
By the way, can anyone here provide pointers to previous work that goes in the
direction of b) ?
Email Gateway (Aug 18 2022 at 15:01):From: Lawrence Paulson <lp15@cam.ac.uk>
Proof stability is an interesting topic to discuss, but the tenor of the discussion may give a misleading impression. Proof stability is chiefly an issue for the Isabelle developers. We have over 600,000 lines of proof scripts to maintain, about half in Isabelle/HOL and half in the AFP. Many of these proof scripts are over 10 years old and refer to numerous deprecated features. They can be a nightmare to maintain.
I would be surprised if proof stability was the leading issue with users. I certainly do not recall losing much time in the course of a proof development to patching up failing proofs, even though (unlike most ordinary users surely) I invariably use potentially unstable development snapshots. The simplest way to achieve proof stability, as advocated particularly by some Coq users, is to avoid automation altogether. The problem with that approach is that it takes much longer to prove anything.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:01):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Apr 29, 2010 at 5:46 AM, steven@obua.de <steven@obua.de> wrote:
b) Develop a versioning system that not only manages source code (like it is
currently done) but also content (theories, theorems, proofs, and so on). Part
of this versioning system is also a mechanism on how to transfer content from
one version to another
"Transferring content" is exactly what an external representation of
proof objects would allow you to do. A format like Joe Hurd's
OpenTheory is designed primarily for transferring theorems between
completely different theorem provers, but the same idea could also be
useful for transferring theorems between different versions of the
same theorem prover.
And yes, this means
that at least a part of the versioning system becomes part of the trusted kernel
of the proof assistant.
The great thing about using proof objects is that you don't need to
trust any new code.
Email Gateway (Aug 18 2022 at 15:01):From: Brian Huffman <brianh@cs.pdx.edu>
I would suggest that using incremental development snapshots actually
makes patching up your proofs easier.
On occasion I have had significant amounts of trouble getting old
proof scripts to work again. The process is most difficult with
theories that were developed for older versions of Isabelle: Porting a
proof directly from Isabelle 2005 to 2009 can be much more difficult
than continuously adapting the same proof to a series of development
snapshots. I would suspect that most users have to deal with these
large version-jumps more often than the developers do.
Email Gateway (Aug 18 2022 at 15:01):From: Makarius <makarius@sketis.net>
Jumping over several Isabelle releases at the same time is indeed very
hard. Users can avoid that by following the official release schedule --
the distances between Isabelle2007 -- Isabelle2008 -- Isabelle2009 --
Isabelle2009-1 are not too big.
Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25 months
between the releases and the result being rather unstable. At that time
it was not completely clear if we would ever recover from a continously
"intermediate" state, and join the fate of notorious projects such as
SML/NJ or the STIX fonts.
Anyway, one should distinguish between really large libraries and the
underlying system infrastructure. A library could well be developed in a
Wikipedia style, and people in Nijmegen are working on that, for example.
Makarius
Email Gateway (Aug 18 2022 at 15:01):From: Makarius <makarius@sketis.net>
While Isabelle is a very complex system, internally everything is reduced
to basic principles, and run through an LCF-style inference kernel. The
kernel can also produce explicit proof objects as a backup, although this
degrades performance greatly. Even without proof terms, the type-safety
of Standard ML gives certain static guarantees (in contrast to OCaml, or
other much less rigid languages).
This does not mean that the system only produces ethernally true results
-- there are other influences beyond a certain architecture and properties
of the implementation languages.
Nonetheless, I would characterize our tradition of theorem proving as
"fundamentalist" in the sense that everything is based on proper
definitions and proofs.
Makarius
Email Gateway (Aug 18 2022 at 15:01):From: Makarius <makarius@sketis.net>
Here is a minimal example:
ML "proofs := 2"
lemma a: "A --> A" by auto
prf a
full_prf a
Proof General also privides a menu item for setting "Full Proofs" -- it
switches between "proofs := 0" and "proofs := 2".
If the system complains about "minimal proof object" you refer to lemmas within
a proof that do not carry a full proof object themselves. The download image
for Isabelle/HOL from the official Isabelle2009-1 distribution contains full
proof objects for everything, but the flag is disabled in the very end, in
order not to degrade user performance by default.
A nicer proof of "A --> A" can be produced like this:
lemma b: "A --> A" ..
prf b
full_prf b
This also works for less trivial structered proofs, e.g. see the proofs in
src/HOL/Isar_Examples/Knaster_Tarski.thy -- the proof terms still make sense.
The Isar proof language does not involve any "magic" by itself, but allows to
appeal to arbitrary complex proof tools in clearly isolated positions, e.g. the
"by auto" above.
Makarius
Email Gateway (Aug 18 2022 at 15:01):From: Steven Obua <steven@obua.de>
I think these issues should be transparent for the end user of the
proof assistant. It is maybe a good idea to use proof objects for
implementing the versioning system, but special cases like a change in
the proof object format (and there will be changes, trust me) and so
on must then be handled transparently by the system, otherwise it
becomes a pain for the user. Also proof objects are big and slow; most
users are willing to trade a vastly improved user experience for a
little bit of trust ...
My point is just that earlier snapshots of the theory development of
a theorem prover should be accessible from the current theory
development, no matter how that is implemented exactly. As an example,
take the theory of the real numbers.
A simple way of approaching this is to first introduce the natural
numbers, then rational numbers, then the real numbers. Later on we
introduce new natural numbers, new rational numbers and so on, so that
they are now subsets of each other. Actually, there is no need now any
more for the original natural numbers and so on. With a versioning
system we can throw them out of our newest version. In our newest
version, we can axiomatically introduce the real numbers (and
justifying this by pointing to the definition in an earlier version).
Also, there are several ways of introducing the real numbers. This is
no problem in our system, each way could belong to a different version.
So for the user, stuff that has been done 10 years ago, is still
there, unchanged, and it is accessible from the newest version of the
system. It is important that the versioning system is elegant and
easy to understand. It provides the high-level view of how the user
thinks about the system.
Email Gateway (Aug 18 2022 at 15:02):From: Dave Thayer <dathayer@microsoft.com>
I think an important aspect of this topic is the issue of legal liability.
If you use a theorem prover to prove a theorem, that is used to create a query into a medical ontology,
which is then used in the diagnostic train for determining a patients treatment protocol you better
be able to stand up in court and defend it. I would not want to tell a judge: "at this step we invoke
the magic word 'auto' which does 'something unknown' and then we went on from there'.
David
Jumping over several Isabelle releases at the same time is indeed very
hard. Users can avoid that by following the official release schedule --
the distances between Isabelle2007 -- Isabelle2008 -- Isabelle2009 --
Isabelle2009-1 are not too big.
Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25 months
between the releases and the result being rather unstable. At that time
it was not completely clear if we would ever recover from a continously
"intermediate" state, and join the fate of notorious projects such as
SML/NJ or the STIX fonts.
Anyway, one should distinguish between really large libraries and the
underlying system infrastructure. A library could well be developed in a
Wikipedia style, and people in Nijmegen are working on that, for example.
Makarius
Email Gateway (Aug 18 2022 at 15:02):From: Dave Thayer <dathayer@microsoft.com>
What is the correct invocation to produce such a proof object?
While Isabelle is a very complex system, internally everything is reduced
to basic principles, and run through an LCF-style inference kernel. The
kernel can also produce explicit proof objects as a backup, although this
degrades performance greatly. Even without proof terms, the type-safety
of Standard ML gives certain static guarantees (in contrast to OCaml, or
other much less rigid languages).
This does not mean that the system only produces ethernally true results
-- there are other influences beyond a certain architecture and properties
of the implementation languages.
Nonetheless, I would characterize our tradition of theorem proving as
"fundamentalist" in the sense that everything is based on proper
definitions and proofs.
Makarius
Email Gateway (Aug 18 2022 at 15:10):From: grechukbogdan <grechukbogdan@yandex.ru>
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
after have.
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
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.
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)?
Sincerely,
Bogdan.
Email Gateway (Aug 18 2022 at 15:10):From: Brian Huffman <brianh@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 <grechukbogdan@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,
Email Gateway (Aug 18 2022 at 15:10):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for tackling those questions. You make some good points about stability of proofs, but somehow you've omitted the most important one: structured proofs are inherently much more robust, because if something does fail then you know exactly which part of the proof is affected; you never get leftover subgoals being given to tactics that were intended to perform a separate part of the proof.
Another small point: if you use sledgehammer to generate metis calls, these will be stable, because they explicitly list all the theorems involved. The only modification to Isabelle that could affect a metis call would be a change to metis itself.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:10):From: Alexander Krauss <krauss@in.tum.de>
Lawrence Paulson wrote:
But even metis calls can break when the library changes under your feet. :-/
Alex
Email Gateway (Aug 18 2022 at 15:10):From: Tobias Nipkow <nipkow@in.tum.de>
Proof by analogy: I wondered if locales would have helped to generalize
the dim/aff_dim lemmas, obtaining both by an interpretation?
Tobias
Brian Huffman schrieb:
Email Gateway (Aug 18 2022 at 15:10):From: Brian Huffman <brianh@cs.pdx.edu>
Maybe they could have, but that kind of misses the point: Writing
libraries using locales means that the library writer needs to know in
advance exactly how it might be generalized in the future. The problem
we are trying to solve is when person A writes a library, and person B
wants to re-use the proofs in a more general setting - without
modifying the original library, or cutting-and-pasting the proofs.
I might summarize it this way: Locale interpretation transforms a
generic theory into a concrete one. What we're looking for is a way to
transform a concrete theory into a different concrete one (or a
new generic one, as the case may be).
Email Gateway (Aug 18 2022 at 15:10):From: Tobias Nipkow <nipkow@in.tum.de>
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.
@Bogdan: Out of intererst: how does John Harrison deal with this
duplication in the original library?
Tobias
Brian Huffman schrieb:
Email Gateway (Aug 18 2022 at 15:11):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Auto is deterministic and insensitive to the country it is run in. It is
sensitive to the version of Isabelle and the theories you run your
theories on top of.
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.
Such an approach is feasible only in principle. You could write all the
proof objects out to a file, expanding all proofs of lemmas used.
Isabelle's proof terms even have a concrete syntax for that. This would
give you a stable but gigantic proof. The requirements in terms of time
and space would make it impossible to process these proofs effectively.
And you would have lost the readable version.
Tobias
Email Gateway (Aug 18 2022 at 15:11):From: grechukbogdan <grechukbogdan@yandex.ru>
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@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 ca
[message truncated]
Email Gateway (Aug 18 2022 at 15:11):From: Steven Obua <steven@obua.de>
It seems to me the way mathematics usually works is to take the
concrete, abstract it, and THEN ONLY apply it to something different
concrete.
Email Gateway (Aug 18 2022 at 15:11):From: Tobias Nipkow <nipkow@in.tum.de>
This is the killer, I believe:
"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!"
Otherwise replaying proofs is uncritical.
Tobias
Paul Jackson wrote:
Email Gateway (Aug 18 2022 at 15:11):From: Peter Lammich <peter.lammich@uni-muenster.de>
Tobias Nipkow schrieb:
A possibility would also be to include the concept of lemma that can be
referenced into the
unpacked proof certificate, and include the proofs of required lemmas
only once. This
would make this certificate format slightly more complex, but avoid
explosion of the certificate
by preserving the modularity of the original proof.
Email Gateway (Aug 18 2022 at 15:11):From: Tjark Weber <webertj@in.tum.de>
I briefly discuss an implementation of this idea in Section 5.5 of my
dissertation
(http://www.cl.cam.ac.uk/~tw333/publications/weber08satbased.html). My
motivation at the time was to achieve stability across different
Isabelle installations in the presence of external provers (which might
be available on one machine, but not on another).
In theory, proof objects could become gigantic, but for Isabelle/HOL the
approach seemed to work reasonably well. I don't think there is
sufficient experimental data to dismiss it as infeasible in practice.
Of course, proofs of lemmas must not be expanded inline, but referenced
(as suggested by Peter). This is already supported by Stefan's proof
objects.
Tjark
Email Gateway (Aug 18 2022 at 15:11):From: Tobias Nipkow <nipkow@in.tum.de>
We have to distinguish two applications of proof objects: to speed up
the loading of theories, where they are fine, and as a means of
producing stable proofs, where I maintain they are problematic (and I am
not aware of any system that supports it). If you want to protect your
proof against a changing basis, you have to include the whole basis into
your proof object. It is not infeasible, but it means you are locked
into this one version of your proofs. And if one day the format for
primitive proofs changes... 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.
Tobias
Tjark Weber wrote:
Email Gateway (Aug 18 2022 at 15:11):From: John Matthews <matthews@galois.com>
Joe Hurd's OpenTheory project may be relevant here:
http://www.gilith.com/research/opentheory
It is designed to provide a standard for sharing theory developments
across higher order logic theorem provers. It doesn't support
Isabelle's type classes, however Alexander Krauss' and Andreas
Schropp's work on translating away typeclasses (Sections 5.1 and 5.2
of the online paper below) might be used to overcome this:
http://www4.in.tum.de/~krauss/holzf
-john
smime.p7s
Email Gateway (Aug 18 2022 at 15:12):From: Tjark Weber <tjark.weber@gmx.de>
On Thu, 2010-04-29 at 14:17 +0200, Tobias Nipkow wrote:
We have to distinguish two applications of proof objects: to speed up
the loading of theories, where they are fine,
If I recall correctly, Makarius and Stefan conducted a few experiments
some years ago and concluded that checking proof objects was typically
not faster than re-playing proof scripts in Isabelle.
and as a means of
producing stable proofs, where I maintain they are problematic (and I am
not aware of any system that supports it). If you want to protect your
proof against a changing basis, you have to include the whole basis into
your proof object. It is not infeasible, but it means you are locked
into this one version of your proofs. And if one day the format for
primitive proofs changes...
Well, being locked into a particular version of Isabelle's proof checker
still seems much better than being locked into a particular version of
Isabelle (and worse, being locked into a particular system configuration
when external provers are used).
Of course proof objects are not the answer to life, the universe and
everything. Size is one issue; the lack of readability is another. But
in terms of stability across Isabelle versions and platforms, proof
objects beat proof scripts (and even well-written Isar proofs) by a wide
margin. The interface is just a lot simpler.
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 objects can refer to lemmas, so one isn't forced to freeze the
library. Of course changes to the library may cause proof checking to
fail then, but at least changes to tactics still won't.
Shipping libraries in binary form is actually quite common, isn't it?
Maybe we need an equivalent for Isabelle theories.
Tjark
Email Gateway (Aug 18 2022 at 15:12):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
I just noticed that STIX have released version 1 of their fonts (May
24th 2010); does anyone have experience with using them for Isabelle?
I would be particularly interested to know if it was possible to get a
fixed-width version of the font. I don't anything about font-design, is
this a very hard thing to do?
best,
lucas
Email Gateway (Aug 18 2022 at 15:12):From: Makarius <makarius@sketis.net>
On Sat, 29 May 2010, Lucas Dixon wrote:
On 30/04/2010 16:09, Makarius wrote:
Isabelle2005 -- Isabelle2007 is in fact a counter example, with 25
months between the releases and the result being rather unstable. At
that time it was not completely clear if we would ever recover from a
continously "intermediate" state, and join the fate of notorious
projects such as SML/NJ or the STIX fonts.I just noticed that STIX have released version 1 of their fonts (May 24th
2010); does anyone have experience with using them for Isabelle?
I've tried it just a few hours after it came out. My impression is that
the quality as a screen font is not ideal, but this might be due to my
homegrown conversion from OpenType to TrueType via fontforge. The latter
does not treat all details of the hinting according to its author. Does
anybody have a high quality font converter?
I would be particularly interested to know if it was possible to get a
fixed-width version of the font. I don't anything about font-design, is
this a very hard thing to do?
The STIX people spent the first half of all these years counting only
glyph coverage. Then they noticed that the spacing between glyhps is just
as hard, and spent five more years on it.
Anyway, the last time when Isabelle symbol fonts were discussed on the
list I promised not to get involved in it again. But after projecting the
expected quality of STIX on the JVM -- which is particularly bad -- I've
had another go at it some months ago. The resulting IsabelleText font is
actually quite nice as a pseudo-fixed width screen font and will be
shipped with the next Isabelle release, i.e. within the next few weeks.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC