1. (A â B) â (B â C) â (C â D) â (E â F â G) â (A â B) â (B â C) â (C â D) â (E â F â G) â AI 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
Description: S/MIME Cryptographic Signature