Proof Assistant GUI "Derive" Feature

See also:
Proof Assistant User Guide
ProofAssistantGUIQuickHOWTO.html
ProofAssistantGUIDetailedInfo.html
StepUnifier.html
WorkVariables.html
PageLocalRef.mmp
StepSelectorSearch.html
UnifyEraseAndRederiveFormulas.html
BottomUpProving-ByNormMegill.html
Quick Explanation:  Given RefX, Derive solves for unknowns in a proof step (imagine equation RefX(hypY, ..., hypZ) = formulaA).

Purpose:

Motivations:

Limitations:

Usage: The Derive Feature requires no change to the format of the Proof Assistant GUI proof text, just 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, 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 "&W1", "&W2", etc. 
  2. Hypothesis Generation: omitted or "?" 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 omitted Hyp or "?". Then, each generated Formula that is completely determined (contains no Work Variables), is compared to the Formulas of the previous proof steps. If a match is found, then the corresponding omitted or "?" Hyp 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 Hyp, omitted or "?" is updated to reflect the inserted Step number.
  3.  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 and Unification is attempted -- then, if Unification fails, the Hyp is set to "?". 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 Work Variables variables) and would unify with an assertion requiring no logical hypotheses!

Example 1: Using Derive as a typing short-cut. Below is the output after File/New Proof + "syl". Notice that syl's hypothesis steps are pre-loaded, as is the 'qed' derivation step. All we need to do is fill in the middle steps!
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::syl.1          |- ( ph -> ps )
h2::syl.2          |- ( ps -> ch )
3::                |- ?
qed::              |- ( ph -> ch )

$)
We enter steps 3 and 4 as shown below.
$( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=

h1::syl.1      |- ( ph -> ps )
h2::syl.2      |- ( ps -> ch )
3:2:a1i
4:3:a2i
qed:1,4        |- ( ph -> ch )

$)
and select the Unify/Unify (check proof) menu item or press the Ctrl and "U" keys simultaneously. The following is output.Notice that step 3's formula is completed but that it contains a Work Variable,  &W1.
$( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=

h1::syl.1      |- ( ph -> ps )
h2::syl.2      |- ( ps -> ch )
3:2:a1i        |- ( &W1 -> ( ps -> ch ) )
4:3:a2i
qed:1,4        |- ( ph -> ch )

$)
The error message screen also appeared, reporting  unification errors in steps 4 and 'qed' -- we ignore those errors for now...and change the "&W1' in step 3 to "ph". Then we select the Unify/Unify (check proof) menu item or press the Ctrl and "U" keys simultaneously. The following screen appears:
$( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=

h1::syl.1      |- ( ph -> ps )
h2::syl.2      |- ( ps -> ch )
3:2:a1i        |- ( ph -> ( ps -> ch ) )
4:3:a2i        |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed::          |- ( ph -> ch )

$)
The error message screen also appears, showing the following message:
E-PA-0411 Theorem syl Step qed: Unification failure in derivation proof step. The step's formula and/or its hypotheses could not be reconciled with an Assertion (axiom or theorem) in the loaded Metamath file(s).
 ---------------------------------------------------------
The problem is that we need to specify either a Ref, or Hyps, or both. To demonstrate Derive's Hyp generation feature, we enter "?" as Hyp for the 'qed' step and ax-mp as the Ref, as shown below:
$( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=

h1::syl.1      |- ( ph -> ps )
h2::syl.2      |- ( ps -> ch )
3:2:a1i        |- ( ph -> ( ps -> ch ) )
4:3:a2i        |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed:?:ax-mp    |- ( ph -> ch )

$)
Then we select the Unify/Unify (check proof) menu item or press the Ctrl and "U" keys simultaneously. The following screen appears:
$( <MM> <PROOF_ASST> THEOREM=syl      LOC_AFTER=

h1::syl.1          |- ( ph -> ps )
h2::syl.2          |- ( ps -> ch )

3:2:a1i            |- ( ph -> ( ps -> ch ) )
4:3:a2i            |- ( ( ph -> ps ) -> ( ph -> ch ) )
1004:?:            |- &W1
2004:?:            |- ( &W1 -> ( ph -> ch ) )
qed:1004,2004:ax-mp |- ( ph -> ch )


$)
Oh boy, still not done! Why!?!

Answer: specifying "?" as the Hyp for ax-mp provided incomplete information.The missing information is represented with the Work Variable, &W1 in steps 1004 and 2004, which were generated by the Proof Assistant --- which unfortunately, is not smart enough to figure out that it should have just taken steps 1 and 4 as the hypotheses for the 'qed' step. However, it is now obvious how to complete the proof: - we delete steps 1004 and 2004, and input "1,4" as the Hyp of the 'qed' step as shown below:
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::syl.1          |- ( ph -> ps )
h2::syl.2          |- ( ps -> ch )

3:2:a1i            |- ( ph -> ( ps -> ch ) )
4:3:a2i            |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed:1,4:ax-mp      |- ( ph -> ch )

$)
Then we select the Unify/Unify (check proof) menu item or press the Ctrl and "U" keys simultaneously. The following screen appears:
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::syl.1          |- ( ph -> ps )
h2::syl.2          |- ( ps -> ch )

3:2:a1i            |- ( ph -> ( ps -> ch ) )
4:3:a2i            |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed:1,4:ax-mp      |- ( ph -> ch )

$=  wph wps wi wph wch wi syl.1 wph wps wch wps wch wi wph syl.2 a1i a2i ax-mp
    $.
$)
Bingo! Ka-ching!

Example 2: Using Derive to develop a proof by working backwards from the conclusion to the hypotheses.

Below is the output after File/New Proof + "dfuz". Notice that dfuz's hypothesis step is pre-loaded, as is the 'qed' derivation step. All we need to do is fill in the middle steps!
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::dfuz.1       |- N e. ZZ
2::              |- ?
qed::            |- { z e. ZZ | N <_ z } =
                    |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }

$)
Ok, that looks simple enough......the user inputs no Hyps and "eqri" in the "qed" step and deletes step 2, as shown below:
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::dfuz.1       |- N e. ZZ

qed::eqriv       |- { z e. ZZ | N <_ z } =
                    |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }

$)
He selects the Unify/Unify (check proof) menu item or presses the Ctrl and "U" keys simultaneously. The following screen appears:
$( <MM> <PROOF_ASST> THEOREM=syl  LOC_AFTER=?

h1::dfuz.1       |- N e. ZZ

1001:?:          |- ( &S1 e. { z e. ZZ | N <_ z } <-> &S1 e. |^| { x | ( N e.
                    x /\ A. y e. x ( y + 1 ) e. x ) } )
qed:1001:eqriv   |- { z e. ZZ | N <_ z } =
                    |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }

$)
OK! A hard problem, deriving the 'qed' step, has been turned into an easy problem, deriving step 1001 -- which we leave as an exercise for the motivated reader. (Good luck!)

P.S. The following RunParm line inserted just before the RunProofAsstGUI line will create a proof for dfuz that can be input into the Proof Assistant using File/Open:

ProofAsstExportToFile,dfuz,dfuz.mmp,new,un-unified,NotRandomized,NoPrint

Options are new/update (the output proof file), unified/un-unified  (the output proof), Randomized/NotRandomized ( proof step Hyp order), Print/NoPrint (the output proof).

This RunParm gives you something to play with and may be useful in cloning proofs or finding shorter proofs.
See also:
Proof Assistant User Guide
ProofAssistantGUIQuickHOWTO.html
ProofAssistantGUIDetailedInfo.html
StepUnifier.html
WorkVariables.html
PageLocalRef.mmp