Email Gateway (Aug 22 2022 at 17:10): Email Gateway (Aug 22 2022 at 17:10):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
it happens quite frequently that a rule in the simp set is oriented
in the wrong direction for a proof to go through (while the same simp
rule works just fine in other proofs; so it's not a matter of picking
the right orientation for the rule, because the required orientation
depends on the context). So I often find myself doing things like
apply (auto simp: foo[symmetric] simp del: foo)
sometimes for more than one rule.
I'm wondering whether it would be worthwhile to add a modifier that
abstracts from this, say
apply (auto simp flip: foo)
What do you think?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:10):From: Lawrence Paulson <lp15@cam.ac.uk>
As it happens, we are investigating precisely this idea right now.
One question is whether to introduce a new modifier or instead just to remove the “flipped” version (if present) whenever you insert a simplification rule. Views would be welcome.
Larry Paulson
Email Gateway (Aug 22 2022 at 17:10):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Lawrence Paulson wrote:
[about having a modifier for flipping simp rules]
I like the idea of making the removal implicit. The main worry is
usually that such magic leads to confusion, but I honestly don't see
that happening in this particular case.
The main advantage I see is that no new vocabulary is required.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:10):From: Tobias Nipkow <nipkow@in.tum.de>
I have implemented a first version with modifier "reorient" and am tempted to go
with that because it saves you the [symmetric] (after all, the whole thing is
suppsed to be short, otherwise we wouldn't need it) and does not change the
behaviour of "add". The word "flip" is a nice too (although a bit generic in the
context of "auto").
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:10):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
just to make what Tobias already said more explicit: I also prefer
(auto reorient: A B C D)
over
(auto simp: A [symmetric] B [symmetric] C [symmetric] D [symmetric])
Alternatives for the name:
reorient
flip
swap
sym
pmis
simp\<^sup>- (not actually supported as identifier)
cheers
chris
Email Gateway (Aug 22 2022 at 17:10):From: Dominique Unruh <unruh@ut.ee>
I have an additional suggestion in this context: If "flip" (or whatever the
name will be) is implemented, perhaps the regular "add" could also check
whether the flipped rule already exists in the simpset, and, if so, print a
message informing the user that "flip" would be the right thing to do? That
will make it easier for people to find out about it, and probably also help
people tracking down accidental looping simpsets.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:11):From: Tobias Nipkow <nipkow@in.tum.de>
I find the multitude of options already out of proportion to the frequency of
the situation; this warning idea adds another dimension. Is adding the symmetric
version of a rewrite rule by accident really an issue? (If it is, it rules out
Larry's solution of silently removing the original one.) I would have thought not.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:11):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
it's been a while, but I vaguely remember that I ran into this when I
was still a beginner with Isabelle. I quickly learned to interpret a
looping simplifier as the suggested warning, but a proper warnings
might have helped, at least during that initial phase of Isabelle use.
Cheers,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 17:11):From: Tobias Nipkow <nipkow@in.tum.de>
OK, point taken.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:11):From: Akihisa Yamada <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear all,
already (simp add: ac_simps) is a magic so I think more magic can be
accepted.
Best regards,
Akihisa
Email Gateway (Aug 22 2022 at 17:20):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Tobias Nipkow wrote:
If a short word like "flip" is used, I would suggest to follow the
"simp del:" pattern and use "simp flip:" for the more elaborate methods
(auto, force, etc.), so it's clear that the simp rules are affected.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:34):From: Tobias Nipkow <nipkow@in.tum.de>
In Isabelle/223172b97d0b I went for Christian's suggestion and renamed
"reorient" to "flip":
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:34):From: Tobias Nipkow <nipkow@in.tum.de>
On 30/04/2018 15:18, Dominique Unruh wrote:
I have an additional suggestion in this context: If "flip" (or whatever the
name will be) is implemented, perhaps the regular "add" could also check
whether the flipped rule already exists in the simpset, and, if so, print a
message informing the user that "flip" would be the right thing to do? That
will make it easier for people to find out about it, and probably also help
people tracking down accidental looping simpsets.
The implementation of this feature is a bit of work because for it to be useful
one has to compare rules modulo renaming of free variables. Not sure if or when
I'll get around to that.
Tobias
Best wishes,
Dominique.On 30 April 2018 at 15:36, Christian Sternagel <c.sternagel@gmail.com>
wrote:Dear all,
just to make what Tobias already said more explicit: I also prefer
(auto reorient: A B C D)
over
(auto simp: A [symmetric] B [symmetric] C [symmetric] D [symmetric])
Alternatives for the name:
reorient
flip
swap
sym
pmis
simp\<^sup>- (not actually supported as identifier)cheers
chris
On 04/30/2018 10:11 AM, Tobias Nipkow wrote:
I have implemented a first version with modifier "reorient" and am
tempted to go with that because it saves you the [symmetric] (after all,
the whole thing is suppsed to be short, otherwise we wouldn't need it)
and does not change the behaviour of "add". The word "flip" is a nice
too (although a bit generic in the context of "auto").Tobias
On 29/04/2018 23:11, Bertram Felgenhauer via Cl-isabelle-users wrote:
Lawrence Paulson wrote:
[about having a modifier for flipping simp rules]
As it happens, we are investigating precisely this idea right now.
One question is whether to introduce a new modifier or instead just to
remove the “flipped” version (if present) whenever you insert a
simplification rule. Views would be welcome.I like the idea of making the removal implicit. The main worry is
usually that such magic leads to confusion, but I honestly don't see
that happening in this particular case.The main advantage I see is that no new vocabulary is required.
Cheers,
Bertram
Last updated: Apr 26 2024 at 08:19 UTC