The InterProver

The InterProver is invoked from the Provers Environment:

It is applicable to all machines, refinements and implementations which are pogenerated and currently have undischarged proof obligations.

If the AutoProver fails to discharge all the proof obligations for a given construct then proofs of the remaining obligations may be attempted by entering the AutoProver-InterProver cycle which has the following structure:

           --> AutoProver
          |        |
          |        |
          |        |              No
          |  POs remaining ?  ---------->  Finished
          |        |
          |        | Yes
          |        |
          |       \|/
           <-- InterProver

The InterProver allows you to investigate why the AutoProver has failed to discharge a proof obligation. It is stressed that it is a BROWSING tool (no `proofs' are committed to the system) which facilitates the inspection of the points at which the AutoProver failed in its attempts to discharge a proof obligation. It enables you to supplement the AutoProver's standard in-built library of mathematical laws with additional laws of your own through the user's PROOFMETHOD file.

InterProving comprises two distinct phases:

Finding an appropriate point in the INCOMPLETE proof where you think you can provide the mathematical insight to enable the proof to proceed. This is achieved by creating one or more lemmas. This phase uses only the in-built tactics and theory of the AutoProver.
Providing the necessary mathematics in order to COMPLETE the proof. This is achieved by discharging the lemmas. This phase uses the in-built tactics and theory of the AutoProver supplemented by user-provided theory and tactics.

Although the InterProver actually constructs proofs, its browsing nature means that such proofs are not committed to the system. The idea is that, having demonstrated to yourself that the mathematical insight that you have provided is sufficient, you then leave the InterProver and invoke the AutoProver, which constructs the next level of proof using your PROOFMETHOD file, which you have already demonstrated is adequate.

The InterProver is invoked from the Provers Environment by first selecting a construct and then activating the InterProver. You are then presented with a selection-list of item names (e.g. operation names). For each item the number of (unproved) proof obligations associated with this item is given.

An editor window is also presented which contains the appropriate PROOFMETHOD file, if one exists, or a template proof method file otherwise. This template can be edited to provide the provers with user-supplied laws of mathematics and proof tactics, as described below. (Each prover cycle (InterProver - AutoProver) creates a new ``proof level'' with its own PROOFMETHOD file stored in the environment subdirectory PMD).

On selection of one of the items (e.g. operation), another selection list of the proof obligations outstanding for that item is presented. Once one of these proof obligations has been selected, that proof obligation is displayed as the Current Goal for the InterProver and you are presented with a menu of options for driving the InterProver in producing an INCOMPLETE proof.

The First Phase - Creation of Lemmas

The options are initially:

Run Prover
Create Lemma

The `Run Prover' option uses the rules in the standard library in an attempt prove the Current Goal; the InterProver uses the same standard library as the AutoProver.

Selecting the `Run Prover' may result in either the goal being discharged or in the InterProver encountering a goal for which no standard rules apply, when it stops and presents the options:

Backtrack
Show Hypotheses
Create Lemma

The `Create Lemma' option discharges the Current Goal through the creation of a Lemma; this should be employed if you believe that the Current Goal is provable, and that you can easily supply some additional laws of mathematics which prove that lemma. (At this point you might provide these additional laws by entering them as rules in the UsersTheory in the provided PROOFMETHOD file, although they won't be used until the second phase).

The hypotheses associated with the Current Goal can be displayed through `Show Hypotheses' at any time. This might assist you in assessing whether a goal is provable. The current set of hypotheses is displayed inside an editor or other tool specified though the Hypothesis Editor (Viewer) setting of the Options.

The `Backtrack' option provides a backtracking mechanism, and should be selected if you think that the Proof Obligation is provable and if you think that the Current Goal is too difficult to justify. Selecting run will backtrack to an intermediate goal and you will at this stage be informed by the InterProver of how (and why) the goal, from which you are backtracking, were produced.

The intermediate goals presented may be altered by setting the `InterProver Reasoning Depth' to the appropriate level of forward reasoning:

InterProver Depth 0
InterProver Depth 1
InterProver Depth 2

(The effects of these settings are the same as those described for the REASONING_DEPTH clause of the PROOFMETHOD)

In order to use the InterProver to produce an INCOMPLETE proof for a Proof Obligation you will have to create a lemma at some point of your choosing, either for a final goal or an intermediate goal. If you do not create any lemmas then repeated use of the run option will eventually return you to the Original Proof Obligation.

If you need to investigate the proof attempt again you can repeat the run. Note that a single proof obligation may give rise to several lemmas. During this first phase, the PROOFMETHOD is not consulted, and so the intermediate goals that are presented stem from the AutoProver's in-built tactics and theory. It is possible to change the intermediate goals only through the the setting of the `InterProver Reasoning Depth'.

The display shows the Original Proof Obligation and the Current Goal (on which the AutoProver can currently make no progress):

See figure.

A combination of the Current Hypotheses and the Current Goal provides the information necessary to enable the user to decide whether or not to create a lemma, and assist in providing the mathematics to be used in the discharge of that lemma in the second phase (all rules are written in the B-Theory Language of theBPlatform):

See figure.

Having created one or more lemmas (which are stored in a selectable item called `Lemmas') you can attempt to prove them completely by returning to the `Select Theory' option - through `Cancel' - and selecting the Lemmas item. Note that when a proof obligation is discharged by the creation of lemmas, you are automatically returned to the `Select Theory' option.

The Second Phase - Proof of Lemmas

This second phase - attempting the proof of a lemma - now simulates the action of the AutoProver which is dictated by the PROOFMETHOD file, and so, after selection of a particular Lemma, that file is automatically loaded (provided that it parses!), and you the are presented with the choice:

Run Prover
Show Hypotheses
Reload PROOFMETHOD

Note that there is now no `Backtracking' option, and that the `InterProver Reasoning Depth' option is no longer available (this is now a simulation of the AutoProver).

On selection of `Run Prover' your PROOFMETHOD file is used by the system to attempt a COMPLETE proof. A tracing mechanism indicates which of your rules are applied, and to which goals they are applied, in order to assist in understanding the proof process.

See figure.

If the attempt is unsuccessful, the tracing information provided should be sufficient to indicate the way in which the PROOFMETHOD should be edited, and having done this it may be loaded using the `Reload' option when the previous PROOFMETHOD is removed and the current one loaded.

The `Show Hypotheses' option will show the hypothesis associated with the final goal produced during a failed attempt to prove a lemma. Note that when the PROOFMETHOD is reloaded all previously proved lemmas re-appear (since they may no longer be provable once the proof method has been edited!).

You can follow this cycle as many times as you want until either the lemma is proved, or you wish to abort the attempt - through `Cancel'.

The PROOFMETHOD file

The PROOFMETHOD file resides in the environment subdirectory PMD and is automatically presented for editing during InterProof. It may also be edited through the `pmd' button of the Provers Environment.

The syntax of a proof method is:

     PROOFMETHOD
         name
     IS
        USETAC tactic 
         [ REASONING_DEPTH  n1 ]
         [ ON lemma_list ] 
        END

       [ &

        THEORY th1 IS rules1 END 

        &
         ... 
        &

        THEORY thN IS rulesN END ]
     END

     [
     DEFINITIONS
         rewrite_rule [ ; rewrite_rule ]
     INCLUSIONS
         incl_file [ , incl_file ]
     ]

Theories th1,..,thN contain the user-supplied rules: rules1,..,rulesN.

The optional DEFINITIONS clause allows macro definitions in the form of rewrite rules to be applied to the user-supplied Theories before use. A DEFINITIONS clause comprising `?' is equivalent to an empty clause.

The optional INCLUSIONS clause allows other PROOFMETHOD files to be loaded (and, of course, the process is recursive). For such included files, however, the USETAC, REASONING_DEPTH and ON clauses are ignored; those settings are taken from the main PROOFMETHOD file.

Each inclusion should be the name of a PROOFMETHOD file enclosed in double quotes, and for proof levels other than zero, the default file produced by the system contains a single INCLUSIONS entry comprising the previous-level PROOFMETHOD file. An INCLUSIONS clause comprising `?' is equivalent to an empty clause.

The optional REASONING_DEPTH clause enables the provers to work with different sets of `forward' rules:-

when n1 = 0
only a simple set of rules for recognising mathematical contradictions are used, and furthermore the antecedent of the proof-obligations is not inspected during proofs;
when n1 = 1
the antecedent of the proof-obligations is used and a simple set of rules for producing further consequences from the specific antecedent are used;
when n1 = 2
an extended set of rules for producing consequences are used.

NOTE: the performance of the provers is affected by this setting.

The optional ON clause enables the AutoProver to subsequently attempt to prove a subset of undischarged proof obligations; `lemma_list' is a comma-separated list containing either:

name
(e.g. an operation name) indicating that all outstanding obligations of that name should be attempted
name.n
indicating that only the n-th obligation of name should be attempted
name.(n,m,..)
indicating that name.n, name.m, name... should be attempted.

If the ON clause is omitted, the AutoProver will use the supplied tactics to attempt all unproved proof obligations.

The tactic is a standard B-TL tactic, i.e. a pair (b,f) consisting of a normal tactic b and a forward tactic f. (See section called ``B-Platform'' for a discussion of proof and tactics.)

In attempting a COMPLETE proof, the InterProver and the AutoProver will follow their own in-built tactics until a goal is (or goals are) generated which the Provers cannot match. At this point, the supplied user tactics are adopted.

Each generated PROOFMETHOD file is provided with a default tactic, which may be edited by the user. The default normal tactic is

     (UsersTheory~)

which is the theory (provided through the PROOFMETHOD) that the provers tactic switches to after the in-built tactic is tried. If progress is made through one of the rules in `UsersTheory', the tactic switches back to the in-built tactic until no progress can be made; again the tactic switches to that of the PROOFMETHOD file and the process repeats until either the proof is complete, or no further progress can be made. The in-built tactic also incorporates a backtracking mechanism so that all possible proofs are attempted before the process is deemed to have been unsuccessful.

The default forward tactic is

     (FwdUsersTheory~/*;FEQL~*/)

Here, FwdUsersTheory is employed (together with FEQL if not commented out) before the library's standard forward tactic.

You should always edit the PROOFMETHOD file using the InterProver editor, since this editor is the means of propagating the effects of changes in the proof method file to the configuration tools (i.e. recording the `level' in the prover cycle).

Having proved all (or some) of the outstanding proof obligations the cycle is completed by returning to the top level of the prover environment and invoking the AutoProver; it uses the proof method file just edited to discharge more proof obligations and, if proof obligations remain, a new level is generated, enabling the cycle to be repeated.

The Global PROOFMETHOD File

A Global PROOFMETHOD may be specified in the Provers Options; if set it is automatically inserted into the INCLUSIONS clause of all newly-created PROOFMETHODs; it may also, of course, be manually inserted or removed when editing a PROOFMETHOD.