Email Gateway (Aug 23 2022 at 08:38): Email Gateway (Aug 23 2022 at 08:38):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I want to ask for feedback on a well-known intricate problem involving
locales.
Symbols ‹f› defined relative to a local are foundationally represented
as ‹c.f x y z› with ‹x› ‹y› ‹z› being the parameters of the locale and a
corresponding abbreviation ‹f = c.f x y z› establishing the syntactic
illusion of a symbol depending on local parameters.
After interpretation (into global theories, into a locale), the
parameters ‹x› ‹y› ‹z› are replaced by their corresponding
instantiations ‹r› ‹s› ‹t›.
Essential is that characteristic theorems about ‹f› refer to the
foundational representation ‹c.f x y z› rsp. ‹c.f r s t›. Hence the
whole machinery breaks badly if e.g. a simplification rules applies to a
redex in ‹x› ‹y› ‹z› rsp. ‹r› ‹s› ‹t› since the resulting goal has
hardly any correspondence to existing theorems (*).
Concerning simplification, the problem can be avoided issuing a
congruence rule ‹⋀a b c. c.f a b c ≡ c.f a b c›. Initially my idea was
to provide such a congruence rule automatically. But this does not cover
arbitrary instantiations – what should be a suitable congruence rule for
‹c.f (g x) v (h y)› involving free parameters ‹x› ‹y›? (A similar
situation occurs e. g. in the AFP in session Affine_Arithmetic).
At TUM we have discussed various alternatives, without a conclusive idea.
Hence my question: who has experience with the problem described above
(*) and can describe typical situations where this occurs?
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:38):From: "lammich@in.tum.de" <lammich@in.tum.de>
Hi
I ran into this problem several times. Usually, it will break a design that
involves locale instantiations, by making it cumbersome to use.
One instance I remember was designing the input language for our cava model
checker with partial order reduction, where this issue literally killed the
initial design.
Peter
Email Gateway (Aug 23 2022 at 08:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
For the record:
http://isabelle.in.tum.de/repos/isabelle/rev/ca3ac5238c41 adds a
congruence rule but does not declare it by default.
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:56):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
after a second round of thoughts my conclusions are:
A congruence rule can only be provided on a per-definition base, not
on a per-interpretation base: the critical syntactic constant c.f
appears in any interpretation.
Having a default congruence rules that must be removed in certain
non-trivial situations is a bad idea: few users are getting in touch
with congruence rules ever.
Hence the best what can be done at the moment is to provide the
congruence rule for each definition but not declare it as a default
congruence rule: it can be declared on demand if needed; the
documentation should give an explicit hint on that.
Any comments on that?
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:56):From: Lawrence Paulson <lp15@cam.ac.uk>
Kind of a side remark: by default, simplification is set up so that the then/else parts of conditional expressions are left unsimplified. I’m probably responsible for this choice but still occasionally get surprised by it, but no one seems to ask about it on this mailing list.
Reverting that decision would probably cause a lot of looping in proofs about recursive functions.
Larry
Email Gateway (Aug 23 2022 at 08:56):From: Tobias Nipkow <nipkow@in.tum.de>
On 16/04/2020 10:54, Klein, Gerwin (Data61, Kensington NSW) wrote:
On 16 Apr 2020, at 16:33, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Kind of a side remark: by default, simplification is set up so that the then/else parts of conditional expressions are left unsimplified. I’m probably responsible for this choice but still occasionally get surprised by it, but no one seems to ask about it on this mailing list.
Reverting that decision would probably cause a lot of looping in proofs about recursive functions.
I am convinced it was the right choice and should stay.
Tobias
Yes. We have set the stronger if_cong rule for parts of the l4v proofs, and it was not the best idea. If you’re not super careful, things loop all the time.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:56):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This is what I think, too: it follows from the observeration that »if«
acts as case combinator on bool.
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:57):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Yes. We have set the stronger if_cong rule for parts of the l4v proofs, and it was not the best idea. If you’re not super careful, things loop all the time.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:58):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
indeed those partial interpretations are IMHO the candidates where
simplification of instances of locale parameters makes sense.
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:58):From: Tobias Nipkow <nipkow@in.tum.de>
Because "partial interpretations" are more likely to be used by experts, I would
not mind if the congruence rules were enabled by default and would have to be
disabled by these experts. However, this is just a mild preference.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:59):From: Thomas Sewell <sewell@chalmers.se>
Given that it's being discussed, I thought I might repeat my opinion on this. I don't think the existing Isabelle setup makes much sense, but it would be a lot of work to change it.
There's two real problems with the setup where weak case congruences are installed by default.
The first is that it makes the simplifier unpredictable. I found myself telling beginner users, over and over again, to watch out for this reason why the simplifier might be refusing to act. Despite this repetition, I sometimes found that I'd missed it myself, and spent time on pointless elaborate workarounds.
The second problem is that, in the case of the boolean type, the presence of 'if_split' or 'split_if' or whatever it's called now contradicts the previous design principle. Many of the cases that were prevented from looping by the weak case congruence loop anyway if the splitter can do the case division.
Finally, this setup isn't really necessary. It permits the equations of more functional programs to be added to the simplifier safely, but not all o
Finally, the Isabelle setup isn't necessary. HOL4 has roughly the same infrastructure, but no weak case congruences. I think the key difference is that the defining equations of a function aren't added to the simplifier by default.
Email Gateway (Aug 23 2022 at 08:59):From: Thomas Sewell <sewell@chalmers.se>
OK, apparently I have a hotkey for sending a partially finished email that I didn't know about.
Let me rephrase the last paragraph of the previous.
The existing setup doesn't have to be the way it is. It sometimes allows the equations of a functional program to be added to the simplifier set safely, but proofs about those programs usually have to handle the simplifier very carefully anyway. A simpler solution is just not to put these rules in the simplifier and single step them when needed - HOL4 does something like that and it roughly works.
But, clearly the current behaviour is embedded pretty deeply into the current definitions and proofs. From memory we learned in l4v that changing the if congruence locally seemed safe but some functions from the library seemed to cause loops, and we only realised later that the congruence was the problem.
Cheers,
Thomas.
Last updated: Nov 21 2024 at 12:39 UTC