ProofAssistantGUIQuickHOWTO

Proof Assistant GUI Quick HOWTO

See also:
Proof Assistant User Guide
ProofAssistantGUIDetailedInfo.html
ProofAssistantGUIDeriveFeature.html
StepUnifier.html
WorkVariables.html
PageLocalRef.mmp
StepSelectorSearch.html
UnifyEraseAndRederiveFormulas.html
BottomUpProving-ByNormMegill.html

Purpose:

The main function of the Proof Assistant GUI is to construct valid Metamath RPN-formatted proofs.
Two distinct approaches to proof development are supported, and these approaches can be combined. Top-Down proving derives a theorem's conclusion by writing a sequence of proof step formulas that logically lead to the conclusion, where each step is justified by referencing an existing Metamath assertion. Bottom-Up also builds a sequence of proof step formulas, but it works backwards from the conclusion, identifying in turn, the existing Metamath assertion which justifies that each derivation step's formula.
mmj2 supports both Top-Down and Bottom-Up proving by providing two important capabilities: 1) it uses a Unification Search algorithm to find an existing assertion that justifies (unifies with) a proof step and its formula; and 2) conversely, it provides a "Derive" feature which generates proof step formulas when given the label (i.e. key) of an existing assertion.
When a proof has been successfully created, mmj2 generates a Metamath RPN-formatted proof that can be exported or copied into a Metamath database.

Motivations:

One motivating idea behind the GUI is that it is difficult to memorize thousands of theorem and axiom statement labels, and it would be nice to have a bit of help from the computer. A person may well be capable of writing a series of formulas deriving the conclusion of a theorem but have difficulty recalling the Metamath statement labels justifying each step. The primary Metamath database, set.mm, has nearly 10,000 statement labels!
Another motivation for the GUI is that metamath.exe's Proof Assistant requires the user to enter proofs backwards, starting from the conclusion and working towards the premises. The Proof Assistant GUI allows the user to work forward or backward; that is, starting from the hypotheses and deriving the conclusion, or the reverse. In fact, it is possible to experiment using the GUI and create proof steps that head off in a tangent without contributing to the conclusion :)

Limitations:

The Proof Assistant GUI does not update Metamath .mm files. A generated proof must either be manually pasted into the .mm file, or "imported" into Metamath using the "eimmimp.cmd" which imports a mmj2 Proof Worksheet into a Metamath .mm database (see Metamath.com for more information).
New theorems, not already present in the Metamath files that are loaded, can be proved, but new theorems not yet saved in the .mm file cannot refer to each other. And, although $d can be added to a proof, and both $d and $e specifications can be coded with a new proof; all variables, constants, variable hypotheses and axioms referred to must already be present in the loaded Metamath .mm file.

Usage:

Trigger/initiate/start the Run ProofAsstGUI using program BatchMMJ2 as described elsewhere (for example, mmj2\mmj2jar\mmj2.bat ).

NOTE -- IMPORTANT: Run the mmj2.bat command from a Command Prompt window. The Proof Assistant GUI is triggered at the end of the regular BatchMMJ2 process and if there are errors in the load, grammatical parse or RunParm validation, error messages print out and the GUI does not appear.

When the GUI screen appears:

Select the File/New Proof menu item
A dialogue box will appear asking "Theorem label?"
Type in the label of a theorem in your .mm file and click "OK".
A skeletal proof appears on the ProofAsstGUI main frame:

$( <MM> <PROOF_ASST> THEOREM=a1i LOC_AFTER=?

h1::a1i.1          |- ph
2:?:               |- ?
qed:?:             |- ( ps -> ph )

$)

The GUI frame is a free-form text frame that is editable. (The contents of the text frame -- the text -- is called a "Proof Worksheet" elsewhere in the mmj2 system, fyi.) Proof Step #2 above is a skeleton proof step with "?"s indicating the location of fields to be entered. As shown below, all we need to enter in Step #2 is a formula; there are no hypotheses involved.

$( <MM> <PROOF_ASST> THEOREM=a1i LOC_AFTER=?

h1::a1i.1          |- ph
2::                |- ( ph -> ( ps -> ph ) )
qed:1,2:           |- ( ps -> ph )

$)

Next select the Unify/Unify (check proof) menu item or press the Ctrl and "U" keys simultaneously.

The Proof Assistant performs validation and unification for each step and generates "Ref" labels for each properly unified step. And, if all proof steps are correctly unified -- particularly especially the final, "qed" step, the Metamath RPN-format proof is also displayed:

$( <MM> <PROOF_ASST> THEOREM=a1i LOC_AFTER=?

h1::a1i.1          |- ph
2::ax-1            |- ( ph -> ( ps -> ph ) )
qed:1,2:ax-mp      |- ( ps -> ph )

$=    wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.

$)

Voila! Proof complete. If desired, save the Proof Assistant GUI text area to a file using the File/SaveAs menu item. And, if desired, use the Edit/Copy menu item to copy the Metamath RPN proof steps and then paste them into to your .mm file.

Now, for reference purposes, please compare the screen layout above to this portion of the Metamath Proof Explorer html page for theorem a1i:

**Proof of Theorem a1i**
Step	Hyp	Ref	Expression
1		a1i.1	. 2 ⊢ φ
2		ax-1 3	. 2 ⊢ (φ → (ψ → φ))
3	1, 2	ax-mp 6	1 ⊢ (ψ → φ)

GENERAL FACTOIDS about the GUI proof text area - AKA "Proof Worksheet":

The Proof Assistant GUI proof text area follows the format and rules of a single Metamath comment statement: it begins with "$(" and ends with "$)", must consist of valid Metamath tokens, and must not contain nested Metamath comments. (This is a "feature" that allows the student/mathelogician to embed GUI proof texts inside a Metamath .mm file, if desired.)
Any text entered prior to the Header's "$(" is treated as an error.
Any text entered after the Footer's "$)" is ignored and will be erased automatically.
Suggestion: use "File/Save" frequently to avoid any mishaps.
There are six (6) types of proof text statements: Header, Proof Step, Comment, Distinct Variables, and Generated Proof, and Footer statements. (The Generated Proof statement is output from by the Proof Assistant and is not (validly) enterable by the user.)
Each instance of one of these proof text statement types must begin in column 1 of the GUI text area!
A blank character in column 1 of a line indicates continuation of the previous statement.
There must be no extra text, no extraneous comments or remarks inside any of the proof text statements. The Comment statement is the only "authorized" way to add commentary about a proof! (This rule makes the parser easier to code.)
The Proof Assistant GUI program does not retain theorem-specific memory about the user's interactions and progress towards a valid proof (note: as of Nov-1-2006, the program does retain a memory of the sequence number/location of the current proof within the Metamath database -- this information is used for browsing forward or backward, but has no effect on processing the Proof Worksheet itself.) All relevant proof information is contained in the Proof Text. This means that, among other things, it is not necessary to begin a proof using the File/New Proof menu option. Proof text can be entered elsewhere, say, with the text editor of your choice, then be pasted (Edit/Paste) into the GUI proof text area. Or, the File/Open menu option can be used to load a file into the Proof Text area. Whatever is in the Proof Text area can be validated/unified at any time using the Unify/Unify (check proof) menu option. It is also possible --and allowed -- to change the Header statement's THEOREM and LOC_AFTER label values to "clone" a proof.
The Proof Assistant GUI allows new theorems -- theorems not already present in the loaded Metamath .mm file -- to be proved. The design of the user interface requires that hypothesis proof step "numbers" be prefixed with an "h", and that the final proof step "number" equal "qed". Given these bits of information, plus the Header's THEOREM= label value and LOC_AFTER= value, plus any (optional) Distinct Variable statements, the Proof Assistant can construct a Metamath theorem in memory and then validate/unify its proof. The only limitation is that the GUI does not provide a way to enter new dummy variable definitions as part of the proof text; any variables referenced in a new theorem proof must be defined at the global scope level of the input Metamath .mm file.
The LOC_AFTER field on the proof text Header statement is used only to specify the logical location of a new theorem in the loaded set of Metamath statements; it is ignored when present on a proof for an existing theorem. Location is significant in Metamath because statements may refer only to previous statements in a Metamath file. If LOC_AFTER is left blank (or = "?"), then the GUI treats the new theorem as if it were the last Metamath statement in the database.
[Gedankenexperiment: do File/New specifying "a1i". Then in the displayed proof text area, change "THEOREM=a1i" in the Header statement to "THEOREM=TESTa1i", and set the Step:Hyp:Ref data on the qed proof step to "qed:1", but.do not change "LOC_AFTER=?". Then select menu item Unify/Unify (check proof). If the Proof Assistant GUI program is working correctly, the unification algorithm will complete the proof, assigning a1i to the qed proof step Ref.]
One or more Distinct Variable statements, such as "$d x y z" may be entered in the proof text area. Each must begin in column 1 of a new, separate line of the proof text (i.e. if two Distinct Variable statements are needed, then each must be entered on a separate proof text area line.) This capability was added to the GUI specification as an afterthought because it was realized that figuring out the needed $d's is an iterative process, with some trial and error, even for highly expert Metamath users. A Distinct Variable statement entered in a GUI proof text is treated as an addition of distinct variable restrictions to those already present for the theorem in the loaded Metamath .mm file (except when option "GenerateNew" is selected on the Edit/Set Soft Dj Vars Error Handling menu item.).

Example of Proof Text area containing Distinct Variables, Comments and free-form Formulas:

$( <MM> <PROOF_ASST> THEOREM=a1i LOC_AFTER=?

* Comment begins with "*" in column 1
and 

  continues until the next line of the Proof

  Text area which does not have a space in

  column 1.



* Note how Formulas may be indented and spaced

  freely by the user, continuing onto as many

  lines as desired.

h1::a1i.1
|-                  ph
2::
|-                  ( ph
                        ->
                        ( ps -> ph )
                      )
qed:1,2:
|-                    ( ps -> ph )

* Following are Distinct Variable
statements

  (may occur anywhere inside the Proof Text

  between the Header and Footer statements):

$d th ta

$d ch ta



* Note: Distinct Variable restrictions added

  are applied in conjunction with any Distinct

  Variable restrictions already contained in

  the Metamath .mm file for the Theorem unless

  "GenerateNew" is selected on the Edit/Set 

  Soft Dj Vars Error Handling menu item.

Tips on Effective Use (and programmer CYAs):

Request Message Window Handling	Error and Informational messages produced by the Proof Assistant GUI appear in a small text window "pane" on the main Proof Assistant GUI window. A separate Request Message window is created containing these messages and can be viewed using Alt-Tab.
Unification Search Sequence	The program searches the loaded Metamath assertions (from the .mm file(s)) in ascending database sequence. That means that if two assertions satisfactorily unify with a given proof step, the assertion that appears earliest in the input files is used. If this is unacceptable the user can simply input the correct assertion label.
Unify Search Exclusions	New RunParm to exclude loaded assertions from the Unification search (example): `ProofAsstUnifySearchExclude,biigb,xxxid`
Distinct Variable Errors and Alternative Unifications	When the user manually inputs a Ref for a proof step and that Ref either does not unify satisfactorily or has Distinct Variable restriction errors, a message is produced showing the assertions that do unify with the proof step. In the case where the user leaves the Ref blank and allows the program to search for a unifying assertion, the first Ref that unifies with the proof step is taken and used, provisionally. If the Ref has a Distinct Variable restriction error, the search continues, looking for a perfect unification without the $d errors; if this secondary search is unsuccessful, an informational message displaying altervative assertions is produced. Note: The Edit menu (and input RunParm file) provide a choice about how "soft" Distinct Variable restriction errors are handled. '"Soft" Dj Vars Errors' refers to missing or incomplete $d statements on the theorem being proved. The default setting is not to report these errors but to "GenerateReplacements", which creates a complete set of $d statements for the theorem being proved once unification is completed for the 'qed' step of the proof. "Hard" errors, which occur when a pair of substitution variables violates the $d restrictions specified by a proof step Ref assertion are always reported and cannot be "fixed" by the mmj2 program.
Annotated RunParms .txt	Many options to customize processing can be set by updating the "RunParms.txt" file which is input in the mmj2.bat command file. All RunParm values and options are documented in mmj2\mmj2jar\AnnotatedRunParms.txt. For some features of mmj2, the AnnotatedRunParms.txt file is the only source of documentation, so you may want to have a look; your experience with the mmj2 Proof Assistant can be easily customized and optimized to satisfy your personal requirements and preferences.