HomePage → metamath → mmj2 → mmj2ProofAssistantFeedback → mmj2ProofAssistantTutorial
Here is how I use Proof Assistant…
First, I open a Windows "Command Prompt" window (to create a desktop shortcut to "Command Prompt" use Start/Programs/Accessories then right-mouse click Command Prompt and select Create Short-Cut.)
Next, I enter these commands
cd c:\aMyName\myproofs runpagui
Those commands trigger the Proof Assistant GUI (unless the input .mm file has load, validation or grammar errors).
The first command does "change directory" in Windows, making the directory "c:\aMyName\myproofs" the home directory for subsequent commands.
The second command runs a Windows "batch" command file named
"c:\aMyName\myproofs\RunPAGUI.bat".
Notice that the "runpagui" command doesn't care about capitalization or the ".bat" file extension, and since it is stored inside of "c:\aMyName\myproofs" I do not need to specify the directory.
[It is theoretically possible to just double-click on the "c:\aMyName\myproofs\RunPAGUI?.bat" file name inside a Windows Explorer window, but the problem with that is that when the program finishes the window closes automatically, and if there were any error messages, they disappear!]
Here are the contents of "c:\aMyName\myproofs\RunPAGUI?.bat" which could be obtained by copying from C:\mmj2\test\windows\RunPAGUI?.bat and changing the input RunParm? file name at the end:
CALL c:\mmj2\test\windows\RunBatchFramework.bat "c:\mmj2" BatchMMJ2 "c:\aMyName\myproofs\RunParmFileRunPAGUI.txt"
Here are the contents of "c:\aMyName\myproofs\RunParmFileRunPAGUI?.txt"
*================================================== * CommentLine: Example Running ProofAsstGUI *================================================== MaxStatementPrintCount,9999 MaxErrorMessages,15000 MaxInfoMessages,1000 LoadEndpointStmtNbr,999999999 LoadEndpointStmtLabel,pm2.521 LoadFile,c:\metamath\expset.mm VerifyProof,* Parse,* RecheckProofAsstUsingProofVerifier,yes ProofAsstFontSize,14 ProofAsstFormulaLeftCol,20 ProofAsstFormulaRightCol,79 ProofAsstRPNProofLeftCol,5 ProofAsstRPNProofRightCol,79 ProofAsstUnifySearchExclude,biigb,xxxid ProofAsstProofFolder,c:\aMyName\myproofs RunProofAsstGUI
OK! Notice the LoadFile? command is set to read
c:\metamath\expset.mm
which contains the contents of set.mm with all of the proofs in "un-compressed" format.
Also notice that the ProofAsstProofFolder? is set to:
c:\aMyName\myproofs
That is the directory holding my ".txt" (text file) "Proof Worksheets".
A "Proof Worksheet" is what I call the contents of the Proof Assistant screen. This screen is just a big text area, and is free-form, subject to the validation rules of Proof Assistant. At any time you can use
File/Save
or
File/SaveAs
to save the contexts of the Proof Assistant GUI screen – your Proof Worksheet, in other words.
[Now, since I am busy re-proving the first 100 theorems of set.mm as a training exercise, I don't need to update set.mm but I am keeping a copy of my Proof Worksheets.]
OK, the runpagui command displayed the following scren (I show just the Proof Text area here, not the menu options):
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 3:2: |- ( ph -> ( ps -> ch ) ) 4:3: |- ( ( ph -> ps ) -> ( ph -> ch ) ) qed:1,4: |- ( ph -> ch ) $)
That is the initial screen displayed by Proof Assistant GUI. It shows a proof of theorem "syl" from set.mm just prior to the user selecting Unify/StartUnification? (or Ctrl-U).
Since I am resuming work, I use the File/Open command to load saved Proof Worksheet "stoppedhere.txt". This is what appears after File/Open:
$( <MM> <PROOF_ASST> THEOREM=mpcom LOC_AFTER=? h1::mpcom.1 |- ( ps -> ph ) h2::mpcom.2 |- ( ph -> ( ps -> ch ) ) 3:2:com12 |- ( ps -> ( ph -> ch ) ) qed:1,3:mpd |- ( ps -> ch ) $= wps wph wch mpcom.1 wph wps wch mpcom.2 com12 mpd $. $)
Apparently I finished "mpcom" yesterday. I can tell that by the "$=" Generated Proof Step line which shows the Metamath RPN format of the proof.
So, I open up my Mozilla browser and display
file:///C:/metamath/althtml/mmtheorems.html
That is a local copy of the webpage from metamath.org which I have stored on my hard drive for convenience. It shows the first 100 theorems in set.mm.
The next theorem after mpcom is syldd, "Nested syllogism deduction". So I use File/New to start the syldd proof. Here is the the Proof Worksheet that is displayed:
$( <MM> <PROOF_ASST> THEOREM=syldd LOC_AFTER=? h1::syldd.1 |- ( ph -> ( ps -> ( ch -> th ) ) ) h2::syldd.2 |- ( ph -> ( ps -> ( th -> ta ) ) ) 3:: |- ? qed:: |- ( ph -> ( ps -> ( ch -> ta ) ) ) $)
OK, notice that steps 1 and 2 are the logical hypotheses for syldd (as designated by the "h" at the start of the line.)
And notice that step 3 is a skeleton step, which contains just a step number and an initialized formula area set to "?".
The "qed" step is the syldd formula. "qed" is always the step number of the last step of a proof (using a special code like "qed" helps the program know what is intended in the proof.)
[OK, now I am looking at the GUI screen and drawing a blank. I cannot remember what I was doing yesterday, so I look at the the mmtheorems.html page for a little while.
still thinking
still thinking
aha!
]
OK, I remember an identity, which I type into step 3, and then, I see a modus ponens result so I create step 4 using cut and paste, linking steps 1 and 3, and indicate that the qed step has hyps 2 and 4. Here is what the page looks like after typing:
$( <MM> <PROOF_ASST> THEOREM=syldd LOC_AFTER=? h1::syldd.1 |- ( ph -> ( ps -> ( ch -> th ) ) ) h2::syldd.2 |- ( ph -> ( ps -> ( th -> ta ) ) ) 3:: |- ( ( ch -> th ) -> ( ( th -> ta ) -> ( ch -> ta ) ) 4:1,3 |- ( ph -> ( ps -> ( ( th -> ta ) -> ( ch -> ta ) ) ) qed:2,4 |- ( ph -> ( ps -> ( ch -> ta ) ) ) $)
OK, now I press Ctrl-U (shortcut for Menu Option Unify/StartUnification?). Here is the updated Proof Text area:
OOOPS! The UnificationErrors? GUI page appears, with this message:
E-PA-0346 Theorem syldd Step 3: Formula contains one of more grammatical parse errors (somewhere in there). The error is probably a typo, like a missing space or unbalanced parentheses. Note that Metamath is case-sensitive, and in Proof Assistant, '$.' is not used to terminate statements. Proof Text input reader last position at Line: 8 Column: 5
OK, so I add an extra ")" on step 3, like this:
$( <MM> <PROOF_ASST> THEOREM=syldd LOC_AFTER=? h1::syldd.1 |- ( ph -> ( ps -> ( ch -> th ) ) ) h2::syldd.2 |- ( ph -> ( ps -> ( th -> ta ) ) ) 3:: |- ( ( ch -> th ) -> ( ( th -> ta ) -> ( ch -> ta ) ) ) 4:1,3 |- ( ph -> ( ps -> ( ( th -> ta ) -> ( ch -> ta ) ) ) qed:2,4 |- ( ph -> ( ps -> ( ch -> ta ) ) ) $)
and do Ctrl-U again!!!
DANGIT. Another UnificationErrors? GUI page!
E-PA-0346 Theorem syldd Step 4: Formula contains one of more grammatical parse errors (somewhere in there). The error is probably a typo, like a missing space or unbalanced parentheses. Note that Metamath is case- sensitive, and in Proof Assistant, '$.' is not used to terminate statements. Proof Text input reader last position at Line: 12 Column: 7
OK, so I add an extra ")" on step 4, like this:
$( <MM> <PROOF_ASST> THEOREM=syldd LOC_AFTER=? h1::syldd.1 |- ( ph -> ( ps -> ( ch -> th ) ) ) h2::syldd.2 |- ( ph -> ( ps -> ( th -> ta ) ) ) 3:: |- ( ( ch -> th ) -> ( ( th -> ta ) -> ( ch -> ta ) ) ) 4:1,3 |- ( ph -> ( ps -> ( ( th -> ta ) -> ( ch -> ta ) ) ) ) qed:2,4 |- ( ph -> ( ps -> ( ch -> ta ) ) ) $)
and do Ctrl-U again!!!
BINGO!
$( <MM> <PROOF_ASST> THEOREM=syldd LOC_AFTER=? h1::syldd.1 |- ( ph -> ( ps -> ( ch -> th ) ) ) h2::syldd.2 |- ( ph -> ( ps -> ( th -> ta ) ) ) 3::imim1 |- ( ( ch -> th ) -> ( ( th -> ta ) -> ( ch -> ta ) ) ) 4:1,3:syl6 |- ( ph -> ( ps -> ( ( th -> ta ) -> ( ch -> ta ) ) ) ) qed:2,4:mpdd |- ( ph -> ( ps -> ( ch -> ta ) ) ) $= wph wps wth wta wi wch wta wi syldd.2 wph wps wch wth wi wth wta wi wch wta wi wi syldd.1 wch wth wta imim1 syl6 mpdd $. $)
Now, I do File/Save to save syldd.txt in my proofs folder.
And that's that!
But…before exiting I also do a File/SaveAs? to store the contents of the GUI, my Proof Worksheet in file "stoppedhere.txt" so I can remember where I left off when I come back later!
P.S. Here is a new, shorter proof for sylcom. I think the new GUI has proven its worth!!!
$( <MM> <PROOF_ASST> THEOREM=sylcom LOC_AFTER=? h1::sylcom.1 |- ( ph -> ( ps -> ch ) ) h2::sylcom.2 |- ( ps -> ( ch -> th ) ) 3:2:a1i |- ( ph -> ( ps -> ( ch -> th ) ) ) qed:1,3:mpdd |- ( ph -> ( ps -> th ) ) *my $= wph wps wch wth sylcom.1 wps wch wth wi wi wph sylcom.2 a1i mpdd $. *expset.mm $= wps wph wth wps wph wch wth wph wps wch sylcom.1 com12 sylcom.2 syld com12 $. $)