Work Variables

Purpose:

• The primary purpose of Work Variables is to facilitate proof entry using just assertion labels (aka "Ref"s) on the Proof Assistant GUI screen, thus providing basic functional compatibility with the metamath.exe Proof Assistant. Instead of entering formulas the user can enter Ref's and allow the Proof Assistant to generate (derive) proof step formulas.

Description:

•  Work Variables provide syntactic placeholders for unknown variables and/or sub-expressions required by a proof (other uses may be found later.)
  
• Work Variables are produced by the mmj2 Proof Assistant GUI's "Derive" feature when a Ref label is input for a derivation step and either the formula is omitted (i.e. to be derived), or one or more of the step's hypotheses are omitted (to be derived), or both.
  
• Work Variables can also be input by the user on the Proof Assistant GUI screen, or in a Proof Worksheet text area or file.
• Work Variables are actual "variables" within mmj2 but they differ in several respects, as described in the following table:

Characteristic	Regular Variables	Work Variables
Definition and Declaration	Declared in Metamath .mm file via the $v command, and are type-defined via $f command.	Defined in mmj2 RunParm file via DefineWorkVarType RunParm command and declared via DeclareWorkVars RunParm command.
Scope	May be global or local, may be accessed by statements the follow its definition with the input .mm file.	Always global scope, may be accessed or used in any derivation proof step (except the "qed" step, and never, of course, in a theorem's logical hypotheses.)
Duration	A regular variable defined within a scope may be redefined within another scope, and may be assigned a different Type Code (this is rare in practice).	A Work Variable's Type Code and assigned Variable Hypothesis are fixed and cannot be changed during a single invocation of the Proof Assistant (multiple definition and declaration RunParms can be processed by mmj2, but only one set can be active at one time.)
Naming	A regular variable must consist only of valid math symbol characters, and must be unique across both the Symbol and Label namespaces (i.e. cannot be the same as any label or other symbol).	Like a regular variable, a Work Variable must consist only of valid math symbol characters, and must be unique across both the Symbol and Label namespaces. In addition a Work Variable must be unique across the Work Variable namespace. A Work Variable name consists of a prefix, such as "WFF" or "&w" and a numeric suffix, such as "1", "2", ..., as defined on the DefineWorkVarType RunParm command -- thus Work Variables "WFF1", "WFF2", ... , or "&w1", "&w2", ..., are possible.
Visibility	Regular variables are added to the mmj2 Symbol Table, may be used in .mm file and Proof Worksheet formulas and are output in the course of normal processing (such as the PrintSyntaxDetails RunParm command, etc.)	Work Variables are not added to the mmj2 Symbol Table and cannot be input in a .mm file, being restricted to use only on Proof Worksheets. They are not output anywhere, except in the Proof Assistant and error messages, and are automatically eliminated from finished proofs.
Unification  Substitution	In normal Metamath and mmj2 Proof Verification and unification processing, substitution can only be made to a variable -- substitution cannot be made to a constant or a sub-expression. For example, in a formula, variable "ph" can be replaced by a variable or sub-expression of the same Type, such as "( ph -> ps )".	A Work Variable in a derivation proof step can be substituted for a variable or a sub-expression having the same Type Code. Thus, a derivation step Work Variable, "WFF1" can be unified with and substituted for a Ref assertion's sub-expression having type "wff", such as "( ph -> ps )".
Mandatory / Optional ("dummy") Variables	In Metamath "mandatory" refers to variables that are used in a theorem's (or axiom's) formula or in one of its logical hypotheses' formulas. "Optional" variables are within a theorem's scope and may be used within the proof as "dummy" variables, that are introduced and referred to in proof steps, but are eliminated in the final derivation proof step's formula.	Work Variables are never in a theorem's Mandatory Frame -- or its Optional Frame (due to space requirements.) They are accessible within a proof, and are automatically assigned as placeholders for "dummy" variables during Derive processing. If not manually replaced by the user, when a proof is completed on the Proof Assistant GUI screen, any Work Variables substituting for "dummy" variables are automatically replaced by "optional" variables within the theorem's Optional Frame (Note: in some cases the automatic conversion of leftover Work Variables to optional variables runs out of available optional variables in scope of the theorem being proved -- manual update of either the Proof Worksheet or the input .mm file will be needed to resolve the problem, but this is an uncommon scenario...)
Proof Assistant GUI Unification Search Processing	Unification Search on the Proof Assistant GUI screen is part of the "Unify" (Ctrl-U) processing which searches the input .mm assertions if a Ref is not input on a derivation proof step -- thus, the user is relieved of the task of entering (and memorizing) Ref labels. Unification Search is performed only for "valid" and complete derivation steps.	Unification Search is not performed for a derivation proof step if the step's formula or one of its hypotheses' formulas contains a Work Variable -- but Unification Hint processing is available for derivation steps containing Work Variables. (NOTE: this somewhat arbitrary and technical restriction may be eased or eliminated at some future date.)
Variable Updates	Regular variables are never modified by the Proof Assistant, whether input by the user or generated by the Derive Feature.	Work Variables are updated by the Proof Assistant during Unification, and may be replaced by regular variables, Work Variables, or sub-expressions containing both regular and Work Variables (e.g. "&W1" might be changed throughout the proof to "( ph -> &W2 )"). A side-effect, which is a bonus feature, is that a given Work Variable that occurs more than once in a set of proof steps, can be changed by the user by simply updating one of the Work Variable occurrences and pressing Ctrl-U --  Unification resolves the "unknown" values with the user entered value (hence, the need for a Search/Replace menu option is greatly reduced!)

---

Work Variable RunParms:



• - The RunParms pertaining to Work Variables are optional, and default settings are applied automatically if the Work Variable RunParms are not input in the RunParm file prior to their first use requirement -- which is the Proof Assistant, at this time.
• - The default settings are intended to be acceptable for use with the set.mm database, and are subject to change.
  

    DefineWorkVarType
           : - Optional. May appear anywhere after the "Parse" RunParm
                         within an input RunParm file, and takes effect
                         when the next DeclareWorkVars RunParm command is
                         processed. If not input prior to first use -- the
                         Proof Assistant -- the default settings are
                         automatically used.
             - Default = One default DefineWorkVarType RunParm is
                         generated for each grammatical Type Code.
                         specifying a prefix of "&x" where "x" is
                         the first character of the grammatical
                         type code, converted to lower case if
                         necessary; 200 work variables are defined
                         by default for each grammatical type code.
             - Value1 = Grammatical Type Code (e.g. "wff", "class",
                        "set", etc.) Must be a valid grammatical
                        Type Code.
             - Value2 = Work Variable Prefix for the grammatical
                        Type Code. Must generate unique variable and
                        variable hypothesis names when concatenated
                        with the Work Variable numerical suffix (1,
                        2, ..., 11, ..., etc.) Note that Work
                        Variable Hypothesis labels are generated
                        automatically and are the same as the Work
                        Variables. A Work Variable Prefix must
                        consist solely of valid Metamath math
                        symbol characters (not "$", for example,
                        or embedded blanks.)
             - Value3 = Number of Work Variables to be declared for the
                        grammatical Type Code. Must be greater than 9
                        and less than 1000 ("stinginess" is recommendedto
                        avoid wasted processing and memory allocations...
                        but, in the event that the supply of available
                        Work Variables is exhausted during processing
                        a pop-up GUI error message will be displayed; the
                        RunParms will need to be modified and re-input
                        in a subsequent run...)
             - Examples:
                *        1         2         3         4
                *234567890123456789012345678901234567890
                DefineWorkVarType,wff,&W,200
                DefineWorkVarType,set,&S,200
                DefineWorkVarType,class,&C,200
             


    DeclareWorkVars
           : - Optional. May appear anywhere after the "Parse" RunParm
                         within an input, and takes effect immediately
                         (any existing Work Variables are deleted and
                         a new set is created.)
             - Default = A default DeclareWorkVars RunParm is executed
                         automatically when first need arises (e.g. at
                         Proof Assistant start-up), if none have been
                         input since the last Clear RunParm or the start
                         of the RunParm file.
             - Value1 = N/A
             - Examples

                *        1         2         3         4
                *234567890123456789012345678901234567890
                DeclareWorkVars



---