(This looks better in html format. it is a throwaway, draft document provided for early review – pending a planned May 1 release of the new code…)
Comments about the new "Derive" Feature should be posted here: mmj2ProofAssistantDeriveFeature
Thanks! --ocat
OK, I would like input on a specific question from anyone who may use the Proof Assistant. It regards the user interface for deriving hypotheses.
The "Derive" feature is triggered for Hypotheses when a Ref label is entered AND the user enters at least one "?" in the Hyp sub-field of the Step:Hyp:Ref token at the start of derivation steps. Like so:
3:?,1:ax-mp |- blah blah
There are validation checks though. If the user enters the following step, an error message complaining about the number of input Hyp numbers is produced:
3:?,1,2:ax-mp |- blah blah
ax-mp uses 2 logical hypotheses, so if the user inputs 2 Hyps there is nothing to derive. Likewise in the case of ax-1 which uses 0 logical hypotheses:
3:?:ax-1 |- blah blah
Question 1: if the Ref requires 0 hypotheses and the user inputs a "?" should the program complain, or should it just make the "?" go away – of course, it would not invoke Derive for hypotheses because there is nothing to derive.
Question 2: if the Ref requires n hypotheses where n > 0 and the user inputs a "?" and n hypotheses should the program complain?
The way it is coded now (fully tested) is to complain. The basis for that is that the user may have typed in the wrong Ref, or that the user is expecting the Derive feature to kick in and may be confused when it doesn't if the program just makes the "?" disappear. Also, after a few error messages, I expect that the user will learn not to put in a "? in this situation, so it is a matter of giving negative feedback at the beginning and then the "problem" goes away.
--ocat 14-Mar-2006
If the action can be documented in the Unify log screen, and nothing would be "hidden" from the user (no things mysteriously disappearing without explanation), then I would prefer just doing it, without interrupting the user with an error message prompt.
Another alternative: in "3::", when the user enters "ax-mp", the program automatically puts in "?,?".
Or, the the program automatically creates new numbered empty steps 1 and 2, and puts in "1,2", when the user enters "ax-mp". (Renumbering would be needed eventually.) When the program gets smart enough some day, the new steps 1 and 2 could be partially filled in with what is known.
--norm 14-May-2006
Actually, I'm a little uncertain about the typical scenario where the user is led to entering the "?", and my comments may be inapplicable. What would typically exist before the ax-mp?
Re your question:
Derive is basically for proving backwards from conclusion to hypotheses. So, at minimum, the hypothesis steps will exist. I don't think Derive will be used all that much except by "experts" – it can reduce the amount of typing needed on those long formulas though!
Re your comments:
1) I am not in favor of writing to the batch window or error log when a "?" is made to disappear. Already the Derive program adjusts the user's Hyp input to make the missing Hyps match the number of Hyps required by the Ref - so "?,2" gets expanded to "?,2,?" if 3 are required.
2) In response to "3::" just generating "?,?". I've tried to retain the old, non-Derive functionality, so entering "3::ax-mp" will generate an error message because the number of input hyps is wrong.
3) The Derive program does automatically create missing hypothesis steps and link the current step to them. So "3:?:ax-mp |- blah" will generate steps 2003 and 3003 (if 3 is the greatest step number on the proof" and it will update step 3 to be: "3:1003,2003:ax-mp |- blah". The generated hypothesis steps are inserted in the proof only if their formulas are not already present – if the Derived hypothesis formula is already there, the program just links the current step to it.
It may be that it will work best to just release the code and let you try it. I would prefer to not have to make any changes, but … some things must be seen to be believed :)
--ocat
Purpose:
* To satisfy expert users of mmj2's Proof Assistant GUI by partially solving the problem of correctly entering certain long and complicated formulas, the new Derive Feature generates missing proof step formulas using input Ref labels. This is the inverse of the normal Unification process of finding a matching assertion Ref label for an input formula and its associated hypotheses. * Also, to assist users in developing proofs by reasoning backwards from conclusion to premisses, proof step hypotheses are automatically generated and/or linked to previous proof steps when the user inputs "?" in the Hyp sub-field of the Step:Hyp:Ref field of a derivation proof step and supplies a Ref label. This powerful capability complements the new formula generation function and aids in the creation of proofs for theorems that are so insanely complex that even typing in the formulas correctly by hand is a superhumanly difficult task :)
Motivations:
* Typing Metamath formulas by hand is error prone and difficult, especially for long formulas. Part of the reason for this is that Metamath has no built-in grammar or syntax beyond the requirements of the input .mm file format. This is a feature, not a bug. The downside of Metamath's agnosticism is that there are no notational short-cuts; outer parentheses cannot be skipped and extra parentheses are not tolerated! Given that there may be dozens of syntax axioms used to build formulas and that even a single typing error generates an error message, the user may find it difficult to even input derivations, much less prove them! At some point a "Formula Builder" helper screen may be added to the mmj2 Proof Assistant GUI, but until then, the new Derive Feature will be useful. Note: the File/New menu option that is used to begin a new proof initializes the Proof Text area with the specified Theorem's hypotheses and conclusion proof steps, so the remaining challenge is to enter derivation steps. * The new Derive Feature provides an educational and investigational "what if?" capability allowing the user to easily answer questions such as, "Given a specific formula and assertion Ref label, what hypotheses do I need to obtain/prove in order to justify this derivation proof step?" Or, "If a specific assertion (Ref) is applied to a set of hypotheses (which may be incomplete), what formula is derived?"
Limitations:
* The mmj2 Proof Assistant GUI requires that each derivation proof step Ref label specify an assertion -- logical axiom or theorem -- in the input Metamath .mm file. The Ref, together with the associated hypotheses may be viewed as being a function call which generates the proof step formula. For example, treating the modus ponens axiom as a function with arguments '|- A|' and '|- ( A -> B )' yields "ax-mp|('|- A', '|- ( A -> B )') = '|- B'". In this case, the Ref, |ax-mp|, together with the hypothesis arguments completely specify and determine the contents of the resulting formula. However, the new Derive Feature allows the hypotheses to be incompletely specified -- missing hypotheses are designated with "?". In these cases the output formula will, of course, be incompletely specified as well! So, "ax-mp('|- A', '?') = '|- ?'". (A similar situation arises for generated hypotheses.) This is a feature, not a bug. But to properly present the unknowns in the generated formulas, the new Derive Feature needs to be able to present the un-determined variables in a helpful way. The Metamath Proof Assistant uses "$1", "$2", etc. for un-determined variables, so the Proof Assistant GUI will follow suit, but will also provide a RunParm option allowing the user to specify an alternate prefix such as "?" instead of "$". (Note: in some cases it may appear obvious to the user that a generated "$1" variable can be unified with a sub-formula of some previous step(s) -- and it is natural to ask why doesn't the program just go ahead and figure out the obvious substitution. The answer? Because that would require an entirely new unification search process inside the Derive Feature, as well as additional intelligence that is not programmed into the code...) * The mmj2 Proof Assistant GUI respects the order of input hypotheses for a derivation proof step during unification, but if the given order does not yield a consistent set of variable substitutions for a Ref assertion, the program methodically tests other sequences and dynamically rearranges its input Hyp's. For example, if the user inputs Hyp "1,2,3" referring to previous steps numbered 1, 2, and 3, but the referenced steps do not unify with the Ref's 1st, 2nd, and 3rd hypotheses, the program seeks an alternate arrangement, such as "3,1,2". In some cases, there may be multiple satisfactory sequences of hypotheses, which is one reason why the program gives the user's initial input order priority. For example, assume hypotheses "|- A" and "|- B" for assertion "|- ( A -> B )". In this example, both possible sequences of hypotheses will satisfy the requirements of unification! Now consider the situation where the user does not completely specify the hypotheses and inputs one or more "?"s in the Hyp sub-field. With incompletely specified hypotheses, the situation is even more ambiguous for the program's attempt to deduce the correct sequence of hypotheses! There is no perfect solution to this problem, but the Proof Assistant GUI will continue to respect the given Hyp order and seek an alternate sequence only if the given order fails unification. Thus, if the user inputs "?,3,?", the program will attempt unification of the 3rd proof step with the Ref's 2nd hypothesis before trying the alternatives. (On the plus side, since hypothesis generation is performed only when a Ref label is input, it may be assumed that the user has access to or knowledge of the Ref assertions hypotheses and their order -- and can use trial and error, if necessary.) * Even with the new Derive Feature, the mmj2 Proof Assistant GUI is far from being the ultimate tool for proving theorems.And, in fact, there is no proof that the Proof Assistant GUI is better for beginners than paper and pencil. The mouse/screen/keyboard interface may even hinder, at least initially, a student's development. The next major step in proof-assistive technology will use handwriting recognition technology, perhaps via a tablet PC equipped with a stylus and appropriate software for emulation of a blackboard. But even virtual reality software supporting an infinite virtual blackboard cannot replace the ultimate tool -- a higly motivated and well-educated mind. In the end, the value of this software or any other software must be measured by the human accomplishments it enables; if the software is helpful, fine, otherwise, do not hesitate to rubbish it and find a new way!
Usage: There is no change to the format of the Proof Assistant GUI proof text, but merely minor changes in the way the user's input is validated and interpreted. The new Derive Feature is tightly integrated into the existing Unification process and is triggered in due course by user input, as follows:
1. Formula Generation: Formula is now an optional entry on derivation proof steps except for the 'qed' (final) step (and remains mandatory on hypothesis steps). Either Formula or Ref must be entered on each derivation proof step. In the case where the Formula is not input then a Ref label is required, and is used along with the input Hyp's to generate a Formula. Variables that are not completely determined by the input Ref and Hyp(s) are shown as "$1", "$2", etc. (or with a different prefix such as "?" according to a new optional RunParm entry.) Note: if the Ref requires no hypotheses and the Formula is left blank, then the Formula's variables are considered -- by definition -- to be completely determined and the generated Formula is simply the Ref'd assertion's formula. 2. Hypothesis Generation: input "?" Hyp sub-field entries are used to generate hypothesis proof steps only if a Ref label is input and the total number of non-"?" Hyp entries is less than the number of hypotheses used by the Ref'd assertion -- and no other errors are found. The process contains a tiny amount of built-in intelligence and works as follows: unification of the input Ref assertion with the derivation step's Formula and given (non-"?") Hyp entries is attempted. If this partial unification is successful, an hypothesis Formula is generated for each input "?". Then, each generated Formula that is completely determined (contains no "$1", "$2", etc. variables), is compared to the Formulas of the previous proof steps. If a match is found, then the corresponding "?" is changed to the Step number of the matching formula. Otherwise, if no matching Formula is found, or if the generated Formula contains un-determined variables, then a new derivation proof step is created and inserted in the proof immediately prior to the current derivation step, and the corresponding "?" is updated to reflect the inserted Step number. Generated Step numbers are assigned sequentially by adding 1000 to the greatest Step number in the proof at that moment. So, if the greatest Step number in the proof = 5, then the generated hypothesis steps are numbered 1005, 2005, ..., etc. Note: for each generated hypothesis inserted in the proof, the output Hyp and Ref sub-fields are set to null. Originally, the plan was to set Hyp to "?", which would automatically prevent unification of the generated step. However, given that in many cases the generated Formula will be completely determined (with no $1, $2 variables) and would unify with an assertion requiring no logical hypotheses! And(!), generated proof steps that are completely determined will be subjected to the unification search process, which will generate an error message if no unifying assertion is found. Proof steps that are not completely determined will not be routed through the unification search, and will not trigger error messages -- unless the user fails to update the Formula, replacing the $1, $2 variables, prior to the next unification request.
Hi Norm, Raph, frl and other mmj2 users (if any):
Brain surgery on the ProofUnifier? to accomplish the new "Derive" Feature in Proof Assistant is complete.
Not tested (or installed) yet though, as I need to go down into ProofWorksheet? and alter the field-level validation routines. The changes in the core unification search/match process were surprisingly minor – basically just allowing "null" formulas to "unify" and keeping track of un-substituted variables for the Derive process.
I added a minor embellishment, which I wanted to mention, but the main reason for communicating involves local- scope variables used in the formulas of theorems and their logical hypotheses.
I understand why it is a good thing to use local variables to keep the Optional Frames small in subsequent theorems.
However, the problem is that these non-global variables are useless outside their defining scope when a program is determining the meaning of a formula – one has to access the Frames to see these variable types.
This is an issue in Embellishment #1, in which I allow the Proof Assistant user to input just a "?" Hyp and an assertion label Ref – no formula and no non-"?" Hyps. In this case I could have treated all of the variables in the assertion and logical hyps as "un-determined", but that would generate a bazillion dummy variables and be a source of user complaints. So, in this case, where all of the variables are, by definition un-determined (i.e. not substituted), I just insert the logical hypotheses (if not already present), along with the assertion's formula in the proof, as is. But since a variable defined in-scope of a Ref'd assertion is out of scope of the proof's theorem, I am required to substitute dummy variables for any locally defined variables if the Ref or its hypotheses (a nuance…)
And, from a database design viewpoint it would be far better then if all variables in formulas were defined globally. Just saying, not complaining, but it seems to me that using locally defined variables should be done rarely if at all, except when dummy variables are needed in proofs. That will facilitate export of Metamath databases to other systems, also…
[Raph's suggestion about having a "*" wildcard option on the Ref field does not seem ideal, and I am not doing it (yet :). For one thing, an explicitly input Ref that fails to unify or that results in a Distinct Variable Restriction error will generate a message showing alternate Ref labels that do unify (and the DV error is automatically fixed if a better Ref is found.) So putting the wildcard option on the proof itself would be cumbersome, and not add much I think. An alternative that might be considered would be a query screen showing full details about the alternative Ref's that unify – or just expanding the content of the existing message text. I think Metamath's Proof Assistant's Search facility will obviate the need for this enhancement, especially when its mmj2 Import/Export feature is ready.]
--ocat 10-Mar-2006
. . .
*mmj2 Proof Assistant GUI – Proposed Addition to Unify Menu: DeriveAndUnify option*
DeriveAndUnify is performed after the standard field validation edits used now prior to Unification. Field validation errors terminate the process prior to Unification or DeriveAndUnify?.
Assuming that there are no field validation errors, DeriveAndUnify works as follows: a "Derive" pre-process is performed, and then if no errors are encountered, and if all variables and hypotheses are fully determined by the derivation constraints, the standard Unification process is performed.
The new Derive pre-process treats the Hyp and Formula portions of a Proof Step as solvable unknowns in a Hyp, Ref, Formula equation. (The existing Unification process, which will not be changed, solves for Ref.)
For clarity, here is the layout of a hypothetical Proof Step (Step 9 with Hyps = Step 1 and Step 2, Ref label = "XXXX", and Formula = "|- BLAH BLAH".)
Step:Hyp:Ref Formula ============ ======================= 9:1,2:XXXX |- BLAH BLAH
|===============================|===============================| | Formula Present | Formula Not Present | |===============================|===============================| | Ref Present |Ref Not Present| Ref Present |Ref Not Present| |===============|===============|===============|===============| | >= 1 | 0->n | >= 1 | 0->n | >= 1 | 0->n | >= 1 | 0->n | |Hyp = ?|Hyp(s) |Hyp = ?|Hyp(s) |Hyp = ?|Hyp(s) |Hyp = ?|Hyp(s) | | |Present| |Present| |Present| |Present| |=======|=======|=======|=======|=======|=======|=======|=======| |#1 |#2 |#3 |#4 |#5 |#6 |#7 |#8 | |Derive |No |No |No |Derive |Derive |Error: |Error: | |Hyp |Change,|Change,|Change,|Formula|Formula|We're |We're | |then |just do|just do|just do|then |then |not |not | |Unify |normal |normal |normal |Derive |Unify |mind |mind | | |Unify |Unify |Unify |Hyp | |readers|readers| | | | | |then | | | | | | | | |Unify | | | | |=======|=======|=======|=======|=======|=======|=======|=======|
Notes:
#1 DeriveHyp?: attempts to determine the formula(s) of the missing Hyp(s). Then, if the formula is already present in the Proof Text area prior to the current Proof Step, the "?" in the Hyp is replaced with the Step number of the matching formula. Otherwise, if there is not already a matching formula in the Proof Text area, a new Proof Step is generated and inserted in the Proof Text just prior to the existing Proof Step; then the "?" in the Hyp is replaced with the newly generated Proof Step number. The new step number = greatest step number in Proof Text area + 1000. Any undetermined variables in the output are shown as "?" and Unification is not performed ("?" is used instead of guessing – if the user does not change the "?"s to actual variables before the next Unification/DeriveAndUnify? request, a field validation error is triggered.)
The generated step will look like this:
1009:?: |- something for missing blah-blah hyp
After DeriveHyp?, assuming that no new errors are encountered, and that there are no undetermined variables or hypotheses, the standard Unification process is performed.
#5/#6 DeriveFormula?: attempts to determine as much of the Proof Step's formula as possible given the input Hyp(s); the input Hyp(s) may only partially determine the formula substitutions (and may not even unify with the input Ref's Hyp(s)!), and any undetermined variable substitutions will be created by mapping from variables in the Frame of the theorem being proved to undetermined variables in the Ref's formula. Processing then proceeds as in #1, with DeriveHyp? if any of the input Hyp sub-fields = "?", and then Unification.
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) qed:?:ax-mp |- ( ph -> ch ) $)
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 2002:?: |- ? 3002:?: |- ( ? -> ( ph -> ch ) ) qed:3002,3003:ax-mp |- ( ph -> ch ) $)
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 3:?:a2i qed:?: |- ( ph -> ch ) $)
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 3003:?: |- ( ph -> ( ps -> ch ) 3:3003:a2i |- ( ( ph -> ps ) -> ( ph -> ch ) qed:?: |- ( ph -> ch ) $)
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 3:2:a1i qed:?: |- ( ph -> ch ) $)
$( <MM> <PROOF_ASST> THEOREM=syl LOC_AFTER= h1:: |- ( ph -> ps ) h2:: |- ( ps -> ch ) 3:2:a1i |- ( ? -> ( ps -> ch ) ) qed:?: |- ( ph -> ch ) $)