Email Gateway (Aug 22 2022 at 14:40): Email Gateway (Aug 22 2022 at 14:40):From: Lawrence Paulson <lp15@cam.ac.uk>
People often ask how to enable the [| ... |] ==> output, which many find more readable than the default. It’s certainly my preference.
To do this, open the Plugin Options panel and type the word “brackets” into Print Mode as shown.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:41):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/12/2016 12:52, Lawrence Paulson wrote:
People often ask how to enable the [| ... |] ==> output, which many find more readable than the default. It’s certainly my preference.
Some students recently asked me about it, too.
Tobias
To do this, open the Plugin Options panel and type the word “brackets” into Print Mode as shown.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:41):From: Makarius <makarius@sketis.net>
Can you explain this? Or is it just due to habits and nostalgy?
The uniform notation of nested ==> goes back to 1998, when Isar concepts
were emerging, with some consequences on Pure. E.g. it became possible
to work with nested rules routinely. Before, rules were mostly flat and
the bracketed notation was adequate. Afterwards, I found nested rules
with brackets very cumbersome to read and to write, and eventually
stopped doing that. Since Isabelle/jEdit is shipped with defaults for
Isar, this print mode also changed approx. 5 years ago.
Note that plain currying (for => and ==>) without any special notational
tricks has the advantage that the depth of nesting is immediately
visible by the parentheses around complex items. This visual clue is
absent in bracket notation (which is better for long lists of flat items).
Moreover, typing [| |] is almost impossible on a non-English keyboard. I
usually prefer input and output to coincide as much as feasible. I
cannot imagine anybody with a German keyword to prefer these special
brackets.
Another reason from 1998: many people not familiar with Isabelle asking
in presentations "What are these semantic brackets? What are these
semicolons?" Any also: What are these question-mark variables?".
Typical introductions to Isabelle talk about programming language
semantics (even until today, e.g. the "Concrete Semantics" book), so it
looks very odd to me to construct an artificial conflict with standard
notation of semantic brackets and sequential composition. Such
applications then require double semicolons (Or maybe bold ones?). We
have managed to get rid of semicolons in outer syntax some years ago
(making them free for sequential composition of proof methods), so maybe
we can one day do the same for inner syntax.
I have actually started using "if" and "for" notation for the clauses in
inductive definitions, especially in introductions to Isabelle. The
postfix notation is like in Prolog (what most people already know) and
the keywords "if" and "for" look self-explanatory. That Isar rule
notation with semantic brackets and semicolons in their conventional
meaning could make a difference for didactic purposes.
Back to occasional complaints about iterated ==> in output. My
impression is that most people talk about goal state output, not rule
output. Today, there is no particular reason why the outer subgoal
structure should be printed with !! / ==> at all. It could be done in
some Isar notation, either fix/assume/show or show/if/for. Moreover it
could be done in a way that makes it easy to copy-paste (or "sendback")
the result into the emerging Isar proof text.
Also note that the ASCII notation of ==> used to have special
line-breaks for pretty printing, maybe to require less space when it is
iterated. Just as historic accident, the symbolic notation ⟹ was lacking
that: it was introduced as plain infixr in
http://isabelle.in.tum.de/repos/isabelle/rev/9dd06eeda95c -- maybe by
accident.
When the default officially changed from ASCII to symbols recently, I
also changed the special formatting of ==> to plain infixr (see
http://isabelle.in.tum.de/repos/isabelle/rev/301833d9013a#l3.77). I
simply did not dare to ask what is the right way to print the long
arrow notation, after everybody got used to the presumably wrong way in
so many years of Isabelle symbols usage (both in the user interface and
in LaTeX output).
Maybe we should just recover that line-breaking for both the ASCII and
symbolic double-arrow? It could make a difference for screen display,
but also cause surprises in LaTeX documents that are tweaked for a
particular layout.
Makarius
Email Gateway (Aug 22 2022 at 14:41):From: Lawrence Paulson <lp15@cam.ac.uk>
Different people have different preferences, of course. For me, it is precisely the nesting that makes a clearly bracketed notation preferable. A flat list like [a,b,c,d,e,f,g] is no less readable if written as a::b::c::d::e::f::g::nil. But consider [a,[b,c],[d,e],[f,g]].
Also, with large formulas, it isn’t always clear whether … ==> A is the conclusion or just another premise.
Larry
Email Gateway (Aug 22 2022 at 14:41):From: Tobias Nipkow <nipkow@in.tum.de>
My (and my students') preference for "brackets" concerns mostly the printing of
the proof state. Indeed, part of the problem may be due to the infixr directive
which leads to displays such as this.
1. (A ⟹ B) ⟹
(B ⟹ C) ⟹
(C ⟹ D) ⟹
(E ⟹ F ⟹ G) ⟹ (A ⟹ B) ⟹ (B ⟹ C) ⟹ (C ⟹ D) ⟹ (E ⟹ F ⟹ G) ⟹ A
I agree with Larry that lots of arrows make it harder to grasp the structure. I
think this is related to the fact that mathematicians write A & B ==> C rather
than A ==> B ==> C.
I am not fixated on the brackets format per se. Something like the suggested
fix/assume/show or show/if/for format may be a decent alternative. It would also
clearly separate assumptions from conclusion.
In the end, it is not clear to me what the optimal format is. AFAIK, in Coq each
assumption is on a separate line. I wonder how well that works if there are many
assumptions. Conversely, with "brackets" you get a very compact representation,
which can be hard to read because all the assumptions merge into one.
Jasmin asked students from a course of his (who had previous exposure to Coq)
which output format they preferred and the majority said Coq. Of course there
are many factors at work here.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:00):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/12/2016 12:52, Lawrence Paulson wrote:
People often ask how to enable the [| ... |] ==> output, which many find more readable than the default. It’s certainly my preference.
To do this, open the Plugin Options panel and type the word “brackets” into Print Mode as shown.
One more thing, in case you have installed Isabelle2016-1 from scratch: you also
need to tick the "Proof state" box to see the proof state in the output window.
It is disabled by default now.
Tobias
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC