Proof Views

Introduction

The Proof Views macro package is designed to allow you to write a structured calculational proof as a single file in HTML + some special macros for the proof bits. The macros then generate every possible view of the proof and make hyperlinks between them. The result is proof whose structure can be browsed using an ordinary web browser. Its a simple, light-weight concept.

To get started you will need to download ProofViews.

Proof Document Format

Essentially your proof file is an ordinary HTML file, but you can also embed browsable derivations in it. All derivations must be set between the following two strings:

_begin(derivation)

and

_end(derivation)

Between these markers you can write any of the following commands, each of which generates a line of proof. (You can substitute any text you want, including HTML mark up, for the things in italics.)

_assum(assumption)

Use this command for setting an assumption.

_focus(expression)

Use this command for setting a focus, an expression which is a step in the proof.

_trans(relation,comment)

Use this command for setting a transformation. You give the relation preserved by the transformation and some comment on it.

_comm(comment)

Use this command for setting a comment.

Note: Since the ","(comma) is used to separate parameters to these commands, you must use the special command "_," if you actually want to place a real comma in the text output by these commands.

Subderivations

You can also include subderivations in your derivations. Subderivations are derivations enclosed between the following markers:

_begin(win)(relation,comment)

and

_end(win)

For each subderivation you provide the relationship preserved by the subderivation and a comment that describes it. The Proof Views package will generate two difference views of each subderivation. One view has the subderivation "closed", in which case it appears as a single line transformation. The other view has the contains the entire subderivation indented one step. Hyperlinks are placed between the two views so that you can move between them with a web browser.

One typical thing you might do with a subderivation transform some subexpression of a focus. In such cases, it is nice to be able to mark the subexpression that is to be transformed in the focus before the subderivation. To do this, just enclose the subexpression with the "open" macro, and it will be marked appropriately.

_open(expression)

Similarly, you can use "close" to mark the subexpression that was transformed in a focus immediately following a subderivation.

_close(expression)

Note: Sometimes you might want to add your own hyperlinks to move around within a proof document. This could be a problem because your document is no longer a single HTML file, but a family of related file, each giving a different view of the overall document. To overcome this the macro "_this" can be used in your document, it will expand out to the URL of the current view of the document. By suffixing this macro with anchor marks you can make links that move around within the current view of a document.

Example

The following is a small example of a browsable proof:

A ==> A \/ B

<A>

A ==> true

This proof was generated by the following macros:

_begin(derivation)
  _focus(A ==> _open(A \/ B))
  _begin(win)(=,Assuming the hypothesis_, 
                we can simplify the consequent.)
    _assum(A)
    _focus(A \/ B)
    _trans(=,Replace A with true_, 
             since it is an assumption.)
    _focus(true \/ B)
    _trans(=,Boolean simplification.)
    _focus(true)
  _end(win)
  _focus(A ==> _close(true))
  _trans(=,Boolean simplification.)
  _focus(true)
_end(derivation)

Bugs

No error checking is performed at the moment. If you make an error in your macros, the package will just generate garbage for output.