path: root/doc/ProofGeneral.texi

\input texinfo   @c -*-texinfo-*-
@c
@c $Id$
@c
@c %**start of header
@setfilename ProofGeneral.info
@settitle Proof General Version 2.0
@paragraphindent 0
@c %**end of header

@ignore
@ifinfo
@format
START-INFO-DIR-ENTRY
* ProofGeneral::Organize your proofs with Emacs!
END-INFO-DIR-ENTRY
@end format
@end ifinfo
@end ignore

@setchapternewpage odd

@titlepage
@sp 10
@comment The title is printed in a large font.
@center @titlefont{Proof General Version 2.0}
@sp 2
@center Organise your proofs with Emacs!
@sp 2
@center D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira
@sp 1
@center LFCS Edinburgh


@c The following two commands start the copyright page.
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1997, 1998 Proof General team, LFCS Edinburgh
@end titlepage


@node Top, Introduction, (dir), (dir)
@comment node-name, next,          previous, up

@b{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:

@itemize @bullet
@item 
@b{LEGO Proof General} for LEGO Version 1.3.1@*
by Thomas Kleymann and Dilip Sequeira
@item 
@b{Coq Proof General} for Coq Version 6.2@*
by Healfdene Goguen
@item 
@b{Isabelle Proof General} for Isabelle@*
by David Aspinall
@end itemize

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.

@menu
* Introduction::                
* Commands::                    
* Multiple Files::              
* An Active Terminator::        
* Proof by Pointing::           
* Walkthrough::                 
* LEGO mode::                   
* Coq mode::                    
* Known Problems::              
* Internals::  
* Variable Index::
* Function Index::
* Concept Index::                 
@end menu


@node Introduction, Commands, Top, Top
@comment node-name, next,          previous, up
@unnumberedsec Introduction

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

@itemize @bullet
@item The @emph{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.

@item The @emph{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.

@item The @emph{Editing} region contains the commands the user is working
on, and can be edited as normal Emacs text.
@end itemize

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 @emph{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 @emph{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 @emph{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!



@cindex Assertion
@strong{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.  

@cindex Retraction
@strong{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.

@node Commands, Multiple Files, Introduction, Top
@unnumberedsec Proof Mode Commands

@table @kbd

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

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

@item 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.

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

@item 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.

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

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

@item C-c c
display the context in the process buffer

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

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

@item C-c C-z
move the end of the locked region backwards to the end of the segment
containing the point. @footnote{Don't try this one at home, kids.}

@item C-c C-t
Send the command at the point to the subprocess, not
recording it in the locked region. @footnote{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.}

@item 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.
@end table

The command @code{proof-restart-script} can be used to completely
restart script management.


@node Multiple Files, An Active Terminator, Commands, Top
@unnumberedsec 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:

@itemize @bullet
@item ``Steal script management?'' 
if Emacs doesn't think the file is already part of the proof development
@item ``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.
@end itemize

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 @samp{Scripting} appears in the minor mode list of the
active scripting buffer.

Caveats:
@itemize @minus
@item 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.

@item 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.
@end itemize

@node An Active Terminator, Proof by Pointing, Multiple Files, Top
@unnumberedsec 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 (@kbd{;}
for LEGO, @kbd{.} 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' (@kbd{C-c ;} or @kbd{C-c .})

@node Proof by Pointing, Walkthrough, An Active Terminator, Top
@unnumberedsec Proof by Pointing

@emph{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
@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent
Thery, to appear in @cite{Information and Computation}, from which
the following example is taken.

@menu
* Proof by Pointing Example::          An example using proof by pointing
@end menu

@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing

Suppose we wish to prove the lego term:

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

Asserting this goal will result in the proof state

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

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

@example
Intros H; Refine H; Intros H0 H1; 
Refine or_elim H0 Then Intros H2; Try Refine H2; 
@end example


The goals buffer will then read 

@example
  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)
@end example

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

@example
allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption;
@end example

are inserted and executed, leaving the proof state as

@example
  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)
@end example

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

@example
  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)
@end example

Clicking on @samp{q x} proves the goal.




@node Walkthrough, LEGO mode, Proof by Pointing, Top
@unnumberedsec A Walkthrough

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

First, we turn on active terminator minor mode by typing @kbd{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)

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

The goal should be echoed in the goals buffer.

@samp{Intros;}

Whoops! @kbd{C-c C-u} to pretend that didn't happen.

@samp{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.

@samp{Refine H; intros; Immed; Refine H; intros; Immed;}

finishes the Goal. 

@samp{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
@kbd{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 @kbd{C-c return}.  Proof mode queues the commands for
processing and executes them.

@node LEGO mode, Coq mode, Walkthrough, Top
@unnumberedsec 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:

@table @kbd
@item C-c i   
intros
@item C-c I   
Intros
@item C-c R   
Refine
@end table


@node Coq mode, Known Problems, LEGO mode, Top
@unnumberedsec 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:

@table @kbd

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

@end table

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

@table @kbd
@item C-c I   
Intros
@item C-c a
Apply
@end table

@node Known Problems, Internals, Coq mode, Top
@unnumberedsec 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
@code{proof-restart-script-management} may be of use.

A few things to avoid: 

@itemize @minus
@item If you're using script management with multiple files, don't start
changing the file names.

@item Script Management doesn't understand how to undo @code{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 @code{Discharge}
command, retract back to the declaration of whatever gets discharged.

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

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

@item 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.
@end itemize

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

@node Internals, Variable Index, Known Problems, Top
@comment  node-name,  next,  previous,  up
@unnumberedsec Internals

@menu
* Handling Multiple Files::     
* Adding New Proof Assistant::  
* Literature::                  
@end menu

@node Handling Multiple Files, Adding New Proof Assistant, Internals, Internals
@comment  node-name,  next,  previous,  up
@unnumberedsubsec 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. 

@menu
* Processing Files::            
* Recording File History::      
* Parent Script Buffers::       
* Processing a New File::       
@end menu

@node Processing Files, Recording File History, Handling Multiple Files, Handling Multiple Files
@comment  node-name,  next,  previous,  up
@unnumberedsubsubsec Processing Files

@vindex proof-shell-eager-annotation-start
@vindex proof-shell-eager-annotation-end

Proof General considers @var{output} delimited by the the two regualar
expressions @code{proof-shell-eager-annotation-start} and
@code{proof-shell-eager-annotation-end} as being important. It displays
the @var{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. 

@vtable @code
@item proof-shell-process-file
is a tuple of the
form (@var{regexp}, @var{match}). If @var{regexp} matches @var{output},
then the @var{match} must match the file name (with complete path)
the system is currently processing. @inforef{Match Data,,lispref}
@end vtable

@node Recording File History, Parent Script Buffers, Processing Files, Handling Multiple Files
@comment  node-name,  next,  previous,  up
@unnumberedsubsubsec Recording File History

The variable

@vtable @code
@item proof-included-files-list
records the file history. It contains an (acyclic) directed graph.
Besides the @samp{'root}, nodes are strings (canonical file names). An
edge from node @samp{n1} to node @samp{n2} indicates that @samp{n2}
depends on @samp{n1}. @samp{n2} is the child, @samp{n1} is a parent.
@end vtable

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

@ftable @code
@item proof-include-files-list-init
Initialises @code{proof-included-files-list} with an empty graph.

@item proof-include-files-list-add 
Adds @var{file} to the history of
processed files. Its optional argument @var{parents} specifies all
direct dependencies. It @var{parents} is nil, @var{file} is assumed to
be top level. 

@item proof-include-files-list-parents
Returns a list of parents for the argument @var{child}.

@item proof-include-files-list-remove
Removes @var{file} and all its children from the record.

@item proof-include-files-list-in-p
Returns @samp{t} if @var{file} has already been processed and nil otherwise.
@end ftable

@node Parent Script Buffers, Processing a New File, Recording File History, Handling Multiple Files
@comment  node-name,  next,  previous,  up
@unnumberedsubsubsec Parent Script Buffers
@cindex Parent Script Buffer

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

@node Processing a New File, ,Parent Script Buffers, Handling Multiple Files
@comment  node-name,  next,  previous,  up
@unnumberedsubsubsec Processing a New File

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

@vtable @code
@item proof-files-query-dependencies-command
Command to send to the prover to query the direct parents of @samp{%s}.
The string @samp{%s} is a placeholder for the file in question. If it is 
@samp{nil}, we assume that files are processed in linear order.
@item proof-files-query-dependencies-response-regexp
Regular expression to catch that the prover has complied with a request
to display dependencies for a particular @var{file}.
@code{proof-files-query-dependencies-response-regexp} may contain
@samp{%s} as a placeholder for @var{file}.
@end vtable

The result is analysed with the help of the function

@ftable @code
@item proof-files-query-dependencies-extract-parents
Returns the list of direct parents for the argument @var{file} by
analysing the previous output of the prover which triggered @code{proof-files-query-dependencies-response-regexp}
@end ftable


@node Adding New Proof Assistant, Literature, Handling Multiple Files, Internals
@comment  node-name,  next,  previous,  up
@unnumberedsubsec Adding Support for a New Proof Assistant

Suppose your new assistant is
called myassistant.

@itemize @minus
@item Make a directory myassistant to put the specific customization and associated files in,  called myassistant
@item 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)
@item Define the derived modes for the new assistant:

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

@node Literature, , Adding New Proof Assistant, Internals
@comment  node-name,  next,  previous,  up
@unnumberedsubsec Literature

The current version supports Script Management as documented in: 

@itemize @bullet
@item
Yves Bertot and Laurent Th@'ery. A generic approach to building
user interfaces for theorem provers. To appear in Journal of
Symbolic Computation.
@end itemize

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

@itemize @bullet
@item
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 
@end itemize

@node Variable Index, Function Index, Internals, Top
@comment    node-name,         next,       previous, up
@unnumbered Variable Index
@printindex vr

@node Function Index, Concept Index,Variable Index, Top
@comment  node-name,  next,  previous,  up
@unnumbered Function Index
@printindex fn

@node Concept Index,,Function Index, Top
@comment  node-name,  next,  previous,  up
@unnumbered Concept Index
@printindex cp

@bye