This package contains the program completeusersproof.c, and a second version of
that program, completeusersproofp.c, and associated files.
*******************************************************************************
*******************************************************************************
DESCRIPTION OF completeusersproof, FILES USED BY completeusersproof,
AND ITS OUTPUT FILE
Program name: completeusersproof.c
Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu http://metamath.org
(for the metamath.c base code)and ALAN SARE alansare at alumni.cmu.edu
(for the completeusersproof() function and functions it
(directly) calls).
License terms: GNU General Public License
This program may be run without GUIs or through a GUI run in parallel
with two loaded instances of mmj2, each with a GUI. One of these two
instances of mmj2 may be called as a service by completeusersproof when
the mmj2Unify() function of completeusersproof is called.
Running through the completeusersproof GUI may not be possible using a
non-Windows operating system incompatible with AutoHotkey scripts.
If completeusersproof is run by pressing the GUI button
"Completeusersproof", it then attempts to complete the User's Proof using
the unification theorem means. If the User presses the GUI button
"Completeusersproof mv", it attempts to complete the User's Proof using
the metavariable deduction unification means. For the definitions of the
unification theorem means and the metavariable deduction unification
means, see the comments at the top of completeusersproof(), which begin
on line 1018.
completeusersproof makes the stepprover() function available to the User
as a stand-alone function. The User may open a User's Proof in the mmj2
GUI and apply the "Stepprover" command by pressing the "Stepprover"
button. completeusersproof will then attempt to 2-step prove any
0-hypothesis proof steps which do not unify with a theorem in set.mm. If
there exists in set.mm some theorem which is a semantic variation of such
a step and if there exists in set.mm some 1-hypothesis deduction which
deduces the proof step from that semantic variation, then
completeusersproof will 2-step prove that proof step. This stand-alone
stepprover capability of completeusersproof is intended to be used for
non-Virtual Deduction User's Proofs. For Virtual Deduction proofs, the
stepprover() function is utilized along with other functions upon
application of either the "Completeusersproof" command or the
"Completeusersproof mv" command. If the "Completeusersproof" command or
the "Completeusersproof mv" command is applied to a User's Proof not
written as a Virtual Deduction Proof, then useless steps may be
generated. Applying the "Stepprover" command to a non-Virtual Deduction
proof may generate useful 2-step subproofs without also generating
useless steps which would have been useful only if the User's Proof was
written as a Virtual Deduction Proof.
When completeusersproof is run the Proof Worksheet input by the User
and the text files derived from that Proof Worksheet are edited by
completeusersproof. Some of these text files are also edited by one or
two instances of mmj2. One instance of mmj2 is loaded with both the
set.mm and fd.txt files. The other instance is loaded with only the
set.mm file. completeusersproof is a procedural program which
sequentially edits text files. At certain points during the execution of
completeusersproof the function mmj2Unify() is called. If run through the
GUI, mmj2Unify() "presses" buttons in the GUI of one of the running
instances of mmj2. These button presses unify the text file passed to
mmj2Unify(). Which instance of mmj2 is invoked depends on the value of
the mmj2BatFile argument passed to mmj2Unify(). The button presses are
executed by AutoHotkey scripts (see: https://autohotkey.com )invoked by
mmj2Unify(). These scripts were compiled using the AutoHotkey program.
It is not necessary to install the AutoHotkey program in order to use the
compiled scripts included in the completeusersproof download.
After downloading all needed files, to run completeusersproof through a
GUI, double-click on the c:\mmj2\mmj2jar\completeusersproofGUI.exe file
or run it from the Command Prompt. Three GUIs will open, one for
completeusersproof and one for each of two instances of mmj2. Open the
User's Proof to be processed by completeusersproof in the GUI of the
instance of mmj2 not loaded with fd.txt and press either the
"Completeusersproof" button, the "Completeusersproof mv" button, or the
"Stepprover" button. As long as the three GUI's are open they remain
available for processing User's Proofs on demand. Close the
completeusersproof GUI by pressing the "Exit/Quit" button. Close each
mmj2 GUI by pressing its "Exit/Quit" button.
Sometimes a script will press buttons or send keystrokes before a mmj2
process has completed. This may cause mmj2 to freeze and/or may corrupt a
text file, usually the duplicateUnificationsThm.txt file. Or,
c:\mmj2\mmj2jar\zz~tools*.tmp files may be generated by
completeusersproof. When any of these errors occur the input User's
Proof will not be correctly processed. Corrupted text files should be
restored by over-writing them with a fresh copy. completeusersproof
will not run correctly again unless this is done. If any
c:\mmj2\mmj2jar\zz~tools**.tmp files are generated by a faulty run of
completeusersproof, completeusersproof will not run correctly again
until these files are deleted. If a faulty run of completeusersproof
occurs, depending on the cause, in addition to the above corrective
measures, completeusersproof may not run correctly again until the three
programs are re-booted. Most often, no corrective measures need to be
taken after a failed attempt to process a User's Proof except to try
again using a fresh copy of the original User's Proof. If the User uses
the mouse or keyboard while completeusersproof is processing, these
actions may sometimes interfere with the processing and cause errors.
If completeusersproof is run on a computer which runs relatively slowly
or if it is run on long proofs, then it is possible the AutoHotkey
scripts included in the download may have Sleep statements of
insufficient duration to permit some mmj2 processes to complete. The User
may try to correct this by renaming unifyLD.exe, unifylongLD.exe, and
unifyFFLD.exe, respectively, unify.exe, unifylong.exe, and unifyFF.exe.
If this is done, it is recommended that copies of the original unify.exe,
unifylong.exe, and unifyFF.exe files are saved before overwriting them.
Each Sleep statement of the "LD" verison of a script has a duration of
2 x duration for non-LD version. "LD" is an abbreviation
for "Long Duration". If even the LD versions of the scripts
execute too quickly, the User has the option of increasing the Sleep
statement durations further. This would require downloading the
AutoHotkey program from the AutoHotkey website in order to compile the
revised .ahk files. Of course, the longer the Sleep durations the longer
the runtime of completeusersproof. The Sleep statement durations of
unify.exe, unifylong.exe, and unifyFF.exe are usually sufficient for the
successful application of "Completeusersproof mv" to a9e2ndeqALTUP of
VirtualDeductionProofs.txt, which is the longest proof contained in that
file. Of all of completeusersproof's commands, "Completeusersproof mv"
requires the longest Sleep durations.
The primary advantage of using AutoHotkey scripts for mmj2 unifying
proofs is that the duration for mmj2 unifying shorter proofs is
less than using the mmj2 batch test run parm. For proofs of more
than on the order of 700 steps, mmj2 unification using the mmj2 batch
test run parm may be preferable because the processing duration is not
much longer and because pressing buttons in an mmj2 GUI is sometimes
unreliable. The User has the option of mmj2 unifying longer proofs using
the mmj2 batch test run parm by assigning the second command line
argument the value "onlyShortScripts". This is valuable for mmj2
unification of the duplicateUnificationThms.txt proofs, which are long
for values of utmax greater than 1. If argv2 is assigned the default
value, all mmj2 unifications are by the mmj2 batch test run parm. This
allows completeusersproof to be run on a non-Windows system for which
AutoHotkey scripts are incompatible.
stepprover() attempts to 2-step prove multiple 0-hypothesis steps in
parallel, placing them and their numerous duplicates in a single Proof
Worksheet, duplicateUnificationThms.txt. With the third command line
argument, the User may specify the maximum number of 0-hypothesis steps
to attempt to 2-step prove in parallel. A long User's Proof with more
than eight 0-hypothesis steps to attempt to 2-step prove generates at
least one duplicateUnificationThms.txt Proof Worksheet having more than
3000 steps. If this is too long, it may be avoided by partitioning the
collection of 0-hypothesis steps to 2-step prove into cells of less than
8.
The first command line argument default value specifies that the attempt
to complete the User's Proof is by the unification theorem means. The
value "runCompleteusersproofmv" specifies processing by the metavariable
deduction unification means. The value "runStepprover" specifies only
running the stepprover() function.
If completeusersproof is not run through a GUI, if the User's Proof is
copied onto the file c:\mmj2\mmj2jar\proofWorksheet.txt, the User's Proof
will be processed by double-clicking on the completeusersproof.exe file.
The default values of the command line arguments apply: the unification
theorem means with mmj2 unificiations by the batch test run parm with a
maximum of 8 0-hypothesis steps in-parallel 2-step proof attempts. If a
.bat file is used or completeusersproof.exe is run through the command
prompt, the User may specify the value of each of the three command line
arguments. The three command line arguments afford the User some choices
as to how completeusersproof processes the input User's Proof.
Files of the completeusersproof download:
completeusersproof.c The source code. Unless otherwise
noted, this and all other downloaded
files should be placed in the
c:\mmj2\mmj2jar folder. The mmj2 program
files must be downloaded into their
default folders for completeusersproof to
run.
completeusersproof.exe completeusersproof.c compiled.
completeusersproofp.c The source code for a version of
completeusersproof with pauses. See below
for a description of this program.
completeusersproofp.exe completeusersproofp.c compiled.
is the full path and
filename of the mmj2 Proof Worksheet opened
by the User in the mmj2 GUI of the mmj2
instance which loads set.mm and not fd.txt.
Any path may be used. Of course, this file
is provided by the User and is not included
in the completeusersproof download
package.
VirtualDeductionProofs.txt Example Virtual Deduction Proofs. See
description below.
labels.txt This text file is a list of 1-hypothesis
set.mm labels, each with the potential to
to deduce some step in the Proof Worksheet
from some theorem in set.mm.
fd.txt An mmj2 input file of "false deductions".
This file should be placed in the
c:\metamath folder. A false deduction is a
true deduction for which one hypothesis, a
"unification theorem", is implicit.
completeusersproof explicates the
implicit hypothesis and 2-step proves it if
it is not in set.mm and a semantic
variation of it is. For example, syl is the
true deduction corresponding to
the false deduction ff1,
|- (. ph ->. ps ). infers |- (. ph ->. ch ).
The implicit hypothesis is ( ps -> ch ) .
A deduction with an implicit unification
theorem as a hypothesis which is true from
the User's perspective is false from
Metamath's perspective because Metamath
is implicit-hypothesis-blind.
mapFfToEelUunNumPerm.txt This file specifies the one-one
correspondence between each false deduction
in fd.txt and its true counterpart in
set.mm. Column one contains the false
deduction labels and column two contains
the true deduction labels.
This file also specifies the mapping of
each ff* false deduction label into its
corresponding 0th premutation uun* label.
That label is in the 3rd column of the same
row. In the 4th column of the same row is
the number of permutations of uun* labels
corresponding to the ff* label. The uun*
deductions are described at the beginning
of the completeusersproof() function
definition.
RunParmsFalseDeductionsG.txt File of mmj2 run parameters referenced by
mmj2FalseDeductionsG.bat. This includes
two Loadfile run parms, one for set.mm and
one for fd.txt. The "G" indicates that the
RunProofAsstGUI is an included run parm.
mmj2FalseDeductionsG.bat Executes mmj2 using the run parameters
specified by RunParmsFalseDeductionsG.txt.
Subproofs having at least 1 hypothesis
step not unifying with a deduction in
set.mm unify with some ff* false deduction
in fd.txt. Runs with a GUI.
RunParmsStepProverG.txt File of mmj2 run parameters referenced by
mmj2StepProverG.bat. This includes a set.mm
Loadfile run parm. It does not include an
fd.txt Loadfile run parm. RunProofAsstGUI
run parm included.
mmj2StepProverG.bat Executes mmj2 using the run parameters
specified by RunParmsStepProverG.txt. Runs
with a GUI.
RunParmsFalseDeductions.txt Similar to "G" counterpart (above), except
without RunProofAsstGUI run parm and with
ProofAsstBatchTest run parm.
mmj2FalseDeductions.bat Executes mmj2 using the run parameters
specified by RunParmsFalseDeductions.txt.
RunParmsStepProver.txt Similar to "G" counterpart (above), except
without RunProofAsstGUI run parm and with
ProofAsstBatchTest run parm.
mmj2StepProver.bat Executes mmj2 using the run parameters
specified by RunParmsStepProver.txt.
completeusersproofGUI.exe This file runs an AutoHotkey script. The
script first loads two instances of the
mmj2 program (with their GUIs) by executing
mmj2FalseDeductionsG.bat and
mmj2StepProverG.bat. It then opens a third
GUI window which contains the buttons
"Completeusersproof",
"Completeusersproof mv", "Stepprover", and
"Exit/Quit". Pressing one of the first
three buttons runs completeusersproof.
completeusersproofGUI.ahk AutoHotkey source code of
completeusersproofGUI.exe.
Document-margins.ico Icon in the Titlebar of the
completeusersproof GUI.
completeusersproof.bat Executes completeusersproof.exe
specifying the value of command line
argument argv1 to be the default value
"""".
completeusersproofMv.bat Executes completeusersproof.exe
specifying the value of command line
argument argv1
"runCompleteusersproofmv".
completeusersproofSp.bat Executes completeusersproof.exe
specifying the value of command line
argument argv1 "runStepprover".
unify.exe Executable AutoHotkey script file invoked
by a call of mmj2Unify() with the value
"unify.exe" for the mmj2BatFile argument.
It "presses" the buttons of the mmj2
instance without fd.txt loaded to open,
unify, and save the file which is the
value of the proofWorksheet argument of
the mmj2Unify() call.
unify.ahk Source code for unify.exe.
unifylong.exe Similar to unify.exe. "unifylong.exe" is
passed by a mmj2Unify() call when
proofWorksheet has the value
"duplicateUnificationThms.txt", which may
be a very long Proof Worksheet requiring
longer-than-normal pauses between button
presses to allow mmj2 processes to
complete.
unifylong.ahk Source code for unifylong.exe.
unifyFF.exe Similar to unify.exe except it presses the
buttons of the mmj2 instance with fd.txt
loaded.
unifyFF.ahk Source code for unifyFF.exe.
unifyLD.exe Long Duration version of unify.exe. Each
Sleep statement has a duration of twice the
duration of the non-LD version. The User
has the option to rename this file
unify.exe if the Sleep statement durations
of unify.exe are too short to process a
long proof or to process proofs on a slow
computer.
unifyLD.ahk Source code for unifyLD.exe.
unifylongLD.exe Long Duration version of unifylong.exe.
unifylongLD.ahk Source code for unifylongLD.exe.
unifyFFLD.exe Long Duration version of unifyFF.exe.
unifyFFLD.ahk Source code for unifyFFLD.exe.
proofWorksheet.mmp This file is to be placed in the
c:\mmj2\mmj2jar\myproofs folder. It is the
placeholder file used for all mmj2
unifications of the instance of mmj2 for
which fd.txt is not loaded.
proofWorksheetFF.mmp This file is to be placed in the
c:\mmj2\mmj2jar\myproofs folder. It is the
placeholder file used for all mmj2
unifications of the instance of mmj2 for
which fd.txt is loaded.
proofWorksheet0.mmp This file is to be placed in the
c:\mmj2\mmj2jar\myproofs folder. It is a
copy of proofWorksheet.mmp. Over-write
proofWorksheet.mmp or
duplicateUnificationThms.txt with this
file if either becomes corrupted.
proofWorksheetFF0.mmp This file is to be placed in the
c:\mmj2\mmj2jar\myproofs folder. It is a
copy of proofWorksheetFF.mmp. Over-write
proofWorksheetFF.mmp with this file if it
becomes corrupted.
The completeusersproof output file:
c:\mmj2\mmj2jar\myproofs\ The User's Proof is edited by
completeusersproof. If the User's Proof
is correct and sufficiently detailed, the
output file may contain a
Metamath-generated RPN proof. Otherwise,
as many subproofs of the User's Proof
will be completed as possible. The output
filename is , where is the theorem
label specified in the header of the Proof
Worksheet input by the User. Another file
which holds the same output proof
temporarily is
c:\mmj2\mmj2jar\proofWorksheet.txt. This
file is overwritten with each sucessive
application of completeusersproof.
Primary Functions:
completeusersproof()
addMvSubtheoremTs()
addMvAssertionSteps()
completeusersproofmv()
addUnionizedAssertionPermutations()
pickAPermutationOfEachUnionizedAssertion()
pickALabelPermutation()
substituteLabels()
stepprover()
removeUnneededFfLabels()
nameUsersProofFile()
Some Utility Functions:
mmj2Unify()
translate()
tagLabeledSteps()
endTag()
addMTLast()
addMTMT()
addMTMF()
addMT()
substituteMTMT()
deleteLabel()
*******************************************************************************
*******************************************************************************
THE completeusersproof.exe COMMAND LINE ARGUMENTS
The *char command line arguments of completeusersproof.exe argv[1], argv[2],
and argv[3] are assigned to, respectively, argv1, argv2, and argv3. The User
may customize what completeusersproof does by assigning particular values to
each of these three command line arguments in accordance with the specification
below. If all three command line arguments are omitted, then the three
default values apply. If the second and third arguments are omitted, then
the default values apply to argv2 and argv3. If only the third argument's
value is omitted, the the default value applies to argv3. For all other
combinations the default value of any command line argument, which is any
character string not one of the values defined below, must be explicit.
As an example, if the User wishes to process the User's Proof using the
metavariable deduction unification means, wishes all calls of mmj2Unify()
except the one used to unify duplicateUnificationThms.txt to use AutoHotkey
scripts, and wishes to attempt to 2-step-prove no more than 6 0-hypothesis
steps at a time, then the command to execute completeusersproof is:
completeusersproof.exe runCompleteusersproofmv onlyShortScripts 6
Note that there must be at least one white space between the .exe file and
argv[1] and between adjacent pairs of command line arguments. If a .bat file is
used, this line is the single line of the .bat file. The .bat file has the path
c:\mmj2\mmj2jar . If completeusersproof is run through the command prompt, then
the User types this line in the command prompt for the directory
c:\mmj2\mmj2jar . If completeusersproof is run through the completeusersproof
GUI, then the User may change the pre-existing values for the second and third
command line arguments in completeusersproof.bat, completeusersproofMv.bat, and
completeusersproofSp.bat to other values.
When the completeusersproof Graphic User Interface (GUI) is used for shorter
proofs, it is recommended that argv[2] has the value "onlyShortScripts" and
argv[3] has the default value of 8. "onlyShortScripts" is preferred to the
default value of mmj2-unifying using the mmj2 batch test run parm.
mmj2-unifying using an AutoHotkey script for a shorter Proof Worksheet not a
duplicateUnificationThms.txt Proof Worksheet is usually reliable and is usually
significantly faster than mmj2-unifying using the mmj2 batch test run parm.
mmj2-unifying a duplicateUnificationThms.txt Proof Worksheet using the mmj2
batch test run parm using the default argv[3] value of 8 is reliable without
increasing the run time significantly. For a long User's Proof the default
argv[2] of mmj2-unifying using the mmj2 batch test run parm is most reliable.
argv** VALUE OF argv** DESCRIPTION
argv1 "runCompleteusersproofmv" Attempt to complete the User's Proof
using the metavariable deduction
unification means.
"runStepprover" Run only the stepprover() function on
the User's Proof to try to 2-step
prove each 0-hypothesis step.
using the unification theorem means.
This is the default value. By
convention, the string """" may be
used for this value.
argv2 "onlyShortScripts" duplicationUnificationThms.txt is
mmj2-unified using the mmj2 batch
test run parm. Any other Proof
Worksheet is mmj2-unified using
the AutoHotkey script unify.exe
or(excl.) unifyFF.exe.
"scripts" mmj2 unify using the AutoHotkey
scripts unify.exe, unifylong.exe,
or(excl.) unifyFF.exe
run parm. This is the default value
of argv2. The character string """"
may be used.
argv3 "i", where i = 1 to 8, i is the maximum number of
inclusive 0-hypothesis steps to attempt to
2-step prove in parallel, with all
duplicates in a single
duplicateUnificationThms.txt text
file. mmj2 unifications using
unifylong.exe may not run properly
for larger values of i.
steps to attempt to 2-step prove in
parallel is 8, the default value.
The character string """" or "8"
may be used.
*******************************************************************************
*******************************************************************************
THE VirtualDeductionProofs.txt FILE:
This text file contains example Virtual Deduction Users' Proofs of theorems. A
Virtual Deduction proof is a Natural Deduction proof using conventional or
virtual deduction notation. More information about Virtual Deduction may be
found in the web page description of the set.mm syntax definition wvd1 .
completeusersproof completes each proof in VirtualDeductionProofs.txt. For any
proof, if the labels specified in the brief description are excluded from the
unification search, then there will be no distinct variable violations.
*******************************************************************************
*******************************************************************************
PROCEDURE FOR USING completeusersproof WITHOUT GUIs
step 1. Download the current version of set.mm from the Metamath website. Place
it in the folder c:\metamath .
step 2. Download the latest version of mmj2.zip from the Metamath website.
Unzip it and place all extracted folders and files in the
c:\mmj2 folder.
step 3. Download completeusersproof.zip from the Metamath website. This file
is connected to the "completeusersproof" hyperlink of
Metamath Home Page > Other Metamath-Related Topics
> Other tools for Metamath. Place the extracted files in the
c:\mmj2\mmj2jar folder.
step 4. Move fd.txt in the c:\mmj2\mmj2jar folder to the c:\metamath folder.
Move proofWorksheet0.mmp, proofWorksheet.mmp, proofWorksheetFF0.mmp,
and proofWorksheetFF.mmp from the c:\mmj2\mmj2jar folder to the
c:\mmj2\mmj2jar\myproofs folder.
step 5. Create a proof of a theorem on a valid mmj2 Proof Worksheet. Use
mmj2 to verify it contains no errors such as, for example, that there
is an invalid symbol in a proof step or a formula contains one or more
grammatical parse errors. If the first command line argument of the
completeusersproof.exe .bat file is "runStepprover", then
completeusersproof will attempt to 2-step-prove each 0-hypothesis step
which does not unify with a theorem in set.mm. The intended User's
Proof is any proof in conventional notation. If this is not the value
of the first command line argument, then the User's Proof should be
a Virtual Deduction proof, although some subproofs of a non-Virtual
Deduction proof may be completed by completeusersproof and any valid
mmj2 Proof Worksheet is acceptable.
step 6. Copy the Proof Worksheet created in step 5 onto
c:\mmj2\mmj2jar\proofWorksheet.txt. This is the input file.
step 7. completeusersproof will process a User's Proof by running only the
stepprover() function, by attempting to complete subproofs by the
unification theorem means, or(excl.) by attempting to complete
subproofs by the metavariable deduction unification means. The value of
the first command line argument specifies which of these three means
will be used to process the User's Proof. If no value is specified,
the User's Proof will be processed by the unification theorem means,
the default means. The command line arguments are described above. The
default values for the second and third command line arguments should
be used because GUIs are not being used. Run completeusersproof.exe
through the command prompt specifying the desired first command line
argument value or by double-clicking either the completeusersproof.bat,
completeusersproofSp.bat, or completeusersproofMv.bat with the second
and third command line arguments omitted. If processing the User's
Proof by the unification theorem means, because that is the
default for the first command line argument, completeusersproof may
be run by double-clicking on the completeusersproof.exe file. The
filename of the output file is the theorem name specified in the header
of the User's Proof. The path of the output file is
c:\mmj2\mmj2jar\myproofs. A second copy of the output file is
c:\mmj2\mmj2jar\proofWorksheet.txt (which overwrites the input file).
This copy will be overwritten with the processing of the next User's
Proof.
step 8. Delete from the c:\mmj2\mmj2jar folder any zz~tools**.tmp files
which may have been generated by running completeusersproof. If a
file needed by completeusersproof can't be found, zz~tools**.tmp
files will be created. After they have been created, subsequent runs
of completeusersproof may be compromised due to the existence of these
files.
*******************************************************************************
*******************************************************************************
PROCEDURE FOR USING completeusersproof WITH GUIs
step 1. Same as step 1 above.
step 2. Same as step 2 above.
step 3. Same as step 3 above.
step 4. Same as step 4 above.
step 5. Same as step 5 above.
step 6. double-click on the c:\mmj2\mmj2jar\completeusersproofGUI.exe file or
run this file through the command prompt. This will run the two mmj2
instances mmj2StepProverG.bat and mmj2FalseDeductionsG.bat and their
GUIs will open. Also, the completusersproof GUI will open.
completeusersproofGUI.exe will not run on a non-Windows operating
system not able to run AutoHotkey scripts. For such systems use the
above "PROCEDURE FOR USING completeusersproof WITHOUT GUIs".
step 7. open the file containing the User's Proof in the GUI entitled
"ProofAsstGUI - proofWorksheet.mmp". The file may have any path and
any filename although the User may prefer that the filename matches
the theorem name in the Proof Worksheet header. The filename of the
output file is the theorem name of specified in the header of the
User's Proof. The path of the output file is c:\mmj2\mmj2jar\myproofs.
A second copy of the output file is c:\mmj2\mmj2jar\proofWorksheet.txt.
This copy will be overwritten with the processing of the next User's
Proof.
step 8. The completeusersproof GUI contains the buttons "Completeusersproof"
for processing using the unification theorem means by running
completeusersproof.bat, "Completeusersproof mv" for processing using
the metavariable deduction unification means by running
completeusersproofMv.bat, and "Stepprover" to run only the stepprover()
function by running completeusersproofSp.bat. Press one of those
buttons and the User's Proof will be processing using the existing
command line arguments of the applicable .bat file. If the second
and/or third command line argument value the User wishes to use is
different from the existing value, the User should change it(them).
If the User wishes to do mmj2 unifications using AutoHotkey scripts,
then it is necessary to open the GUIs. With the GUIs open, the user
may specify the second argument value "scripts", "onlyShortScripts",
or(excl.) """" . If "scripts" is specified, every mmj2 unification
is by an AutoHotkey script. If "onlyShortScripts" is specified, then
the file duplicateUnificationThms.txt is mmj2-unified using the
mmj2 batch test run parm and each other Proof Worksheet is
mmj2-unified using an AutoHotkey script. If value of argv[2] is
the default value, then each Proof Worksheet is mmj2-unified using
the mmj2 batch test run parm. The default value of argv[3] creates
duplicateUnificationThms.txt Proof Worksheets with a maximum of 8
0-hypothesis steps to be attempted to be 2-step-proved in parallel. If
the value of argv[3] is specified to be "i" for 0 < i < 9 , then a
maximum of i 0-hypothesis steps will be attempted to be 2-step-proved
in parallel. See above for the command line argument values
specification.
step 9. If an error or errors occurred, most often because a script run has
errors, e.g., the GUI freezes and the execution of the script must
be terminated, then corrupted text files should be overwritten with
fresh copies. For example, proofWorksheet.mmp should be overwritten
by proofWorksheet0.mmp and a corrupted duplicateUnificationThms.txt
file should be overwritten with proofWorksheet0.mmp (or any other
uncorrupted text file). Delete from the c:\mmj2\mmj2jar folder any
zz~tools**.tmp files which may have been generated by running
completeusersproof.
step 10. While the GUIs remain open the User may return to step 7 to process
another User's Proof. As many User's Proofs may be processed as
desired. Press the "Exit/Quit" button in the completeusersproof GUI to
close it. Press the "Exit/Quit" button in each mmj2 GUI to close each.
*******************************************************************************
*******************************************************************************
DESCRIPTION OF completeusersproofp.c
completeusersproofp.c is identical to completeusersproof.c except for
intermittent "printf("point **");" or "printf("");"
and "getchar();" pairs of statements which pause execution until the User
presses . "point **" or "" identifies the line
in the program at which execution has paused. At each pause the User is
afforded the opportunity to observe the text file being edited by the
program and to observe which statement executions caused the observed
alterations.
Files which the User may be interested in observing include proofWorksheet.txt,
proofWorksheet0.txt, unifThms.txt, and duplicateUnificationThms.txt.
To observe a text file as it changes, keep the text file displayed during
execution of the program. While execution is paused, click anywhere in the text
file window. This will minimize the ms-dos window and, if TextPad is the text
editor being used, cause a window to pop up stating: "Another application has
updated file c:\mmj2\mmj2jar\.txt. Reload it?" Press "Yes" to update the
file. After viewing the updated text file, maximize the ms-dos window and press
enter to resume execution. Repeat this procedure for every pause in program
execution or only for pauses at points of interest. If completeusersproofp.c
is also kept open during execution of completeusersproofp.exe, then one may
concurrently observe the text file changes and the statements of the code
causing them. The code statements causing changes may be identified by the
statements printed in the console. For example, the changes made to
proofWorksheet.txt immediately preceding the pause at "Point 7 of
completeusersproofmv()" are due to the three statements occurring between the
"Point 6 of completeusersproofmv()" (line 2345 of completeusersproofp.c) and
"Point 7 of completeusersproofmv()" (line 2359 of completeusersproofp.c) print
statements.
The real-time observation of text file changes and the code statements causing
them may be useful for learning the program, for finding program bugs, for
finding deficiencies in data files used by the program, and for finding errors
in the input Proof Worksheet.
completeusersproofp.exe should not be run through with GUIs because the
button-pressing actions associated with observing the text files as they
change may interfere with the running of the AutoHotkey scripts. The default
value for argv[2] should be used so that mmj2 unifications are performed by
the mmj2 batch test run parm. The User may choose values for argv[1] and
argv[3]. For example, the following command prompt command will run
completeusersproofp.exe processing the User's Proof using only the stepprover()
function with a maximum of 4 0-hypothesis step 2-step proof attempts made in
parallel for each duplicateUnificationThms.txt file with mmj2 unifications
performed by mmj2 batch test.
c:\mmj2\mmj2jar>completeusersproofp.exe runStepprover "" 4
*******************************************************************************
*******************************************************************************
AVOIDING UNIFICATIONS WITH REFERENCE THEOREMS WITH UNNECESSARY DISTINCT
VARIABLE REQUIREMENTS
completeusersproof may sometimes unify some proof steps with a reference
theorem(s) with distinct variable requirements which are not necessary to the
proof. In such a case, another(other) reference theorem(s) without distinct
variable requirements or with fewer distinct variable requirements also
unifies(unify) with the relevant proof step(s). The only reason the reference
theorem(s) with the unnecessary distinct variable requirements is(are) picked
by completeusersproof over the reference theorem(s) with no or lesser distinct
variable requirements is because it(they) precede(s) the latter reference
theorem(s) in set.mm.
The unnecessary distinct variable requirements may be avoided by temporarily
adding the offending theorem(s) to the list of theorems to be excluded
from the mmj2 unification search of the RunParmsStepProver.txt,
RunParmsStepProverG.txt, RunParmsFalseDeductions.txt, and
RunParmsFalseDeductionsG.txt run parm ProofAsstUnifySearchExclude. If the
program is run again on the original User's Proof, unless another reference
theorem(s) with unnecessary distinct variable requirements unifies(unify) with
the same step(s), the completed proof will not have any unnecessary distinct
variable requirements for that(those) step(s). If a non-excluded reference
theorem(s) with distinct variable requirements unifies with the same step(s),
it(they) too should be excluded. This may be repeated until a completed proof
with the minimum distinct variable requirements is found. If a reference
theorem(s) with distinct variable requirements is(are) excluded and the
User's Proof does not complete, then it is easily determined which reference
theorems with distinct variable requirements are necessary with respect to the
input User's Proof. It is possible that a different proof may exist with fewer
or no distinct variable requirements.
A search exclusion(s) should be specific to a particular proof and should be
removed from the search exclusion list after applying it(them) to that proof.
Otherwise, a future proof may not complete only because a step(s) of the proof
require(s) an excluded reference theorem(s).
A similar strategy may be employed as an alternative means of avoiding
unifications with theorems not in the main set.mm (theorems in Mathboxes).
A computer-assisted procedure to remove labels which violate the distinct
variable requirements of the User's Proof is as follows.
step 1. Complete the User's Proof using completeusersproof.
step 2. If the distinct variable requirements of the Proof
generated by completeusersproof are greater than necessary,
add the proof to set.mm and specify the lesser distinct variable
requirements of the User's Proof. Run the "verify proof" command
of the metamath program. The program will identify the distinct
variable requirement violations.
step 3. Add the offending labels as labels to be excluded to the
ProofAsstUnifySearchExclude run parms.
step 4. Run completeusersproof again.
step 5. Repeat steps 2, 3, and 4 until all distinct variable violations
are removed.
*******************************************************************************
*******************************************************************************
DETAILED DESCRIPTION OF THE completeusersproof.c PROGRAM
MOTIVATION FOR COMPLETEUSERSPROOF. As explained in the description of
wvd1, Natural Deduction is a powerful strategy for proving theorems
and deductions. Natural Deduction uses a Gentzen-type system. We are
motivated to write Natural Deduction proofs (for the power of proving
using a Gentzen-type system) and verify them using Metamath's
proofchecking capability. Metamath uses a Hilbert-type deductive system.
As explained in wvd1, the virtual deduction notation has been added to
set.mm to have a language of a Hilbert-type deductive system which
can be used like a Gentzen-type system. Using the virtual deduction
notation of set.mm, one can effectively write Natural Deduction Proofs
in the virtual deduction language of Metamath. We call these proofs
Virtual Deduction proofs. A Virtual Deduction proof is the
Metamath-specific version of a Natural Deduction Proof.
A Virtual Deduction proof generally cannot be directly input on a mmj2
Proof Worksheet and completed by the mmj2 tool because it is usually
missing some technical proof steps which are not part of the Virtual
Deduction proof but are necessary for a complete Metamath Proof. These
missing technical steps may be automatically added by an automated
proof assistant. completeusersproof is such a proof assistant.
completeusersproof adds the missing technical steps and finds the
reference theorems and deductions in set.mm which unify with the
subproofs of the proof.
The User may write a Virtual Deduction proof and automatically transform
it into a complete Metamath proof using the completeusersproof tool. The
completed proof has been checked by the Metamath program. The task of
writing a complete Metamath proof is reduced to writing what is
essentially a Natural Deduction Proof.
Generally, proving using Virtual Deduction and completeusersproof
reduces the amount Metamath-specific knowledge required by the User.
Often, no knowledge of the specific theorems and deductions in set.mm
is required to write some of the subproofs of a Virtual Deduction
proof. Often, no knowledge of the Metamath-specific names of reference
theorems and deductions in set.mm is required for writing some of the
subproofs of a User's Proof. Often, the User may write subproofs of
a proof using theorems or deductions commonly used in mathematics and
correctly assume that some form of each is contained in set.mm and that
completeusersproof will automatically generate the technical steps
necessary to utilize them to complete the subproofs. Often, the fraction
of the work which may be considered tedious is reduced and the total
amount of work is reduced.
* * *
completeusersproof() is the single primary function of the
completeusersproof program. All other functions used by the
completeusersproof program are called by completeusersproof().
The input Proof Worksheet is the "User's Proof". It is intended to be a
correct Virtual Deduction proof. completeusersproof completes each
subproof of the translated User's Proof it is capable of
completing.
What do we mean by the term "subproof"? A subproof of the User's
Proof might have been called simply a deduction within the User's Proof.
We do not call it a deduction because a technical step or steps
automatically added to the proof which are associated with the deduction
may change the deduction into a deduction with more steps or may create
an additional deduction associated with the modified or unmodified
original deduction. The new collection of associated steps may not be a
single deduction and therefore cannot properly be called a deduction.
Therefore, we call the original deduction and this new collection of steps
arising from the original deduction a subproof. Our narrow definition
differs from the usual definition of subproof. For the usual definition of
subproof, a subproof may include many deductions of a proof. For our
narrow definition, a subproof arises from and is associated with a single
deduction of the original User's Proof. The original single deduction is
also a subproof.
DEFINITION OF A VIRTUAL DEDUCTION.
A Theorem fine is Deduction,
For it allows work-reduction:
To show "A implies B",
Assume A and prove B;
Quite often a simpler production.
-- Stefan Bilaniuk
In Sequent Calculus, for the implication ( ( ph /\ ps ) -> ch ) , each
conjunct of the antecedent is thought of as a hypothesis and the
consequent is thought of as an assertion of the deduction ph and ps infers
ch. ph and ps are not actual hypotheses and ch is not an actual assertion.
We call ph a "virtual hypothesis" because it is not an actual hypothesis.
ch is a "virtual conclusion" because it is not an actual assertion. Just
as the virtual image seen in a plane mirror is not actual or real because
it is formed in a location light does not actually reach,
( ( ph /\ ps ) -> ch ) is a "virtual deduction" because it is not an
actual or real deduction. We are motivated to think in terms of virtual
objects because "it allows work-reduction" and because proving is "Quite
often a simpler production." We call the proving style where one
interprets the well-formed formula of each proof step to be a virtual
deduction "Virtual Deduction" instead of "Natural Deduction" because
Virtual Deduction may be given the above meaning and because Natural
Deduction has a broader meaning than this Metamath-specific style with its
own special notation.
In the written description of wvd1 a virtual deduction is defined to be
the analog in H of a sequent in G1. The connective ->. (a mediator
connective) separates the virtual hypothesis collection on the left side
of ->. from the virtual conclusion on the right side of ->. . A virtual
deduction with no ->. connective is a virtual deduction with no virtual
hypotheses. A virtual deduction with no virtual hypotheses may be
alternatively written in "standard T form". The empty virtual hypothesis
collection is defined to be T. . |- and |- (. T. ->. ).
denote equivalent virtual deductions, the latter being the former in
standard T form. More about the standard T form may be found below.
Only the User's Proof is written using Virtual Deduction notation. The
User's Proof with as many subproofs as possible completed by
completeusersproof is in conventional notation. This conventional
notation complete or partially complete proof may be interpreted as a
conventional notation virtual deduction proof.
DEFINITION OF A CONVENTIONAL NOTATION VIRTUAL DEDUCTION. A conventional
notation virtual deduction is a virtual deduction with conventional
notation symbols substituted for virtual deduction symbols. If a
conventional notation virtual deduction has no -> connective, then it
has no virtual hypotheses. If one or more -> connectives occur in it,
then the outermost -> connective is the mediator connective or(excl.)
none of the -> connectives is the mediator connective and there are no
virtual hypotheses.
Some conventional notation virtual deductions are susceptible to more than
one interpretation. The virtual deduction's context usually fully
determines which interpretation is the correct one. As an example of
ambiguity, the conventional notation virtual deduction
|- ( x e. A -> x C_ B ) may correspond to the virtual deduction
|- (. x e. A ->. x C_ B ). or(excl.) to the no-virtual-hypotheses
virtual deduction |- ( x e. A -> x C_ B ) .
The reason each step of a User's Proof is specified to be a virtual
deduction with virtual deduction notation is to assure that each
step of the proof has a unique interpretation. After the proof is
translated, the correct interpretation of any original step, now a
conventional notation virtual deduction, may be determined by its
interpretation prior to translation if context alone is insufficient for
disambiguation.
The completeusersproof program relies on the virtual deduction notation
because there is no ambiguity. Therefore, it is necessary for the User's
Proof to be in Virtual Deduction notation in order to utilize the full
potential of completeusersproof to complete as many of the subproofs of
the User's Proof as possible. If a User's Proof is not written as a
Virtual Deduction proof, then completeusersproof will interpret each step
of the proof to be a virtual deduction with no virtual hypotheses.
One sufficient reason why conventional notation virtual deductions are
used is because the theorems and deductions in set.mm are in conventional
notation and are fully utilized if and only if the steps of the User's
Proof are translated into the same conventional notation after the
disambiguation information contained in the original Virtual Deduction
proof is extracted and saved. It is saved in the ff* labels. A virtual
deduction subproof cannot unify with a theorem or deduction in the main
set.mm unless it is in conventional notation.
The power of Natural Deduction in simplifying proving is fully realized
by writing proofs using virtual deduction wwfs, which are the analog in H
of sequents in G1 (see: the description of wvd1). It is possible to use
only conventional notation virtual deductions and prove by Natural
Deduction, but, in so doing, the proof writer has the burden of writing
in a language for which some wffs are subject to more than one
interpretation. More importantly, the full proof-completing potential of
completeusersproof is not realized.
* * *
We will sometimes refer to a conventional notation virtual deduction as
a "virtual deduction". Context usually determines whether "virtual
deduction" means a virtual deduction in non-conventional notation or a
conventional notation virtual deduction.
It is intended that any User's Proof to which completeusersproof will
be applied is input as a Virtual Deduction proof in non-conventional
notation. A proof is a Virtual Deduction proof in non-conventional
notation if every step of the proof is a virtual deduction in
non-conventional notation.
Early in the execution of completeusersproof the original Virtual
Deduction proof in non-conventional notation is translated into
a conventional notation Virtual Deduction proof. Of the steps of the
proof automatically generated by completeusersproof towards the goal
of completing the original proof, which the exception of non-unionized
assertion steps, each added step is a conventional notation virtual
deduction. The wff of a non-unionized assertion step is not a virtual
deduction unless every element of its collection of virtual hypothesis
collections is a virtual hypothesis. Many of the terms used above are
defined below.
The virtual deduction
|- (. (. Tr A ,. ( z e. y /\ y e. A ) ). ->. z e. A ). (wff1)
is automatically translated by completeusersproof to be
|- ( ( Tr A /\ ( z e. y /\ y e. A ) ) -> z e. A ) (wff2)
wff2 is the conventional notation virtual deduction counterpart of the
virtual deduction wff1. There are two virtual hypotheses. One is Tr A .
The other is ( z e. y /\ y e. A ) . The virtual conclusion is z e. A .
Every virtual deduction has one and only one virtual conclusion. For a
virtual deduction in Virtual Deduction notation, " ,. " separates pairs of
adjoining virtual hypotheses. In a conventional notation virtual deduction
" /\ " may have the role of separating a pair of adjoining virtual
hypotheses or(excl.) may be a component symbol (the conjunction symbol) of
a virtual hypothesis or a virtual conclusion.
( Tr A /\ ( z e. y /\ y e. A ) ) is the virtual hypothesis collection of
wff2.
With translation, " ,. " becomes " /\ ", " ->. " becomes " -> ", " (. "
becomes " ( ", and " ), " becomes " ) ".
There are three possible interpretations of wff2. The correct
interpretation is the same interpretation as wff1. One incorrect
interpretation interprets wff2 to have a single virtual hypothesis,
( Tr A /\ ( z e. y /\ y e. A ) ) . The other incorrect interpretation is
that wff2 has no virtual hypotheses, the entire wff being a virtual
conclusion.
A metavariable deduction is a deduction for which each hypothesis step may
be interpreted to be a conventional notation virtual deduction having a
virtual hypothesis collection which is a wff variable. We use the term
"metavariable" for the wff variable as Mario Carneiro has in his
presentation "Natural Deduction in the Metamath Proof Language" presented
in the summer of 2014. We say a metavariable deduction is in standard form
if the elements of the collection on the left side of the mediator -> of
its assertion are exactly the virtual hypothesis collections of the
hypothesis steps. Unless a standard form metavariable deduction has only
one hypothesis, its assertion is not a virtual deduction because its
collection of virtual hypothesis collections is not a virtual hypothesis
collection. We could have defined this collection to be a virtual
hypothesis collection on the ground that a wff variable is an single
variable. We don't use that definition because a wff variable is a
schemata for a virtual hypothesis collection. An example of a standard
form metavariable deduction in set.mm is trelded.
We say that the collection of virtual hypothesis collections of the
assertion of a standard form metavariable deduction with more than one
hypothesis is "non-unionized" and that the assertion is a non-unionized
assertion. We use the term "union" because unionizing a collection of
virtual hypothesis collections to obtain a virtual hypothesis collection
is analogous to taking the union of a class. We define a "unionized
assertion" to be an assertion derivable from a non-unionized assertion by
unionizing its collection of virtual hypothesis collections. The
unionized collection is a virtual hypothesis collection consisting of the
elements of the elements of the collection of virtual hypothesis
collections of the non-unionized assertion. We adopt the convention that
the virtual hypothesis collection of a unionized assertion contains no
duplicate elements. It is undesirable for a virtual hypothesis collection
to contain duplicate virtual hypotheses because the virtual hypothesis
collection is denoted by a longer and more complex character string which
does not contain more information. More importantly, if the operation of
unionizing a non-unionized collection of virtual hypothesis collections
did not include the removal of duplicate virtual hypotheses, then there
would exist a multiplier effect whereby proof steps with virtual
hypothesis collections containing duplicate virtual hypotheses which are
hypothesis steps of other proof steps would spawn more duplicate virtual
hypotheses.
One possible way a subproof may be completed is by unifying it with a
standard form metavariable deduction in set.mm. If the unifying
standard form metavariable deduction in set.mm is a 1-hypothesis
deduction, then it will unify with the original deduction of the subproof.
If the unifying standard form metavariable deduction in set.mm has more
than one hypothesis, then it will not unify with the original deduction of
the subproof because the assertion of the original deduction is unionized
whereas the assertion of the metavariable deduction in set.mm is not.
completeusersproof generates a non-unionized assertion. The deduction of
that non-unionized assertion, which has the same hypotheses as the
original deduction, unifies with the metavariable deduction in set.mm.
The assertion of the original deduction is deduced from the non-unionized
assertion with a 1-hypothesis uun* deduction. That deduction is the second
deduction of the subproof. The number of steps of the subproof
increases by one step. That added step is the non-unionized assertion.
The non-unionized assertion immediately precedes the unionized assertion,
which is the original assertion of the subproof. completeusersproof
automatically generates the contents of the hypothesis field of the
non-unionized assertion step to be the same as the original contents of
the hypothesis field of the original assertion. completeusersproof deletes
the original contents of the original assertion's hypothesis field and
inserts into that hypothesis field the step number of the non-unionized
assertion step.
Each metavariable deduction in standard form in set.mm has a particular
ordering of metavariable virtual hypothesis collections within the
collection of virtual hypothesis collections of its assertion. The
ordering of the virtual hypothesis collections of the collection of
virtual hypothesis collections of the generated non-unionized assertion of
a deduction of a subproof of a Proof Worksheet to be unified with a
metavariable deduction in set.mm must match the ordering of the collection
of the assertion of the metavariable deduction in set.mm. Therefore, all
possible permutations of the ordering of the virtual hypothesis
collections within the collection of virtual hypothesis collections of the
non-unionized assertion must be tried. completeusersproof generates one
non-unionized assertion for each permutation. The hypothesis steps of each
deduction corresponding to each non-unionized assertion permutation are
the same. They are the hypothesis steps of the original subproof. If one
or more of these deductions unifies with one or more standard form
metavariable deductions in set.mm, then one of the unifying deductions is
picked by completeusersproof to be that metavariable deduction in set.mm
to complete the non-unionized asssertion's deduction of the subproof. The
remaining non-unionized assertion permutations are deleted. If no
deduction permutation unifies with a standard form metavariable deduction
in set.mm, then all non-unionized assertion permutations are deleted and
the subtheorem is not completed.
For each ff* false deduction corresponding to a subproof of the User's
Proof there corresponds a collection of uun* labels which contains all
possible permutations of uun* deductions which deduce the unionized
assertion from the non-unionized assertion permutations. For example, the
virtual hypothesis collections for the two hypotheses of a subproof of a
User's Proof may be ( /\ ) and . Then there are a
total of two uun* permutations, each deducing the unionized assertion from
one of the two non-unionized assertion permutations. One has as its
hypothesis an assertion with the collection of virtual hypothesis
collections ( ( /\ ) /\ ) and the other
( /\ ( /\ ) ) . The unionized assertion for both
deductions is the same and is the assertion of the original subproof. Its
virtual hypothesis collection is either ( /\ ) or(excl.)
( /\ ) . If there exists a non-unionized assertion deduction
permutation which unfies with a standard form metavariable deduction in
set.mm and that deduction is picked by completeusersproof, then the uun*
deduction corresponding to the former deduction's non-unionized assertion
deduces the unionized assertion of the original subproof from that
non-unionized assertion. Both deductions of the subproof are completed and
the subproof is completed. This means by which an attempt is made to
complete a subproof is called the metavariable deduction unification
means. Included in this means is putting in standard T form any
no-virtual-hypothesis steps of the original subproof.
If the virtual hypothesis collections of the hypotheses of a metavariable
deduction in standard form in set.mm are identical, then the union of the
the collection of virtual hypothesis collections of its hypotheses is
identical to the virtual hypothesis collection of each hypothesis. Any
metavariable deduction in set.mm having the same virtual hypothesis
collection metavariable for each hypothesis may have as its assertion a
virtual deduction having the same virtual hypothesis collection as the
hypotheses. A metavariable deduction in this form will unify with a
subproof in a Proof Worksheet using mmj2 alone. Mario Carneiro has
employed this metavariable deduction form for many deductions he has
added to set.mm. He discussed it in his presentation "Natural Deduction
in the Metamath Proof Language". We shall call a metavariable deduction in
this form a MC metavariable deduction.
Some steps of a User's Proof may have no virtual hypotheses. For example,
|- A C_ suc A (wff3)
may be such a step in a User's Proof. It is originally a virtual deduction
in non-conventional notation. Upon translation of the proof, it becomes a
conventional notation virtual deduction. Because it has no virtual
hypotheses, the syntax of wff3 is the same whether it is interpreted as a
virtual deduction in non-conventional notation or a conventional notation
virtual deduction. wff3 may be put in "standard T form" so that it is a
virtual deduction having a virtual hypothesis collection which is empty.
|- (. T. ->. A C_ suc A ). (wff4)
wff4 is wff3 in standard T form. wff4 translated is
|- ( T. -> A C_ suc A ) (wff5)
Both wff4 and wff5 are virtual deductions. wff4 is a virtual deduction in
non-conventional notation and wff5 is a conventional notation virtual
deduction. Both have the same interpretation.
In order for completeusersproof to attempt to mv-complete a subproof
of the User's Proof (complete it by unifying it with a metavariable
deduction in set.mm) it puts each no-virtual-hypotheses step of the
subproof into standard T form. This is necessary because every
hypothesis of a metavariable deduction in set.mm has a metavariable
virtual hypothesis collection.
The union of a singleton is its element. U. { A } = A . A virtual
hypothesis collection differs from a class in that, among other things, a
singleton virtual hypothesis collection is identical to the virtual
hypothesis it contains. If x e. A is the virtual hypothesis of a singleton
virtual hypothesis collection, then that collection must be denoted by
x e. A because ( x e. A ) is syntactically invalid.
If the virtual hypothesis collection of each hypothesis of a subproof is
a singleton and these virtual hypothesis collections are distinct, then
the collection of these virtual hypothesis collections is a virtual
hypothesis collection. This collection may be denoted by each one of n
possible wffs, one wff for each virtual hypothesis ordering permutation,
where n is the number of virtual hypothesis ordering permutations. One of
those permutations is the virtual hypothesis collection of the (unionized)
assertion of the original subproof. If there exists a standard form
metavariable deduction in set.mm whose assertion has a collection of
virtual hypothesis collections with a virtual hypothesis collection
ordering matching that of the assertion of the original subproof, then it
will unify with the original subproof and the subproof will be completed
by mmj2 unification alone. No non-unionized assertion will be generated.
If the standard form metavariable deduction in set.mm which completes the
subproof has an assertion with a collection of virtual hypothesis
collections with a different ordering, then completeuserproof will
find the non-unionized assertion permutation which matches the permutation
of the standard form metavariable deduction in set.mm and the subproof
will be completed by adding that non-unionized assertion permutation step.
( /\ ( /\ ) /\ T. ) is a collection of virtual
hypothesis collections occuring in a completeusersproof-generated
non-unionized assertion of a subproof of a Proof Worksheet. is
the virtual hypothesis collection of one hypothesis of that
subproof, ( /\ ) is another, and T. is the third. The
collection of the unionized assertion for this subproof, which is a step
of the original subproof, is ( /\ ) . The collection of the
non-unionized assertion is not a virtual hypothesis collection because the
element T. is not a virtual hypothesis and the element
( /\ ) is not a virtual hypothesis. The latter element is
not a virtual hypothesis because it is not atomic - it contains two
virtual hypotheses. Even if this element was divided to create
( /\ /\ /\ T. ) , the resultant collection is
not a valid virtual hypothesis collection because it contains two
virtual hypotheses.
Any subproof of a Proof Worksheet for which the virtual hypothesis
collection of the original assertion is identical to each virtual
hypothesis collection of each hypothesis of the subproof does not
need a non-unionized assertion and will be completed by mmj2
unification alone if a unifying MC metavariable deduction exists in
set.mm. If the only unifying metavariable deduction in set.mm is in
standard form, then a non-unionized assertion step must be added for
completion of the subproof.
A subproof of a translated User's Proof may unify with a deduction in
set.mm without any steps added to the original subproof. Such subproofs
are said to be completed by the mmj2 unification means. This is the sole
means by which the mmj2 program completes subproofs. completeusersproof
is designed to first attempt to complete each subproof of the User's
Proof by this means. If completeusersproof is not run in default mode, if
a subproof is not completed by the mmj2 unification means, then an attempt
is made to complete it by the metavariable deduction unification means. If
a subproof is not completed by either of these two means, then
completeusersproof attempts to complete it by adding a unification
theorem. If the unification theorem does not unify with a theorem in
set.mm, then completeusersproof will attempt to 2-step prove the
unification theorem in order to complete the subproof. We call the means
of adding a unification theorem and, if it does not unify, trying to
2-step prove it the unification theorem means. If a subproof does not
complete by any of these three means, the subproof will not be completed
by completeusersproof. Generally, some subproofs of a proof will complete
upon application of the mmj2 unification means, some will complete upon
application of the metavariable deduction unification means, some will
complete upon application of the unification theorem means, and some will
not complete. If all subproofs are completed, an RPN proof will be
generated.
If a subproof unifies with a MC metavariable deduction in set.mm, it is
completed by the mmj2 unification means, not by the metavariable deduction
unification means. If a non-unionized assertion's deduction of a subproof
is unified with a metavariable deduction in set.mm by applying the
metavariable deduction unification means, the metavariable deduction with
which it unifies is in standard form and has more than one hypothesis.
Every 1-hypothesis metavariable deduction is both a MC metavariable
deduction and is a metavariable deduction in standard form. If a subproof
unifies with such a metavariable deduction, it completes by the mmj2
unification means.
Not all subproofs which complete by the mmj2 unification means unify with
a MC metavariable deduction. Generally, a subproof completing by the mmj2
unification means often does not unify with a MC metavariable deduction.
For example, the subproof
5:: |- ( x e. A -> x e. suc A )
9:2: |- x e. A
15:5,9:ax-mp |- x e. suc A
completes by the mmj2 unification means by unifying with the deduction
ax-mp . ax-mp is not a MC metavariable deduction. Neither its hypotheses
or its assertion have a virtual hypothesis collection.
In order to run completeusersproof in non-default mode, the User must
include the matchstring "don't skip completeusersproofmv()" on any
comment line of the User's Proof. If this matchstring is omitted,
completeusersproof will run in default mode. Running in default mode,
completeusersproof will first attempt to complete each subproof by the
mmj2 unification means. The unification theorem means is then attempted on
any subproofs which did not complete by the mmj2 unification means. Any
subproofs not completing by either of these means are not completed. The
metavariable deduction unification means is not used when
completeusersproof is run in its default mode.
Including a special matchstring in any comment line is used in
completeusersproof to attempt to complete subproofs by the metavariable
deduction unificiation means, but is not used in completeusersproofg. For
completeusersproofg, the User presses the "Completeusersproof mv" button in the
GUI window to attempt to complete subproofs by the metavariable deduction
unification means. Pressing the "Completeusersproof" button attempts to
complete subproofs by the unification theorem means. Pressing the "Stepprover"
button of the GUI attempts only to 2-step prove each 0-hypothesis step which
does not unify with a theorem in set.mm.
We now discuss in greater detail the unification theorem means of
completing a subproof. A subproof having more than one step unifies with
either a deduction in set.mm or(excl.) with a ff* false deduction in
fd.txt. 1-step subproofs unify with a theorem in set.mm or(excl.) do not
unify. There are no 0-hypothesis ff* deductions in fd.txt. Each ff* false
deduction corresponds to an eel* deduction which is the same as the ff*
deduction, except it is in conventional notation and has an additional
hypothesis, a "unification theorem". Presuming the User wrote a correct
subproof, that subproof is true before a unification theorem is added to
it. If the translated subproof did not complete upon application of the
mmj2 unification means, the subproof does not unify with any deduction in
set.mm. It does unify with a ff* false deduction in fd.txt. The translated
ff* deduction is false only because it is missing the unification theorem
hypothesis step which its corresponding eel* deduction has. The eel*
deduction is contained in set.mm. completeusersproof adds the unification
theorem to the subproof by replacing the ff* label with its corresponding
eel* label and applying the mmj2 unify command. The modified subproof
unifies with the eel* deduction.
The unification theorem of a virtual deduction deduction is that unique
virtual deduction whose virtual hypothesis collection is the collection of
the virtual conclusions of the hypotheses of the virtual deduction
deduction and whose virtual conclusion is the virtual conclusion of the
assertion of the virtual deduction deduction. Every unification theorem is
a theorem which may or may not unify with a theorem in set.mm.
If set.mm is sufficiently rich with respect to the mathematics which is
the subject of the User's Proof, then it is likely that the unification
theorem of a subproof or a semantic variation of it will be a theorem in
set.mm. If the unification theorem unifies with a theorem in set.mm, then
completeusersproof completes the subproof by adding it alone. If the
unification theorem does not unify with a theorem in set.mm, then the
stepprover() function of completeusersproof() will attempt to 2-step prove
the unification theorem. If there exists in set.mm at least one semantic
variation of the unification theorem and if there exists in set.mm at
least one 1-hypothesis deduction which deduces the unification theorem
from one of its semantic variations in set.mm, then stepprover()
automatically generates an additional step which is a semantic variation
of the unification theorem and which unifies with a theorem in set.mm and
completes the subproof. Otherwise, the added unification theorem remains
unproven and the subproof, although proveable (assuming the original
subproof is correct), is not completed.
The capabilities of completeusersproof which the mmj2 program does not
have include: 1) the ability to generate a unification theorem as an
additional hypothesis step of a subproof in order to complete that
subproof; 2) the ability to 2-step prove a unification theorem which does
not directly unify with a theorem in set.mm but is a semantic variation of
a theorem which does unify with a theorem in set.mm; 3) the ability to
generate a non-unionized assertion step of a subproof when a metavariable
deduction in standard form in set.mm will unify with that non-unionized
assertion's deduction of the subproof, and to complete the second deduction
of the same subproof which deduces the unionized assertion of the original
subproof from the added non-unionized assertion; and 4) the ability to
automatically put no-virtual-hypotheses steps of the original User's Proof
into standard T form, which is needed in order complete a subproof by the
metavariable deduction unification means if some of the hypothesis steps of
the original subproof have no virtual hypotheses.
*