Bottom-Up Proving by Norm Megill

See also:
Proof Assistant User Guide
ProofAssistantGUIQuickHOWTO.html
ProofAssistantGUIDetailedInfo.html
ProofAssistantGUIDeriveFeature.html
StepUnifier.html
PageLocalRef.mmp
WorkVariables.html
StepSelectorSearch.html
UnifyEraseAndRederiveFormulas.html


Quick Tip:  mmj2 for Metamath Solitaire Users

With the advent of "work variables", the latest releases of mmj2 have hidden inside of them the same algorithm that Metamath Solitaire uses for its unification. (Well, the algorithm may be different, but I mean the same in terms of its outcome.)

So, it is possible to emulate Metamath Solitaire with mmj2.  And unlike the Metamath Solitaire applet, you can save a partially completed proof to continue to work on later.  In addition, mmj2 not only can be used to create proofs forward as Metamath Solitaire does, it can also be used to create them backwards from the conclusion.

Backwards proof example

I'll start with a backwards proof example, since it can be entered "blindly" from an existing Metamath Solitaire proof in a very simple manner.

I'll start at the beginning, assuming you are using Windows, so you won't have to read the mmj2 documentation.  Download the latest mmj2.zip and put it in c:\mmj2.zip.  Extract the Zip file to create c:\mmj2 with default settings.  From the result, move or copy the directory c:\mmj2\mmj2jar to c:\mmj2jar (run c:\mmj2\mmj2jar\copymmj2jar.bat to create and copy c:\mmj2jar -- see below for instructions on running a ".bat" file.)

I assume you have Java installed.  If not, I guess you'll have to read the mmj2 documentation after all.

Next, download set.mm (6MB) into the directory c:\metamath.  Or, if you want it somewhere else, change the parameter

  LoadFile,set.mm

accordingly, using a text editor like Notepad to edit

   c:\mmj2jar\RunParms.txt

You may also need to update the "mmj2Path" parameter in mmj2.bat (command line argument #3 after "mmj2.jar") in:

   c:\mmj2jar\mmj2.bat

Then

In Windows, select Start -> Run, type "cmd", click OK, and a Command Prompt window will open.  Type

  c:\mmj2jar\mmj2.bat

following by Enter to start mmj2.

NOW set mmj2's ProofAsstGUI screen Edit/Set Incomplete Step Cursor menu item to "3" - Last.

A useful reference file for playing with Metamath Solitaire is the http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt pmproofs.txt - Shortest known proofs list.  Each of the 193 proofs begins with two lines:  the theorem itself and the "Result of proof" when you enter the proof into the Metamath Solitaire applet.  The "Result of proof" line is what you want to focus on:  the theorem itself often requires the introduction of definitions, which is beyond the scope of this tutorial and is an exercise for advanced users.

It turns out that all of these 193 theorems also exist in set.mm.  Most of them have definitions incorporated and don't match the "Result of proof".  But some of them do, such as set.mm's "imim2" for theorem "*2.05 Syll".  So for this example, we will pick that one, since it is already in set.mm and we won't have to type it in.

From the mmj2 ProofAsstGUI screen, select File -> New Proof -> imim2.
The screen will look like this:

 $( <MM> <PROOF_ASST> THEOREM=imim2  LOC_AFTER=?

 * A closed form of syllogism (see ~ syl ).  Theorem *2.05 of
   [WhiteheadRussell] p. 100.

 qed::              |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

 $)

We can see that the "qed" step matches the "Result of proof" for theorem "*2.05 Syll", which is what we want.  (For other proofs where it doesn't, we can change the qed step so that it does.)

Look at the proof in the pmproofs.txt file:

  DD2D121; ! 7 steps

Unlike the Metamath Solitaire applet, we are going to enter this proof from left-to-right instead of right-to-left.  The letter D means ax-mp, 2 means ax-2, and 1 means ax-1.

On the mmj2 ProofAsstGUI screen, the cursor should be positioned immediately after the second colon in "qed::".  Here are the exact stepsto enter the proof, following the "DD2D121" above exactly:

Type ax-mp (just the 5 characters "ax-mp" with no Enter), ctrl-u (hold down the ctrl key and press "u"), ax-mp, ctrl-u, ax-2, ctrl-u, ax-mp, ctrl-u, ax-1, ctrl-u, ax-2, ctrl-u, ax-1, ctrl-u.  Voila, the proof is done and will look like this:

 $( <MM> <PROOF_ASST> THEOREM=imim2  LOC_AFTER=?

 * A closed form of syllogism (see ~ syl ).  Theorem *2.05 of
   [WhiteheadRussell] p. 100.

 1000::ax-1             |- ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )
 5000::ax-2         |- (  ( ch -> ( ph -> ps ) )
                       -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
 6000::ax-1         |- (  (  ( ch -> ( ph -> ps ) )
                          -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
                       -> (  ( ph -> ps )
                          -> (  ( ch -> ( ph -> ps ) )
                             -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) ) )
 3000:5000,6000:ax-mp
                    |- (  ( ph -> ps )
                       -> (  ( ch -> ( ph -> ps ) )
                          -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )
 4000::ax-2         |- (  (  ( ph -> ps )
                          -> (  ( ch -> ( ph -> ps ) )
                             -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )
                       -> (  ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )
                          -> (  ( ph -> ps )
                             -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) ) )
 2000:3000,4000:ax-mp
                    |- (  ( ( ph -> ps ) -> ( ch -> ( ph -> ps ) ) )
                       -> ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )
 qed:1000,2000:ax-mp     |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

 $=  wph wps wi wch wph wps wi wi wi wph wps wi wch wph wi wch wps wi
     wi wi wph wps wi wch ax-1 wph wps wi wch wph wps wi wi wch wph wi
     wch wps wi wi wi wi wph wps wi wch wph wps wi wi wi wph wps wi wch
     wph wi wch wps wi wi wi wi wch wph wps wi wi wch wph wi wch wps wi
     wi wi wph wps wi wch wph wps wi wi wch wph wi wch wps wi wi wi wi
     wch wph wps ax-2 wch wph wps wi wi wch wph wi wch wps wi wi wi wph
     wps wi ax-1 ax-mp wph wps wi wch wph wps wi wi wch wph wi wch wps wi
     wi ax-2 ax-mp ax-mp $.
 $)

[Forward Proving Narrative excised by editor]

As a final note, it is sometimes interesting to see if the proof as a whole leads to a more general theorem than the one shown by the 'qed' step.  To do that, just add the last ax-mp in its own new step instead of modifying the 'qed' step.  In this example, a more general theorem does not result, as you can verify as an exercise.

-- Norm 22 Jan 2008.