Email Gateway (Aug 19 2022 at 09:06): Email Gateway (Aug 19 2022 at 09:06):From: Joachim Breitner <breitner@kit.edu>
Dear Tobias,
Am Sonntag, den 18.11.2012, 09:31 +0100 schrieb Tobias Nipkow:
We are planning to provide a much improved tracing facility for the simplifier
which will certainly keep track of such things and will tell you, for example,
if a rule you added explicitly was not used at all. We could also provide the
list of all rules used.
great!
The output window would then say something along the lines simplification
used 5 lemmas. Use "apply (simp only: foo bar baz bam bang)" (12ms) to
reproduce. and in the IDE I could click on that to replace the original
invocation with this more explicit command.I doubt we want to go down that route. The simplifier often uses lots of
rules, which would lead to a very long list if supplied explicitly, which is
ugly. Moreover it would expose information we want to hide: how exactly a lot
of basic computations are organized, especially rewriting on numbers. Your
suggestion would create simplifier calls that hardwire that information and
make such steps very brittle under change. I don't want to encourage that.
I understand the rationale here, and it certainly makes sense when
working with a theory that does, say, lots of arithmetic. But other
applications may make very little use of basic stuff from Main; hardly
more than just lists. I’d suggest that the call should be left to the
user: If he sees lots of lemmas he did not write himself or does not
know, he can leave the simp call as it is. But if the lemmas are roughly
what he expected, why not allow him to make that explicit?
(The situation is not different with sledgehammer, which also
occasionally produces internal lemmas, yet it is a useful feature that
is mostly used in a “good” way.)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:06):From: Manuel Eberl <eberlm@in.tum.de>
What i would find more useful would be output in the form of 'Use "apply
(simp add: foo bar baz bam bang)"', i. e. if it showed a list of the
rewrite rules that it used and that are not in the simp set anyway.
This, if I am not mistaken, would not lead to the problem of exposing
any of these these internal details but still provide a similar
functionality. I for one use "simp add:" much more often than "simp
only:" and have often found myself removing rules from the "add" clause
by trial and error to find out which of them are actually necessary.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 09:06):From: Tobias Nipkow <nipkow@in.tum.de>
That is a version of the feedback we intend to give: which of the added rules
were actually used.
Tobias
Email Gateway (Aug 19 2022 at 09:08):From: Tobias Nipkow <nipkow@in.tum.de>
Am 18/11/2012 10:51, schrieb Joachim Breitner:
Dear Tobias,
Am Sonntag, den 18.11.2012, 09:31 +0100 schrieb Tobias Nipkow:
We are planning to provide a much improved tracing facility for the
simplifier which will certainly keep track of such things and will tell
you, for example, if a rule you added explicitly was not used at all. We
could also provide the list of all rules used.great!
The output window would then say something along the lines
simplification used 5 lemmas. Use "apply (simp only: foo bar baz bam
bang)" (12ms) to reproduce. and in the IDE I could click on that to
replace the original invocation with this more explicit command.I doubt we want to go down that route. The simplifier often uses lots of
rules, which would lead to a very long list if supplied explicitly, which
is ugly. Moreover it would expose information we want to hide: how
exactly a lot of basic computations are organized, especially rewriting
on numbers. Your suggestion would create simplifier calls that hardwire
that information and make such steps very brittle under change. I don't
want to encourage that.I understand the rationale here, and it certainly makes sense when working
with a theory that does, say, lots of arithmetic. But other applications
may make very little use of basic stuff from Main; hardly more than just
lists. I’d suggest that the call should be left to the user: If he sees
lots of lemmas he did not write himself or does not know, he can leave the
simp call as it is. But if the lemmas are roughly what he expected, why not
allow him to make that explicit?
We don't forbid that at all. We just don't want to encourage it in general.
(The situation is not different with sledgehammer, which also occasionally
produces internal lemmas, yet it is a useful feature that is mostly used in
a “good” way.)
Sledgehammer (currently) has no alternative.
Tobias
Greetings, Joachim
Email Gateway (Aug 19 2022 at 09:13):From: Timothy Bourke <tim@tbrk.org>
I wonder if such a feature would be more practical and useful if
restricted to a particular theory (or set of theories):
apply (simp minimize: Invariants add: foo)
where rules from a theory called "Invariants" would be listed for
possible one-click substitution.
During the verification of a model, for instance, it's certainly more
efficient (for the user) to have most lemmas applied automatically,
but afterward it would sometimes be nice to know exactly which lemmas
(from a subset of interesting ones) were actually used. Both for
refactoring, as already mentioned, and for better understanding the
result.
But, perhaps this would be better in a separate "reporting tool"?
Tim.
signature.asc
Email Gateway (Aug 19 2022 at 09:13):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks for the suggestion, but this is getting a bit fine-grained and I can
imagine (too) many variations on this idea.
Tobias
Email Gateway (Aug 19 2022 at 09:24):From: Joachim Breitner <breitner@kit.edu>
Dear Isabelle users (and devs, I guess),
I am using sledgehammer/metis more and more even for very simple and
obvious lemmas that I could mostly also solve with simp or auto. The
great thing about sledgehammer is that it searched a proof taking many
lemmas into account, but then produces a command that explicitly
mentions the lemmas that are required, which is very useful feedback to
me, and helps, for example, in refactoring.
Is there a chance to get a similar feature for the simplifier? I could
imagine that when I write
apply (simp minimize add: foo)
the simplifier would run as usual, but it would also keep track of which
simplification rules were actually used. The output window would then
say something along the lines
simplification used 5 lemmas.
Use "apply (simp only: foo bar baz bam bang)" (12ms) to
reproduce.
and in the IDE I could click on that to replace the original invocation
with this more explicit command.
It could work similarly (but maybe harder to implement, I presume) for
auto.
More generally, as I’m basically working with Isabelle fulltime these
days, there are more usability improvement ideas cropping up. Is this
the right forum and form to suggest them?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:25):From: Tobias Nipkow <nipkow@in.tum.de>
Am 16/11/2012 23:25, schrieb Joachim Breitner:
Dear Isabelle users (and devs, I guess),
I am using sledgehammer/metis more and more even for very simple and
obvious lemmas that I could mostly also solve with simp or auto. The great
thing about sledgehammer is that it searched a proof taking many lemmas
into account, but then produces a command that explicitly mentions the
lemmas that are required, which is very useful feedback to me, and helps,
for example, in refactoring.Is there a chance to get a similar feature for the simplifier? I could
imagine that when I write apply (simp minimize add: foo) the simplifier
would run as usual, but it would also keep track of which simplification
rules were actually used.
We are planning to provide a much improved tracing facility for the simplifier
which will certainly keep track of such things and will tell you, for example,
if a rule you added explicitly was not used at all. We could also provide the
list of all rules used.
The output window would then say something along the lines simplification
used 5 lemmas. Use "apply (simp only: foo bar baz bam bang)" (12ms) to
reproduce. and in the IDE I could click on that to replace the original
invocation with this more explicit command.
I doubt we want to go down that route. The simplifier often uses lots of
rules, which would lead to a very long list if supplied explicitly, which is
ugly. Moreover it would expose information we want to hide: how exactly a lot
of basic computations are organized, especially rewriting on numbers. Your
suggestion would create simplifier calls that hardwire that information and
make such steps very brittle under change. I don't want to encourage that.
It could work similarly (but maybe harder to implement, I presume) for
auto.More generally, as I’m basically working with Isabelle fulltime these days,
there are more usability improvement ideas cropping up. Is this the right
forum and form to suggest them?
It is, thanks.
Tobias
Greetings, Joachim
Last updated: Apr 25 2024 at 16:19 UTC