HomePage RecentChanges

mmj2ProofAssistantDeriveFeature

(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…)


Links

Comments about the new "Derive" Feature should be posted here: mmj2ProofAssistantDeriveFeature

Thanks! --ocat


User Interface Question: "Derive" Hypotheses

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?

The "Usage:" section a few scrolls down (after Purpose, Motivations and Limitations) covers it pretty well. After trying "Derive" I find it isn't as super fantastic as I had envisioned. Derive generates Formula and/or Hyps, so now the (mental) equation 'Ref(Hyps) = Formula' can be solved for the unknowns on any step except the hypothesis or 'qed' steps (Formula is always required on the 'qed' step and isn't derived).

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

Proof Assistant GUI "Derive" Feature


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.

Discussion, 10-Mar-2006

Hi Norm, Raph, frl and other mmj2 users (if any):

Yes, there is at least one other active user who corresponds with me. Due to an unexpected project, my proof worksheet interface is behind schedule but is very much part of my plan. Then I'll bet you are going to see an influx of new users. --norm 11-Mar-2006

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


OBSOLETE PRIOR VERSION OF DOC FOLLOWS

. . .

*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

DeriveAndUnify Processing

    |===============================|===============================|
    |       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.


Sample #1: Input

    $( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=
    
    h1::           |- ( ph -> ps ) 
    h2::           |- ( ps -> ch ) 
    
    qed:?:ax-mp    |- ( ph -> ch )     
    
    $)
    

Sample #1: Output

    $( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=
    
    h1::            |- ( ph -> ps ) 
    h2::            |- ( ps -> ch ) 
    
    2002:?:         |- ?
    3002:?:         |- ( ? -> ( ph -> ch ) ) 
    qed:3002,3003:ax-mp |- ( ph -> ch )     
    
    $)
    

Sample #5: Input

    $( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=
    
    h1::           |- ( ph -> ps ) 
    h2::           |- ( ps -> ch ) 
     
    3:?:a2i    
    qed:?:         |- ( ph -> ch )     
    
    $)
    

Sample #5: Output

    $( <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 )     
    
    $)
    

Sample #6: Input

    $( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=
    
    h1::           |- ( ph -> ps ) 
    h2::           |- ( ps -> ch ) 
     
    3:2:a1i    
    qed:?:         |- ( ph -> ch )     
    
    $)
    

Sample #6: Output

    $( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=
    
    h1::           |- ( ph -> ps ) 
    h2::           |- ( ps -> ch ) 
     
    3:2:a1i        |- ( ? -> ( ps -> ch ) )    
    qed:?:         |- ( ph -> ch )     
    
    $)