Proof Assistant GUI Detailed Info

back to ProofAssistantGUIQuickHOWTO.html
forward to ProofAssistantGUIDeriveFeature.html

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

Proof Text Area Statement Types:
HEADER Statement Type

Header:
  • Mandatory.
  • Identified by a "$(" token in column 1 of the first line of the Proof Text area (by "token" we mean that whitespace follows the "$(" characters), followed by the  "<MM>" and "<PROOF_ASST>"   tokens.
  • Contains the keyword parameter fields THEOREM= followed by LOC_AFTER= 
  • Any tokens following the LOC_AFTER= value and prior to the start of the next Proof Assistant Statement (Comment, Proof Step, Distinct Variable or Footer) are absolutely forbidden :)

Header Fields
 ================================================
THEOREM=
  • Mandatory
  • Specifies the Label of a Theorem in the loaded Metamath .mm database, or a Label that does not exist in the Metamath .mm database.
  • If the THEOREM Label already exists in the database, then it must designate a Metamath Theorem, and the Type Code of the Theorem must match the Grammar's Provable Logic Statement Type (default is "|-" -- Proof Assistant does not do syntax proofs :)
  • Otherwise, if the THEOREM Label does not exist in the loaded Metamath .mm database, then the Proof Text area will first be used to build a temporary theorem in memory, after which the Proof Text is validated/unified.
LOC_AFTER=
  • Optional
  • Follows the THEOREM=  parameter value
  • Used only if the THEOREM= Label does not already exist in the loaded Metamath .mm database; otherwise it is ignored.
  • Can specify any Label in the Metamath database (Metamath statements that have Labels are the $e, $f, $p and $a statements -- the hypotheses and assertions.)
  • If the specified Label does not exist, an error message is displayed and validation/unification processing is halted.
  • If left blank or equal to "?" for a new Theorem (THEOREM= not in the database), then the logical location of the new Theorem for parsing/validation/unification purposes is the end of the database (recall that a Metamath statement can only refer to statements defined earlier in the .mm database/file.)






PROOF STEP Statement Type

Proof Step:
  • Mandatory that at least one Proof Step be present -- the "qed" step.
  • A proof step consists of Step:Hyp:Ref fields combined into one token (no intervening space characters), followed by a Formula.
  • There are two types of Proof Steps: Hypothesis Steps and Derivation Steps.
  • Hypothesis Proof Steps are denoted with 'h' prefixing Step in Step:Hyp:Ref and correspond to the theorem's Logical Hypotheses.
  • Derivation Proof Steps are denoted by the absence of an 'h' prefixing Step in Step in Step:Hyp:Ref.
Example stating that Proof Step #3, using Proof Steps #1 and 2 as hypotheses, justified by  statement label ax-mp validly derives the Formula "|- ( ps -> ph )":
  • 3:1,2:ax-mp |- ( ps -> ph )
The user could also input this, leaving off the Ref field which is generated by the Proof Assistant:
  • 3:1,2       |- ( ps -> ph )
Or, if the hypotheses for the step are unknown or not yet input, the following can be input signifying that the step is incomplete (but can be used for unification of subsequent steps):
  • 3:?,?       |- ( ps -> ph )
Or, using the "Derive" feature, the user can input Ref along with and omit one or both Hyps (or signify a missing Hyp using "?"), and/or omit the Formula, like this:
  • 3:?:ax-mp
Or this:
  • 3::ax-mp
Or this:
  • 3:1,?:ax-mp
The sequence of Proof Steps is arbitrary (need not be in final Metamath order), except that:
  • the final Proof Step must be the "qed" step,  the conclusion or thing-to-be-proved step; and
  • the Hyp's for a given Proof Step may only refer to previously entered Proof Steps in the Proof Text area -- or '?'.

Proof Step Fields
 ===============================================
Step:Hyp:Ref
  • Mandatory
  • Must begin in column 1 of a proof text area line
  • Must be a single token -- i.e. no embedded whitespace characters
  • Colon (":") characters are used to separate the Step, Hyp and Ref sub-fields, but can be omitted if no remaining sub-fields are needed.
  • Example: "h1" could be a valid Step:Hyp:Ref entry because a hypothesis should not refer to other hypotheses, and the Proof Assistant outputs Ref as part of Unification!
Step
  • Mandatory
  • Must be a positive integer except for the last step "number", which must equal "qed"
  • Prefix with "h" to indicate that the step's Formula is one of the theorem's hypotheses (the "h" is not used in subsequent Proof Step Hyp fields.)
  • Need not be assigned in numeric order (numbers are being used to maintain semantic cohesiveness, not for doing arithmetic.)
  • Must not duplicate the Step number of any other Proof Step
  • Terminate the Step field with a Colon (":") if the Step field is to be followed by Hyp and/or Ref fields.
Hyp
  • Optional (depending on the Ref assertion's hypotheses).
  • Specifies the hypotheses needed by the theorem or axiom used to derive the Proof Step's Formula.
  • The number of hypotheses input controls the Unification search: if 2 hypotheses are input and Ref is blank (to be computed), then only assertions with 2 Logical Hypotheses are searched during Unification.
  • If present, Hyp must be a sequence of positive integers  or "?"s separated by Comma (",") characters with no embedded whitespace characters.
  • Do not prefix with "h" when referring to previous Step that is one of the theorem's hypotheses.
  • Example of multiple Hyp's in Step:Hyp:Ref: "3:1,2:ax-mp"
  • Code as null, not as space character(s) if unused (the Ref theorem or axiom uses no hypotheses.)
  • Example of omitted Hyp field in Step:Hyp:Ref: "5::ax-1" (ax-1 requires no hypotheses).
  • Should not be input on a hypothesis Proof Step (that is illogical, it does not compute -- an hypothesis does not have hypotheses! :)
  • Terminate the Hyp field with a Colon (":") if the Hyp field is to be followed by a Ref field.
  • Note: Hyp numbers will be resequenced by Proof Assistant during Unification to match the Metamath sequence of the hypotheses for the theorem or axiom. For example, if Theorem XYZ has Hypotheses XYZ.1 and XYZ.2 and the user specifies the Hyp as "3,4", but the Proof Assistant determines that step 4 corresponds to XYZ.1 and step 3 corresponds to XYZ.2, then, when the proof text is redisplayed after unification, the Hyp field will be shown as "4,3" instead of "3,4". The intent of this automatic resequencing is to speed up unification processing if a repeat is requested (the Metamath Proof Engine is quite strict about the order of hypotheses!)
Ref
  • Optional
  • Ref identifies the Label of a theorem, axiom or logical hypothesis that justifies derivation of the proof step's Formula -- or may be a "Local Ref" (e.g. "#1" or "#syl.1") as described below.
  • Ref is output by the Proof Assistant during Unification if it finds an assertion in the database that justifies the proof step -- even if there are unsatisfied Distinct Variable Restrictions associated with the assertion (the Unification search continues even after a $d error, looking for a unifying assertion that does not have a $d error, and if no such assertion is found, a message is produced showing the alterniative assertion choices.)
  • Ref may be input if the correct Label is known in advance, and/or if the user wishes to override the output of Proof Assistant.
  • If Ref is input and one or more Hyps is omitted or = "?", and/or Formula is omitted, the "Derive" feature is invoked -- the input Ref is used to generate the missing Hyp and/or Formula entries. (Derive operates on Derivation steps only, not on Hypothesis steps.)
  • If Ref is present in the Proof Text when Unification is requested, the Proof Assistant will attempt unification with the given Ref first. Then, and only if  the given Ref is incorrect (invalid label, does not unify, etc.), will the algorithm go through the tedious and perhaps horribly lengthy unification search process to find the correct Label.
  • If Ref is input but does not unify correctly, the program produces a message showing alternative assertions that do unify with the step.
  • For a new theorem, the Refs generated by Proof Assistant for the theorem's logical hypotheses consist of the THEOREM= value suffixed with ".1", ".2", etc., in the order of the appearance of the hypothesis Proof Steps.
  • Example: for new THEOREM=XYZ, the Proof Assistant generates logical hypothesis Labels = XYZ.1, XYZ.2, etc. for the Proof Steps prefixed with "h", based on the order of their appearance in the proof text area. If this is unsatisfactory, input the desired Labels in the Ref fields to override the default Ref values (for example "maj" and "min" are the statement labels in set.mm for ax-mp 's logical hypotheses.)
  •  Note that Labels on Logical Hypotheses must be unique within the Metamath statement label namespace (no two statements can have the same Label). In the event that the automatically generated Labels already exist in the database -- highly unlikely -- an error message will be generated and either the database should be modified or the Theorem's label should be changed. Likewise if the user enters just some of the Ref's and those conflict with the database or other automatically generated Labels (moral of story is, enter all of the Refs or none of them ...)
  • Note also (!) that the order of logical hypotheses within a Metamath Theorem is the order of their appearance within the database, which is not necessarily the same as the order of their appearance within a proof. The Proof Assistant, likewise, internally orders the hypotheses of new theorems in the order of their appearance within the Proof Text area; it does not alter the order of hypotheses for existing theorems. Either way, this should have no impact on the RPN sequences of the proofs of new theorems but those contemplating future enhancements involving real-time updating might want to pay attention: the order of logical hypotheses in a theorem's frame affects the RPN sequences of proofs that refer to the theorem in question.
  • "Local Ref" -- as a text-editing short-cut for use by "advanced" users, a "Local Ref" feature is provided. In the Ref field, enter "#" followed by the Ref or Step of a previous proof step and press Ctrl-U (or other Unification menu item). If there are no fields in error in the Proof Worksheet then the proof step containing the Local Ref is deleted automatically and any subsequent proof steps that refer to it as an hypothesis are updated to point to the Local Ref'd step as the new hypothesis.  Note: A tutorial page has been added demonstrating the "Local Ref" feature. To use it, run the     mmj2PaTutorial.bat batch command while in the mmj2jar directory. Then in the Proof Assistant GUI, use the File/Open Proof File menu item to open file mmj2\mmj2jar\PATutorial\PageLocalRef.mmp.
Formula
  • Mandatory on Hypothesis Proof steps and the 'qed' Derivation Proof Step.
  • Optional if Ref is entered on a non-'qed' Derivation step -- Derive will attempt to generate the Formula from the Ref and Hyp input.
  • Formula begins with the first non-whitespace token following the Step:Hyp:Ref string in a Proof Step statement, and continues until the next proof text area statement begins.
  • The Formula must begin with the Metamath file's designated mmj2 "Provable Logic Statement Type" (default = "|-", may be overridden via a BatchMMJ2 RunParm).
  • Formula is free-form and may be spaced or indented as the user desires, and may be continued onto as many lines as needed of the proof text area.
  • Unlike formulas in a Metamath .mm file, a Proof Step Formula may not contain embedded comments (or non-whitespace symbols that are not part of the formula!). Nor is the Formula terminated with "$=" or "$.".
  • The end of a Proof Step Formula field is designated by the start of the next Proof Assistant text area statement, not the Metamath "$." or "$=" tokens (which are not used in the Proof Assistant GUI.)
  • The Proof Assistant GUI will not alter the spacing or indentation of a user-input Formula except when necessary for insertion of a Ref  label in the Proof Step line -- or when Work Variables are updated during unification, in which case the entire formula is reformatted according to the current TMFF settings.
  • The Formula on a hypothesis Proof Step statement must be the exactly the same, symbol for symbol, as the corresponding formula in the input Metamath .mm file/database.  Likewise with the formula on the "qed" Proof Step. (The easiest way to accomplish this is with the File/New menu item which preloads the hypotheses and "qed" Proof Steps.)
  • Each Proof Step Formula must be parseable using syntax axiom statements in the loaded Metamath .mm file that are located prior to the theorem being proved or the LOC_AFTER location. Syntactic analysis is performed as a necessary part of validation/unification to construct a parse tree for the Formula (this should be obvious, but be prepared in advance for ugly error messages coughed up by mmj2's Grammar's Parser! :)
  • "Work Variables" may be generated by the Derive Feature, and can be input by the user (except in the 'qed' and hypothesis steps).  The Work Variables represent unknown sub-expressions (or variables) and have names corresponding to Type Code: "&W1", "&W2", etc. for Type Code "wff"; "&C1", "&C2", ... for Type Code "class", etc. Refer to \mmj2jar\AnnotatedRunParms.txt for more information -- (hint: search for "WorkVar" in the file.) Also, refer to StepUnifier.html and WorkVariables.html.


COMMENT Statement Type

Comment:
  • Identified by an Asterisk ("*") character in column 1 of a line in the proof text area.
  • A Comment statement can continue onto multiple lines of the proof text  area
  • A continuation line is identified by a space character in column 1 of a line.
  • Any valid Metamath tokens can be contained in a Comment statement except for  "$(" or "$)"  (Note: the GUI itself does not validate the Comment contents, but Metamath.exe and mmj2 do, so if a Proof Text containing embedded Metamath comments is itself embedded as a comment in a Metamath file and input to these programs, an error message will be generated and the problem will need to be corrected before continuing.)


DISTINCT VARIABLE Statement Type

Distinct Variable:
  • Identified by a "$d" token in column 1.
  • Must be a valid Metamath format $d but without the standard terminator "$.", with no embedded Metamath comments.
  • May be located anywhere within the Proof Text area, applies to the entire proof.
  • More than one Distinct Variable Statement Type can be input for a single proof.
  • The Distinct Variable restrictions specified are accumulated with those already specified in the loaded Metamath .mm database. Note: the new Set Soft Dj Vars Error Handling option on the Edit Menu (and via RunParm) causes $d statements to be generated during Unification, instead of reporting missing $d statements as errors. Refer to mmj2\mmj2jar\AnnotatedRunParms.txt for additional information.



FOOTER Statement Type

Footer:
  • Identified by a "$)" token in column 1 of the first line of the Proof Text area (by "token" we mean that whitespace follows the "$)" characters.)
  • Any text following the "$)" token will be treated as an error or ignored.


GENERATED PROOF Statement Type

Generated Proof:
  • Output by the Proof Assistant during Unification. Do not input, will be erased!
  • Identified by a "$=" token starting in column 1 of a Proof Text line (just before the Footer).
  • Consists of the Metamath RPN-format proof steps for the theorem, presented in columns 6 thru 79 of proof text lines (defaults may be adjusted using RunParms), and continued onto as many lines as needed, and followed by a "$." token.