     START-INFO-DIR-ENTRY
     * ProofGeneral::Organize your proofs with Emacs!
     END-INFO-DIR-ENTRY

Proof General is a generic Emacs interface for proof assistants. It works ideally under XEmacs, but can also be used with Emacs 19. It is supplied ready-customised for these proof assistants:

  * LEGO Proof General for LEGO Version 1.3.1

     by Thomas Kleymann and Dilip Sequeira

  * Coq Proof General for Coq Version 6.2

     by Healfdene Goguen

  * Isabelle Proof General for Isabelle 98-1

     by David Aspinall

Proof General itself was written by the above with help from Yves Bertot and using ideas from Projet CROAP.

Proof General is suitable for use by pacifists and Emacs lovers alike.

The code is designed to be generic, so you can adapt Proof General to other proof assistants if you know a little bit of Emacs Lisp. Our aim is provide a powerful and configurable Emacs mode which helps user-interaction with interactive proof assistants.

Please help us with this aim! Configure Proof General for your proof assistant, by adding features at the generic level wherever possible. Send ideas, comments, patches, code to proofgen@dcs.ed.ac.uk. Please feel free to download Proof General to customize it for another system, and tell us how you get on.

Introduction
============

A Script Buffer is the primary buffer for developing proof scripts. Its major mode is proof mode. A script buffer is divided into three regions:

  * The Locked region appears in blue (underlined on monochrome displays) and contains commands which have been sent to the proof process and verified. The commands in the locked region cannot be edited.

  * The Queue region appears in pink (inverse video) and contains commands waiting to be sent to the proof process. Like those in the locked region, these commands can't be edited.

  * The Editing region contains the commands the user is working on, and can be edited as normal Emacs text.

These three regions appear in the buffer in the order above; that is, the locked region is always at the start of the buffer, and the editing region always at the end. The queue region only exists if there is input waiting to be sent to the proof process.

Proof mode has two operations which transfer commands between these regions: assertion and retraction. These cause commands to be sent to the proof process. The Process Buffer records the complete communication between the prover and the Script Buffers. Error messages and other important messages are highlighted in the Process Buffer. The current proof obligations (if any) are always visible in the Goals Buffer.

Proof General is generous. It is not a perfect interface and users may occasionaly want to freely interact with the prover without being watched over by the Proof General. Users may interact directly with the prover by entering text in the Process Buffer instead of invoking commands in a Script Buffer. Proof mode supports a variety of means to interact with the prover. Try these first!

Assertion causes commands from the editing region to be transferred to the queue region and sent one by one to the proof process. If the command is accepted, it is transferred to the locked region, but if an error occurs it is signalled to the user, and the offending command is transferred back to the editing region together with any remaining commands in the queue.

Retraction causes commands to be transferred from the locked region to the editing region (again via the queue region) and the appropriate 'undo' commands to be sent to the proof process.

As commands are transferred to the locked region, they are aggregated into segments which constitute the smallest units which can be undone. Typically a segment consists of a declaration or definition, or all the text from a `goal' command to the corresponding `save' command, or the individual commands in the proof of an unfinished goal.  As the mouse moves over the the region, the segment containing the pointer will be highlighted.

Commands in the editing region can be freely edited while commands in the queue are transferred to the proof process. However, assertion and retraction commands can only be issued when the queue is empty.

Proof Mode Commands
===================

C-c C-b
     assert the commands in the buffer.

C-c return
     assert the commands in the editing region up to and including the one containing the point.

C-c u
     retract the segments in the locked region back to and including the one containing the point. If point is outside the *Locked* region, the last segment is undone.

C-c C-u
     retract the last segment in the locked region, and kill the text in it. (Be careful with this, as it may delete more than you anticipate. However, you can always recover the killed text using Emacs Undo.)

C-c '
     move the point to the end of the locked region.  If you are in a script buffer other than the active scripting buffer, this will also transfer you to the active one.

C-c C-e
     move the point to the next terminator

C-c C-p
     display the proof state in the goals buffer

C-c c
     display the context in the process buffer

C-c h
     print proof-system specific help text in the process buffer

C-c C-c
     interrupt the process. This may leave script management or the proof process (or both) in an inconsistent state.

C-c C-z
     move the end of the locked region backwards to the end of the segment containing the point.  (Don't try this one at home, kids.)

C-c C-t
     Send the command at the point to the subprocess, not recording it in the locked region.  (This is supplied in order to enable the user to test the types and values of expressions. There's some checking that the command won't change the proof state, but it isn't foolproof.)

C-c C-v
     Request a command from the minibuffer and send it to the subprocess. Currently no checking whatsoever is done on the command.

The command proof-restart-script can be used to completely restart script management.

Multiple Files
==============

Proof mode has a rudimentary facility for operating with multiple files in a proof development. This is currently only supported for LEGO. If the user invokes script management in a different buffer from the one in which it is running, one of two prompts will appear:

  * ``Steal script management?'' if Emacs doesn't think the file is already part of the proof development

  * ``Reprocess this file?'' if Emacs thinks the file is already included in the proof process. If the user confirms, Emacs will cause the proof process to forget the contents of the file, so that it is processed afresh.

Currently this facility requires each script buffer to have a corresponding file.

When working with script management in multiple buffers, it is easy to lose track of which buffer is the current script buffer. As a mnemonic aid, the word Scripting appears in the minor mode list of the active scripting buffer.

Caveats:

  - Note that if processing a buffer causes other files to be loaded into the LEGO process, those files will be imported from disk rather than from any Emacs buffer in which it is being edited, i.e. if your file is going to be included indirectly, save it.

  - However much you move around the file system in Emacs, the LEGOPATH will be the LEGOPATH you started with. No concept of "current directory" is currently supported.

An Active Terminator
====================

Proof mode has a minor mode which causes the terminator to become active. When this mode is active, pressing the terminator key (; for LEGO, . for Coq) outside a comment or quote will cause the character to be entered into the buffer, and all the commands in the editing region up to the point to be asserted.

This mode can be toggled with the command `proof-active-terminator-minor-mode' (C-c ; or C-c .)

Proof by Pointing
=================

This mode is currently very unreliable, and we do not guarantee that it will work as discussed in this document.

Proof by pointing is a facility whereby proof commands can be generated by using the mouse to select terms. When proving a goal, a summary of the current proof state will appear in the goals buffer. By moving the mouse over the buffer, the structure of the goal and hypothesis terms will be shown by highlighting.

If a selection is made using the second (usually the middle) mouse button, Emacs will generate the appropriate commands, insert them in the script buffer, and send them to the proof process. These commands are aggregated in the locked region as a single segment, so that a mouse-generated command sequence can be retracted with a single retraction command.

Further Information about proof by pointing may be found in the paper User Interfaces for Theorem Provers by Yves Bertot and Laurent Thery, to appear in Information and Computation, from which the following example is taken.

Suppose we wish to prove the lego term:

     (((p a) \/ (q b))  /\ {x:Prop}(p x) -> (q x)) -> (Ex ([x:Prop] q(x)));

Asserting this goal will result in the proof state

     ?0 : ((p a \/ q b) /\ {x:Prop}(p x)->q x)->Ex ([x:Prop]q x)

appearing in the goals buffer. Suppose our strategy is to use a case analysis on the disjunction, starting with the p(a) subterm. Clicking on this term will cause script management to insert the following command sequence in the script buffer, and execute it.

     Intros H; Refine H; Intros H0 H1;
     Refine or_elim H0 Then Intros H2; Try Refine H2;

The goals buffer will then read

       H : (p a \/ q b) /\ {x:Prop}(p x)->q x
       H0 : p a \/ q b
       H1 : {x:Prop}(p x)->q x
       H2 : p a
       ?10 : Ex ([x:Prop]q x)

Clicking on the subterm (p x) in the hypothesis H1 will instruct script management to prove an instance of (p x) and deduce the corresponding (q x). The commands

     allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption;

are inserted and executed, leaving the proof state as

       H : (p a \/ q b) /\ {x:Prop}(p x)->q x
       H0 : p a \/ q b
       H1 : {x:Prop}(p x)->q x
       H2 : p a
       H3 : (p a)->q a
       ?20 : (q a)->Ex ([x:Prop]q x)

Now clicking on the q x) subterm in ?20 will prove the subgoal. We are left with the other half of the original case analysis:

       H : (p a \/ q b) /\ {x:Prop}(p x)->q x
       H0 : p a \/ q b
       H1 : {x:Prop}(p x)->q x
       H2 : q b
       ?26 : Ex ([x:Prop]q x)

Clicking on q x proves the goal.

A Walkthrough
=============

Here's a LEGO example of how script management is used.

First, we turn on active terminator minor mode by typing C-c ; Then we enter

`Module Walkthrough Import lib_logic;'

The command should be lit in pink (or inverse video if you don't have a colour display).  As LEGO imports each module, a line will appear in the minibuffer showing the creation of context marks. Eventually the command should turn blue, indicating that LEGO has successfully processed it. Then type (on a separate line if you like)

Goal bland_commutes: {A,B:Prop} (and A B) -> (and B A);

The goal should be echoed in the goals buffer.

Intros;

Whoops! C-c C-u to pretend that didn't happen.

intros; andI;

A proof summary will appear in the goals buffer. We could solve the goal by pointing now, but we'll stay with the keyboard.

Refine H; intros; Immed; Refine H; intros; Immed;

finishes the Goal.

Save bland_commutes;

Moving the mouse pointer over the locked region now reveals that the entire proof has been aggregated into a single segment. Suppose we decide to call the goal something more sensible. Moving the cursor up into the locked region, somewhere between `Goal' and `Save', we enter C-c u.  The segment is transferred back into the editing region. Now we correct the goal name, move the cursor to the end of the buffer, and type C-c return.  Proof mode queues the commands for processing and executes them.

LEGO mode
=========

LEGO mode is a mode derived from proof mode for editing LEGO scripts. There are some abbreviations for common commands, which add text to the buffer:

C-c i
     intros

C-c I
     Intros

C-c R
     Refine

Coq mode
========

Coq mode is a mode derived from proof mode for editing Coq scripts. As well as custom popup menus, it has the following commands:

C-c C-s
     search for items in the library of a given type.  This runs the Search command of Coq.

In addition, there are some abbreviations for common commands, which add text to the buffer:

C-c I
     Intros

C-c a
     Apply

Known Problems
==============

Since Emacs is pretty flexible, there are a whole bunch of things you can do to confuse script management. When it gets confused, it may become distressed, and may eventually sulk. In such instances proof-restart-script-management may be of use.

A few things to avoid:

  - If you're using script management with multiple files, don't start changing the file names.

  - Script Management doesn't understand how to undo Discharge commands in LEGO, and any attempts it makes to do so may leave it in an inconsistent state. If you're undoing the effects of a Discharge command, retract back to the declaration of whatever gets discharged.

  - Proof by Pointing doesn't work very well, and is inefficiently implemented.

  - The locked and queue regions are not quite read-only: in particular Emacs Undo can insert text into them.

  - When a LEGO import command fails, the created "Mark" is not forgotten, and the proof process thinks the file has been included. So if you assert the command again, it will probably be accepted by LEGO, because the relevant mark is in the namespace.

Fixes for some of these may be provided in a future release.

Internals
=========

Granularity of Atomic Commands
------------------------------

The *Locked* region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of atomic sequences of commands (ACS). Retraction is supported to the beginning of every ACS. By default, every command is an ACS. But the granularity of atomicity can be adjusted for different proof assistants. This is essential when arbitrary retraction is not supported. Usually, after a theorem has been proved, one may only retract to the start of the goal. One needs to mark the proof of the theorem as an ACS.

proof-atomic-sequents-list
     is a list of instructions for setting up ACSs. Each instruction is a list of the form (END START &optional FORGET-COMMAND). END is a regular expression to recognise the last command in an ACS. START is a function. Its input is the last command of an ACS. Its output is a regular expression to recognise the first command of the ACS. It is evaluated once and the output is successively matched against previously processed commands until a match occurs (or the beginning of the current buffer is reached). The region determined by (START,END) is locked as an ACS. Optionally, the ACS is annotated with the actual command to retract the ACS. This is computed by applying FORGET-COMMAND to the first and last command of the ACS.

Handling Multiple Files
-----------------------

Large proof developments are typically spread across multiple files. Many provers support such developments by keeping track of dependencies and automatically processing scripts. Proof General supports this mechanism.

However, the prover must let the Proof General know whenever it processes a file directly. Such files are being marked by Proof General as having been processed by an atomic action (regardless of whether an error occurs or not). The file can then only be edited after retracting to the beginning of the file.

When retraction is requested in a buffer which is not the current script, Proof General duely retracts in this buffer. It then arranges a little conference with the prover to find out which other files have also been retracted. With this strategy, Proof General doesn't have a hard time to keep track of dependencies.

Proof General considers OUTPUT delimited by the the two regualar expressions proof-shell-eager-annotation-start and proof-shell-eager-annotation-end as being important. It displays the OUTPUT in the Response buffer and analyses their contents further. Among possibly other important messages characterised by these regular expressions, the prover must tell the interface whenver it processes a file and retracts across file boundaries.

proof-included-files-list
     records the file history. Whenever a new file is being processed, it gets added to the front of the list. When the prover retracts across file boundaries, this list is resynchronised. It contains files in canonical truename format see Truenames (lispref).

proof-shell-process-file
     is either nil or a tuple of the form (REGEXP, FUNCTION). If REGEXP matches a substring of STR, then the function FUNCTION is invoked with input STR. It must return a script file name (with complete path) the system is currently processing. In practice, FUNCTION is likely to inspect the match data. See Match Data (lispref). Care has to be taken in case the prover only reports on compiled versions of files it is processing. In this case, FUNCTION needs to reconstruct the corresponding script file name. The new (true) file name is added to the front of proof-included-files-list.

proof-shell-retract-files-regexp
     is a regular expression. It indicates that the prover has retracted across file boundaries. At this stage, Proof General's view of the processed files is out of date and needs to be updated with the help of the function proof-shell-compute-new-files-list.

proof-shell-compute-new-files-list
     Takes as argument the current output of the prover. It needs to return an up to date list of all processed files. Its output is stored in proof-included-files-list. In practice, this function is likely to inspect the previous (global) variable proof-included-files-list and the match data see Match Data (lispref) triggered by proof-shell-retract-files-regexp.

Adding Support for a New Proof Assistant
----------------------------------------

Suppose your new assistant is called myassistant.

  - Make a directory called 'myassistant' under the Proof General home directory, to put the specific customization and associated files in.

  - Add a file myassistant.el to the new directory.

  - Edit proof-site.el to add a new entry to the PROOF-INTERNAL-ASSISTANTS-TABLE variable.  The new entry should look like this:

     (myassistant "My New Assistant" "\\.myasst$")

     The first item is used to form the name of the internal variables for the new mode as well as the directory and file where it loads from.  The second is a string, naming the proof assistant. The third item is a regular expression to match names of proof script files for this assistant.  See the documentation of PROOF-INTERNAL-ASSISTANTS-TABLE for more details.

  - Define the new modes in myassistant.el, by looking at the files for the currently supported assistants for example. Basically you need to define some modes using define-derived-mode and set the configuration variables.  You could begin by setting a minimum number of the variables, then adjust the settings via the customize menus, under Proof-General -> Internals.

Literature
----------

The current version supports Script Management as documented in:

  * Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. To appear in Journal of Symbolic Computation.

It has the beginnings of support for Proof by Pointing, as documented in:

  * Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286