I'm writing proofs in my mathematical studies, and have learned of a structured formal proof typesetting layout invented by Leslie Lamport, of LaTeX fame. (See his paper, "How to Write a Proof", on-line.) I like the format, and want to use it in TeXmacs, since I agree with his assessment regarding the ambiguity and step-skipping inherent in human-language prose presentations of mathematical proofs.
Often the mathematician will have something in mind that never makes it to paper, and a step will be skipped in a proof. He'll get interrupted, and come back later to finish, and find that he's lost track of what he had in mind, or will re-form the not-quite-right thing, and ultimately produce an incorrect proof. This is quite devastating, since all potential future results based on that particular proof are thus placed in jeopardy. In experimenting with existing TeXmacs (1.0.6) features, attempting to re-create Mr. Lamport's proof format by hand, I learned several things that may be of interest to others, as well as to anyone with sufficient skills to implement an environment for writing that style of proof in TeXmacs. I would like to create or help create it, time permitting. We can co-ordinate here, on this list. I want to have the mathematics on the left and the justification comments out to the right, left justified against some tab stop or absolute position relative to the right or left hand margin. I could not find any way to create such a tab stop in TeXmacs. M-Tab shoves the comment all the way over to the right margin, leaving it left-ragged. The only way that I could get it to do something like what I wanted was to create a table. The first try, I wrote the proof in a multi-column table wrapped by a display-math environment, hand numbering the lines of the proof. When it came time to indent a sub-proof, however, I had difficulty. Perhaps a sub-table would have worked; I did not try that. At some point, I had to insert a new row for something, and had to renumber the proof by-hand. That is error prone, since it's easy to miss changing a line number in a justification comment, rendering the proof ostensibly invalid. Since the justification comment refers to the previous lines of the proof that are used by the named deduction rule, it is important that they continue to refer to the correct line of the proof. On the second try, just for further exploration, I made a two column one row table inside of a display-math environment, and then made the first cell have multi-paragraph hyphenation. Inside of it, I put a numbered list, and started writing the proof. It did not work well because then the comments do not follow along when a new item is inserted into the list---they were not tree-attached to the line they belong with. What I really want is a special kind of outline editor, where the numbered list items can be moved up and down, in a level or out a level, at will. OpenOffice.org has such a feature, and it's fairly natural to use and very nice. You can move a list item up or down with C-arrow, and move it down or up an outline level with Tab and Shift-Tab. I bet I'm not the only one who would like to see that feature in the TeXmacs list environments. For the structured formal proof environment, I'd like to have each line be able to move up, down, in, or out like that, and for any numbering to automatically renumber when the lines move. In the comment area, there should be a key binding that starts a reference to a proof line, reserving \ref for references to explicitly placed document labels. The lines of the proof should be hiddenly and automatically \label in some way so that pushing the key and then typing the number, as you see it on your screen, without knowing the hidden label string, will do the right thing. The implementation will require a simple parser. Another nice thing that you can do in OpenOffice.org is that you can set a tab stop, and start text at that tab. Later, you can drag the tab stop, and all text aligned on it will also move... Well, having just tried that, I can see that it does not really work the way I expected it to. It seems to keep a different tab-stop setting for each line of a numbered list, rather than one for the entire list. Setting a tab stop should operate on the entire enclosing environment. When set for the outermost list in a nested list environment, the tab stops should propagate inward to all of the sublists, so that all sublists can have comment columns along the same vertical line. For generality, perhaps they should be over-ride-able in inner lists, removing or adding them there as required. Of course, a tab stop should be use-able from within a macro, and like table size, etc, it should be possible to make it non-user-adjustable if requested by the macro author. Of course it would probably also be useful in an 'align' and 'gather' environment. I'd like to put the pointer there and say "put a tab stop here", with a measurement showing in the status area. I'd also like to be able to type a shortcut character (something-&) or hybrid command, have it be invisible, but set a tab stop that I can jump to lower down by activating some key binding (perhaps M-;, as in Emacs, for hanging comments). Within the structured proof writing environment, it should automatically mark justification comments that refer to a line of the proof (or a previous proof theorem?) that has been modified since the comment was written. That way, when you edit a previous line, it flags the lines that depend on it, so you can recheck your proof to be sure you have not altered the meaning or validity in the wrong way. This feature would be useful, in general, since the similar thing can happen any time you are referring to a previous document element. It would be nice to have the editor help you keep track of potential dependency cascades in that fashion, ala VisiCalc. Having not yet studied the Coq proof assistant, I have no way of knowing, at this point, whether there's going to ever be any useful way of tying it into this proposed proof-writing environment for TeXmacs. It will be another day before I can attempt to grok that all. What I've come up with so far, using existing features and writing the markup by-hand, is to make a list, and on each line there is a two-column table. The first cell is .66par wide, the second is .33par. Inside the first cell is a $math$ with display mode set. I have to fix up the numbering by hand when I check the proof. A simpler way is to just use the space bar to push the comments off to the right, but then they don't line up exactly, and it doesn't look as professional as it must. We are, after all, mathematicians, new and newer. Any ideas? -- Karl Hegbloom <[EMAIL PROTECTED]> Those who do not study Emacs are doomed to edit using CUA key bindings. _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
