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
completeusersproof is a proof assistant designed to automatically
complete Virtual Deduction Users' Proofs. A Virtual Deduction proof is
a Metamath-specific Natural Deduction proof. A Virtual Deduction User's
Proof uses Virtual Deduction Notation. Generally, a Virtual Deduction
proof lacks some of the detail needed for it to be (after translation
into conventional notation) a complete Metamath proof for which a
Metamath RPN proof may be generated. completeusersproof automatically
generates these missing details. For example,
www.virtualdeduction.com/chordthmaltvd.html is a Virtual
Deduction User's Proof. From it, completeusersproof has automatically
generated chordthmALT , a completed Metamath Proof.
completeusersproof 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 completes each subproof completable by the mmj2
unification means by that means. It attempts to complete each remaining
subproof by the unification theorem means, completing those which are
completable. If the User presses the GUI button "Completeusersproof smv",
it completes each subproof completable by the mmj2 unification means by
that means. It completes each remaining subproof completable by the
single metavariable deduction unification means by that means. It atempts
to complete each remaining subproof by the unification theorem means,
completing those which are completable. If the User presses the GUI
button "Completeusersproof mv", it completes each subproof completable by
the mmj2 unification means by that means. It completes each remaining
subproof completable by the metavariable deduction unification means by
that means. It attempts to complete each remaining subproof by the
unification theorem means, completing those which are completable. For
the definitions of the mmj2 unification means, the unification theorem
means, the single metavariable deduction unification means, and the
metavariable deduction unification means, see the
"DETAILED DESCRIPTION OF THE completeusersproof.c PROGRAM" below.
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, the
"Completeusersproof smv" command, or the "Completeusersproof mv" command.
If the "Completeusersproof" command, the "Completeusersproof smv"
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 smv" 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
twice the duration of the 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 "runCompleteusersproofsmv" specifies processing by the single
metavariable deduction unification 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 without pauses. 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 with pauses.
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 File of example Virtual Deduction Proofs.
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 eel* 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.
A false ffsmv* deduction is used to
construct a subproof which may unify with a
single metavariable deduction in set.mm. A
false ffTmv* deduction is used for a
subproof for which each original step has
no virtual hypothesis collection. The
ffTmv* deduction puts each of these steps
into standard T form. It is used to
construct a subproof which may unify with a
single metavariable deduction in set.mm.
Each ffTmv* deduction is, strictly
speaking, a true deduction because its
assertion is deducible from its last
hypothesis.
mapFfToEelUunNumPermFfsmv.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.
This file also specifies the mapping of
each ff* false deduction label into it
corresponding ffsmv* or ffTmv* label, which
is in the 5th column of the same row.
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 smv",
"Completeusersproof mv", "Stepprover", and
"Exit/Quit". Pressing one of the first
four 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
"""".
completeusersproofSmv.bat Executes completeusersproof.exe
specifying the value of command line
argument argv1
"runCompleteusersproofsmv".
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.
_README.txt This file contains instructions on using
completeusersproof and other information
pertaining to completeusersproof.
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()
completeTheoremSteps()
pickUnifThmPermutations()
removeDecoupledSteps()
substituteLabels()
stepprover()
removeUnneededFfLabels()
nameUsersProofFile()
editHypFieldOfHypSteps()
editHypFieldOfTAssertions()
editHypFieldOfAssertions()
Some Utility Functions:
deleteStepsWithWorkVariables()
mmj2Unify()
translate()
tagLabeledSteps()
endTag()
addMTLast()
addMTMT()
addMTMF()
addMT()
substituteMTMT()
deleteLabels()
removeATypeOfLabel()
*******************************************************************************
*******************************************************************************
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
single 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 runCompleteusersproofsmv 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, completeusersproofSmv.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 "runCompleteusersproofsmv" Complete each subproof completable by
the mmj2 unification means by that
means. Complete each remaining
subproof completable by the single
metavariable deduction means by that
means. Attempt to complete each
remaining subproof by the unification
theorem means. Complete each subproof
completable by that means.
"runCompleteusersproofmv" Complete each subproof completable by
the mmj2 unification means by that
means. Complete each remaining
subproof completable by the
metavariable deduction means by that
means. Attempt to complete each
remaining subproof by the unification
theorem means. Complete each subproof
completable by that means.
"runStepprover" Run only the stepprover() function on
the User's Proof to try to 2-step
prove each 0-hypothesis step. Complete
each 2-step provable 0-hypothesis step.
the mmj2 unification means by that
means. Attempt to complete each
remaining subproof by the unification
theorem means. Complete each subproof
completable by that means. This is the
default value. By convention, the
string """" may be used for this
value.
argv2 "onlyShortScripts" mmj2 unify using the AutoHotkey
scripts unify.exe or unifyFF.exe
"scripts" mmj2 unify using the AutoHotkey
scripts unify.exe, unifylong.exe, or
unifyFF.exe
run parm. This is the default value
of argv2. The character string """"
may be used.
argv3 "**", where i = 1 to 7, ** 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, by attempting to complete subproofs by the
single metavariable deduction unification 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 four 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 value should be used for the
second command line argument because GUIs are not being used. Run
completeusersproof.exe through the command prompt specifying the
desired command line argument values or by double-clicking either the
completeusersproof.bat, completeusersproofSmv.bat,
completeusersproofMv.bat, or completeusersproofSp.bat file, with the
command line arguments specified as desired. If processing the User's
Proof by the unification theorem means using the default values for all
command line arguments, 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 smv" for processing using
the single metavariable deduction unification means by running
completeusersproofSmv.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. Additional information
about the command line arguments may be found above.
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, proofWorksheetTrFfLabeled.txt, unifThms.txt,
duplicateUnificationThms.txt, tags.txt, and hypFields.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 3032 of completeusersproofp.c) and
"Point 7 of completeusersproofmv()" (line 3046 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 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. Examples of
Virtual Deduction User's Proofs are
https://www.virtualdeduction.com/chordthmaltvd.html and
https://www.virtualdeduction.com/iunconlem2vd.html.
A Virtual Deduction proof generally cannot be directly input on a mmj2
Proof Worksheet and, after being translated into conventional notation,
completed by the mmj2 tool because it is usually missing some proof steps
which are not part of the Virtual Deduction proof but are necessary for a
complete Metamath Proof. These missing steps may be automatically added
by an automated proof assistant. completeusersproof is such a proof
assistant. For some subproofs, completeusersproof may automatically
generate one or more additional steps and may edit the hypothesis field of
some steps. The mmj2 unify command labels assertion steps of the proof,
unifying them with reference theorems or deductions in set.mm.
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 a Virtual Deduction User's Proof with the assistance of
the completeusersproof tool 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 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". 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 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. Generally, each original
n-hypothesis deduction of the User's Proof, where n is any positive
integer including 0, is a subproof, and may be modified by
completeusersproof to be a different subproof which is the original
subproof with the "details" necessary for a complete Metamath subproof
added.
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
For the conventional notation virtual deduction ( ( 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 the set.mm syntax definition 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 initial virtual deductions in Virtual Deduction
notations are translated into conventional notation virtual deductions is
because the theorems and deductions in set.mm are in conventional notation
and may be 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, which may also be referred to as
labels of type ff. A virtual deduction subproof cannot unify with a
theorem or deduction in the main set.mm unless it is in conventional
notation.
Natural Deduction which is not Virtual Deduction may be and has been used
as a way to simplify proving in Metamath. Some Users may find that even
greater simplicity is achieved by constructing their Users Proofs to
be compatible with the completeusersproof tool. That is, by writing Users
Proofs as Virtual Deduction proofs in Virtual Deduction notation. If a
User's Proof is not a Virtual Deduction proof in Virtual Deduction
notation, the completeusersproof tool will generally not be useful. An
exception to this is that the completeusersproof tool will attempt to
2-step prove each 0-hypothesis step (each theorem) of the User's Proof and
will complete any of these steps which are completable. If the argument
completeusersproof tool is used with the value of the command line
argv[1] equal to "runStepprover", then only the stepprover() function of
completeusersproof will process the User's Proof and the User's Proof
should not use Virtual Deduction notation.
A Virtual Deduction proof in Virtual Deduction notation is written in what
may be thought of as sort of a "higher level language", permitting the
omission of some of the detail required by a conventional notation
Metamath proof. The omitted details are the steps automatically generated
by the completeusersproof proof assistant. These steps may be considered
"technical steps" and the steps of the Virtual Deduction User's Proof may
be considered to be the more creative steps of the proof.
* * *
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.
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. A virtual deduction with no virtual hypotheses and no empty
virtual hypothesis collection is a virtual deduction in Virtual Deduction
notation (non-conventional notation) and a virtual deduction in
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, with the exception of non-unionized
assertion steps (used only in attempting to complete subproofs by the
metavariable deduction unification means), 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 single 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 complete a subproof
of the User's Proof using the metavariable deduction unification means, 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 single 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 the value of argv1 is "runCompleteusersproofmv",
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. All subproofs completable by this means and not completable by the
mmj2 unification means are completed by the metavariable deduction
unification means. If a subproof is not completable 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. For an argv1 value of
"runCompleteusersproofmv", 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 single 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 single 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 single metavariable deduction. Generally, a subproof completing by the
mmj2 unification means often does not unify with a single 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 single metavariable deduction. Neither its
hypotheses or its assertion have a virtual hypothesis collection.
Any subproof completable by the mmj2 unification means is completable
using the mmj2 program alone. completeusersrpoof also has this same
capability, relying exclusively on invocation of the mmj2 program.
None of the steps of a Virtual Deduction User's Proof should be labeled.
Given this restriction, the mmj2 unification means can only complete a
subproof of a Virtual Deduction User's Proof if that subproof, after
translation, without any steps automatically added and without the
hypothesis field of any step edited, unifies with a theorem or deduction
in set.mm. If a translated subproof of a User's Proof, unmodified, does
not unify with a theorem or deduction in set.mm, then it may be
automatically completable using the additional capabilities of
completeusersproof, by automatically generating an additional step or
steps, or by adding steps and editing the hypothesis field of some steps.
These additional capabilities provide greater Virtual Deduction User's
Proof subproof completing power than available using the mmj2 program
alone.
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.
Let's illustrate use of the unification theorem means by way of an
example. The subproof of suctrALT4UP whose assertion is step 15 is shown
in its original form below. The proof of suctrALT4UP is contained in
the VirtualDeductionProofs.txt file included in the completeusersproof
download.
8:7: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
...
...
12:11: |- (. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
...
14:13: |- (. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
15:8,12,14: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
The "..." lines represent other steps of the User's Proof which are not
hypothesis steps of the example subproof which are interspersed between
hypothesis steps of the example subproof. The subproof translated into
conventional notation is
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
15:14,12,8: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
completeusersproof automatically finds and adds to the assertion step the
label, eel2221, of the deduction in set.mm which deduces the assertion
step from the original hypotheses and the unification theorem, step d3.
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:: |- ( ( ( y e. A \/ y = A ) /\ ( y = A -> z e. suc A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:14,12,8,d3:eel2221 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
This particular unification theorem, although a true theorem, does not
unify with any theorem in set.mm. If it did, the subproof would have
been completed at this point. But there does exist a 1-hypothesis
deduction in set.mm which deduces the unification theorem from a semantic
variation of it, a semantic variation which is in set.mm. That deduction
is 3imp31. The semantic variation is jao. completeusersproof automatically
finds these and 2-step proves the unification theorem using the
stepprover() function. This completes the subproof. The completed subproof
is
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d6::jao |- ( ( y e. A -> z e. suc A ) -> ( ( y = A -> z e. suc A ) -> ( ( y e. A \/ y = A ) -> z e. suc A ) ) )
d3:d6:3imp31 |- ( ( ( y e. A \/ y = A ) /\ ( y = A -> z e. suc A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:14,12,8,d3:eel2221 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
Note that each of steps 8, 12, and 14 is the (translated)
assertion of another subproof of the (translated) User's Proof. Those
subproofs also complete. The labels of the set.mm deductions which
complete these other subproofs are not shown only because those subproofs
are not being discussed here.
If ff2221 was not in fd.txt or(incl.) eel2221 was not in set.mm the above
subproof wouldn't complete by the unification theorem means for labels of
type eel and not of type ffeel. The type ffeel label is a subtype of type
eel. A label of type ffeel is of type eel. Not all type eel labels are of
type ffeel. Labels of type ffeel are more general than eel labels not of
type ffeel. Type ffeel deductions are false deductions but are not of
type ff. The type ff label corresponding to a type ffeel label is of the
form ff**h, where ** is the number of hypothesis steps of the type
ff false deduction and is number of hypothesis steps of the ff
deduction having no virtual hypotheses and no virtual hypothesis
collection.
The above subproof of the suctrALT4UP User's Proof has 3 hypothesis steps,
none of which have no virtual deductions. The type ff labels for this
subproof are ff2221, corresponding to the more specialized
type eel label eel2221, and ff3h0, corresponding to the label of types
eel and ffeel, ffeel3h0. When both of these type ff labels occur in fd.txt
the more specialized, ff2221, is picked. If ff2221 is temporarily removed
from fd.txt, ff3h0 is picked. Given that ff2221 does not occur in fd.txt,
the present subproof subproof will unify with ff3h0 which will be replaced
with ffeel3h0 by substituteLabels(). The unification theorem means
completes type ffeel subproofs differently than type eel subproofs not of
type ffeel. We'll illustrate how the unification theorem means completes
type ffeel deductions using the subproof whose assertion is step 15 of
suctrALT4UP. This subproof of the User's Proof is
8:7: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
...
...
12:11: |- (. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
...
14:13: |- (. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
15:8,12,14: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
Upon mmj2 unification with fd.txt and set.mm loaded this subproof
becomes
8:7:int3 |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
...
...
12:11:int2 |- (. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
...
14:13:ff1 |- (. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
15:8,12,14:ff3h0 |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
The subproof translated into conventional notation after the
substitutelabels() is called is
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13:syl |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
15:14,12,8:ffeel3h0 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
The subproof after another mmj2 unification is
8:7:3expia |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11:ex |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13,d2:syl |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
d5:: |- ( &W5 -> ( y e. A -> z e. suc A ) )
d6:: |- ( ( ( y = A -> z e. suc A ) /\ ( y e. A \/ y = A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:12,d3,14,d4,d5,8,d6:ffeel3h0 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
Steps d3,d4, and d5 correspond, respectively, to the original hypothesis
steps 12,14, and 8. Because the virtual hypothesis collection of step 8 is
equal to that of the assertion step, the generation of an intermediate
hypothesis step is not required. Step d5 is not needed. The existence of
a work variable in d5 implies that that step is not needed.
completeusersproof deletes each generated step in which at least one work
variable occurs. completeusersproof deletes step d5.
The subproof after the hypothesis fields of the hypothesis steps have been edited is
8:7:3expia |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11:ex |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13,d2:syl |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:12: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:14: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
d5:: |- ( &W5 -> ( y e. A -> z e. suc A ) )
d6:: |- ( ( ( y = A -> z e. suc A ) /\ ( y e. A \/ y = A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:12,d3,14,d4,d5,8,d6:ffeel3h0 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
Step d3 is deducible from step 12 and step d4 is deducible from
step 14. Step d6 is the unification theorem. The subproof after the
hypothesis field of the assertion step has been edited, step d5 has
been eliminated, all existing labels have been removed, and after mmj2
unifying again is
8:7:3expia |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11:ex |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13,d2:syl |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:12:adant1 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:14:adant1 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
d6:: |- ( ( ( y = A -> z e. suc A ) /\ ( y e. A \/ y = A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:d3,d4,8,d6:syl3anc |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
d6, the unification theorem, does not unify with a theorem in set.mm, but
is deduced from jao by 3imp231. After the stepprover() function does
this the completed subproof is
8:7:3expia |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11:ex |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13,d2:syl |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:12:adant1 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:14:adant1 |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
d9::jao |- ( ( y e. A -> z e. suc A ) -> ( ( y = A -> z e. suc A ) -> ( ( y e. A \/ y = A ) -> z e. suc A ) ) )
d6:d9:3imp231 |- ( ( ( y = A -> z e. suc A ) /\ ( y e. A \/ y = A ) /\ ( y e. A -> z e. suc A ) ) -> z e. suc A )
15:d3,d4,8,d6:syl3anc |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
Note that syl3anc is the name of the deduction in set.mm which whould have
been named eel111 if the eel label naming convention was used. As with the
unification theorem means for labels of type eel and not of type ffeel,
the unification theorem means for labels of type eel and type ffeel
generates a unification theorem. Unlike the unification theorem means for
labels not of type ffeel, for each hypothesis step without a virtual
hypothesis collection equal to the virtual hypothesis collection of the
assertion step, the unfication theorem means generates an intermediate
hypothesis step having a virtual hypothesis collection equal to that of
the assertion's virtual hypothesis collection. The virtual conclusion is
the same as that of the corresponding original hypothesis step. Or, if the
original hypothesis step has no virtual hypotheses, the virtual conclusion
of the generated intermediate hypothesis step is equal to the wff of the
original hypothesis step.
Each hypothesis step of the assertion's deduction has a virtual hypothesis
collection equal to the assertion's virtual hypothesis collection. It is a
single metavariable deduction. The deduction of the assertion step of
every n-hypothesis User's Subproof processed by the unification theorem
means for labels of type ffeel unfies with the unique label eel11...1,
where there are n "1"s. This single eel11...1 label applies for all
permutations of original hypothesis step virtual hypothesis collections.
There are many such permutations because, generally, the virtual
hypothesis collection of an original hypothesis step may be any virtual
hypothesis collection which is a subcollection of the assertion's virtual
hypothesis collection. By using eel labels of type ffeel it becomes
unnecessary for the many possible permutations of specialized eel
deductions to exist in set.mm. Those specialized eel deductions which are
included in set.mm are included because they are frequently used. The
ground for their existence in set.mm is to shorten frequently occurring
subproofs completed by the unification theorem means.
A Virtual Deduction User's Proof may have steps with many-element virtual
hypothesis collections. Because conventional notation virtual deductions
may not have more than 3-conjunct conjunctions, completeusersproof
translates a more-than-3-element virtual hypothesis collection into a
left-nested conjunction. For example, the conventional notation
counterpart of the Virtual Deduction virtual hypothesis collection
(. ,. ,. ,. ,. ).
is
( ( ( ( /\ ) /\ ) /\ ) /\ )
The unification theorem means using type ffeel labels is especially useful
for Users' Proofs containing steps with virtual hypothesis collections
having more than 3 elements because, otherwise, it would be necessary to
have a large number of specialized eel permutations. Additional adant*
deductions are required, but their number is much smaller than the number
of specialized eel permutations that would otherwise be required.
If the value of argv1 is not specified by the User or the User presses the
"Completeusersproof" button in the completeusersproofGUI, then
completeusersproof completes each subproof of the input User's Proof
completable by the mmj2 unification means by that means. It attempts to
complete the remaining subproofs by the unification theorem means. All
subproofs completable by the unification theorem means are completed by
that means. If all subproofs are completed, the proof is completed and a
RPN proof is generated.
If argv1 is specified by the User to have the value
"runCompleteusersproofsmv", then completeusersproof completes each
subproof competable by the mmj2 unification means by that means. It
completes the remaining subproofs which are completable by the single
metavariable deduction unification means by that means. It attempts to
complete the remaining subproofs by the unification theorem means. Each
remaining subproof completable by the unification theorem means is
completed by that means. If all subproofs are completed, a RPN proof is
generated. Otherwise, each remaining subproof not a single step has a
generated unification theorem, but is not completed because the unification
theorem does not unify with a theorem in set.mm and is not deducible by a
2-step proof from a theorem in set.mm which is a semantic variation of the
unification theorem. Each remaining single step subproof, a theorem, does
not unify with a theorem in set.mm and is not deducible by a 2-step proof
from a theorem in set.mm which is a semantic variation of the theorem of
the subproof.
Earlier, we described the metavariable deduction unification means. By this
means, a subproof unifies with a standard form metavariable deduction in
set.mm. Here we describe the single metavariable deduction unification
means, which is distinct from the metavariable deduction unification means.
If a subproof of the original User's Proof, without modification, unifies
with a single metavariable deduction in set.mm, then it is completable by
the mmj2 unification means, as explained above. The virtual hypothesis
collection of each hypothesis step of the original subproof is identical
to the virtual hypothesis collection of the assertion. When some of the
original hypothesis steps have a virtual hypothesis collection which is a
proper subcollection of the virtual hypothesis collection of the assertion,
for each such hypothesis step, in implementing the single metavariable
unification deduction means, completeusersproof automatically generates
a corresponding hypothesis step which has the same virtual conclusion as
the original hypothesis step and whose virtual hypothesis collection is
identical to the virtual hypothesis collection of the assertion step.
Each generated hypothesis step is deducible from its original hypothesis
step by a 1-hypothesis deduction in set.mm. After these additional
hypothesis steps are generated the subproof may then unify with a a single
metavariable deduction in set.mm, completing the subproof. We illustrate
the completion of a subproof by the single metavariable deduction
unification means with an example. Again, we use the subproof of
suctrALT4UP whose assertion step is step 15. This subproof happens to be
completable by both the unification theorem means and the single
metavariable deduction unification means. The subproof of the original
User's Proof is
8:7: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
...
...
12:11: |- (. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
...
14:13: |- (. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
15:8,12,14: |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
The subproof translated into conventional notation is
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
15:14,12,8: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
The virtual hypothesis collection of step 8 (in conventional notation),
( Tr A /\ ( z e. y /\ y e. suc A ) ), is identical to the virtual
hypothesis collection of the assertion step, step 15. It is in single
metavariable deduction form. An additional step is not required. The
virtual hypothesis collection for each of steps 12 and 14 is not
identical to the assertion's virtual hypothesis collection. For step
12, step d3 is generated. Step d3 is deducible from step 12 and its
virtual hypothesis collection is identical to the assertion's
virtual hypothesis collection. Similarly, step 14's virtual
hypothesis collection is not identical to step 15's, so step d4 is
generated. We say that, with these steps added, the subproof will complete
if there exists a single metavariable deduction in set.mm which unifies
with it. In saying this, it is implicitly assumed that a deduction exists
in set.mm which unifies with the deduction whose assertion is step d3 and
that a deduction exists in set.mm which unifies with the deduction whose
assertion is step d4. More precisely stated, the subproof will complete if
there exists a single metavariable deduction in set.mm which unifies with
the deduction whose assertion is step 15 and whose hypotheses are steps 8,
d3, and d4. In addition to generating the steps d3 and d4,
completeusersproof also fills their hypothesis fields and edits the
hypothesis field of the assertion step, step 15, as required. The subproof
becomes
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:12: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:14: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
15:d3,d4,8: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
In fact, there does exist a single metavariable deduction in set.mm which
unifies with the deduction whose assertion is step 15, there exists a
deduction in set.mm which unifies with the deduction whose assertion is
step d4, and there exists a deduction in set.mm which unifies with the
deduction whose assertion is step d3. Upon mmj2 unification the subproof
completes. The completed subproof is
8:7: |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
...
...
12:11: |- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
...
14:13: |- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
d3:12:adantl |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
d4:14:adantl |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
15:8,d3,d4:mpjaod |- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
mpjaod is the single metavariable deduction in set.mm that unfies with the
subproof.
Where the assertion of a subproof of a User's Proof has no virtual
hypotheses that assertion should not have a virtual hypothesis collection
because there is no need for it. Similarly, the hypotheses of the subproof
have no virtual hypotheses and should not be in standard T form. An
example of such a subproof is the subproof whose assertion is step 43 of
the User's Proof a9e2ndeqALTUP, contained in VirtualDeductionProofs.txt.
It is
39:: |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
...
41:40: |- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
42:: |- ( A. x x = y \/ -. A. x x = y )
43:39,41,42: |- ( u = v -> E. x E. y ( x = u /\ y = v ) )
It is completable by the single metavariable deduction unification means.
In order to unify with a single metavariable deduction in set.mm, step d13
is generated. It is the original assertion step in standard T form. For
each hypothesis step a step deducible from it with the same empty virtual
hypothesis collection is generated. The contents of the hypothesis field
for each of these generated steps is automatically generated by
completeusersproof. Below is the completed subproof. The modifications to
the original subproof are similar to the subproof of the last example,
except there is an extra generated step, a step from which the original
assertion step is deduced by the set.mm deduction trud. This extra step is
needed to complete a subproof by the single metavariable deduction
unification means only when the assertion has no virtual hypotheses and no
empty virtual hypothesis collection.
39:: |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
...
41:40: |- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
42:: |- ( A. x x = y \/ -. A. x x = y )
d10:41:a1i |- ( T. -> ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
d11:39:a1i |- ( T. -> ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
d12:42:a1i |- ( T. -> ( A. x x = y \/ -. A. x x = y ) )
d13:d11,d10,d12:mpjaod |- ( T. -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
43:d13:trud |- ( u = v -> E. x E. y ( x = u /\ y = v ) )*