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
Comments about the new "Derive" Feature should be posted here: mmj2ProofAssistantDeriveFeature
Thanks! --ocat
Welcome!
Here is a tutorial: mmj2ProofAssistantTutorial
And this has more helpful information, including a "quick howto" and a detailed reference for the Proof Assistant GUI!
http://aux.planetmath.org/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 about 10 seconds by not loading 6000+ theorems, only the first 100.
Try it! I think the new mmj2 GUI is lots more fun than the metamath.exe Proof Assistant!
1. The Edit/Cut and Edit/Paste options work well :)
2. I like the way it allows me to focus on the properties of the formulas instead of theorem labels. Last night I was working on re-proving the first 100 theorems and I was just ripping them: boom, boom, boom. Very nice! Labels may change but the properties of the formulas are forever.
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 for the tidy-up release of 01-Mar-2006 (if not sooner :)
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
Once you get yourself set up there should be no need to mess around with this stuff. I hope it works out well for you.
5. In the file C:\mmj2\test\windows\expandSetMM.bat, you have
cd c:\metamath\metamath
However, based on the previous instructions at http://planetmath.cc.vt.edu/~mmj2/mmj2.html ("unzipping it to the "C" drive"), the correct command should be
cd c:\metamath
(I realize you also say "make any directory changes", but it would be good if the default was correct.) – norm 12-Mar-2006
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.
3. I want it to renumber the proof steps after I am done (even though I am proposing that to myself, my reaction to me is "Give me a freaking break!")
4. I want it to pop up an informational message whenever a proof is completed and the new proof's RPN is shorter than the RPN proof in the Metamath .mm file that was input. It would be a shame if someone in Timbuktu created an amazing new proof and did not tell anyone because s/he did not even notice that it was an improvement – someone might assume that the total obviousness of the new proof was self-evident to all! :The program should provide a comparison count of the number of logical steps and RPN steps.
5. Have you asked http://www.nfb.org/ for suggestions to make the mmj2 Proof Assistant GUI easier to use? :No response. Obviously, making sure error-cursor positioning works reliably is a biggie. And perhaps adding sound feedback for a) successful proof vs. b) parse error; vs. c) other error. Probably some other stuff
6. Make the start-up Proof Worksheet area, presently "syl", a RunParm? option. This would allow "stoppedhere.txt" to be used to pick up where left off, as well as customization.
7. Create pop-up formula building screen that loads a formula into the clipboard/cut-paste buffer. Keep the window open until closed. Allow expressions to be assigned to variables and plugged into selected formulas.
8. Is search/replace feasible?
9. For training exercises and review, it would be nice to have a "File/NewRandom?" menu option that randomly selects a theorem for proving.
10. Another training exercise feature would be to randomly generate theorems for proving. I am not sure how hard it would be to code something meaningful, but it would be educational. Seeing new formulas should help reinforce old lessons. (It is possible to load more than one Metamath file using multiple mmj2 LoadFile? RunParms?. No reason why a teacher cannot create supplementary files for homework.
11. Add code to the very beginning of BatchMMJ?2 to verify that the Java runtime environment is compatible with the compiled code. This would be useful if/when compiled code is distributed.
12. Consider building a distribution CD/zip containing everything needed to just run mmj2 Proof Assistant, including a sample of the first 1000 set.mm theorems AND a user manual. It should be set up to run from the unzipped directory, as-is. Try the "jar" technique for simplicity. Make the directory names completely separate from the existing mmj2 directory structure. Try to find some educational material to either include or link to, as well as the obligatory linkbacks and license stuff for Metamath, mmj2, etc.
13. It seems as if elementary boolean logic could be taught to high school sophomores as a supplement to the standard (American) Euclidean Geometry course. What needs to happen to make the mmj2 Proof Assistant approachable for beginners? Video training material on DVD's with instructors that look like Lara Croft? Things to check out:
14. (from Raph): "You should be able to sit on qed, enter a label, and have it spit out the terms needed."
mmj2ProofAssistantDeriveFeature – Proposed 'Derive' Feature Specs
1. The cursor positioning code is mentally challenged.
2. The default file type is ".txt" for mmj2 proof files. I expected it to be ".mmp". (Should I mmj2 have a RunParm? to define the user's preferred file type or just stick with .txt as the default and ".mmp" as the accepted alternative?)
3. I should have gotten a warning message from mmj.verify.Grammar when using the old set.mm about the overloading of "=" by syntax axioms weq and wceq. Grammar went ahead and built the Grammar Rules but 10% of set.mm theorems could not be unified in Proof Assistant without modifying weq to be a "syntax theorem". Likewise for wel/wcel and wsb/wsbc.
4. It is impossible to prove the "dummylink" theorem.
Hello "Mr Big",
I hear you.
I don't know if you're using Windows Explorer to look at the file directory structure and contents of c:\mmj2. There is a lot of stuff mentioned in c:\mmj2\doc. Specifically answering your questions are:
c:\mmj2\doc\ProofAssistantGUIQuickHOWTO.html
c:\mmj2\doc\ProofAssistantGUIDetailedInfo.html
Those are included in-toto in the "mmj2.html" web page available at:
http://aux.planetmath.org/mmj2/
I also answer your specific questions now:
What are the syntax requirements of proof step labels?
--> 1, 2, ... n except for final step number which
must be 'qed'. can be 10, 20, ...
Must they be in numerical order?
--> No, but a hypothesis reference must be to a
previous step in the proof (like 2:1 |- blabblah
where "2:1" means step 2 has previous step 1 as a
hypothesis for formula "|- blahblah".
Must hypothesis step labels start with h?
--> yes. file/new will build the skeleton for you.
Do you type in the actual proof steps?
--> sometimes. also cut and paste the step being
derived from. cut and pasted the "com*" proofs
and it was magical the way PA finished the
proofs!
At what point do you attempt to unify - as you are doing the proof, or only at the end?
--> you can unify step by step or wait until
the end. for steps that are un-finished, like
the qed step, you can put hypothesis = "?"
signifying "I don't know yet". that allows you
to work backwards, too!
An example of what you actually do - maybe down to keystrokes and mouse clicks, maybe even including how you recover from dumb typos you make - as you "rip" through a proof would help people overcome that big initial learning hurdle.
--> I hear you! Try out the various Menu items
including the Help screen (which is probably where
I would put a tutorial?)
Hi ocat,
Congratulations on your Proof Assistant GUI!
In my ramblings that follow, it is easy for me throw out ideas, since I'm not doing the hard work. :) Nonetheless some of them might be useful to contemplate for the long term, or at least serve to inspire further discussion.
1. Even though one of its purposes is to avoid the need for memorizing labels - and that is good - I believe labels can still be useful. Most people probably become familiar with at least a few very common ones, and when you do know the label, it is more efficient to type it than to type a string of special ASCII characters. Yes, there is copy-and-paste, but at some point you have to type the starting symbol string. Anyway, the idea would be to let you bring in a known theorem as a template for a proof step. It would be like the reverse of your Unify - instead of typing in the symbols and having the PA find the theorem, you would type in the theorem label after the "::" and it would fill the symbols (or a template when they can't be determined - see #5 below).
2. There are theorems like syl that are used all the time. Perhaps the most-used 20 or 100 theorems could be presented in a drop-down list to choose from, kind of like the drop-down list of axioms in Metamath Solitaire.
3. Obviously, I have become expert at using the CLI PA. While I probably have memorized many more labels than anyone else, I really have only the most common ones - maybe a few hundred? - on the "tip of my tongue" as it were, out of the 6000+. I am generally aware, at least vaguely, of general categories of theorems available, but have a poor memory for their exact forms, variable names, etc., and rarely remember labels of the lesser used ones. The most useful feature in the CLI, for me, is the 'search' command with its wildcards. Next to the actual 'assign' statement (and possibly 'delete'/'initialize'/'unify' to fix mistakes when I haven't had my coffee), 'search' is probably the most frequent command I use.
4. I think the biggest drawback of the current CLI is that it forces you to work backwards, so you pretty much have to have to proof worked out on paper or in your head before you even start. In principle the power of GUI could let you work on different, independent pieces of the proof, eventually bringing them together and perhaps discarding some that are failed experiments.
5. An ideal GUI might somehow combine the backwards proving method of metamath's CLI with the forward method of the Metamath Solitaire applet, giving us the best of both worlds. Along those lines, for the forward method especially there will have to be temporary variables, analogous the unknown $1, $2, etc. in the CLI PA. I could see the user highlighting one of the variables and pasting an expression on top of it, then watch as the same expression ripples into all occurrences of that variable throughout the proof.
6. Just as in the CLI PA, when a label is assigned to an expression with the temporary variables mentioned in #5, it would be checked on the fly to see if it could be unified, and if so, then the temporary variables would be replaced according to the unification just as in the present CLI PA.
7. If I'm working on two disconnected pieces of the proof, sometimes I know that this subexpression of wff A is going to match that subexpression of wff B when pieces are finally put together. But it would be nice to know what it would look like before we actually connect them. I can envision the following advanced feature: you highlight subexpression 1, ctrl-highlight subexpression 2 (ctrl so the 1st highlight won't go away), then Unify. Variable replacements to make them match would take place, propagating through the rest of the proof as required.
8. (A possibly hard example for the present PA GUI?) I am curious: how would you prove biigb (if your goal is to obtain that particular proof, not the normal one)? Can it be done, practically? In Metamath Solitaire, it would be 17 clicks on the drop-down axiom list, and the incredibly long steps would automatically be created by the unification. (In effect, these clicks are specifying labels to assign.) This is one case where I'd prefer to type labels instead of entering symbol strings.
9. (Another possibly hard example for the present PA GUI?) Another case like this was the proof of grothprim. The statement of the theorem was actually clipped from a partial proof - I didn't type it in. What I did was temporarily specify "$p |- ( [ax-groth] <- > ph )" where "ph" served no purpose other than giving us a legal wff. Then (proving backwards) I broke this up with bitr over and over, each time applying more definitions into [ax-groth], until they were all eliminated. I ended up with the unknown step "|- ( [longexpression] <- > ph )" and clipped out [longexpression] from 'show proof' to create the final theorem statement. So in a sense I was tricking the "backwards prover" of the CLI to act like the "forwards prover" of MM Solitaire.
--norm 3-Feb-2006
An "ideal" Proof Assistant GUI might eventually have, in one form or another, the features currently available in the metamath program's PA CLI ("MM-PA"). Some of these might be improved by implementing a graphical equivalent. For example, the current PA GUI ("mmj2") implements an more flexible version of the MM-PA's "let step n =" assignment via pasting to a cursor position. Other features might exist in dual form, say by analogy with a text editor that does the normal GUI stuff in the typing area but also has a place at the bottom to enter a command line.
In its present form, I will most likely use mmj2 in some combination with MM-PA, using one or the other depending on which is the most efficient for the task at hand.
As time goes on, I can imagine that more MM-PA features will slowly be integrated into mmj2, but in the meantime it would be very useful if we could seamlessly go back and forth between them. Right now it is awkward, requiring an edit to or rewrite of the source file, and exiting/reentering the metamath program (or 'erase'/'read').
Here is what I envision, which could hopefully give us, as an interim measure, the best of the two currently existing approaches without a whole lot of pain. On the computer screen, we would have two windows open, one for mmj2 and the other for MM-PA. We would define an import/export format for partially completed proofs understood by each, that allows them to communicate while they are in their respective sessions. Each would have a command to refresh its partial proof with the one exported by the other, without having to exit either proof session. This way we could go back and forth to work on the proof with different tools.
MM-PA could be modified to read in a file with a standard RPN metamath proof, with the "?" convention for unknown steps. Of course, I would be the one making this modification. A new 'import' command would erase the existing proof in progress, read in the proof exported from mmj2, and unify.
I don't know what the best (easiest) format is for mmj2 to understand for partial proofs. Is it just the RPN partial proof with "?"s? Or are the actual step contents needed, since they may contain more information about the unknown steps? Metamath's 'show proof' can output proofs in various formats with varying levels of detail, and ocat will have to tell me which would be best to adapt to an export format that mmj2 could easily read.
One of the problems (there are always problems!) would be that certain intermediate stages of partial proofs in mmj2 are not representable in MM-PA, and possibly vice-versa. For example, mmj2 can develop proofs in independent pieces, whereas MM-PA requires a partial proof built backwards in a single tree. I guess the only solution to this, short of a major rewrite of MM-PA, is either not allow the export when the proof is in one of the incompatible stages, or allow it with loss of information by overriding a warning.
dummylink.1 $e |- ph $. $( Transparent pass-thru input. $) dummylink.2 $e |- ps $. $( "Don't care" input. $) dummylink $p |- ph $= dummylink.2 $.
What do you think?
norm 6-Feb-2006
Congratulations! I see that you have made dummylink the first theorem in the set.mm database? I am adding it to the mmj2 set.mm "ProofAsstUnifySearchExclude?" RunParm? to exclude it from the automatic matching process during Unification (the excluded labels can still be entered manually). Here is what I have now in the distributed file C:\mmj2\data\runparm\windows\RunParmFileRunPAGUI?.txt
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
Let me know if there are others that you know should be excluded. --ocat 8-Feb-2006
I am planning an update to mmj2 for 1-May-2006 to incorporate the most important and doable enhancements. It will definitely have the label-input-instead-of-formula feature, and the play-Star-Spangled-Banner-when-proof-complete option.
As far as mmj2's Proof Assistant goes, the easiest solution is to have metamath.exe's PA be capable of reading the mmj2 "Proof Worksheet" AKA "Proof Text area" format. Then the mmj2 PA's user simply hits Save or File/Open to exchange data with MM PA. Nice!
The reason mmj2 PA abandons attempts to process RPN proofs containing '?'s is that it views proofs as trees and a missing RPN step can destroy structure (The attempt is made only in the testing-use "ProofAsstExportToFile?" RunParm? command that generates a Proof Worksheet from the Metamath proof and writes it to a file.)
P.S. In theory the mmj2 PA could kick out a specially formatted file (or copy to clipboard), but it would be best if the MM PA could just read the Proof Worksheet text. The MM PA need not go through the entire rigamarole that mmj2 does with the 101 different possible errors. Just kick it back if it isn't acceptable for import. Being able to read the Proof Worksheet text has other benefits, like being able to export/import with other proof systems, and keeping things simple for your users. I really don't know what you would want from a special export anyway. There are two parts needed for building the proof tree for each step: the unification variable substitution parse trees, and the proof step's hypotheses' proof trees; a step can be unified but if its hypotheses don't have proof trees themselves then it cannot have a proof tree. So…essentially that means that mmj2 has a separate, possibly incomplete proof tree for each proof step that passes the unification process. Tricky to convert that mess without loss in both directions using RPN arrays, which is why I think having MM PA read the native Proof Worksheet format is ideal (bit of work on your end though :) ocat 6-Feb-06
That sounds like a good approach. Is the Proof Worksheet format stable enough at this point to be considered a standard? norm 7-Feb-06
Yes, with provisos:
1) The new label-instead-of-theorem feature you requested/suggested represents a change to the validation -- i.e. the user can input "2:1:xyz" with no following formula.
2) The mmj2 PA allows $d statements to be input which are treated as additions to the theorem in the database. But it does not allow the input of new "dummy" variable/variable hypothesis definitions. And none of the statements are terminated with "$.", the Metamath standard.
Assuming that these design choices are not questioned, then there are no other changes ahead to the text format of the "Proof Worksheet", which is a very minimalistic format.
P.S. #1 need not affect the MM PA import. When the user in mmj2 PA presses Ctrl-U, if there are no errors, the formula corresponding to "2:1:xyz" will be generated. In fact, a solid approach to the MM PA import might be to stipulate that an acceptable imported Proof Text area is what is displayed on the mmj2 PA screen after Ctrl-U (Unification). That would mean that, as one example, the order of hypotheses on each proof step matches the the sequence of hypotheses of the Assertion specified by the step's Ref label – which is the case after successful Unification (figuring out the sequence in mmj2 is a tricky bit of work.) The only "error" condition you would need to worry about would be "?" in the Hyp fields, which signifies that the step is not ready for Unification. And there could be the situation, as you covered, where there are multiple, unconnected sections of proof steps.
--ocat 7-Feb-2006
I tried it out and was generally fairly impressed. Cool!
I definitely agree with the sentiments above that it should be possible to make progress either by unification against term strings or by supplying a label. One thing I've thought about is tab completion for labels that match. If you're not sure which syl<n> to use, just type "syl" and hit tab.
Also, I think it's very useful to be able to work both backwards and forwards. You should be able to sit on qed, enter a label, and have it spit out the terms needed.
I looked at the code a bit, especially the Earley parser (because I need something similar to implement Ghilbert syntax plans. I think the choice of the Earley parser is a sound one, but I'm a little less thrilled with the code. For one, in the face of ambiguity, I don't consider it acceptable to enumerate all valid parses - that leads to exponential blowup. For what I want to do, anyway, it's important to choose one ambiguous parse using precedence values. To this end, I've started hacking my own Earley parser in Python. I am curious, though, whether you've looked at any of the techniques to improve the performance of Earley parsing, such as Nigel Horspool's.
--raph 18-Feb-2006
Thanks, Raph!
I will be providing the capability (god willing) to supply a label instead of a formula. This enhancement is contrary to the intention of the GUI, but the customer Rules :)
However, syl* matching is beyond where I am willing to go, at this time. It should not be needed; asis, if the user can provide the formulas the program will figure out the correct label.
I also note, fyi, that working forwards or backwards is already a feature. For step 'n', enter "?" in the Hyp sub-field of Step:Hyp:Ref, and the program allows Step 'n' to be used in subsequent steps as an hypothesis without requiring it to be completed. I may need to default the 'qed' step Hyp to "?" to make this more obvious (but did not because I wanted the error message to kick out in case the user wasn't sure what to do next – now I am not so sure that is best.)
Re, Earley Parser. 1) The easy part is parsing. Putting the parse tree together from the Itemsets is the challenge.
2) mmj2/Grammar provides two modes, via RunParm?, with the "basic" and "extended" ambiguity checking. For parsing this means that if "basic" is chosen, the first parse is taken, and if "extended" is chosen, then up to 'n' parses are generated, but still the first parse is taken. In practice, 'n' = 2 for "extended" (a hardcoded constant), but it is possible to generate an arbitrary number of parse trees for academic purposes (with a recompile.) The default is "basic" and 'n' = 1.
3) I did take a quick look at various options for enhancing the algorithm but ended up doing my own optimization of Grune's algorithm:
http://www.cs.vu.nl/%7Edick/PTAPG.html
If you look at the code for completed items, the "bring forward" is done only once for each type, and that is a significant bit right there. I added a couple of other enhancements as well, including the lookahead by 1 and sorting the Earley Rules by database sequence (See mmj.lang.Cnst.java for "earley".)
The rotten part of my Earley Parser is the tree building after the parse. I had to do that part twice. The first attempt used recursive calls and was incomprehensible immediately after it was written. The replacement is still really hard to understand.
4) Your suggestion, "You should be able to sit on qed, enter a label, and have it spit out the terms needed." sounds great. I added it to the suggestion list above. I'll have to think about it in terms of doability and how much it is really needed (there is apparently no substitute for mathematical skill – Norm can work miracles with a pencil and the fastest supercomputer in the galaxy still won't make me smart :)
--ocat 18-Feb-2006
Hi ocat, my pleasure to use metamath is renewed by the new features brought by mmj2. Well Here are the points that could be improved according to me.
#1 The save/open subsystem has to be improve: one can very easily delete a proof when closing a proof and opening a new one.
#2 When the proof is finished, I transfer it to the mm database and it's a pain because the two formats are very different.
ProofAsstRPNProofLeftCol,5
ProofAsstRPNProofRightCol,79
So after the proof is complete and the $= line is generated in the mmj2 proof, simply copy the RPN statement labels into the .mm file – which has a free format and simply requires that the RPN labels follow the "$=" and precede "$." in the Metamath $p statement.
Another (preferable) solution is to wait and see if Norm completes his metamath.exe Import facility. That will provide the capability to jump back and forth between the Metamath.exe and mmj2 Proof Assistants. Since Metamath.exe has many advanced features, such as UPDATING a .mm file, the new Import feature is something I am very excited about. (mmj2 is not presently in the business of updating .mm files – though the technical requirements are not exceedingly difficult, the staff at mmj2 demanded a pay raise when management broached the topic and now we're trying to decide whether to outsource the programming staff to India…)
P.S. I am planning to implement the Renumber feature you requested. I hope that renumbering by 1's is sufficient (1, 2, 3, … qed)?
--ocat
– frl 27-Feb-2006