Email Gateway (Aug 18 2022 at 14:50): Email Gateway (Aug 18 2022 at 14:50):From: Timothy Bourke <timothybourke@gmail.com>
Manually running:
find_theorems solves
or
C-c C-f solves
should have the desired effect.
You could also make a more specific key binding if you need this
often.
Tim.
signature.asc
Email Gateway (Aug 18 2022 at 14:58):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users,
I am working on project, which includes 1) convex analysis formalization in Isabelle, and 2) provide a feedback about Isabelle, including comments and suggestions.
Here is my first feedback letter, mostly about the search in Isabelle.
When I want to prove some result, the first question is if this result new or not, and it would be nice to know this without reading the theories from the Library. Fortunately, if I guess the exact formulation of existing lemma, I can do search, or just formulate the lemma and get message like “The current goal could be solved directly with...”. The first important problem here is that if I formulate such a lemma inside the proof in command “have”, no suggestion is given, and it is hard to guess to check every time, as a result I already reproved some existing results.
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. Ideally, something like this should work when the existing result appears as a subgoal in the proof, etc.
The first part of this (about “have”) I have suggested during my first visit in June, and the reply was “good point. We will think about it”. This is very important because it will help to avoid duplicate job. Is it hard for realization?
Unfortunately, this mechanism is very sensitive for reformulations. For example, there exist a lemma “id x = x”, but I have no suggestions for lemma “x = id x”. In this and many similar cases Sledgehammer can help, but the same question arises: is it possible to run it in the background automatically, every time when I formulate a lemma or “have” statement?
Suggestion 2: It should be a possibility to run Sledgehammer in the background automatically, every time when I formulate a lemma or “have” statement . If this is already possible, the suggestion is to make it more clear how to turn it on, because I cannot find the way to do this.
Unfortunately, even Sledgehammer does not help for a little bit more complicated lemmas. For example, it cannot prove the lemma
f = g ↔ (!x. f x = g x) (1)
although this lemma is present in the library. As a result, a reformulation like
f = g ↔ (!x. g x = f x) (2)
is not addressed neither by Sledgehammer nor by lemma suggestion mechanism, and I see no simple way for the user to find out that this lemma is not essentially new. May be, this way exists, and I just do not know about it?
Suggestion 3: As a minimum, merge lemma suggestion with Sledgehammer to create a new Sledgehammer which would prove at least (1). Ideally, it should be a mechanism which proves a reformulations like (2), and it should work automatically, to prevent user from reproving result. If there is another simple way to see that statements like (2) are not essentially new, it should be more clear documented, because I cannot find a simple way to do this.
In my work, I need a definition of dimension. It states
dim V = (SOME n. EX B<=V. independent B & V<=span B & card B =n)
I know from the tutorial that SOME is Hilbert operator, but when I tried to find the definition of SOME in Isabelle, the search failed. It turned out this was because SOME is an abbreviation, but it took me a long time and finally I needed help of another person.
Suggestion 4: There should be a simple way to see the any definition in Isabelle, even if I do not know in advance, is this a lemma, method, term, abbreviation, notation, or something else.
But even knowing the definition, I do not know how to work with this SOME. For example, if I assume that “dim V = m” I have “(SOME n. EX B<=V. independent B & V<=span B & card B =n) = m”, but I do not know how to extract this B from this definition and derive, say, that
dim V = m ==> (EX B<=V. independent B & V<=span B & card B =m) (3)
Ideally, together with definition it should be small set of example how to work with, say, SOME, but may be it is too much to formulate this as a suggestion (although such a help exists in many systems like Mathematica). Ok, could you please just tell me how to work with SOME, for example, how to prove (3)?
Also, to proceed with proof of my lemma, I will need to obtain this B and say that it is a basis in R^n, whence affine hull V = R^n But again, I cannot understand the definition of basis in Isabelle, because it contains symbol \<chi>, which is not in table A.1 in the tutorial, and it is hard to find what it means, see suggestion 4. Could you please explain me this notation, and how to work with basis, for example, how to prove that n independent vectors form a basis in R^n.
Sincerely,
Bogdan.
Email Gateway (Aug 18 2022 at 14:59):From: Tobias Nipkow <nipkow@in.tum.de>
In my work, I need a definition of dimension. It states
dim V = (SOME n. EX B<=V. independent B & V<=span B & card B =n)
Such definitions are notoriously tricky to work with. In particular,
dim V = m ==> (EX B<=V. independent B & V<=span B & card B =m) (3)
does not hold. What if V has no dimension? Then "dim V" is still
defined, but you don't know what it is. In it cannot possibly fulfill
the defining predicate. Another way to see that (3) is strange,
instantiate m with "dim V" in (3).
The rules for working with SOME are all in Hilbert_Choice. The closest
you can get to (3) is
lemma someI2: "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
This requires that you know that there is an "a" that satisfies P.
Some further hints:
There is also THE and LEAST which may or may not be more convenient
than SOME.
Look though the "What's in Main" manual (it's only 10 pages) to
discover what there is. You can also use the pdf search facility to
search for symbols in there.
There is also THE and LEAST which may or may not be more convenient
than SOME.
Sometimes it is convenient to set "undefined" values to a fixed value.
For example, card A = 0 if A is infinite. Maybe something similar makes
sense for dim.
Tobias
Email Gateway (Aug 18 2022 at 14:59):From: Makarius <makarius@sketis.net>
On Thu, 25 Mar 2010, grechukbogdan wrote:
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. Ideally, something like this should work when the existing
result appears as a subgoal in the proof, etc.
The goal-print-hook mechanism is essentially just a temporary workaround
(since some years already). There is a fundamental bottle-neck in the
synchronous interaction model of Proof General here, which is inherited
from the plain tty model. I.e. there is just a single read-eval-print
loop, and while the system is trying to find smart suggestions the user
has to wait for it.
Activating this crude suggestion mechanism in more places would degrade
system reactivity even further.
Suggestion 2: It should be a possibility to run Sledgehammer in the
background automatically, every time when I formulate a lemma or “have”
statement . If this is already possible, the suggestion is to make it
more clear how to turn it on, because I cannot find the way to do this.
Same problem, even worse. Users certainly do not want to wait several
seconds until they can continue typing.
The crude asynchronous mode of Sledgehammer is also just a temporary
workaround.
Quite some time ago, I've started an effort to introduce true interaction
into interactive theorem proving, by giving up the tty read-eval-print
loop, and Proof General, heading towards a document-oriented editor model.
This is much easier said then done. There are many technical issues, part
of them already solved. At least initially it was hard to find a
replacement for the Emacs operating system (with its modest
single-threaded editor). What has emerged already is this new
Isabelle/Pure.jar Scala library for system programming, and a small demo
application based on the powerful jEdit, which is a real editor, not an
operating sytem like Emacs or Eclipse.
I hope to see some usuable asynchronous proof editor within the next few
months. The asynchronous model will provide a natural playground for
various "user agents" based on find_theorems, external ATPs etc. There is
lots of implementation work still ahead of us -- as well as unlearning the
way of thinking in terms of a TTY-loop.
Suggestion 4: There should be a simple way to see the any definition in
Isabelle, even if I do not know in advance, is this a lemma, method,
term, abbreviation, notation, or something else.
You cannot easily have a "whatis FOO" command that tells you about an
uncategorized entity FOO -- it would violate the internal data abstraction
of Isabelle tools and packages. But such a command would belong to the
old TTY world anyway.
What works already is a universal markup mechanism that decorates all
input and output of the system by formal references to defining and
referencing locations etc. For example, looking at some bit of text like
"SOME x. P x" that has been digested by the system at some point, you
could click on the "SOME" or even the "." to refer to the formal entity
behind it, say a constant definition with notation for concrete syntax.
Too bad there is still no user interface, or even just HTML browser to
make use of this information emitted by Isabelle. The Proof General setup
strips it all away -- the single LISP thread would choke on all that
semantic information anyway.
Moreover, if you look at modern Isabelle documentation, it is all based on
formal theories. Manuals such as isar-ref have further formal markup in
the running text, say @{method_def induct} (defining position) or
@{method_ref induct} (interesting referencing position), or @{method
induct} (other reference). Right now this is only used to produce a
traditional LaTeX index, but the pointing and clicking on formal entities
as sketched above could be applied as well.
For example, lets say you look at some bits of theory somewhere in the
library:
lemma fixes n :: nat shows "P n" by (induct n) auto
To understand what "induct" is, you merely right-click and select from
whatever manuals are presented there, you should quickly get to
reference-manual style definitions of it, or some specially marked
examples etc.
Isabelle already provides a good portion of such mechanisms internally,
but the front-ends are still lacking. Something like two years ago I've
started to engage myself into the Scala/JVM programming language, to get
access to JVM based editor and browser technologies, without having to
work with the crude oil industry stuff around Java. Thus the ML (and HOL)
culture of Isabelle can be extended into the JVM, thanks to the smart guys
from EPF Lausanne.
Stay tuned for more to come here soon.
If anybody wants to help me out, what I desparately need is:
* A really good PDF browser for the JVM (as pure jar, no JNI crap);
hyperlinks and copy-paste need to work properly.
* A really good HTML browser in the same manner. Presently I am using
Lobo/Cobra, which is quite good, but also has some shortcomings.
(I've tried Flying Saucer already.)
Of course, all of that needs to be Open Source.
Makarius
Last updated: Apr 25 2024 at 01:08 UTC