Proof General is a generic Emacs interface for proof assistants. It works ideally under XEmacs 20.4, but can also be used with Emacs 19.34. 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

     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.  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
=========

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

Proof General is laid back concerning multiple file developments. It relies on the prover to tell it whenever the prover processes files. A buffer corresponding to such a file is immediately marked as processed. The list of all processed files is also kept in a table so that files which get loaded in Emacs at a later stage can be handled correctly.

Processing Files
................

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 minibuffer 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.

The variable proof-shell-process-file is a tuple of the form (REGEXP, MATCH). If REGEXP matches OUTPUT, then the MATCH match must match the file name (with complete path) the system is currently processing. See Match Data (lispref)

Recording File History
......................

The variable

proof-included-files-list
     records the file history. It contains an acyclic graph. The nodes are strings (canonical file names). An edge from node n1 to node n2 indicates that n1 depends on n2. n1 is the child, n2 is a parent.

The variable proof-included-files-list should not be modified directly. Instead use one of the following methods:

proof-include-files-list-init
     Initialises proof-included-files-list with an empty graph.

proof-include-files-list-add
     Adds FILE to the history of processed files. Its optional argument PARENTS specifies all direct dependencies. It PARENTS is nil, FILE is assumed to be top level.

proof-include-files-list-parents
     Returns a list of parents for the argument CHILD.

proof-include-files-list-remove
     Removes FILE and all its children from the record.

proof-include-files-list-in-p
     Returns t if FILE has already been processed and nil otherwise.

Parent Script Buffers
.....................

Parent Script Buffers are script buffers which have already been processed. If retraction is requested on such a BUFFER, retraction is first propagated to BUFFER's children.

Processing a New File
.....................

When the prover reports that a new file is being processed, it needs to be added to the variable proof-included-files-list with the help of the function proof-include-files-list-add. Dependencies are computed with the help of:

proof-files-query-dependencies-command
     Command to send to the prover to query the direct parents of %s. The string %s is a placeholder for the file in question. If it is nil, we assume that files are processed in linear order.

proof-files-query-dependencies-response-regexp
     Regular expression to catch that the prover has complied with a request to display dependencies for a particular FILE. proof-files-query-dependencies-response-regexp may contain %s as a placeholder for FILE.

The result is analysed with the help of the function

proof-files-query-dependencies-extract-parents
     Returns the list of direct parents for the argument FILE by analysing the previous output of the prover which triggered proof-files-query-dependencies-response-regexp

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

Suppose your new assistant is called myassistant.

  - Make a directory myassistant to put the specific customization and associated files in,  called myassistant

  - Add a file myassistant.el to the new directory, and a customization group: (defcustom myassistant-settings nil "Customization of MyAssistant specifics for Proof General." :group 'proof-general)

  - Define the derived modes for the new assistant:

  - Edit proof-site.el to add a new case to the 'proof-general-supported-assistants' variable

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