HomePage RecentChanges

mmj2ProofAssistantFeedbackV20061101

Feedback About the new mmj2 Proof Assistant GUI

The policy here at MMJ2 Research Labs, LTD. is to catapult installation files over the castle walls, old school style. We love to hear the agonized shrieks and outraged complaints of our customers :) …So…

Feel free to complain about the Proof Assistant here!!!

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

Previous Version of Feedback: mmj2ProofAssistantFeedbackV20060129


Links


Note for Newcomers

Welcome!

Here is a tutorial: mmj2ProofAssistantTutorial

And this has more helpful information, including a "quick howto", a detailed reference for the Proof Assistant GUI and information about the powerful new Derive feature:

     http://planetmath.cc.vt.edu/~mmj2/
    

For someone new to Metamath proving techniques, a good start is to save a copy of this page showing the first 100 proofs in set.mm and then work through proving them, one by one:

    http://us.metamath.org/mpeuni/mmtheorems.html

If you do not have unicode Math fonts you should go get them, but as a workaround use the GIF directories at Metamath, like this:

    http://us.metamath.org/mpegif/mmtheorems.html

The 100th theorem in set.mm is pm2.521, so in your mmj2 RunParm file add this line right before the "LoadFile" RunParm line:

    LoadEndpointStmtLabel,pm2.521

That will reduce the GUI time by a 10(?) by not loading 6000+ theorems, only the first 100.

Things I like about it

1. The Proof Assistant has Derive, Renumber and Decompress, as requested! Derive, especially, is very powerful. Renumber was a quick fix, but helpful. Decompress speeds up the LoadFile operation by 50%, so that is very nice!

Installation Grievances

1.

    You say to download the "JDK 1.5 compiler (Java Development Kit)"
    from http://java.sun.com/j2se/1.5.0/download.jsp.
    There are several downloads on that page that mention "JDK" and
    none mention anything about a "1.5 compiler".  I selected "JDK 5.0
    Update 6". Perhaps it would be good to make this explicit.
    
Good feedback. Will modify install.txt.
Ooops. I forgot. Next time :) ocat 28-Mar-2006.

2.

    When you say "Windows Command Prompt", you mean
    Start -> Run -> cmd, _not_ Start -> Run -> command.
    Maybe everyone "knows" this, but I rarely use it and
    keep mixing them up as I try to unremember my Windows 95 days.
    

I should say Windows Command Prompt Window, which is the modern analogue of the old DOS Window under Windows 3.1 etc. What I do is Start/Programs/Accessories and then right mouse button click "Command Prompt" and select "Create Shortcut" to put the Command Prompt Window icon on the desktop.

3.

    When I ran C:\mmj2\compile\windows\CompMMJ.bat I got:
    
    C:\tmp>C:\mmj2\compile\windows\CompMMJ.bat
    ...
    C:\mmj2>javac @compile\windows\javacTCompilePaths.txt   @compile\mmj\mmio\mmioClasses.txt 'javac' is not recognized as an internal or external command, operable program or batch file. … C:\mmj2>ECHO "*** CompMMJ?.bat ERROR ENCOUNTERED!" "*** CompMMJ?.bat ERROR ENCOUNTERED!" …
    I had to do this:
        Start -> Settings -> Control Panel -> System -> Advanced ->
        Environmental Variables -> 
        edit Path to append ";C:\Program Files\Java\jdk1.5.0_06\bin"
        
    and restart the Windows Command Prompt.  
    (Later - I now see you mention this at the bottom of the page, 
    but it should probably be part of the in-line instructions.  
    Also, the path is obsolete in the bottom-of-page instructions.
    I wonder why Sun doesn't add to the Path in its Java installation?)

So noted. Thanks!

4.

    You might mention C:\mmj2\test\windows\!BatchMMJ2Sample001.bat
    is the one for set.mm (or rather expset.mm).  Or perhaps a more
    obvious name? The others seem to be test cases that probably
    wouldn't be of general interest.
    

C:\mmj2\test\windows\RunPAGUI.bat is the sample to kick off the GUI Proof Assistant. What I am doing is setting up a separate directory/folder elsewhere that is customized for my proof studies. Like c:\myproofs and then copy "RunPAGUI.bat" to there, along with its RunParm file, "RunParmFileRunPAGUI.txt" (update the "LoadFile" and "ProofAsstProofFolder" RunParm commands to point to the correct input files.

Then go into the Command Window and execute

    cd: c:\myproofs
    runpagui
    

Suggestions and Things I do not like about it

1. The proof text area is always in "Insert Mode", and the insert key doesn't toggle between replace and insert.

2. There is no Undo/Redo feature.

   --> Added in Nov-1 Release. Note that after Unification
       Undo must be pressed TWICE -- the GUI creates two
       undoable actions when resending the page: update
       the text and position the cursor. The code to combine
       two undoable actions into one is a little tricky and
       I am not in the mood to attempt at this time. The
       bad part is that after the first Undo what is 
       presented is a blank text area, but the second Undo
       restores the text in correct status.

3. Add code to the very beginning of BatchMMJ2 to verify that the Java runtime environment is compatible with the compiled code. This would be useful if/when compiled code is distributed.

    --> Added in Nov-1 Release. Looking for version 1.5 or
        higher. Not sure how well this works in non-Sun
        runtime environments, but given the fact that
        Java Swing would be almost impossible to reverse
        engineer in a clean room, the open source community
        will need to wait just a bit more for Java to be
        released as open source...and then things will be
        beautiful...As is, we know that the Macintosh/Apple
        Java does not support mmj2's needs, but that mmj2
        is runnable on Linux and Windows (using Sun's JRE
        environment.)

4. It does not output proofs in Metamath compressed format.

    --> This is not impossible, but it is computationally
        intensive. Given that Metamath.exe now has an
        import/export facility for mmj2 Proof Worksheets,
        the priority of this item is lower than low. The
        reason why it might be done is that there are 
        interesting algorithms for checking for repeated
        subproofs and this is an active area of research.
        My idea is to create a hash key for each node of
        a proof tree and then check a hash table to see
        if the sub-proof already exists for the proof. 
        

5. Formulas are displayed as long strings that are hard to read. For example, Step 10 of theorem cdaassen comes out as

    12::eqeng  |- ( ( ( ( A X. { (/) } ) u. ( B X. { 1o } ) ) X. { (/) } ) e. V -> ( ( ( ( A X. 
                  { (/) } ) u. ( B X. { 1o } ) ) X. { (/) } ) = ( ( ( A X. { (/) } ) X. { (/) } )
                  u. ( ( B X. { 1o } ) X. { (/) } ) ) -> ( ( ( A X. { (/) } ) u. ( B X. { 1o } ) )
                  X. { (/) } ) ~~ ( ( ( A X. { (/) } ) X. { (/) } ) u. ( ( B X. { 1o } ) X. { (/) 
                  } ) ) ) ) 
    
    --> The new TMFF -- Text Mode Formula Formatting enhancement
        is a glorious achievement :) Will be available in the
        Nov-1 release!

Would it be possible/useful to output using the Unicode typesetting specified in the input .mm file, along with new typesetting specifications at the syntax axiom level (the formula parse trees would be input to the formatter)? The user would continue to input the ASCII equivalents (as shown above), which would be converted to Unicode for re-output. A switch to a variable width font might help too. --ocat 3-Apr-2006

6. (Suggestion) On the mmj2 doc page, you have:

 2. As of April 1, 2005, mmj2 contains processing to perform
 validation of www.Metamath.org ".mm" files (also called Metamath
 databases), Proof Verification, extremely basic printing of the
 contents of a .mm file, grammatical parsing, and proving with a
 GUI Proof Assistant.
    - It does not do anything with Metamath Comment Statements
    - It does not produce beautiful html pages like
      metamath.exe.
    - It does not update an existing .mm file.

Regarding the last point, you may want to mention the worksheet export/import facility eimm that does allow (indirectly) updating a .mm file, as well as allowing you to go back and forth between the mmj2 and metamath PAs, giving you access to the best features of each. I also wonder if anyone other than myself is actually exploiting the power of eimm, since I've heard no feedback. Or maybe it's just because there are no bugs. :) But more likely it's because almost no one is aware of it, so it might be useful to mention it in your doc page. --norm 14 Aug 2006

So noted. Thanks. If memory serves…eimm was released after the most recent version of mmj2; no slight was intended by omission of eimm from the documentation. On the functionality side, is it true that eimm only updates a .mm file with proofs for theorems that already exist in the .mm file? (For mmj2's part in this I must also note that completing a proof in mmj2, with or without eimm does not update the information available to mmj2 for follow-on proofs. Now that eimm is available, that functionality is more approachable – and even without it, restarting mmj2 to pick up the new .mm data takes only 5 seconds or so…) P.S. The next version of mmj2 incorporating "Text Mode Formula Formatting" is closer to the coding stage now, and I think it will be really helpful for people whose eyes go "swimmy". --ocat 14-Aug-2006

with a proof,

Bugs and Things that do not work as expected

1. The cursor positioning code does not always put the cursor exactly at the first error on the screen.

    --> Big improvements coming in Nov-1 release!!!

2. A very minor nuisance (put it near the bottom of your to-do list):

If you Exit/Quit, the getYesNoCancelAnswer() box comes up. In most programs, if you click on the upper right X in such a box, the action is the same as if you clicked on Cancel. In mmj2, the action is the same as if you clicked No.

If, instead of Exit/Quit, you click on the upper right X in the main screen, the getYesNoAnswer() box comes up. First, there is no Cancel option. (Most programs have one under this condition.) But again, if you click the upper X of the getYesNoAnswer() box, the action is No rather than Cancel, so once you get to that box there's no way to cancel.

    --> Will be fixed in Nov-1 release. 'x' button press to close
        window invokes yes/no/cancel dialog if changes need saving,
        and the yes/no/cancel dialog treats 'x' button press
        (close of the dialog window) as a CANCEL.

Talk

Hi frl, Glad to see you are back on the Lambda Calculus My brain is tired so I cannot begin to comprehend what you wrote, but it is nice to hear from you again! The Renumber feature in mmj2 is now available. I think you will also appreciate the Derive feature. --ocat 4-Apr-2006

Hi ocat, I'm happy you released a new version. I shall try it as soon as possible (i.e. as soon as I remember to take a usb key and to go to a place where I can download it ). – frl 4-Apr-2006

That's ok. I've tried it and everything works perfectly. Thank you for the "Renumber" feature. Proving is much easier this way. I have not yet used the "Derive" feature. It is less important for me since I often make my proofs using cutting and pasting but I shall try it as well. What are your plans for the future ? – frl 5-Apr-2006

Hi frl, glad to hear your report :) The future is indeterminate. Thus far mmj2 has been a great learning experience but I don't yet know everything I need to know to rewrite it properly. It seems that the Proof Assistant needs proper output formatting. That is probably the biggest immediate hole – and it must not only provide decent formatting of formulas but provide for input. My own personal future is uncertain but I probably won't be able to rest in peace until I create one more version…just one more time! :) --ocat 5-Apr-2006

I've tried the "Derive" feature. It's nice as well. If you need end-user requirements, don't hesitate: I have some. – frl 6-Apr-2006

Please divulge! That is the purpose of this page. Renumber, Derive and Decompress were the result of "end-user requirements". I am of the view that the narrow path should be taken until mmj2 enlightenment is achieved – that which is really needed is the priority because all the rest does not matter if the basic needs are not met. --ocat 6-Apr-2006

Use case #1

Ok I'm working on a proof. After some time. I get something like this:

  h1::        # G |- fubar
  210::          # G |- farbu
  21:210:           # G |- barbar
  20:1,210:           # G |- barfu
  2:20,21:        # G |- bar
  qed:1,2:     # G |- fu

Now I use the renumber derive feature, I get:

  h1::       # G |- fubar
  2::e          # G |- farbu
  3:2:d           # G |- barbar
  4:1,2:c           # G |- barfu
  5:4,3:b        # G |- bar
  qed:1,5:a   # G |- fu

Much better. But I'd like that the #s are in a row (new possible feature #1).

  h1::        # G |- fubar
  2::e        # G |- farbu
  3:2:d       # G |- barbar
  4:1,2:c     # G |- barfu
  5:4,3:b     # G |- bar
  qed:1,5:a   # G |- fu

This way it's pretty esthetical. But the tree-like aspect of the proof is not respected. 2 and h1 should be duplicated. And the order of the lines should be reorganized. ( new feature #2)

  h1::        # G |- fubar
  2::e        # G |- farbu
  3:2:d       # G |- barbar
  h1::        # G |- fubar
  4::e        # G |- farbu
  5:1,4:c     # G |- barfu
  6:5,3:b     # G |- bar
  qed:1,6:a   # G |- fu

And even we could increment the number of spaces in the most metamath-like manner ( new feature #3).

  h1::         # G |- fubar
  2::e           # G |- farbu
  3:2:d         # G |- barbar
  h1::           # G |- fubar
  4::e           # G |- farbu
  5:1,4:c       # G |- barfu
  6:5,3:b      # G |- bar
  qed:1,6:a   # G |- fu
Of course you will eventually want an instant-gratification mmj2 menu option for indentation, but since you'll have to wait at least until ocat finishes his 2020 report (what is that?), in the meantime you can do it the "hard" way - import then export the proof with eimm (see Use Cases 5a and 5b below). That would also help provide a good test of eimm. (If eimm export screws up and wipes out your proof, the old worksheet will be in <theorem>.mmp~1.) Currently the indentation is 2 spaces per indent level, although that could be a parameter if it is deemed important. Also, wffs are not currently line-wrapped by eimm - that would be easy to do, but I'm torn about whether it is useful since the mmj2 PA has horizontal scrolling. It could also be a parameter if people want it. Or maybe an mmj2 menu option? --norm 19-Apr-2006

This time a marvellous feeling of joy fills up the amateur of logic I think. frl 7-04-2006

Thanks! OK! Do you have more requirements? To me, the key to improving appearance is enabling output of the Unicode math symbols with helpful, automatically generated line breaks when a formula's length exceeds the specified width of the screen. Perhaps colors? Perhaps parentheses/brackets of different sizes? Perhaps … These sorts of changes become necessities when viewing some of Norm's formulas!!! With 300 symbols in a formula, it isn't acceptable to just shoot them out of the mmj2 cannon onto the screen :) ocat 7-Apr-2006

Use case #2

I open mmj2 with let's say nat.mm. But when the proof is completed I need to copy it and to paste it into another editor. I never work with Windows, so I don't have good editors under it. So I would prefer to be able to load nat.mm in another tab in mmj2, and perhaps set.mm as well. Obviously I would need to be able to search for strings in these two tabs. frl 7-Apr-2006

Those are expansive ideas/requirements. You probably know that metamath.exe handles most of cases #1 and #2 – and I think Norm is still planning to add an Import facility to metamath.exe so that mmj2 can be used as a tool in the metamath.exe Swiss Army knife of capabilities? Maybe we need to expand mmj2 as you request in order to acquire more than 2 users :) Or maybe invent a non-Hilbert version of Metamath? Or perhaps a whole new approach – like virtual reality I/O with an infinite blackboard and speech synthesis/recognition PLUS something else … --[[ocat] 7-Apr-2006
Expansive means what ? That it would take time to realize them ? In fact new features #1 and #2 are not important to format the proof at the end but to do so while working on a proof. So we can't say metamath handles these cases. But it's true that these requirements only try to slightly improve metamath framework. In fact I really like metamath framework.
I hope you will find more than two users. According to me mmj2 is a good work. It really brings something to metamath: the ability to work with proofs in both directions. Don't give up. --frl 8-Apr-2006
The Import facility is up there on my to-do list, but it may be a sizeable project and I haven't been able to fit it into my spare time yet. (Currently I'm coauthoring 3 papers, my taxes are due soon, and I just finished an emotionally draining couple of days of jury duty. And I must allocate time to prove a theorem or two each day, so my brain won't decay.) --norm 8-Apr-2006
My taxes were mailed and my papers await my coauthor, so I was able to get back on this. The eimm import command (see User Case 5b below) will let you bring your partial proof into metamath.exe's PA and save it in the .mm file. And the export command will then let you convert it back to a proof worksheet, since I don't think mmj2 handles partial .mm proofs. --norm 19-Apr-2006

Use case #3

I'm in an internet café. I have some time to spend. I want to make a proof. I connect myself to a very good web site (let's call it www.metamath-inline.org ). An interface appears on the screen that really looks like mmj2. I can ask to work with a database available on the server. For example set.mm (or nat.mm). I click on "new". I enter a proof. While working I can browse proofs in another good site (www.metamath.org). One hour later the proof is not finished. I save it in a private area on the server. Later I resume. This time I load set.mm and my new partial proof. --frl 8-Apr-2006

Where is the café? Is it in Amsterdam, Paris or Brussels?
Mine are usually in Paris ? Why :-)
Motivation – metaphysical self-actualization. I now see myself in the cafe. But I don't see you there :) Ahh! I am in Amsterdam and you are in Paris. That explains it.
As you know, Amsterdam is a town where it is easy to lose one's reputation. You should come to Paris. Paname, as French call it
OK. Perhaps. One day, if I am permitted to leave the Homeland :).
I like this scenario. The idea of a server version is very interesting – a take-no-prisoners redesign with multi-threading and multi-processing. As you know, mmj2 does not update .mm files. There are reasons for that. The data structures are complex and self-referential. I would like to design a database containing the .mm file elements! Fun stuff. That might be worth doing, after I figure out how to properly display formulas on the Proof Assistant…And we need to see Ghilbert in action. It will be exceptional, I think, and may obviate the need for "mmj3". --ocat 8-Apr-2006

Use case #4

    Suppose I want to revise an existing proof ...  How do I bring
    the existing proof into the GUI window?
    
    If I select "New" (I don't see any other option for this)
    and specify an existing and proved theorem e.g. a1i, it 
    pulls in the hypothesis and conclusion correctly, but the
    proof is gone.  Perhaps you have to reenter all the steps
    by hand, but somehow I don't think you did this ...
    
    Also, the "default" syl _is_ brought in with its complete
    proof, so I assume there must be a way to do this.
    

Right now the primary way to do this is with the "ProofAsstExportToFile" RunParm command, which puts an existing proof into a file. Here is an example:

    ***********************************************************
    * NOTE: An asterisk or blank in column 1 signifies Comment.
    * The following commands are indented for the Asteroid,
    * so shift following lines LEFT by 4 columns before use!
    ***********************************************************
     *==================================================
     * CommentLine: Example Running ProofAsstGUI
     *==================================================
    MaxStatementPrintCount,9999
    MaxErrorMessages,15000
    MaxInfoMessages,1000
    LoadEndpointStmtNbr,999999999
    LoadEndpointStmtLabel,ZZZZZ.999999999
    LoadFile,c:\metamath\set.mm  
    VerifyProof,*
    Parse,* 
    * VerifyParse,* 
    *PrintSyntaxDetails
    *PrintStatementDetails,dummylink
    RecheckProofAsstUsingProofVerifier,yes
    ProofAsstFontSize,12 
    ProofAsstFormulaLeftCol,20
    ProofAsstFormulaRightCol,100 
    ProofAsstRPNProofLeftCol,5
    ProofAsstRPNProofRightCol,79
    ProofAsstUnifySearchExclude,biigb,xxxid,dummylink 
    ProofAsstMaxUnifyAlternates,10
    ProofAsstDummyVarPrefix,$
    ProofAsstProofFolder,c:\mystuff\mmj2\myproofs\oldfix
    ProofAsstExportToFile,unxpdom2,unxpdom2.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,sucxpdom,sucxpdom.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,uncdadom,uncdadom.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,cdaen,cdaen.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,cda1en,cda1en.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,cdacomen,cdacomen.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,cdaassen,cdaassen.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,xpcdaen,xpcdaen.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,mapcdaen,mapcdaen.mmp,new,unified,NotRandomized,Print
    ProofAsstExportToFile,cdadom1,cdadom1.mmp,new,unified,NotRandomized,Print
    * ProofAsstBatchTest,xpmapenlem3,xpmapenlem3V1.mmp,unified,NotRandomized,Print
    RunProofAsstGUI
    

The output files are using a ".mmp" suffix, but ".txt" is good too. Specify "new" if the file does not exist, or "update" if it does.

Use "File/Open" option in GUI to open .mmp file created by ProofAsstExportToFile RunParm.

The C:\mmj2\test\windows\RunVolumeTest2.bat file distributed with mmj2 shows how to run every proof in set.mm through the Proof Assistant in batch mode (takes a few minutes to run).

Perhaps a GUI option to display an existing proof will be added some day…

--ocat 12-Apr-2006

Use case #5a

Suppose you're working on a proof in the Metamath program's Proof Assistant, then you decide you'd like to switch over to mmj2's PA GUI to finish it.

I wrote a proof-of-concept program, "eimm" (pronounced "aim"), that exports a proof-in-progress (that can have unknown steps) from the Metamath program's Proof Assistant. It can be downloaded here: eimm

To run it, you put the files eimm.exe (or compiled eimm.c on Linux) and eimm.cmd somewhere in your directory path, such as the current directory you are in. Inside the Metamath proof assistant, type "submit eimm.cmd".

For example, suppose we 'prove equid2' and 'delete step 33'. That simulates an incomplete proof in progress. Then we type

  MM-PA> submit eimmexp.cmd
  Taking command lines from file "eimmexp.cmd"...
  ...
  The output file will be called "equid2.mmp".
  MM-PA> [End of command file "eimmexp.cmd".]

which will produce the file "equid2.mmp":

  $( <MM> <PROOF_ASST> THEOREM=equid2  LOC_AFTER=?
  1::a9e                   |- E. y y = x
  2::ax-17                   |- ( x = x -> A. y x = x )
  3::                          |- ( y = x -> ( y = x -> x = x ) )
  4:3:pm2.43i                |- ( y = x -> x = x )
  5:2,4:19.23ai            |- ( E. y y = x -> x = x )
  qed:1,5:ax-mp          |- x = x
  $)

When Open'ed with the mmj2 GUI PA, "StartUnification" will automatically figure out the missing step in this example and produce the completed proof.

The created file "equid2.mmp" will not overwrite previous versions; instead they will be renamed to "equid2.mmp~1", "equid2.mmp~2", etc.

The eimm C program can also be run stand-alone; see "eimm --help". Eventually it might be possible to add a native export command to the metamath program after some experience is gained with eimm. However, it doesn't seem overly inconvenient to run the way it is, for the time being.

--norm 13-Apr-2006

Wow! Nice. (Why the "?" in Ref on step 3? Leave blank?) I could see "Ctrl-E" to create the proof in progress file in the current directory and "Ctrl-I" to import, both using the file naming convention employed by eimm. There will be Norman Megill statues in villages all over the planet one day, and millions of young nerdlings proving Metamath theorems on their $100 laptops :) Nice job saving the planet from the forces of illogic and superstition!!! Way to go! --ocat 13-Apr-2006
(Why the "?" in Ref on step 3? Leave blank?) I don't know. I thought "?" was a trigger for mmj2 to take action in certain cases, but I am confused. mmj2 didn't complain about the "?". Anyway eimm now produces a blank, as shown above, and mmj2 seems to work the same. --norm 13-Apr-2006
I had to look it up (doh!), but "?" in Ref on a Derivation Step is converted to " " automatically (see c:\mmj2\src\mmj.pa.ProofWorksheet.getValidDerivationRefField()). The valid use of "?" is restricted to the Hyp subfield. A missing/blank Formula on a Derivation Step (other than the QED step) triggers derive, and a missing/blank Ref is generated as part of the normal function of Unification.
P.S. Regarding importing a proof worksheet from mmj2 into the Metamath.exe Proof Assistant: I suggest that importation be restricted to mmj2 Proof Worksheets that have been unified without error and that you do not attempt the full input specification processing for mmj2. A Proof Worksheet that is unified without errors may be incomplete in only one situation: when a Derivation Step Hyp field contains a "?" – and Ref is blank, and the Formula is valid; this is considered an "incomplete but valid" Derivation Step. Otherwise, if there are no errors (and no "incomplete but valid" steps), a proof will be generated. So that means that Metamath.exe's PA could import an Incomplete But Valid Proof Worksheet, or a Complete Proof Worksheet, and any other errors encountered would just generate an error message and importation would terminate. The alternative approach would mean replicating mmj2's Unification and its Derive functionality, which would be, I think, excessive in measure for the value obtained; the user could as easily finish using mmj2's PA and then do the import. --ocat 14-Apr-2006

Use case #5b

Suppose you're working on a proof in the mmj2 GUI Proof Assistant, then you wax nostalgic and decide you'd like to switch over to the Metamath program's old-fashioned CLI for a while (see 5a above for going back to the GUI; also note that eimm.cmd was changed to eimmexp.cmd there).

The eimm program has been enhanced with an import option. The new version is here: eimm. Important: The Metamath program must be upgraded to version 0.07.16 or greater in order to use the import feature of eimm.

To run it, you put the files eimm.exe (or compiled eimm.c on Linux) and eimmimp.cmd somewhere in your directory path, such as the current directory you are in. Inside the Metamath proof assistant, type "submit eimmimp.cmd", followed by "submit tmp.cmd".

For example, suppose we have a proof worksheet for equid2, called equid2.mmp. To import this worksheet, we type

  MM> prove equid2
  MM-PA> submit eimmimp.cmd
  MM-PA> submit tmp.cmd

which will delete any existing proof of equid2 and build a new one from the mmj2 worksheet equid2.mmp. (The file tmp.cmd is generated by elimmimp.cmd, but it has to be run separately because Metamath doesn't allow 'submit's inside of a command file.)

Most incomplete proof worksheets should be acceptable, including ones with "incomplete but valid" steps that ocat described above. Orphaned subproofs (which metamath's MM-PA doesn't allow natively) are patched into the main proof by using the "dummylink" theorem, so that their information will not lost; after the proof is complete, MM-PA's 'minimize' command will purge all dummylinks.

--norm 17-Apr-2006

A newer, slightly cleaned up version (0.03) of eimm is available today. --norm 18-Apr-2006.

That's fantastic, Norm! I haven't tried it yet -- I will need a couple more weeks to finish my report on 2020. I plan to be working on this stuff again early in May. --ocat 18-Apr-2006

Some notes:

I chose to make eimm an external program for easier debugging. It talks to metamath.exe via command files, so you see a lot of stuff scroll by on the screen, which is annoying but at least it helps debugging. Once the algorithm is perfected, I could eventually add native 'export' and 'import' commands to metamath.exe, so all the stuff could happen silently. Oh, the bloat inside of metamath.exe…

By the way, the change in Metamath 0.07.16 added relative 'assign' and 'let step' step numbers that extend the concept of the existing 'assign last' that assigns the last unknown step, so that 'assign -1 syl' will assign syl to the penultimate unknown step, 'assign -2 syl' to the antepenultimate, etc. 'help assign' and 'help let' describe these. These made it possible for eimm to skip unknown proof worksheet steps without knowing the step numbers, making eimm much easier to write, but I can also see them as handy for human users such as myself. --norm 19-Apr-2006

Use case #6

I think $d statements should be treated as any other hypothesis. In particular they should appear in the window and the Unification feature should not try to unify if the proviso is not mentionned on the page. – frl 16-Apr-2006

Oh, please. Thou strainest at the gnat but swalloweth the camel :)

mmj2's ProofAssistant goes to eXtreme lengths in support of $d restrictions.

First of all, it employs $d restrictions contained in the input .mm file – but it does not display the existing $d's on the screen because of the problem of combinatorial explosion, which results in bazillions of $d pairs for many theorems, and would fill the screen; the user can simply look at the source file and see the pre-explosion information. (In theory the internal set of distinct variable pairs could be re-converted back to a minimal set of $d statements, for display purposes – and then un-re-converted at proof check time.)

I think the $d statements in a group could simply be memorized when *.mm is read. The problem is that $d statements are a bit puzzling by themselves whereas they are mere hypotheses like the others. If they are not printed it seems to me they still seem a bit more puzzling than before. --frl 16-Apr-2006
One feature that could be added, in theory, perhaps enabled/disabled by a configuration RunParm is to display the existing $d restrictions as a Comment at the top of the Proof Text Area. That would have the benefit of displaying the existing .mm information without altering the processing specification for an input Proof. Alternatively, and I am not in favor of this but would bow to the unanimous and fervent wishes of the mmj2 user population, the existing $d restrictions from the .mm file could be loaded into the Proof Text Area and wholly override the contents of the .mm restrictions – that would add complexity for not much gain over the former option, IMO. --ocat 16-Apr-2006

Second, the mmj2 Proof Assistant allows extra $d's to be added, either to an existing proof or to a new proof not in the input .mm file.

good thing ! I didn't know. --frl 16-Apr-2006

Third, in the event that the computed Ref (Assrt label) results in a $d error, the Unification search process provisionally accepts the Ref, generates an error message and then continues the search through the assertion database (list), looking for a Ref which meets the unification criteria but does not violate $d restrictions. If a better fit is found it is accepted, and if not, an error message listing the alternative Refs (that also have $d errors) is displayed.

The problem is that I sometimes want to unify a step with some previous steps. But I'm at the moment when I cannot do that yet. Thus I leave everything blank in order that the system do not try to unify anything. Alas I have somewhere a theorem that allows the unification modulo some $d statements and the consequence is that the unification process find a proof but not the desired one. --frl 16-Apr-2006
This would be a good time to provide an actual example. However, I believe I have a clue to what you mean. First, if you input a "?" in the Hyp subfield, leave the Ref blank, and input a valid Formula, the program will not attempt to Unify that Derivation Step; it is regarded as Incomplete But Valid. Secondly, if you do specify a Ref label, the program will not override it even if there is another Assrt without $d errors – but a message listing the alternative Assrts that satisfy Unification is displayed. Third, if, as in your example here, you leave Ref blank (and Hyp?), and the program finds an Assrt during Unification but there are $d errors: a) a list of alternative unifying labels is provided in a message if any exist; and b) if there is a unifying label that does not have any $d errors, that label overrides any earlier match that has $d errors! --ocat 16-Apr-2006

Finally, in the event that the mmj2 Proof Assistant's method of generating a unifying set of substitutions that are consistent across the set of proof assertions has a theoretical flaw, a RunParm option is provided to always double-check the Proof Assistant's generated proof using the Metamath Proof Verification algorithm (and I recommend always using this RunParm unless/until the unification algorithm is proven to be mathematically perfect – which I cannot/have not done.)

But in the case I'm speaking the proof is good. Simply it uses $d statements I don't want to use. --frl 16-Apr-2006

So for any given Derivation step the user has two choices: chooose another Ref or add $d restrictions to the proof. And, I think Norm has a utility that will generate $d's ex post facto.

--ocat 16-Apr-2006

Use case #7

frl dons his VR gear and logs on to an OpenCroquet server to view the latest art exhibit:

http://www.wetmachine.com/itf/item/477

Inside he meets his friends ocat and norm who are debating the latest quirks of Metamath. All three decide to jump to the Metamath Metaverse which is running on a Croquet server in a different country, but the jump is instantaneous. They appear at the entrance to the Hall of Logic.

Just inside the Hall of Logic are exhibits that look like abstract art but are actually the latest quantum-modal logic axiom scheme which is represented in 3D systems of equations involving multi-colored shapes, symphonies of music and "smello-vision" :)

They hop on a tram because the Metamath Metaverse is too big to traverse on foot, because of the 1 billion Mathelogicians laboring inside the Truth Mines (not counting the AI's working the knowledge faces on a contract basis.) Thanks to full 3D VR typesetting of Metamath equations, and particularly the VR interface, Math and Logics have become the latest planetary fad -- a fad that has persisted for centuries but shows no signs of dying out. (The ocat avatar is a simulation -- ocat's 9th life was lost during the Biq Quake of 2006, but norm and frl are "real", geezers who have been rejuved many times…for the year is 3006…)

blah-blah.

--ocat 22-Apr-2006

Is it the server I was speaking of in the use case #3? To have my diploma of engineer I had to write an essay about software redocumentation. I read many articles about the subject. One of them suggested to represent software as a three-dimensions town. It seems to me it pretty looked like your site. frl 23-Apr-2006
If you like, yes. The vision is documented in the sci-fi classics, "Signal to Noise" by Eric S. Nylund and "Diaspora" by Greg Egan. The former involves neural implants, the latter autonomous, non-biological intelligences. I like the idea of entering a "scape" and manipulating the objects therein. My other dream has been neglected for many years: during the software development process the programmers are obliged to explain each bit of code as it is written. The explanations are saved as digital audio-visual recordings and are put to two uses: 1) the DVD files are hyperlinked to the shapes and connectors on data-flow and ER diagrams for instant replay upon double-clicking; and 2) when a severe bug is located, we pull out the old recordings of the original programmers and play them back for helpful clues and big laughs! (But for now, I think we should pursue the ASCIIMathML route on a plain 2D view screen. That will be a big step up and can also be plugged into 3D VR with Smellovision at a later date. The key idea is that instead of hardcoding the ASCII symbols in the code we will bootstrap them from the input .mm file, along with the grammar, and then output a custom version of the ASCIIMathML program at runtime! Doesn't that sound great??? It will be challenging but not impossible because the mmj2 ProofAsstGUI program has zero intelligence and doesn't know the difference between a proof and a pot pie, so it will be as easy as falling off a log to replicate its behavior in another guise.) --ocat 23-Apr-2006

Use case #8

The adventurous mmj2 user fires up the mmj2 process using the new RunXhtmlProofAssistant run parm and a webpage interface appears with MathML rendered formulas. He double-clicks on a formula and a clone of the ASCIIMathML program is invoked for editing of the Metamath symbols that are cunningly stored in the ALT Text area. After modifying a formula the user clicks the Unify button and the unification request is sent to a server running on the user's PC – the server calls the mmj2 ProofUnifier.java function to handle the request and receives back the updated Xhtml page (the .mmp text version of the proof text area is also stored on the user's hard drive to maintain compatibility with Metamath's eimm.exe Export/Import utility.)

(Note: a new mmj2 utility program creates a clone of ASCIIMathML based on the contents of an input .mm file.)

Later, the user visits metamath.org/mathml/* to view the MathML-rendered webpages for set.mm.

Update: A quick review indicates that - ASCIIMathML provides the technological approach we need, but not as-is. Output MathML codings will need to be based on Metamath syntax axioms, not just the Unicode character codings desired. Therefore, an input formula will need to be parsed by mmj2 before handoff to the ASCIIMathML-variant's MathML encoder. - A standalone webserver will be needed that can read the HTML page containing the proof and invoke mmj2's Proof Assistant routines. It appears that something like NanoHTTPD would do the job – or, if necessary, Jetty, for the full-blown server.

This enhancement would be the single-user, single-threaded version of the mmj2 Proof Assistant. Ideally, the user would be able to toggle between the Java GUI version and the HTML version of a proof. Regardless of that though, the output proof text file – the .mmp – must be unchanged so as to maintain compatibility with Metamath's new "eimm" feature (export/import of mmj2 proofs).

Note: it may be that an enhancement to the formatting of the mmj2 GUI's formulas should be done at the exact same time – this would continue to display formulas in ASCII as is done today, but would insert line breaks intelligently using the syntax axiom formatting specifications that will be needed for the HTML pages.

Any insights on the nature of the webpage design would be appreciated. It might be that something very similar to the Metamath Proof Explorer webpages could be used (it would be wild to have the program capable of actually reading those pages!) Something more graphical might be considered, but I have no expertise in these matters and unless I get some help from a smart person I'll end up doing it the simplest way possible that gets the job done.

--ocat 25-Apr-2006


I think that three things are needed. In a window, an editor (in the mmj2 style), in another window an access to the database (in the metamath proof explorer style). I think it is also needed to perform regular expression searching in the database. I don't know how Norm or you look for theorems in set.mm but for my own part, I often using M-x string-search in emacs using inputs like ( A. x ph → A. y ph ) or data keywords like 'axiom of choice' and so on. Such a simple device should be included to the whole server structure.

You had suggested that we could give a graphical appearance to the formula using TeX? as a server. In my opinion it is the simplest way. We can imagine that each line is formatted using TeX? and that pictures are combined together then to form an html page. – frl 27-Apr-2006

Hi frl, my primary motivation right at this moment is to typeset/format formulas in mmj2, particularly in Proof Assistant, which is the most interesting and appealing portion of mmj2 (perhaps the only interesting and appealing part of mmj2 from the perspective of most users :)

What the means in practical terms is that I want to focus like a laserbeam on this one thing and make it happen in my lifetime. Then, when this major piece of the puzzle is in place, there may be time to redo everything properly with a multi-threaded, multi-user server architecture with tight integration of all features.

For now I am hoping that you can continue to use emacs to do searching, and metamath.exe to do what it specializes in, and so on.

If we look here, set.mm definitions, we see that just Unicode and basic html coloring, etc. can produce a visual improvement over the ASCII encodings (which, as I understand them, were originally based on LaTex?).

I am thinking that MathML is a good tool for adding typesetting and formatting to a Proof Assistant front-end because MathML is tightly integrated into many web browsers, along with SVG, which may also be of use (somehow.) I am not opposed to using LaTex or Tex or whatever, in theory, but…

I do not believe that a user would find either the raw MathML or Tex encodings useful for editing, not for long, complicated formulas anyway; so my question is, what will produce the best results for viewing Metamath formulas?

Here are a few related items I came up with:

1. A typesetting preference/parameter file should be separate from set.mm (or ql.mm, etc.) so that a user may choose his/her own viewing experience.

2. It may be that visual perceptions of Metamath formulas will be enhanced if nested parentheses (and other bracketing constants) have varying sizes. So, the outermost parentheses would be largest and the innermost would be the smallest. It may be that using bold or colors would also be helpful. Either way, this concept would be controlled by user-settable preference/parameters.

3. The number one problem in typesetting Metamath formulas is intelligent linebreaking. This is especially grievous for the really long formulas(!)

4. The number two problem in typesetting Metamath formulas is ???

--ocat 27-Apr-2006


A source of confusion about the mmj2 Proof Assistant is that a New Proof's scope is always at the global level, regardless of its position as specified by LOC_AFTER on the Proof Worksheet (if LOC_AFTER is not specified the position of the new proof for validation purposes is at the end of the input .mm database.) For example, assume that the input .mm file has these $e statements which serve at "placeholders" for future work:

     ${  $( new scope begin, level is global + 1 $)
      
         xyz.1 $e |- blah blah $.
     
         abc.1 $e |- blahblah blah blah $.
      
     $}
     

Now, if the mmj2 Proof Assistant user starts a new proof for theorem xyz – which does not exist in the input .mm database – a "duplicate label" error message results.

     h1::xyz.1      |- blah-blah
     2:1            |- ergo blah blah
     qed:2          |- daDa!
     

In fact, if the user had not explicitly entered "xyz.1" as the Ref for Step 1, the program would have generated it – and then flagged the error. That is because the default label for hypothesis step Refs is label.1, label.2, label.3, etc.

To eliminate the error simply change the Ref on Step 1 to "xyz.h1" or go back into the .mm file and add a "xyz $p" statement in scope of the "xyz.1 $e" statement.

Note also that LOC_AFTER cannot – does not – insert a statement within a nested scope level in the input .mm statements. Once the scope is closed via a "$}" statement, that scope is closed to the world like matter beyond the event horizon of a black hole.

Another topic of interest is $d's. The Metamath.exe Proof Assistant does not validate distinct variable restrictions, and so may consider a proof valid even though it contains $d errors. However, when such a proof is exported via EIMM.exe to a Proof Worksheet and Unified via the mmj2 Proof Assistant, the user may be shocked when he/she receives 100 error messages about violations of $d restrictions.

Note also that when mmj2 directly imports a Metamath RPN-format proof, if the proof is incomplete or invalid, mmj2 will report an error and, depending on context, produce nothing or a skeletal proof. This is a result of mmj2's very primitive algorithm for converting an RPN format proof to the Proof Worksheet format.

Fortunately for everyone, mmj2 and Metamath.exe can work well as a team. You can run mmj2 in one command window and Metamath.exe in another. The fact that mmj2 does not update Metamath .mm databases is not a problem because Metamath's EIMM.exe can Import a proof that is in mmj2 Proof Worksheet format (even incomplete mmj2 proofs!)

mmj2 and Metamath.exe's "teamwork" is one reason why mmj2 makes no attempt to replicate every feature of Metamath.exe – it would be redundant because metamath.exe works great for these tasks that mmj2 does not attempt.

--ocat Oct-8-2006.