[Texmacs-dev] Formal Proof environment requirements (Draft, RFC)

[Karl Hegbloom]

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 <address@hidden>
Those who do not study Emacs are doomed to edit using CUA key bindings.