Proof Assistant Step Selector Search

See also:
Proof Assistant User Guide


Step Selector Search Cheat Sheet


    Double-click Derivation step OR
    Ctrl-8 with cursor on Derivation step 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" goofy and awkward sounding!
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.


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 )

           |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


In ascending order by assertion number of hypotheses and within that, by assertion database sequence.
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.
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.
The same assertions are excluded as elsewhere in the mmj2 Proof Assistant, by RunParm:


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. 

The Step Selector Search does not consider Distinct Variable restrictions in the matching process.
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.
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.
Of The
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...) 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


Results from the Step Selector Search are displayed in ascending order by assertion number of hypotheses and within that, by assertion database sequence.
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.
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:

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

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:

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!

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

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

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

        h1::   |- blah-blah
        h2::   |- blah-blah
        3:1,2: |- &W1
        qed:?: |- blah-blah

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