The Unix+(X) Jape Interface

Abstract

A Session with Jape

Here we give an account of how you may conduct a Jape session with the small theory of functions and lists supplied with the distribution. Find out where Jape has been installed on your system (we'll call the place $JAPEHOME in what follows). Start Jape in the usual way by giving the shell command

        $JAPEHOME/bin/jape $JAPEHOME/EXAMPLES/functions.jt

After a short time Jape will start to give an account of what it's doing to the terminal window -- look for something along the following lines

Jape: release 3.0b [$JAPEHOME/bin/japeserver]
[OPENING "$JAPEHOME/EXAMPLES/functions.jt"]
[OPENING "$JAPEHOME/EXAMPLES/equality_rules.j"]
[CLOSING "$JAPEHOME/EXAMPLES/equality_rules.j"]
[OPENING "$JAPEHOME/EXAMPLES/equality_menus.j"]
[CLOSING "$JAPEHOME/EXAMPLES/equality_menus.j"]
[OPENING "$JAPEHOME/EXAMPLES/functions_rules.j"]
[CLOSING "$JAPEHOME/EXAMPLES/functions_rules.j"]
[OPENING "$JAPEHOME/EXAMPLES/functions_menus.j"]
[CLOSING "$JAPEHOME/EXAMPLES/functions_menus.j"]
[CLOSING "$JAPEHOME/EXAMPLES/functions.jt"]
Jape Interface Server $JAPEHOME/bin/japeserver
[$JAPEHOME/bin/japeserver.ob]
[Looked for an option file named /users/sufrin/Jape.options]
[Looked for an option file named ./Jape.options]

The Session window:

The Definitions Panel:

The Conjectures Panel:

The Provisos window:

The first thing to do is to place these top-level windows in convenient places on your display. The Session window is the one which is going to require most of your attention. Most of your mouse clicks will be directed at the Definitions and Conjectures panels and the Rules menus from the Session window. (Incidentally, you can use the commands on the File menu to save yourself the trouble of rearranging windows whenever you're going to work again with a theory.)

Selecting a Conjecture to Prove

Move to the Conjectures panel, and select (by clicking on it) a conjecture to prove: the conjecture will be displayed with foreground and background colours reversed.

Once we've selected it, we press that panel's Prove button: this tells Jape that we want to prove the selected conjecture, whereupon the Session window changes to look like this:

The box around the line labelled 1: indicates that our current goal is to prove this conjecture; the ellipsis (...) just above it is intended to indicate that we have to fill in the rest of the proof. In fact the conjecture relates the functions zip, map, and -- which are defined in a theory of cat-lists by the laws

In the absence of any special information relating these functions, the first step we shall take is to use the extensionality rule. We would normally do so by selecting it from the Rules menu in the Session window. But since it's likely that we will be using that menu several times we shall tear it off the menu bar. We do so by clicking on the dotted-line entry at the top of the menu which pops up when we press on the Rules menu button. Shortly after we click on the dotted-line, a new window appears, leaving the session looking something like this

The new window is the Rules menu, and it can be moved around the screen using your X window manager's usual facilities for doing such things. It's a good idea to do that now, because we don't want to obscure our view of the session.

Clicking on the fifth entry on the rules menu invokes the simple extensionality rule, and leaves the proof record looking like this:

We're now going to use the fact that the theory designer has kindly provided a button which will repeatedly unfold subexpressions in the goal which match the left-hand-sides of certain definitions and theorems. We press the Unfold * button on the Conjectures panel, and a few moments later the proof record changes to:

What's happened is that the definitions of composition and have been used to rewrite appropriate subexpressions in our goal. The reason lines 2, 3, and 4 are ``greyed out'' is that they may not themselves be used in the proof of the currently-selected goal, which is labelled 1:. If you deselect the goal (by clicking outside the region of the proof record), then the proof record is coloured uniformly:

Next we'll be using list induction on x. So we text-select (by dragging with the middle button) all instances of x,

If we click on the formula on line 4 of the proof, then all formulae except for the hypotheses which may be used during the proof of that formula) will be greyed-out. Conversely, if we click on one of the hypotheses on line 3, all formulae save those at which the hypothesis is in scope will be greyed out. Try this yourself.

Now let's make a mistake. Select line 4, and one of the hpotheses on line 3 by clicking on them. Now invoke BoolCases from the Rule menu. An error notification pops up, looking something like this:

You can dismiss it by clicking on the -- indeed you must dismiss it before you you can do anything else at all in Jape.

Now deselect everything (by clicking anywhere outside the proof record). Double click on line 1 -- this uses the definition of map to rewrite the right hand side of the equation to the empty list. Now double click again on (the new) line 1, and notice that the leftmost map term on the left hand side has also been reduced to the empty list.

The designer of the theory of functions and lists decided to bind the double click gesture to a Jape tactic which searches the current goal formula for a subterm which matches the left hand side of one of the laws accessible from the search list. The search list is controlled by the menu labelled Searching , which is shown below:

The rules (and conjectures) defined in this theory are grouped by subject. A group's laws are made part of the search list by pressing the appropriate ``enable'' button; they are withdrawn from the search list by pressing the appropriate ``disable'' button. Hypotheses currently in scope are treated as a group for the purposes of this facility.

We're now impatient to finish the proof, so we invoke Unfold * three times -- wating, after each invocation, for the proof record to show what progress has been made. After the third invocation, the proof record looks something like this:

We now need to prove that the lengths of the two lists map F xs and map G xs are the same. We recall that there's a conjecture relating length and map

So we try to transform this goal into that form. We do so by selecting the composition symbol (o) on the Definitions panel, and pressing the Fold button on that panel twice. The interesting part of the proof is now

We can't be bothered proving the conjecture, so we move to the Edit menu and enable the application of Conjectures by pressing Apply both conjectures and theorems.

Next we select

in the Conjectures panel, and press the Unfold button twice. This not only completes the proof of the antecedent of the third rule of the definition of zip, it conceals the detail of this sub-proof from us.

If we wish to, we can reveal the detail by double clicking on the explanation of the line numbered 14, or by selecting the equation on that line and invoking the Expand/Contract detail command on the Edit menu.

There's not much more to do now, and Unfold * can do it all for us. Try it yourself, and see what happens.

Miscellaneous Notes

Finishing a Proof

When the proof you are conducting is finished, you may invoke the Done command on the Edit menu to record it as the ``definitive'' proof of its root sequent. The Done command is greyed out unless the proof really is complete.

Getting Help in a Window

In every Jape window there is an ``information please'' button, which looks something like this

Switching Proofs

You can start a new proof of any conjecture (including one you're in the middle of proving, or one you've already proved) at any stage. Just go to a Conjectures panel, select the conjecture, and press the Prove button on that panel. If there's a proof already active, then that is suspended, and the new conjecture is placed in the session window. The Proof Selection window allows you to switch between the proofs which are currently in progress. When there's a single proof in progress it will look something like this:

when more than one proof is in progress, it will look something like the picture below. You can switch between proofs by pressing the appropriate button, and you can abandon a proof by switching to it, then pressing the Close button.

The Edit Menu

The edit menu (shown below) provides several commands which are commonly used for navigation within a proof.

Documentation for most of these commands can be obtained by clicking on the Edit menu button while holding down a modifier key (Control, Shift, or Meta).

Box/Tree Display Style

these buttons switch between the box style of proof presentation, and the proof tree style. You can switch between these styles whenever you wish. The tree style takes much more real estate.

Automatic/Manual Goal Selection

The user can switch between open goals in a proof at any stage. When automatic goal selection is enabled, Jape suggests a new goal whenever a proof move is made; when manual goal selection is enabled, Jape doesn't presume -- it leaves goal selection to the user.

Apply (both conjectures and theorems / only theorems)

Unproved conjectures may not normally be used in the proof of a conjecture. But when Jape is in the mode established by pressing Apply both conjectures and theorems it relaxes this restriction, and permits unproven conjectures to be used.

Printable proof records

At any stage in the evolution of a proof you can capture the record by invoking the Output printable proof entry on the File menu. This pops up a window which looks something like this

You are being invited to choose the name for a file in which to save a printable version of the Jape proof record which is currently visible in the session. If it's not obvious to you what to do next, then you can always press the button. This results in a scrollable information box appearing, which tells you what you'll need to know.

If you have several proof states to record, then you keep this file selection window alive (don't press cancel). Every time you press the OK button on it, the currently visible proof record is saved in the file whose name is in the File: entry box.

A .pjp file isn't directly printable but it can be used to generate Latex source text for inclusion in a Latex document. The program which performs this magic is $JAPEHOME/bin/jape2tex -- its source (in Standard ML) is also available in the directory $JAPEHOME/Jape2Tex if you wish to generate different forms of output.

Changing Font Sizes

You can change the font sizes in which proofs (and Panel entries) are rendered by using the Sizes control panel -- this is raised by clicking on the Set Font Sizes entry of the File menu. This pops up a window which looks something like the one below: pressing the appropriate ``radio button'' changes the size of the font in the proof session to a point size which approximates the number on the button. It changes the size of the size of the font used in the Panels proportionately. The OHP entry means ``choose a size suitable for projection''.

Leaving Jape

If at any point you want to leave Jape, you can do so by clicking on Close or Quit Jape from the File menu. The Close entry will be greyed out if it really isn't a good idea for you to leave Jape right now, but the Quit Jape entry can always be used.

If there are proofs in progress, or proofs which have been completed since the last time you saved your proofs in this Jape Session, then Jape will pop up the following invitation

Links