Email Gateway (Feb 11 2023 at 13:09): Email Gateway (Feb 11 2023 at 13:09):From: David Fuenmayor <davfuenmayor@gmail.com>
(See file attached)
As an example, below I use the keyword "abbreviation" (instead of
"definition") and the system blocks/freezes in the next lemma
abbreviation app::"'a ⇒ ('a ⇒ 'b) ⇒ 'b" ("@_ _")
where "@a F ≡ F a"
lemma "(@a F) = (F a)" by simp (blocks!)
abbreviation swap::"('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'a ⇒ 'c)"
where "swap f ≡ λa b. f b a"
lemma "(swap F) a b = (F b a)" .. (blocks!)
I have been having this problem since many years. It appears every time I
introduce shorthand for function application or the swapping of arguments.
It would be nice (from a DSL designer perspective) to be able to introduce
domain-specific abbreviations for the cases above (and similar ones)
without the overload of constantly having to unfold definitions in proofs.
Best
David
Email Gateway (Feb 12 2023 at 08:35):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi David,
abbreviations are applied both for parsing and pretty-printing of terms. For parsing, your
abbreviations work just fine. Pretty-printing however ends up in an endless loop. Since
abbreviations disappear during parsing, Isabelle's pretty printer tries to fold all
abbreviations again, and the right-hand side of swap can be applied over and over again.
You can declare your abbreviations to be used only for parsing or for pretty-printing
using the input and output modes, respectively. For example, the following should work.
abbreviation (input) app::"'a ⇒ ('a ⇒ 'b) ⇒ 'b" ("@_ _")
where "@a F ≡ F a"
lemma "(@a F) = (F a)" by simp (blocks!)
abbreviation (input) swap::"('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'a ⇒ 'c)"
where "swap f ≡ λa b. f b a"
lemma "(swap F) a b = (F b a)" .. (blocks!)
I'm not sure that this is what you want though; you can write the abbreviations in your
DSL, but you won't see them in the terms that Isabelle displays in the state or output
windows.
Hope this helps,
Andreas
Email Gateway (Feb 12 2023 at 11:11):From: David Fuenmayor <davfuenmayor@gmail.com>
Hi Andreas
This is in fact very helpful, since I always wanted to 'decouple' parsing
and pretty-printing of abbreviations. Thank you!
With hindsight, the endless-folding issue with pretty-printing makes now
total sense. Still, since this literally crashes the system (even if
recoverably), I still think this might be something to have fixed in future
Isabelle releases.
Best
David
Email Gateway (Feb 12 2023 at 14:10):From: Makarius <makarius@sketis.net>
There is nothing broken and nothing to be "fixed".
Theorem proving involves many operations that may not terminate. Here we are
applying a version of the Simplifier to abstract syntax: the "simp" method may
also run into non-terminating situations.
Makarius
Email Gateway (Feb 12 2023 at 14:47):From: David Fuenmayor <davfuenmayor@gmail.com>
I think you misunderstood the bug report.
The problem is not the simplifier or any proof method. As Andreas rightly
noted, the problem seems to be the pretty-printer which crashes the system
with endless folding.
To see why try just replacing in the example I gave the "by simp" by an
"oops" and then move on to proving anything, e.g. "True = True".
abbreviation app::"'a ⇒ ('a ⇒ 'b) ⇒ 'b" ("@_ _")
where "@a F ≡ F a"
lemma "(@a F) = H" oops (dummy whatever stuff)
lemma "True = True" by simp (crash!)
Thanks for the attention
David
Email Gateway (Feb 12 2023 at 18:37):From: Makarius <makarius@sketis.net>
What bug?
Here is an extract from the isar-ref manual:
"""
➧ ⬚‹abbreviation c where eq› introduces a syntactic constant which is
associated with a certain term according to the meta-level equality ‹eq›.
Abbreviations participate in the usual type-inference process, but are
expanded before the logic ever sees them. Pretty printing of terms involves
higher-order rewriting with rules stemming from reverted abbreviations. This
needs some care to avoid overlapping or looping syntactic replacements!
The optional ‹mode› specification restricts output to a particular print
mode; using ‹input›'' here achieves the effect of one-way abbreviations.
The mode may also include an ⬚‹output›'' qualifier that affects the
concrete syntax declared for abbreviations, cf.\ ⬚‹syntax› in
\secref{sec:syn-trans}.
"""
We have some more mechanisms in Isabelle syntax that might not terminate:
'translations'. There could be also severe scalability problems with plain
mixfix grammar, especially in the face of ambiguity.
This might be surprising to users elsewhere, but theorem proving is full of
potential nontermination everywhere.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC