Email Gateway (Feb 09 2024 at 16:38): Email Gateway (Feb 09 2024 at 16:38):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Just a small note observing that the HOL-Library.Array_Braun theory adds
Let_def to the simpset with a declare:
https://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/Array_Braun.html
This has an annoying effect on automation when importing this theory, and
perhaps should be removed or limited in its scope with a notes, or similar?
Thanks,
Dominic
Email Gateway (Feb 12 2024 at 06:30):From: Tobias Nipkow <nipkow@in.tum.de>
Dominic,
The theories in HOL-Data_Structures are all about functional programs and many
of them declare Let_def [simp]
Cant't you just disable it with [simp del]?
Tobias
Email Gateway (Feb 13 2024 at 09:56):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi Tobias,
The theories in HOL-Data_Structures are all about functional programs and
many
of them declare Let_def [simp]
Yes. My quibble was this simpset modification having a global—rather than
localised—effect, not the need for the simpset change.
Cant't you just disable it with [simp del]?
Yes, this would work in a narrow technical sense. However, I don't think
this is a practical way of working:
- We need to remember to do that every time we import the theory, in
addition to performing point-fixes for suboptimal simpset, notation, and
whatever else, setups we inherit from theories distributed with
Isabelle/HOL and our other external dependencies. As an Isabelle user I
surely should be able to expect that theories distributed with the base
system set up notation and automation in a generally useful state.
- We incur technical debt as our code becomes littered with point fixes
for problems inherited from upstream which—six months in the future—nobody
can remember the need for or understand whether they're still relevant.
- It's just another (minor) hassle when theorem proving and issues like
this are why, over time, an increasing amount of brain cycles on large
proof efforts comes to be dominated by issues related to the theorem
proving tool itself, rather than the proof at hand.
- This particular style of working is discouraged by the Isabelle linter
which has an explicit lint dedicated to spotting these types of global
simpset changes in "global_attribute_changes".
In this respect, it's far better if problems like this are fixed upstream
when they are noticed.
Thanks,
Dominic
On Mon, 12 Feb 2024 at 06:30, Tobias Nipkow <nipkow@in.tum.de> wrote:
Dominic,
The theories in HOL-Data_Structures are all about functional programs and
many
of them declare Let_def [simp]Cant't you just disable it with [simp del]?
Tobias
On 09/02/2024 17:38, Dominic Mulligan (via cl-isabelle-users Mailing List)
wrote:Hi,
Just a small note observing that the HOL-Library.Array_Braun theory adds
Let_def
to the simpset with a declare:https://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/Array_Braun.html
<
https://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/Array_Braun.htmlThis has an annoying effect on automation when importing this theory,
and
perhaps should be removed or limited in its scope with a notes, or
similar?Thanks,
Dominic
Email Gateway (Feb 23 2024 at 07:06):From: hannobecker@posteo.de
Hi all,
FWIW, I agree with Dominic. I don't think a general purpose library such
as Array_Braun should make global modifications to the attributes of
external theorems, esp. something as ubiquitous as Let_def.
Is it not an option to declare Let_def[simp del] at the end of
Array_Braun for now (or bracket everything in a context notes
Let_def[simp] begin ... end block), and adjust the (hopefully few)
places that depend on Array_Braun and have ossified around Let_def
being in the simpset?
Best,
Hanno
Email Gateway (Feb 23 2024 at 09:35):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes – agree.
Hardly any theories import Array_Braun directly. But one of them is Code_Setup, so it will be interesting to see what changes turn out to be necessary.
Larry
Email Gateway (Feb 23 2024 at 10:08):From: Tobias Nipkow <nipkow@in.tum.de>
I beg to differ. When you import a library you import a design philosophy, in
this case the conviction, born out of long experience, that in the context of
the verification of functional programs you almost always want to expand "let".
Moreover, it can be reversed easily and we even have comments in Isabelle to
remind you why you reversed it.
You may also be interested to learn that the basic setup expands let's in
certain situations via a simproc that may (or may not) be easy to turn off. In
fact, it is not easy to work out what those situations are.
If anything, you may complain that not all theories in Data_Structures activate
Let_def. I'd be happy to make that more uniform.
Tobias
Email Gateway (Feb 23 2024 at 13:37):From: Peter Lammich <lammich@in.tum.de>
There's another view on it:
when you import a library into a bigger project, you do not want to
import its (internal) design philosophy, which might be very nice for
proving data structures, but get in the way for other things. Actually,
you want to import as few as possible, in particular no changes that
'pollute' the global state.
What you want to import if you use the trees is: an abstraction function
(invar ideally hidden in typedef), operations, and lemmas that concrete
operations commute with abstract ones (these would typically be in the
simpset, as they only affect concepts defined by this library). That's
it. Everything internal used to prove these lemmas should be hidden by
default, and require some manual effort to get back (like manually
augmenting the simpset).
Email Gateway (Feb 24 2024 at 13:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
just a remark on the mail subject: the theory we are talking about is
better referred to as HOL-Data_Structures.Array_Braun rather than
HOL-Library.Array_Braun.
Having said that, there are basically two options for development-local
declarations like Let_def [simp]:
(+) Keeps particularities really local.
(+) Easy to get right.
(-) Clutters developments with some incantations.
(+) Repeated incantations not necessary.
(-) No (officically supported) selective use of single theories from the
development.
(-) Brittle to maintain, inconsistencies might leak over time.
Just my contribution to the ongoing discussion.
Cheers,
Florian
Am 09.02.24 um 17:38 schrieb Dominic Mulligan (via cl-isabelle-users
Mailing List):
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Mar 01 2024 at 14:20):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Yes, sorry for any unintended confusion—I did in fact mean
HOL-Data_Structures.Array_Braun rather than HOL-Library.Array_Braun.
Thanks,
Dominic
Last updated: Jan 04 2025 at 20:18 UTC