Step Selector Search

Proof Assistant Step Selector Search

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

to build

           Step
Selector Dialog screen.

    Double-click
selected assertion or hit

          "Apply Selection
To Step And Unify Proof"

          button, or
right-mouse click selection.

    Ctrl-Z
twice to Undo previous selection

          then press
Ctrl-9 to Reshow Step Selector

          Dialog (just as
it was before selecting.)

What Is It?

The Step Selector Search provides an extremely powerful search capability to the mmj2 Proof Assistant GUI. With it you can search the entire input Metamath database looking for all assertions meeting the criteria you specify -- namely, those which can be unified with a proof step and its hypotheses, and where some or all of the proof step conclusion and hypothesis formulas are either missing or incomplete due to the presence of Work Variables. The search treats Work Variables and incomplete hypothesis specifications as, in effect, wildcards which match assertions according to the pattern you specify.

But what is it really? The name, "Step Selector Search"...is goofy and awkward sounding!

Step -- refers to the fact that the search pertains to a single Derivation proof stop, the step designated by the location of your input (keyboard) cursor. All step-specific mmj2 Proof Assistant GUI functions are available via the right (alt) mouse button.
Selector -- refers to the goal of proving a step in Metamath, which is to select an existing assertion to justify the given proof step. In this context, the Step Selector Search produces the Step Selector Dialog screen from which you can select one of the matching unifiable assertions, at which point the label of the selected assertion is edited/pasted into the Ref field of the proof step and the proof unification process is initiated!
Search -- refers to a search of the input Metamath database looking for assertions which can validly be unified with the given proof step and its hypotheses (taking into account the "?" Hyp wildcard which indicates that zero or more additional, unspecified hypotheses are acceptable.) The search produces the Step Selector Results which are displayed on the Step Selector Dialog...

OK? So the name is nerdy, but it makes some kind of sense. The good names were already taken...

Here is a quick demonstration for you. Fire up mmj2's Proof Assistant. The "demo" Proof Worksheet for theorem "syllogism" is displayed initially.

$(
<MM> <PROOF_ASST>
THEOREM=syllogism LOC_AFTER=



h1::          
|- (
ph -> ps ) 

h2::          
|- (
ps -> ch ) 

3:2:          
|- (
ph -> ( ps -> ch ) ) 

4:3:          
|- ( (
ph -> ps ) -> ( ph -> ch ) ) 

qed:1,4:      
|- ( ph -> ch ) 



$)

Next, double-click the 'qed' step -- or manually position the input cursor on the 'qed' step, either by left-clicking it with the mouse, or by using the cursor keys on the keyboard, and then press Ctrl-8. Here is what you see (a text-only mockup):

Step
Selector Dialog

Step
qed Unifiable Assertions

ax-mp
::= |- ( ph -> ps )

     &&  |- ( ( ph -> ps ) -> (
ph -> ch ) )

     ==> |- ( ph -> ch )

***END***

          
|Hide Dialog|  |Apply Selection To Step And Unify Proof|

Only one assertion matches the search criteria, ax-mp, and it is displayed on three (selection) lines with the actual, context-dependent substitutions which would be made if "ax-mp" were edit/pasted into the Ref field of the 'qed' step and then Ctrl-U was pressed to perform Unification.

Simply double-click on one of the ax-mp selection lines to update the 'qed' step Ref and Unify the proof! Simple as pie!

Try it!

Step Selector Search Detailed Specifications

Search Sequence	In ascending order by assertion number of hypotheses and within that, by assertion database sequence.
Number of Hypotheses	If the designated Derivation proof step Hyp field contains a "?" or a null/empty hyp number (e.g. "?" "1,2," or "1,,,,,,,," or "?,1") , then only assertions which contain at least the number of input hypotheses are matched by the search. Thus, if the Hyp field equals "1,?" then only assertions with at least one logical hypothesis -- and perhaps more -- will be matched. If the step's Hyp field contains no null/empty hyp numbers and does not contain a "?" then only assertions with exactly the same number of logical hypotheses are matched. Thus, if the Hyp field equals "", then assertions with zero logical hypotheses are matches; if Hyp equals "1", then only assertions with exactly one logical hypothesis are matched, etc.
Hypothesis Sorting	Proof step hypotheses and candidate assertion hypotheses are pre-sorted for input to the StepUnifier algorithm in order to speed up unification. Hypotheses are sorted into descending order by formula length. In addition, for assertion hypotheses, if two hypothesis formulas have the same length, then if a formula has variables in common with the assertion formula that hypothesis sorts first. Note: if incomplete hypotheses or Work Variables are involved in the unification then multiple, different unifications are possible. The specific unification shown on the Step Selector Dialog is merely indicative, and will not always be the same when the assertion label is edited/pasted into the step's Ref field and unification is performed. The regular Proof Worksheet Unification process first attempts unification with the hypotheses in the same order as given by the user, matching them to the unsorted logical hypotheses of the candidate assertion; only if this initial unification fails will the normal Unification process sort the hypotheses.
Assertion Exclusions	The same assertions are excluded as elsewhere in the mmj2 Proof Assistant, by RunParm: `ProofAsstUnifySearchExclude,biigb,xxxid`In addition...the following criteria are used: If the theorem being proved is not new -- it already exists in the input Metamath database -- then only assertions which occur earlier in the Metamath database (have a lower sequence number) are further processed by the search; the rest are excluded. If the theorem is new, then the LOC_AFTER field on the Proof Worksheet comes into play. If LOC_AFTER is not blank, then it contains the label of a Metamath statement, and only assertion which occur earlier in the Metamath database than the LOC_AFTER statement (have a lower sequence number) are further processed by the search; the rest are excluded. Otherwise, if LOC_AFTER is blank and the theorem is new then any assertion in the input Metamath database is further processed by the search.
Distinct Variable Errors	The Step Selector Search does not consider Distinct Variable restrictions in the matching process.
Search Result Maximum	To limit the number of unifiable assertions returned by the Step Selector Search, a Step Selector Max Results menu item is provided on the Unify menu. There is also a "StepSelectorMaxResults" RunParm. The default setting is 50, and the maximum setting is 9,999. This value may be overridden if desired, but caution is advised! Once this number of unifiable assertions is reached during the Step Selector Search process, the search is halted.
Initiation Of Step Selector Search	Double-clicking a Derivation proof step is the easiest and fastest way to initiate the Step Selector Search. It can also be initiated from the Unify menu, or via Ctrl-8, or via the right(alt) mouse click "pop-up" menu. Before the Step Selector Search is actually initiated, the Proof Worksheet text area and the location of the input (keyboard) cursor are input to the Proof Worksheet Parser which attempts to determine which proof step the cursor is on, and whether or not the proof text satisfies the basic field-level and syntactic requirements of a Proof Worksheet. If the Proof Worksheet Parser encounters any errors then an error message is displayed on the Proof Assistant GUI and the Step Selector Search in not initiated. Finally, just prior to initiation of the actual search algorithm, the Proof Unifier attempts unification of the proof steps prior to the selected step within the Proof Worksheet which contain either Work Variables or require use of the "Derive" feature. These preliminary unifications complete the formulas which provide the context in which the selected step will be considered by the Step Selector Search. (Also, a failed "Derive" in an earlier step may result in an error message and prevent initiation of the Step Selector Search.) These preliminary unifications are not returned to the user for display on the Proof Worksheet when the Step Selector Dialog is displayed -- they simply establish the anticipated content of the Proof Worksheet as it will be once an item is selected via the Step Selector Dialog.
Termination Of The Step Selector Search	The Step Selector Search is normally fairly speedy and completes in less than one second. However, if Step Selector Max Results is set to 9999 and certain complex conditions are encountered (involving a combinatorial explosion of unification possibilities for an assertion with a large number of logical hypotheses) -- or if there is a program bug -- the Step Selecteor Search might appear to "hang" or "loop", or just not complete in a reasonable amount of time. A program bug, for example, triggering a Java Runtime error such as "NullPointerException" can trigger termination of the search process behind the scenes and give the appearance of "looping", when in reality processing has stopped altogether (the Command Prompt window will display an ugly looking system dump message...) Anyhooooo...to terminate the search use the "Cancel" menu on the Proof Assistant GUI screen. This will force termination. If all else fails, click on the "X" in the upper-right corner of the Proof Assistant GUI screen and kill the whole thing!. (This information is provided solely for the sake of completeness -- just in case. We find no pleasure in needlessly alarming people with alarmist concerns about horribly catastrophic scenarios...If you ever do encounter a problem like this, simply document the error condition and forward the information to mmj2 Laboratories HQ along with a 100 Euro note; we will cheerfully take the programmers out behind the barn, beat them senseless with shovels, and then feed them to the pigs.)

Step Selector Dialog

The Step Selector Dialog displays the results from the Step Selector Search. Unifiable assertions returned by the search are displayed on the Step Selector Dialog on one line -- aka "selection item" -- per formula. Making a selection on the dialog involves moving the cursor to the desired item, and then either double-clicking the item, clicking on the "Apply..." button, or clicking the right(alt) mouse which displays a pop-up window (with its own buttons and formula display.)

The Step Selector Dialog doesn't just display assertions. When a selection is made the label of the selected assertion is edit/pasted into the Ref field of the designated proof step and then the entire Proof Worksheet is unified. If the results are not what you intended, hit Ctrl-Z twice to Edit/Undo the results of the selection and unification, and then press Ctrl-9 to Reshow the Step Selector Dialog!

This is really very simple and powerful. There are, however, fine points to discuss which may be useful for you to know...

Step Selector Dialog Detailed Specifications

Display Sequence	Results from the Step Selector Search are displayed in ascending order by assertion number of hypotheses and within that, by assertion database sequence.
Display Limit	The Step Selector Max Results parameter (set via Unify menu or RunParm) limits the number of assertions displayed on the Step Selector Dialog. Note that assertions are displayed one line per conclusion and hypothesis, so there will usually be more selection lines than assertions. If fewer unifiable assertions than the Max Results parameter -- or none -- are returned by the Step Selector Search, the final selection item line is "`*END`". If the Max Results parameter is exceeded by the Step Selector Search then the final selection item line is "`MORE*`", which indicates that you may want to rerun the search after updating the Step Selector Max Results parameter.
Show Substitutions	Unifiable assertions are displayed, by default, with the unification substitutions (from the Proof Worksheet into the assertion). If you prefer to see the assertion formulas without substitutions, as they exist in the input Metamath database you can use the "Step Selector Show Substitutions" item on the Unify menu, or via RunParm: `StepSelectorShowSubstitutions,false` Note: the displayed substitutions are indicative and may change slightly when a Step Selector Dialog item is selected and the proof is unified. One reason for this is that the Step Selector Search attempts unification using the sorted hypotheses of the proof step and each candidate assertion, whereas in the normal Unification process unification is first attempted using the proof step hypotheses in the order given on the Proof Worksheet, matching them against the assertion hypotheses in database sequence. And there may be multiple "valid" unifications due to the availability of Work Variables. For example, ax-mp is shown with unification substitutions which are (nearly) always different than a human would choose because the "maj" hypothesis is unified first. (Our bad! Sorry!!! It is not really feasible at this time for mmj2 to explore all possible unifications of a proof step and figure out which is "best" -- the code is fast and stupid.)
Dialog Pane Size	The Step Selector Dialog window "pane" is resizeable, but with imperfect effect. The default pixel size is width = 720, height = 440. You can change these settings with the following RunParms: `StepSelectorDialogPaneWidth,720 StepSelectorDialogPaneHeight,440`
Dialog Is Non-Modal	The Step Selector Dialog is "non-modal", meaning that when the dialog is displayed it does not prevent other windows from being active. And it remains present in the system even though it is "hidden" until you begin work on a different proof.. Together, these characteristics provide you the following capabilities: You can move the Step Selector Dialog pane to the side or bottom of your screen so that you can examine -- and even modify -- the Proof Worksheet. Naturally, if you delete the designated proof step and then select an item on the dialog an error message results! You can "hide" the Step Selector Dialog and then Reshow it using Ctrl-9 or via the Unify menu or the right(alt) mouse button pop-up menu. This allows you to try out various selection items to see how they work -- with judicious use of Ctrl-Z to Edit/Undo and File/Save -- without having to rerun the Step Selector Search!
Step Selector Dialog Popup Window	The Step Selector Dialog pane width is limited and therefore some formulas are too long to be shown on a single line. It is possible to scroll horizontally, but another method is provided so that long formulas can be viewed: right(alt) mouse click on a selection item and a popup window is displayed showing the entire formula. The Step Selector Dialog pop-up window has the title, "Apply Selection To Step And Unify", plus "Yes" and "No" buttons. If you click "Yes" the Step Selector Dialog and the popup window are hidden, and then the selected assertion's label is edit/pasted into the step's Ref field, and the proof is unified. If you click "No", the pop-up window disappears leaving the Step Selector Dialog on display as it was.

Step Selector Search Use Scenarios

1) Bottom-Up Proving: cursor at 'qed' step:

(a)

       
h1::   |- blah-blah

        qed:?: |- blah-blah

or (b)

       
h1::     |- blah-blah

        qed:1:   |-
blah-blah

or (c1)

       
h1::     |- blah-blah

        qed:1,?: |- blah-blah

or (c2 - equivalent to (c1))

       
h1::     |- blah-blah

        qed:1,:  |- blah-blah

   The Step Selector Dialog shows assertions which:

       (a) unify with the 'qed' formula regardless
            of the number of assertion hypotheses
           (>= 0 hypotheses).
       (b) unify with 'qed' formula using just
           step 1 as hypothesis (= 1 hypothesis).
       (c1 and c2) unify with qed step and step 1
           as hypothesis, and have 0 or more
           additional hypotheses.

Unification *will* invoke the standard "Derive" feature and insert the additional hypotheses into the Proof Worksheet as part   of unification.

2) Top-Down Proving -- works exactly the same as Bottom-Up with respect to Step Selector Dialog except that you can do this to find out possibilities for step 3 (below):

   (d1)

       
h1::   |- blah-blah

        h2::   |- blah-blah

        3:1,2: |- &W1

        qed:?: |- blah-blah

(d2)

       
h1::    |- blah-blah

        h2::    |-
blah-blah

        3:1,2,: |- &W1

        qed:?:  |- blah-blah

   The Step Selector Dialog shows assertions which:

       (d1) have exactly two hypotheses that unify
            with steps 1 and 2.
       (d2) have two hypotheses that unify with steps
            1 and 2 -- and have 0 or more additional
            hypotheses.

Notice that step 3's formula is a "dummy" formula consisting of just "&W1", which equates to any wff. If you wish you can constrain the search to any pattern you like by using Work Variables (which may or not already be present in the proof). For example, you would write step 3 like this:

      
3:1,2    |- ( &W1 -> &W2)

      
3:1,2    |- &C1 e. { &S1 e. &C2 | &W1 }

...whatever (as long as it is syntacticallly valid.)

Contents:

`Step Selector Search Cheat Sheet`

What Is It?

Step Selector Search Detailed Specifications

Step Selector Dialog

Step Selector Dialog Detailed Specifications

Step Selector Search Use Scenarios