"Unify + Erase And Rederive Formulas" Feature

See also:
Proof Assistant User Guide
ProofAssistantGUIQuickHOWTO.html
ProofAssistantGUIDetailedInfo.html
ProofAssistantGUIDeriveFeature.html
StepUnifier.html
PageLocalRef.mmp
WorkVariables.html
StepSelectorSearch.html
BottomUpProving-ByNormMegill.html

Function

The function of the "Unify+Erase And Rederive Formulas" feature (available on the Proof Assistant GUI Unify menu) is fairly simple: it preprocesses the Proof Worksheet, before parsing and unification, to erase formulas on Derivation proof steps -- except the 'qed' step -- which have a non-blank Ref field. Erasing the formulas triggers the "Derive" feature of the mmj2 Proof Assistant GUI, which re-generates the formulas using the theorem's hypotheses, the 'qed' step, and the contents of the Step:Hyp:Ref fields on the Derivation proof steps. This is a fairly drastic option for a user to choose, but pressing Ctrl-Z twice, to Edit/Undo the results of the erasure and unification will restore the Proof Worksheet to its previous state.

To properly explain why someone would wish to perform this function, the best source is the inventor, Norm Megill. What follows is stolen from the Asteroid Meta wiki mmj2ProofAssistantFeedback.html webpage.


Feedback: unification lockups

(This is a general mmj2 issue, not related specifically to the beta.)

Suppose we are developing a proof and have gotten to this point:

 $( <MM> <PROOF_ASST> THEOREM=xxx  LOC_AFTER=?
 1::ax-1            |- ( &W1 -> ( &W2 -> &W1 ) )
 2::ax-2            |- (  ( &W7 -> ( &W4 -> &W7 ) )
                       -> ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) ) )
 3::ax-1            |- ( &W7 -> ( &W4 -> &W7 ) )
 4:3,2:ax-mp        |- ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) )
 5::ax-2            |- (  ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) )
                       -> (  ( ( &W7 -> &W4 ) -> &W7 )
                          -> ( ( &W7 -> &W4 ) -> &W7 ) ) )
 6:4,5:ax-mp        |- (  ( ( &W7 -> &W4 ) -> &W7 )
                       -> ( ( &W7 -> &W4 ) -> &W7 ) )
 qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
 $)

Then we realize, oops, step 4 should be "4:2,3:ax-mp" and not "4:3,2:ax-mp". But after we make this correction, the proof is "stuck" because the work variables now have the wrong patterns.

If we ctrl-z all the way back, which could have been a long time ago, we will lose all the work we did in the meantime.

On the other hand, if we completely erase the proof's formulas by hand:

 $( <MM> <PROOF_ASST> THEOREM=xxx  LOC_AFTER=?
 1::ax-1
 2::ax-2
 3::ax-1
 4:2,3:ax-mp
 5::ax-2
 6:4,5:ax-mp
 qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
 $)

then press ctrl-u, everything is magically corrected to exactly what I want to see:

 $( <MM> <PROOF_ASST> THEOREM=xxx  LOC_AFTER=?
 1::ax-1            |- ( &W1 -> ( &W2 -> &W1 ) )
 2::ax-2            |- (  ( &W3 -> ( &W4 -> &W5 ) )
                       -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) )
 3::ax-1            |- (  (  ( &W3 -> ( &W4 -> &W5 ) )
                          -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) )
                       -> (  &W6
                          -> (  ( &W3 -> ( &W4 -> &W5 ) )
                             -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) ) )
 4:2,3:ax-mp        |- (  &W6
                       -> (  ( &W3 -> ( &W4 -> &W5 ) )
                          -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )
 5::ax-2            |- (  (  &W6
                          -> (  ( &W3 -> ( &W4 -> &W5 ) )
                             -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )
                       -> (  ( &W6 -> ( &W3 -> ( &W4 -> &W5 ) ) )
                          -> ( &W6 -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) ) )
 6:4,5:ax-mp        |- (  ( &W6 -> ( &W3 -> ( &W4 -> &W5 ) ) )
                       -> ( &W6 -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )
 qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
 $)

This shows that mmj2 inherently has the ability to recover from such mistakes. However, erasing all the proof's formulas to recover from such mistakes is tedious to do by hand. Annoying even. :)

I would be happier if there were an option that simply erases the entire wff content. Or at least resets work variables back to their "most general" state. This will give me the freedom to experiment without fear that an accidental bad unification will lock up the proof.