Proof Assistant GUI Quick HOWTO

See also:
Proof Assistant User Guide





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:


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.


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:


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":

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


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

  |-                  ph

  |-                  ( ph
                        ( ps -> ph )

  |-                    ( 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):

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.
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.
New RunParm to exclude loaded assertions from the Unification search (example):

Errors and
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.
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.

See also:

Proof Assistant User Guide