HomePage RecentChanges

mmj2ProofAssistantFeedback20080113

Back to: mmj2

note about the wiki

NOTE: To update the wiki your "username" must be whitelisted. Send an email to the wikilord if you are not already a user – and, if you don't care to do that, I authorize you to post as "ocat" for the purposes of mmj2 feedback and problem reports, etc. (Just put some initials on your edits so I know who is doing what…)

ALSO, you may get the "Cannot acquire main lock" error message when attempting to post to the wiki. In this case, hit the Back button on your browser, open a new window and go to RecentChanges then click on Administration, then Unlock Wiki. Wait, and then return to your original post and click on "submit" again.

other links

Previous Version of Feedback: mmj2ProofAssistantFeedbackV20070716

(Complaints about other aspects of mmj2 – general grievances -- should go here: mmj2Feedback )

The Cook Samples The Broth

The latest mmj2 release, implementing Work Variables, works great. Finally, I have the tool I always wanted for studying Metamath!

Here is one neat thing. Say you want to re-prove Metamath theorems. Like from the beginning. But that requires you to remember what has already been proven up to the point of the theorem you are working on. So, use Alt-U/H, for "Unify + Get Hints" immediately after starting the new proof with File/New Proof. mmj2 gives you back a message containing the assertions that are permissible at the current location within the database which have conclusion formulas that unify with the 'qed' step formula! (The 'qed' step's Ref label must be one of those – there are no other possibilities…fyi.)

Here is another neat thing: the new mmj2 Step Unifier, the new unification algorithm unifies a proof step formula(s) with itself. For example, say you are just beginning to proof theorem "19.20", and you have selected "syl" as the Ref for step 'qed'. The screen looks like this just before you press Ctrl-U to Unify:

    $( <MM> <PROOF_ASST> THEOREM=19.20  LOC_AFTER=?
     
    * Theorem 19.20 of [Margaris] p. 90.
     
    qed:?:syl          |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
     
    $)
     

The "Derive" feature kicks in because syl has 2 logical hypotheses and zero were supplied. The screen looks like this after Ctrl-U:

    $( <MM> <PROOF_ASST> THEOREM=19.20  LOC_AFTER=?
     
    * Theorem 19.20 of [Margaris] p. 90.
     
    1000:?:            |- ( A. x ( ph -> ps ) -> &W1 )
    2000:?:            |- ( &W1 -> ( A. x ph -> A. x ps ) )
    qed:1000,2000:syl |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
     
    $)
     

Now, suppose you decide that "&W1" should actually be "( ph → ps )". All you need to do is update one of the &W1 occurrences, press Ctrl-U, and all of them are set to the value you specified! It is automatic.

Here is another example. Say you input this proof step because you plan to use axiom ax-5 in your proof:

    55::ax-5
    

Then you press Ctrl-U and voila:

    55::ax-5           |- (  A. &S2 ( A. &S2 &W2 -> &W3 )
                          -> ( A. &S2 &W2 -> A. &S2 &W3 ) )
          

And, lets say you find that hard to read but you already know that &S2 = x and &W2 = ph. So you update the first &S2 and the first &W2 like this:

    55::ax-5           |- (  A. x ( A. &S2 ph -> &W3 )
                          -> ( A. &S2 &W2 -> A. &S2 &W3 ) )
               

Then you press Ctrl-U and the following screen appears:

    55::ax-5           |- (  A. x ( A. x ph -> &W3 )
                          -> ( A. x ph -> A. x &W3 ) )
          

That's neat: self-unification! I was surprised to see this behavior when I began testing; it was not predicted. If you recall, way back we discussed the need for a Search/Replace function on the mmj2 Proof Assistant GUI screen, but this pretty much eliminates those arguments!

Another cool thing which is very helpful is that although the Unification Search for a Ref label to unify with a proof step is not performed if the proof step formula or its hypotheses contain a Work Variable, once you determine the correct assignments for the Work Variables in a proof step, you can then make the changes and press Ctrl-U to initiate the unification search.

So, for example if you had this:

    55::               |- (  A. x ( A. x ph -> &W3 )
                          -> ( A. x ph -> A. x &W3 ) )
        

AND then determined that &W3 = ps, just make both of the assignments like so:

    55::               |- (  A. x ( A. x ph -> ps )
                          -> ( A. x ph -> A. x ps ) )
        

Then hit Ctrl-U, and voila:

    55::ax-5           |- (  A. x ( A. x ph -> ps )
                          -> ( A. x ph -> A. x ps ) )
     

(Ok, that example is contrived. But if &W3 existed in other proof steps with blank Ref fields, then they too would have been shipped through the Unification Search process – because the "self-unification" updates all logically-linked occurrences of a Work Variable on every proof step.

So, in conclusion, the combination of the original mmj2 Unification Search and the Metamath.exe "Derive" + Work Variables features work very well together. The mmj2 Unification Search is very good once you are able to create a valid formula but cannot remember the Ref label that applies. And the Metamath.exe "Derive", which generates the formula and hypotheses using an input Ref label allows you to build proof formulas quickly and correctly – using the aforementioned "self-unification" feature should also come in very handy as you instantiate Ref'd assertions for your proof!

By the way, I always found ax-5 a little puzzling -- and annoying in the way that it didn't exactly match the "textbook". But now I see 19.20 and wow, isn't that neat!

mmj2 is a very good tool, and I hope it enables many more people to now get into the Metamath databases. The combination of mmj2 + metamath.exe is excellent, by the way, as metamath.exe provides many features that mmj2 is afraid to attempt…

Here is one new feature that I believe will be most excellent…

For students wishing to re-prove set.mm theorems in order, there is a File/New-Next Proof (Alt-F + e) menu option to create a skeletal Proof Worksheet for the next theorem in the database after the current location. So, say you are finished with a1i and press Alt-F + e. Here is what you see:

    $( <MM> <PROOF_ASST> THEOREM=a2i  LOC_AFTER=?
     
    * Inference derived from axiom ~ ax-2 .
     
    h1::a2i.1          |- ( ph -> ( ps -> ch ) )
    2:?:               |- ? 
    qed:?:             |- ( ( ph -> ps ) -> ( ph -> ch ) )
     
    $)
     

Now, suppose there is a student ambitiously working their way through set.mm re-proving everything. Would she even notice if she invented a proof that is shorter than the set.mm proof? What if her proof is tremendously inventive and she imagines that everyone already sees the truth that she sees – and just presses Alt-F + e to begin work on the next theorem?

In practice, just being able to prove a theorem is an accomplishment. The fact that the proof is longer than the set.mm proof is not all that important. Some of the proofs are "tricky". The important thing is being able to do a proof at all. Still, on the other hand, it can be very educational to see the set.mm proof. But perhaps the student is too bothered or distracted to take that extra step and compare proofs?

So here is what I propose: a new Unify menu option "Unify/Unify + Compare To DB". What this will do is the normal unification and additionally, if the proof is completed successfully, it will perform a detailed comparison of the new proof versus the database proof. If the new proof is longer, shorter, or equal in length to the database proof, a message will report that fact. And, if the new proof is shorter then a metric will be used which approximates Norm's criteria for accepting shorter proofs for inclusion in set.mm: compare the number of symbols in the Proof Worksheet proof steps against the analogous number for the database proof. If less than the database, then the is a fairly good chance that the new proof will qualify for inclusion in set.mm – subject to a tedious list of criteria that must also be checked manually, such as html page size, etc.

I believe that with this new "Unify + Compare To DB" feature additional excitement and interest will be generated. And at the very least, a report that the new proof has the same size as the existing proof will save time -- the student knows immediately that she is on target with set.mm. (What would be really great would be a benefactor providing prize money of $5 per accepted shorter proof. Say, for example, a Warren Buffett or Sergei Brin is willing to contribute up to $10,000 for students who contribute shorter proofs – one prize per theorem per student, of course… This might stimulate an entire new industry in China: "proof farming". Or it might motivate someone to write a proof generator. Or it might motivate hundreds of students to learn math and logic, students who might never have even heard of predicate calculus…)

--ocat 23-Jul-2007

Feedback About the mmj2 Proof Assistant GUI