Email Gateway (Aug 19 2022 at 09:10): Email Gateway (Aug 19 2022 at 09:10):From: Joachim Breitner <breitner@kit.edu>
Dear developers,
I’d like to share some ideas how working with Isabelle could be a bit
more efficient, at least for me and my workflow.
All I am describing is the 2012 release, used via jEdit.
Generally, I could imagine the output window being a bit more
informative, in particular with error messages.
For example, a failed "by method" currently just prints “Failed to
finish proof.” To fix this, I now have to change the "by" to "apply",
look at the result, fix it, and change it back. Could it not print
“Failed to finish proof. Remaining goals: ....”?
A command that does not provide any output at all is “lemma” (and also
“lemmas”). Sometimes, I feel the need to check how Isabelle actually
sees the lemma, e.g. to see what types she has inferred, or to check
whether I am really done or if there is still a [!] behind the lemma¹.
Currently, I have to use “thm name” after the lemma for that (and give
the lemma a name if it does not have one yet). Would it be possible to
have the lemma command already print that information?
Another error that could be make more helpful is “Unknown fact "..."”.
Often I don’t remember the name of a lemma exactly – was it set_finite
or finite_set? I then have to fire up "find_theorems name:..", which is
quite a bit of typing.
GHC recently has started to give spelling corrections (the 10 best fits
based on edit distance, IIRC) for every kind of unknown-something error.
If Isabelle could do the same, this would be great. I’d imagine that in
the context of Isabelle lemmas the edit distance should give special
treatment to reordering the parts of the string that are separated by
‘_’, as it is often the order of the components of the name that I fail
to remember, and count that as one step.
I guess Isabelle usually has many more lemmas in scope than GHC has
functions and this might be a bit slow. But the output does not have to
be generated at once and if the error message is printed before the list
is calculated, this should not harm anyone.²
Last on my list for today is a more interactive variant of print_cases.
When I currently write
lemma "n + 1 = 1 + (n::nat)"
proof(induct n)
I have
proof (state): step 1
goal (2 subgoals):
1. 0 + 1 = 1 + 0
2. ⋀n. n + 1 = 1 + n ⟹ Suc n + 1 = 1 + Suc n
and with
print_cases
it prints
cases:
0:
let "?case" = "0 + 1 = 1 + 0"
Suc:
fix n_
let "?case" = "Suc n_ + 1 = 1 + Suc n_"
assume Suc.hyps: "n_ + 1 = 1 + n_" and Suc.prems:
What I am missing is a combination of both that is ready to be used as
the structure of an Isar proof, e.g. either completely explicit:
show "0 + 1 = 1 + 0"
sorry
next
fix n
assume "n + 1 = 1 + (n::nat)"
show "Suc n + 1 = 1 + Suc n"
sorry
qed
or, depending on personal preference and number and complexity of the
hypotheses, using the provided case names (and using "case goal1..." if
there are no case names):
case 0
show ?case
sorry
next
case (Suc n)
show ?case
sorry
qed
From there I guess it would be a small step to allow the user to insert
the output of this command (say print_isar_structure) into the proof
document with one click, similar to how sledgehammer works.
That’s it for today. Thanks for your work,
Joachim
¹ And just to not only list things that I am missing: I find this
marking of lemmas whose prove contains a sorry very useful feedback. It
it were not done, I’d have to ask for it :-)
² Actually, it seems that implementing this feature would be a very
local task that is suitable for first-time Isabelle contributors. If you
say that such a feature would be accepted, I could give it a shot.
signature.asc
Email Gateway (Aug 19 2022 at 09:11):From: Makarius <makarius@sketis.net>
That is not a function of the output window, but of the prover to report
things in a certain way. During this summer, and now in fall moving
towards the coming winter release, I've made many refinements in both
areas, and hopefully manage to add 2-3 more rounds of refinement before
the next release. The general tendencies are like this:
(1) Output is becoming less and less important (it is an old TTY thing).
Instead the information is directly attached to the source. So the
messages are right there where things happen, while remaining
accessible in output for nostalgic reasons (for people who want to
make long moves with the mouse in the old way).
(2) Error feedback of Isar commands involving search/enumertion of
possibilities: this is an ancient issue from > 10 years ago, which I
have re-opened some weeks ago. So in the next release, you will see
proper errors for "by method", and the need to use 'apply' to imitate
that will be no longer there.
Makarius
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
This is in a transitional state, between old TTY things that no longer
work, and proper global status summaries in the Prover IDE.
Conceptually, the internal derivation object cannot be displayed to the
user while editing and asynchronous/parallel checking continues. I've no
particular plans for the coming release here -- too many other things need
to be consolidated first.
Makarius
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
Sounds like the GHC guys have 10 times more resources to spend. There are
many ideas about formal entity lookup in the pipeline, including
context-sensitive completion, but nothing like the above so far.
Ask again after some more years of Isabelle/jEdit Prover IDE development.
Makarius
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
'print_cases' is indeed a dinosaur from the TTY age. Producing proof
outlines for induction proofs is the standard application for smart
templating, I have it on my list for a long time already. This summer I
got quite close to see how it can be implemented relatively easily, at
least the abstract case / show ?case form, because printing of terms in a
parsable way is still needs further investigation. It is unlikely to
happen for the coming release, though.
Also note that goal1, ..., goal42 are not Isar-conformant at all: they
produce fragile proofs with lots of funny indices. It is often better
make an unstructured script in the traditional manner here.
Makarius
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
The implementation work for anything is usually an order of magnitude more
than first anticipated, and an order of magitude less than the cumulative
efforts for maintaining the result in the long run.
Makarius
Last updated: Apr 20 2024 at 01:05 UTC