This package contains the program completeusersproof.c, a second version of
that program, completeusersproofp.c, which may be used as an aid for reading
the program and error detection, and associated files.
Program name: completeusersproof.c
Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu http://metamath.org
(for the metamath.c base code)and ALAN SARE alansare at alumni.cmu.edu
(for the completeusersproof() function and functions it
(directly) calls).
License terms: GNU General Public License
This program is built on top of the metamath.c code in order to utilize
the Metamath tools commands. c-emulations of the Metamath tools commands
have been added as functions, created by minor revisions to the
metamath.c code. These functions are called by the
completeusersproof() function and by the functions called by it. The
original metamath.c code is retained in its entirety, including its
comments, except for minor revisions. Most of it is not used by the
functions added to metamath.c.
completeusersproof is intended to automatically complete User's Proofs
written as Virtual Deduction proofs. A Virtual Deduction proof is
a Metamath-specific version of a Natural Deduction proof.
completeusersproof() first invokes mmj2 alone to unify any subproofs it
can. If run in default mode, it then generates a unification theorem for
each incomplete subproof in a second attempt to automatically complete
it. If the unification theorem is not in set.mm but is a semantic
variation of one that is, then it attempts to 2-step prove the
unification theorem to complete the subproof. If the User inserts the
matchstring "don't skip completeusersproofmv()" in any comment line of
the User's Proof, then completeusersproof will also attempt to complete
each subproof not completed by mmj2 alone by adding non-unionized
assertion permutations for unification with a metavariable deduction in
set.mm.
Inputs:
proofworksheet.txt This text file is a Proof Worksheet
conforming to mmj2 requirements. It
initially contains the User's Proof.
The path of set.mm and fd.txt is the
default path specified in
mmj2FalseDeductions.bat and
mmj2StepProver.bat. This default path is
specified to be c:\metamath\ and may be
changed by the User. The program runs
correctly if the folders containing the
mmj2 files are the default folders
generated by the mmj2 download and all
other files of the completeusersproof
download are placed in the mmj2jar folder
of the mmj2 download.
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".
A false deduction is a true deduction
for which one hypothesis, a "unification
theorem", is implicit.
completeusersproof explicates the
implicit hypothesis and 2-step proves it if
it is not in set.mm and a semantic
variation of it is. For example, syl is the
true deduction corresponding to
the false deduction ff1,
|- (. ph ->. ps ). infers |- (. ph ->. ch ).
The implicit hypothesis is ( ps -> ch ) .
A deduction with an implicit unification
theorem as a hypothesis which is true from
the User's perspective is false from
Metamath's perspective because Metamath
is implicit-hypothesis-blind.
mapFfToEelUunNumPerm.txt This file specifies the one-one
correspondence between each false deduction
in fd.txt and its true counterpart in
set.mm. Column one contains the false
deduction labels and column two contains
the true deduction labels.
This file also specifies the mapping of
each ff* false deduction label into its
corresponding 0th premutation uun* label.
That label is in the 3rd column of the same
row. In the 4th column of the same row is
the number of permutations of uun* labels
corresponding to the ff* label. The uun*
deductions are described at the beginning
of the completeusersproof() function
defintion.
RunParmsFalseDeductions.txt A text file of mmj2 run parameters
referenced by mmj2FalseDeductions.bat.
Two input files are loaded. The first
is set.mm and the second is fd.txt.
mmj2FalseDeductions.bat A .bat file which executes mmj2 using the
run parameters specified by
RunParmsFalseDeductions.txt. It is the
value of the second argument of the first
call of mmj2Unify() by
completeusersproof(). False deductions are
intended to unify with all deductions of
the User's Proof which do not unify with
a true deduction in set.mm.
RunParmsStepProver.txt A text file of mmj2 run parameters
referenced by mmj2StepProver.bat which
invokes the mmj2 unification command.
Distinguishing RunParmsStepProver.txt from
RunParmsFalseDeductions.txt, set.mm is the
sole mmj2 input file of the former.
mmj2StepProver.bat A .bat file which executes mmj2 using the
run parameters specified by
RunParmsStepProver.txt.
Output:
proofWorksheet.txt 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.
Primary Functions:
completeusersproof()
addMvSubtheoremTs()
addMvAssertionSteps()
completeusersproofmv()
addUnionizedAssertionPermutations()
pickAPermutationOfEachUnionizedAssertion()
pickALabelPermutation()
substituteLabels()
stepprover()
removeUnneededFfLabels()
Some Utility Functions:
mmj2Unify()
translate()
tagLabeledSteps()
endTag()
addMTLast()
addMTMT()
addMTMF()
addMT()
substituteMTMT()
deleteLabel()
THE VirtualDeductionProofs.txt FILE:
This text file contains 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 .
Each proof contained in VirtualDeductionProofs.txt may be input into
completeusersproof by copying it onto proofWorksheet.txt. Upon execution of
completeusersproof an RPN Metamath proof in conventional notation is
generated. If the labels specified in the brief description are excluded
from the unification search, then any distinct variable requirements will
not be violated.
PROCEDURE FOR USING completeusersproof.c
step 1. It is assumed that set.mm is in the c:\metamath folder and the mmj2
files exist in the default c:\mmj2 and c:\mmj2\mmj2jar folders.
Download completeusersproof.zip using the link found on the Metamath
web site.
step 2. Unzip it.
step 3. Place fd.txt in c:\metamath folder. If the default path of set.mm
and fd.txt, as specified in mmj2FalseDeductions.bat and
mmj2StepProver.bat, is not c:\metamath, then use the differrent
specified path for fd.txt.
step 4. Place all other extracted files in the c:\mmj2\mmj2jar folder. If
mmj2.bat and associated files are in another folder, then place all
other files in that 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. Whether the proof is intentionally
constructed as a Natural Deduction proof using Virtual Deduction
notation or not, any valid mmj2 Proof Worksheet constitutes is
acceptable.
step 6. Copy the Proof Worksheet created in step 5 onto proofWorksheet.txt.
step 7. To attempt to complete subproofs by the method of unifying them with
metavariable deductions in set.mm having non-unionized assertions as
well as by the method of mmj2 unification alone and by the unification
theorem method, type "don't skip completeusersproofmv()" on a comment
line of Proof Worksheet. Otherwise, completion of subproofs will be
attempted only by the method of mmj2 unification alone and by the
unification theorem method.
step 8. Double-click on the completeusersproof.exe file to execute
the program. Assuming no errors, the proof will be translated into
conventional notation and completed as much as possible. If the proof
is completed in its entirety an RPN Metamath proof will be generated.
If the User did not intentionally construct the input proof to be
a Virtual Deduction proof, completeusersproof will nevertheless
complete the proof as much as possible.
step 9. Delete from the c:\mmj2\mmj2jar folder (or whichever folder files were
placed in for step 4) 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.
DESCRIPTION OF completeusersproofp.c
completeusersproofp.c is identical to completeusersproof.c except for
intermittent printf("point **"); and getchar(); pairs of statements
which pause execution until the User presses . "point **"
identifies the line in the program at which execution has paused. At each
pause the User is afforded the opportunity to observe any 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,
unifThms.txt, and duplicateUnificationThms.txt.
To observe a text file as it changes, keep the text file displayed during
execution of the program. While execution is paused, click anywhere in the text
file window. This will minimize the ms-dos window and, if TextPad is the text
editor being used, cause a window to pop up stating: "Another application has
updated file c:\mmj2\mmj2jar\.txt. Reload it?" Press "Yes" to update the
file. After viewing the updated text file, maximize the ms-dos window and press
enter to resume execution. Repeat this procedure for every pause in program
execution or only for pauses at points of interest. If completeusersproofp.c
is also kept open during execution of completeusersproofp.exe, then one may
concurrently observe the text file changes and the statements of the code
causing them. The code statements causing changes may be identified by the
statements printed in the console. For example, the changes made to
proofWorksheet.txt immediately preceding the pause at "Point 7 of
completeusersproofmv()" are due to the three statements occurring between the
"Point 6 of completeusersproofmv()" (line 1879 of completeusersproofp.c) and
"Point 7 of completeusersproofmv()" (line 1893 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.
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.c
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 and
RunParsmsFalseDeductions.txt command 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 run parms.
step 4. Run completeusersproof again.
step 5. Repeat steps 2, 3, and 4 until all distinct variable violations
are removed.
DETAILED DESCRIPTION OF THE completeusersproof.c PROGRAM
MOTIVATION FOR COMPLETEUSERSPROOF. As explained in the description of
wvd1, Natural Deduction is a powerful strategy for proving theorems
and deductions. Natural Deduction uses a Gentzen-type system. We are
motivated to write Natural Deduction proofs (for the power of proving
using a Gentzen-type system) and verify them using Metamath's
proofchecking capability. Metamath uses a Hilbert-type deductive system.
As explained in wvd1, the virtual deduction notation has been added to
set.mm to have a language of a Hilbert-type deductive system which
can be used like a Gentzen-type system. Using the virtual deduction
notation of set.mm, one can effectively write Natural Deduction Proofs
in the virtual deduction language of Metamath. We call these proofs
Virtual Deduction proofs. A Virtual Deduction proof is the
Metamath-specific version of a Natural Deduction Proof.
A Virtual Deduction proof generally cannot be directly input on a mmj2
Proof Worksheet and completed by the mmj2 tool because it is usually
missing some technical proof steps which are not part of the Virtual
Deduction proof but are necessary for a complete Metamath Proof. These
missing technical steps may be automatically added by an automated
proof assistant. completeusersproof is such a proof assistant.
completeusersproof adds the missing technical steps and finds the
reference theorems and deductions in set.mm which unify with the
subproofs of the proof.
The User may write a Virtual Deduction proof and automatically transform
it into a complete Metamath proof using the completeusersproof tool. The
completed proof has been checked by the Metamath program. The task of
writing a complete Metamath proof is reduced to writing what is
essentially a Natural Deduction Proof.
Generally, proving using Virtual Deduction and completeusersproof
reduces the amount Metamath-specific knowledge required by the User.
Often, no knowledge of the specific theorems and deductions in set.mm
is required to write some of the subproofs of a Virtual Deduction
proof. Often, no knowledge of the Metamath-specific names of reference
theorems and deductions in set.mm is required for writing some of the
subproofs of a User's Proof. Often, the User may write subproofs of
a proof using theorems or deductions commonly used in mathematics and
correctly assume that some form of each is contained in set.mm and that
completeusersproof will automatically generate the technical steps
necessary to utilize them to complete the subproofs. Often, the fraction
of the work which may be considered tedious is reduced and the total
amount of work is reduced.
* * *
completeusersproof() is the single primary function of the
completeusersproof program. All other functions used by the
completeusersproof program are called by completeusersproof().
The input Proof Worksheet is the "User's Proof". It is intended to be a
correct Virtual Deduction proof. completeusersproof completes each
subproof of the translated User's Proof it is capable of
completing.
What do we mean by the term "subproof"? A subproof of the User's
Proof might have been called simply a deduction within the User's Proof.
We do not call it a deduction because a technical step or steps
automatically added to the proof which are associated with the deduction
may change the deduction into a deduction with more steps or may create
an additional deduction associated with the modified or unmodified
original deduction. The new collection of associated steps may not be a
single deduction and therefore cannot properly be called a deduction.
Therefore, we call the original deduction and this new collection of steps
arising from the original deduction a subproof. Our narrow definition
differs from the usual definition of subproof. For the usual definition of
subproof, a subproof may include many deductions of a proof. For our
narrow definition, a subproof arises from and is associated with a single
deduction of the original User's Proof. The original single deduction is
also a subproof.
DEFINITION OF A VIRTUAL DEDUCTION.
A Theorem fine is Deduction,
For it allows work-reduction:
To show "A implies B",
Assume A and prove B;
Quite often a simpler production.
-- Stefan Bilaniuk
In Sequent Calculus, for the implication ( ( ph /\ ps ) -> ch ) , each
conjunct of the antecedent is thought of as a hypothesis and the
consequent is thought of as an assertion of the deduction ph and ps infers
ch. ph and ps are not actual hypotheses and ch is not an actual assertion.
We call ph a "virtual hypothesis" because it is not an actual hypothesis.
ch is a "virtual conclusion" because it is not an actual assertion. Just
as the virtual image seen in a plane mirror is not actual or real because
it is formed in a location light does not actually reach,
( ( ph /\ ps ) -> ch ) is a "virtual deduction" because it is not an
actual or real deduction. We are motivated to think in terms of virtual
objects because "it allows work-reduction" and because proving is "Quite
often a simpler production." We call the proving style where one
interprets the well-formed formula of each proof step to be a virtual
deduction "Virtual Deduction" instead of "Natural Deduction" because
Virtual Deduction may be given the above meaning and because Natural
Deduction has a broader meaning than this Metamath-specific style with its
own special notation.
In the written description of wvd1 a virtual deduction is defined to be
the analog in H of a sequent in G1. The connective ->. (a mediator
connective) separates the virtual hypothesis collection on the left side
of ->. from the virtual conclusion on the right side of ->. . A virtual
deduction with no ->. connective is a virtual deduction with no virtual
hypotheses. A virtual deduction with no virtual hypotheses may be
alternatively written in "standard T form". The empty virtual hypothesis
collection is defined to be T. . |- and |- (. T. ->. ).
denote equivalent virtual deductions, the latter being the former in
standard T form. More about the standard T form may be found below.
Only the User's Proof is written using Virtual Deduction notation. The
User's Proof with as many subproofs as possible completed by
completeusersproof is in conventional notation. This conventional
notation complete or partially complete proof may be interpreted as a
conventional notation virtual deduction proof.
DEFINITION OF A CONVENTIONAL NOTATION VIRTUAL DEDUCTION. A conventional
notation virtual deduction is a virtual deduction with conventional
notation symbols substituted for virtual deduction symbols. If a
conventional notation virtual deduction has no -> connective, then it
has no virtual hypotheses. If one or more -> connectives occur in it,
then the outermost -> connective is the mediator connective or(excl.)
none of the -> connectives is the mediator connective and there are no
virtual hypotheses.
Some conventional notation virtual deductions are susceptible to more than
one interpretation. The virtual deduction's context usually fully
determines which interpretation is the correct one. As an example of
ambiguity, the conventional notation virtual deduction
|- ( x e. A -> x C_ B ) may correspond to the virtual deduction
|- (. x e. A ->. x C_ B ). or(excl.) to the no-virtual-hypotheses
virtual deduction |- ( x e. A -> x C_ B ) .
The reason each step of a User's Proof is specified to be a virtual
deduction with virtual deduction notation is to assure that each
step of the proof has a unique interpretation. After the proof is
translated, the correct interpretation of any original step, now a
conventional notation virtual deduction, may be determined by its
interpretation prior to translation if context alone is insufficient for
disambiguation.
The completeusersproof program relies on the virtual deduction notation
because there is no ambiguity. Therefore, it is necessary for the User's
Proof to be in Virtual Deduction notation in order to utilize the full
potential of completeusersproof to complete as many of the subproofs of
the User's Proof as possible. If a User's Proof is not written as a
Virtual Deduction proof, then completeusersproof will interpret each step
of the proof to be a virtual deduction with no virtual hypotheses.
One sufficient reason why conventional notation virtual deductions are
used is because the theorems and deductions in set.mm are in conventional
notation and are fully utilized if and only if the steps of the User's
Proof are translated into the same conventional notation after the
disambiguation information contained in the original Virtual Deduction
proof is extracted and saved. It is saved in the ff* labels. A virtual
deduction subproof cannot unify with a theorem or deduction in the main
set.mm unless it is in conventional notation.
The power of Natural Deduction in simplifying proving is fully realized
by writing proofs using virtual deduction wwfs, which are the analog in H
of sequents in G1 (see: the description of wvd1). It is possible to use
only conventional notation virtual deductions and prove by Natural
Deduction, but, in so doing, the proof writer has the burden of writing
in a language for which some wffs are subject to more than one
interpretation. More importantly, the full proof-completing potential of
completeusersproof is not realized.
* * *
We will sometimes refer to a conventional notation virtual deduction as
a "virtual deduction". Context usually determines whether "virtual
deduction" means a virtual deduction in non-conventional notation or a
conventional notation virtual deduction.
It is intended that any User's Proof to which completeusersproof will
be applied is input as a Virtual Deduction proof in non-conventional
notation. A proof is a Virtual Deduction proof in non-conventional
notation if every step of the proof is a virtual deduction in
non-conventional notation.
Early in the execution of completeusersproof the original Virtual
Deduction proof in non-conventional notation is translated into
a conventional notation Virtual Deduction proof. Of the steps of the
proof automatically generated by completeusersproof towards the goal
of completing the original proof, which the exception of non-unionized
assertion steps, each added step is a conventional notation virtual
deduction. The wff of a non-unionized assertion step is not a virtual
deduction unless every element of its collection of virtual hypothesis
collections is a virtual hypothesis. Many of the terms used above are
defined below.
The virtual deduction
|- (. (. Tr A ,. ( z e. y /\ y e. A ) ). ->. z e. A ). (wff1)
is automatically translated by completeusersproof to be
|- ( ( Tr A /\ ( z e. y /\ y e. A ) ) -> z e. A ) (wff2)
wff2 is the conventional notation virtual deduction counterpart of the
virtual deduction wff1. There are two virtual hypotheses. One is Tr A .
The other is ( z e. y /\ y e. A ) . The virtual conclusion is z e. A .
Every virtual deduction has one and only one virtual conclusion. For a
virtual deduction in Virtual Deduction notation, " ,. " separates pairs of
adjoining virtual hypotheses. In a conventional notation virtual deduction
" /\ " may have the role of separating a pair of adjoining virtual
hypotheses or(excl.) may be a component symbol (the conjunction symbol) of
a virtual hypothesis or a virtual conclusion.
( Tr A /\ ( z e. y /\ y e. A ) ) is the virtual hypothesis collection of
wff2.
With translation, " ,. " becomes " /\ ", " ->. " becomes " -> ", " (. "
becomes " ( ", and " ), " becomes " ) ".
There are three possible interpretations of wff2. The correct
interpretation is the same interpretation as wff1. One incorrect
interpretation interprets wff2 to have a single virtual hypothesis,
( Tr A /\ ( z e. y /\ y e. A ) ) . The other incorrect interpretation is
that wff2 has no virtual hypotheses, the entire wff being a virtual
conclusion.
A metavariable deduction is a deduction for which each hypothesis step may
be interpreted to be a conventional notation virtual deduction having a
virtual hypothesis collection which is a wff variable. We use the term
"metavariable" for the wff variable as Mario Carneiro has in his
presentation "Natural Deduction in the Metamath Proof Language" presented
in the summer of 2014. We say a metavariable deduction is in standard form
if the elements of the collection on the left side of the mediator -> of
its assertion are exactly the virtual hypothesis collections of the
hypothesis steps. Unless a standard form metavariable deduction has only
one hypothesis, its assertion is not a virtual deduction because its
collection of virtual hypothesis collections is not a virtual hypothesis
collection. We could have defined this collection to be a virtual
hypothesis collection on the ground that a wff variable is an single
variable. We don't use that definition because a wff variable is a
schemata for a virtual hypothesis collection. An example of a standard
form metavariable deduction in set.mm is trelded.
We say that the collection of virtual hypothesis collections of the
assertion of a standard form metavariable deduction with more than one
hypothesis is "non-unionized" and that the assertion is a non-unionized
assertion. We use the term "union" because unionizing a collection of
virtual hypothesis collections to obtain a virtual hypothesis collection
is analogous to taking the union of a class. We define a "unionized
assertion" to be an assertion derivable from a non-unionized assertion by
unionizing its collection of virtual hypothesis collections. The
unionized collection is a virtual hypothesis collection consisting of the
elements of the elements of the collection of virtual hypothesis
collections of the non-unionized assertion. We adopt the convention that
the virtual hypothesis collection of a unionized assertion contains no
duplicate elements. It is undesirable for a virtual hypothesis collection
to contain duplicate virtual hypotheses because the virtual hypothesis
collection is denoted by a longer and more complex character string which
does not contain more information. More importantly, if the operation of
unionizing a non-unionized collection of virtual hypothesis collections
did not include the removal of duplicate virtual hypotheses, then there
would exist a multiplier effect whereby proof steps with virtual
hypothesis collections containing duplicate virtual hypotheses which are
hypothesis steps of other proof steps would spawn more duplicate virtual
hypotheses.
One possible way a subproof may be completed is by unifying it with a
standard form metavariable deduction in set.mm. If the unifying
standard form metavariable deduction in set.mm is a 1-hypothesis
deduction, then it will unify with the original deduction of the subproof.
If the unifying standard form metavariable deduction in set.mm has more
than one hypothesis, then it will not unify with the original deduction of
the subproof because the assertion of the original deduction is unionized
whereas the assertion of the metavariable deduction in set.mm is not.
completeusersproof generates a non-unionized assertion. The deduction of
that non-unionized assertion, which has the same hypotheses as the
original deduction, unifies with the metavariable deduction in set.mm.
The assertion of the original deduction is deduced from the non-unionized
assertion with a 1-hypothesis uun* deduction. That deduction is the second
deduction of the subproof. The number of steps of the subproof
increases by one step. That added step is the non-unionized assertion.
The non-unionized assertion immediately precedes the unionized assertion,
which is the original assertion of the subproof. completeusersproof
automatically generates the contents of the hypothesis field of the
non-unionized assertion step to be the same as the original contents of
the hypothesis field of the original assertion. completeusersproof deletes
the original contents of the original assertion's hypothesis field and
inserts into that hypothesis field the step number of the non-unionized
assertion step.
Each metavariable deduction in standard form in set.mm has a particular
ordering of metavariable virtual hypothesis collections within the
collection of virtual hypothesis collections of its assertion. The
ordering of the virtual hypothesis collections of the collection of
virtual hypothesis collections of the generated non-unionized assertion of
a deduction of a subproof of a Proof Worksheet to be unified with a
metavariable deduction in set.mm must match the ordering of the collection
of the assertion of the metavariable deduction in set.mm. Therefore, all
possible permutations of the ordering of the virtual hypothesis
collections within the collection of virtual hypothesis collections of the
non-unionized assertion must be tried. completeusersproof generates one
non-unionized assertion for each permutation. The hypothesis steps of each
deduction corresponding to each non-unionized assertion permutation are
the same. They are the hypothesis steps of the original subproof. If one
or more of these deductions unifies with one or more standard form
metavariable deductions in set.mm, then one of the unifying deductions is
picked by completeusersproof to be that metavariable deduction in set.mm
to complete the non-unionized asssertion's deduction of the subproof. The
remaining non-unionized assertion permutations are deleted. If no
deduction permutation unifies with a standard form metavariable deduction
in set.mm, then all non-unionized assertion permutations are deleted and
the subtheorem is not completed.
For each ff* false deduction corresponding to a subproof of the User's
Proof there corresponds a collection of uun* labels which contains all
possible permutations of uun* deductions which deduce the unionized
assertion from the non-unionized assertion permutations. For example, the
virtual hypothesis collections for the two hypotheses of a subproof of a
User's Proof may be ( /\ ) and . Then there are a
total of two uun* permutations, each deducing the unionized assertion from
one of the two non-unionized assertion permutations. One has as its
hypothesis an assertion with the collection of virtual hypothesis
collections ( ( /\ ) /\ ) and the other
( /\ ( /\ ) ) . The unionized assertion for both
deductions is the same and is the assertion of the original subproof. Its
virtual hypothesis collection is either ( /\ ) or(excl.)
( /\ ) . If there exists a non-unionized assertion deduction
permutation which unfies with a standard form metavariable deduction in
set.mm and that deduction is picked by completeusersproof, then the uun*
deduction corresponding to the former deduction's non-unionized assertion
deduces the unionized assertion of the original subproof from that
non-unionized assertion. Both deductions of the subproof are completed and
the subproof is completed. This means by which an attempt is made to
complete a subproof is called the metavariable deduction unification
means. Included in this means is putting in standard T form any
no-virtual-hypothesis steps of the original subproof.
If the virtual hypothesis collections of the hypotheses of a metavariable
deduction in standard form in set.mm are identical, then the union of the
the collection of virtual hypothesis collections of its hypotheses is
identical to the virtual hypothesis collection of each hypothesis. Any
metavariable deduction in set.mm having the same virtual hypothesis
collection metavariable for each hypothesis may have as its assertion a
virtual deduction having the same virtual hypothesis collection as the
hypotheses. A metavariable deduction in this form will unify with a
subproof in a Proof Worksheet using mmj2 alone. Mario Carneiro has
employed this metavariable deduction form for many deductions he has
added to set.mm. He discussed it in his presentation "Natural Deduction
in the Metamath Proof Language". We shall call a metavariable deduction in
this form a MC metavariable deduction.
Some steps of a User's Proof may have no virtual hypotheses. For example,
|- A C_ suc A (wff3)
may be such a step in a User's Proof. It is originally a virtual deduction
in non-conventional notation. Upon translation of the proof, it becomes a
conventional notation virtual deduction. Because it has no virtual
hypotheses, the syntax of wff3 is the same whether it is interpreted as a
virtual deduction in non-conventional notation or a conventional notation
virtual deduction. wff3 may be put in "standard T form" so that it is a
virtual deduction having a virtual hypothesis collection which is empty.
|- (. T. ->. A C_ suc A ). (wff4)
wff4 is wff3 in standard T form. wff4 translated is
|- ( T. -> A C_ suc A ) (wff5)
Both wff4 and wff5 are virtual deductions. wff4 is a virtual deduction in
non-conventional notation and wff5 is a conventional notation virtual
deduction. Both have the same interpretation.
In order for completeusersproof to attempt to mv-complete a subproof
of the User's Proof (complete it by unifying it with a metavariable
deduction in set.mm) it puts each no-virtual-hypotheses step of the
subproof into standard T form. This is necessary because every
hypothesis of a metavariable deduction in set.mm has a metavariable
virtual hypothesis collection.
The union of a singleton is its element. U. { A } = A . A virtual
hypothesis collection differs from a class in that, among other things, a
singleton virtual hypothesis collection is identical to the virtual
hypothesis it contains. If x e. A is the virtual hypothesis of a singleton
virtual hypothesis collection, then that collection must be denoted by
x e. A because ( x e. A ) is syntactically invalid.
If the virtual hypothesis collection of each hypothesis of a subproof is
a singleton and these virtual hypothesis collections are distinct, then
the collection of these virtual hypothesis collections is a virtual
hypothesis collection. This collection may be denoted by each one of n
possible wffs, one wff for each virtual hypothesis ordering permutation,
where n is the number of virtual hypothesis ordering permutations. One of
those permutations is the virtual hypothesis collection of the (unionized)
assertion of the original subproof. If there exists a standard form
metavariable deduction in set.mm whose assertion has a collection of
virtual hypothesis collections with a virtual hypothesis collection
ordering matching that of the assertion of the original subproof, then it
will unify with the original subproof and the subproof will be completed
by mmj2 unification alone. No non-unionized assertion will be generated.
If the standard form metavariable deduction in set.mm which completes the
subproof has an assertion with a collection of virtual hypothesis
collections with a different ordering, then completeuserproof will
find the non-unionized assertion permutation which matches the permutation
of the standard form metavariable deduction in set.mm and the subproof
will be completed by adding that non-unionized assertion permutation step.
( /\ ( /\ ) /\ T. ) is a collection of virtual
hypothesis collections occuring in a completeusersproof-generated
non-unionized assertion of a subproof of a Proof Worksheet. is
the virtual hypothesis collection of one hypothesis of that
subproof, ( /\ ) is another, and T. is the third. The
collection of the unionized assertion for this subproof, which is a step
of the original subproof, is ( /\ ) . The collection of the
non-unionized assertion is not a virtual hypothesis collection because the
element T. is not a virtual hypothesis and the element
( /\ ) is not a virtual hypothesis. The latter element is
not a virtual hypothesis because it is not atomic - it contains two
virtual hypotheses. Even if this element was divided to create
( /\ /\ /\ T. ) , the resultant collection is
not a valid virtual hypothesis collection because it contains two
virtual hypotheses.
Any subproof of a Proof Worksheet for which the virtual hypothesis
collection of the original assertion is identical to each virtual
hypothesis collection of each hypothesis of the subproof does not
need a non-unionized assertion and will be completed by mmj2
unification alone if a unifying MC metavariable deduction exists in
set.mm. If the only unifying metavariable deduction in set.mm is in
standard form, then a non-unionized assertion step must be added for
completion of the subproof.
A subproof of a translated User's Proof may unify with a deduction in
set.mm without any steps added to the original subproof. Such subproofs
are said to be completed by the mmj2 unification means. This is the sole
means by which the mmj2 program completes subproofs. completeusersproof
is designed to first attempt to complete each subproof of the User's
Proof by this means. If completeusersproof is not run in default mode, if
a subproof is not completed by the mmj2 unification means, then an attempt
is made to complete it by the metavariable deduction unification means. If
a subproof is not completed by either of these two means, then
completeusersproof attempts to complete it by adding a unification
theorem. If the unification theorem does not unify with a theorem in
set.mm, then completeusersproof will attempt to 2-step prove the
unification theorem in order to complete the subproof. We call the means
of adding a unification theorem and, if it does not unify, trying to
2-step prove it the unification theorem means. If a subproof does not
complete by any of these three means, the subproof will not be completed
by completeusersproof. Generally, some subproofs of a proof will complete
upon application of the mmj2 unification means, some will complete upon
application of the metavariable deduction unification means, some will
complete upon application of the unification theorem means, and some will
not complete. If all subproofs are completed, an RPN proof will be
generated.
If a subproof unifies with a MC metavariable deduction in set.mm, it is
completed by the mmj2 unification means, not by the metavariable deduction
unification means. If a non-unionized assertion's deduction of a subproof
is unified with a metavariable deduction in set.mm by applying the
metavariable deduction unification means, the metavariable deduction with
which it unifies is in standard form and has more than one hypothesis.
Every 1-hypothesis metavariable deduction is both a MC metavariable
deduction and is a metavariable deduction in standard form. If a subproof
unifies with such a metavariable deduction, it completes by the mmj2
unification means.
Not all subproofs which complete by the mmj2 unification means unify with
a MC metavariable deduction. Generally, a subproof completing by the mmj2
unification means often does not unify with a MC metavariable deduction.
For example, the subproof
5:: |- ( x e. A -> x e. suc A )
9:2: |- x e. A
15:5,9:ax-mp |- x e. suc A
completes by the mmj2 unification means by unifying with the deduction
ax-mp . ax-mp is not a MC metavariable deduction. Neither its hypotheses
or its assertion have a virtual hypothesis collection.
In order to run completeusersproof in non-default mode, the User must
include the matchstring "don't skip completeusersproofmv()" on any
comment line of the User's Proof. If this matchstring is omitted,
completeusersproof will run in default mode. Running in default mode,
completeusersproof will first attempt to complete each subproof by the
mmj2 unification means. The unification theorem means is then attempted on
any subproofs which did not complete by the mmj2 unification means. Any
subproofs not completing by either of these means are not completed. The
metavariable deduction unification means is not used when
completeusersproof is run in its default mode.
We now discuss in greater detail the unification theorem means of
completing a subproof. A subproof having more than one step unifies with
either a deduction in set.mm or(excl.) with a ff* false deduction in
fd.txt. 1-step subproofs unify with a theorem in set.mm or(excl.) do not
unify. There are no 0-hypothesis ff* deductions in fd.txt. Each ff* false
deduction corresponds to an eel* deduction which is the same as the ff*
deduction, except it is in conventional notation and has an additional
hypothesis, a "unification theorem". Presuming the User wrote a correct
subproof, that subproof is true before a unification theorem is added to
it. If the translated subproof did not complete upon application of the
mmj2 unification means, the subproof does not unify with any deduction in
set.mm. It does unify with a ff* false deduction in fd.txt. The translated
ff* deduction is false only because it is missing the unification theorem
hypothesis step which its corresponding eel* deduction has. The eel*
deduction is contained in set.mm. completeusersproof adds the unification
theorem to the subproof by replacing the ff* label with its corresponding
eel* label and applying the mmj2 unify command. The modified subproof
unifies with the eel* deduction.
The unification theorem of a virtual deduction deduction is that unique
virtual deduction whose virtual hypothesis collection is the collection of
the virtual conclusions of the hypotheses of the virtual deduction
deduction and whose virtual conclusion is the virtual conclusion of the
assertion of the virtual deduction deduction. Every unification theorem is
a theorem which may or may not unify with a theorem in set.mm.
If set.mm is sufficiently rich with respect to the mathematics which is
the subject of the User's Proof, then it is likely that the unification
theorem of a subproof or a semantic variation of it will be a theorem in
set.mm. If the unification theorem unifies with a theorem in set.mm, then
completeusersproof completes the subproof by adding it alone. If the
unification theorem does not unify with a theorem in set.mm, then the
stepprover() function of completeusersproof() will attempt to 2-step prove
the unification theorem. If there exists in set.mm at least one semantic
variation of the unification theorem and if there exists in set.mm at
least one 1-hypothesis deduction which deduces the unification theorem
from one of its semantic variations in set.mm, then stepprover()
automatically generates an additional step which is a semantic variation
of the unification theorem and which unifies with a theorem in set.mm and
completes the subproof. Otherwise, the added unification theorem remains
unproven and the subproof, although proveable (assuming the original
subproof is correct), is not completed.
The capabilities of completeusersproof which the mmj2 program does not
have include: 1) the ability to generate a unification theorem as an
additional hypothesis step of a subproof in order to complete that
subproof; 2) the ability to 2-step prove a unification theorem which does
not directly unify with a theorem in set.mm but is a semantic variation of
a theorem which does unify with a theorem in set.mm; 3) the ability to
generate a non-unionized assertion step of a subproof when a metavariable
deduction in standard form in set.mm will unify with that non-unionized
assertion's deduction of the subproof, and to complete the second deduction
of the same subproof which deduces the unionized assertion of the original
subproof from the added non-unionized assertion; and 4) the ability to
automatically put no-virtual-hypotheses steps of the original User's Proof
into standard T form, which is needed in order complete a subproof by the
metavariable deduction unification means if some of the hypothesis steps of
the original subproof have no virtual hypotheses.*