Re: [isabelle] how to set "brackets" mode



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

On 20/12/2016 19:31, Makarius wrote:
On 20/12/16 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.

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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.