> > When you say to use " MM-PA> minimize * /no *" when should I use that? I > do proofs in mmj2, do I need to load them in metamath.exe somehow? >
It is not mandatory, so do not do it if it's a hassle. Yes, it is done in the metamath program once the proof is finished. As for me, when doing a long proof, I have three windows open: mmj2, a text editor with set.mm, and the metamath program (actually, I also have a web browser since metamath.org/mpeuni can be useful). When I finish the proof in mmj2 (i.e. when after a ctrl+U, the compressed proof appears), I copy-paste the proof in the text editor (together with the generated $d conditions, if any), and in the metamath program, I run: MM> er [for "erase"] MM> r set.mm ["r" for "read"] MM> pr xxx [to open the proof assistant with said theorem] MM-PA> min */no * and if the program indicates that some minimization has been done, then either MM-PA> sh n/c [to show the new proof in compressed format and copy-paste it in the text editor] or MM-PA> sa n/c [to have the metamath program save the new proof internally] MM-PA> exi MM> wr so set.mm/rew [to write the new proof, and rewrap] Of course, if you do several proofs at a time, then some operations need be done for each proof and some only once, and you can guess which ones, with possibly a few trials and errors. For shorter proofs, I do not use mmj2, but only the metamath program. Side note: MM> min */no * is to avoid introducing new dependencies on axioms or definitions. If you only want to avoid dependencies on new axioms, then use MM> min */no ax-*, and if you do not care at all, use MM> min * For all of these commands, look at the metamath help by typing MM> help [command] , especially to learn about the available options. > When following the list of instructions: > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md > <https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fmetamath%2Fset.mm%2Fblob%2Fdevelop%2FCONTRIBUTING.md&sa=D&sntz=1&usg=AFQjCNE1OXgquSEjXLP2JjG7C0sp1frjMw> > I > get this error, not sure what is happening, maybe it is not important to > verify markup > MM> verify markup */file_skip/top_date_skip > ^^^^^^^^^^^^^ > ?Expected DATE_SKIP, FILE_SKIP, or VERBOSE. > MM> > It is happy if I use: MM> verify markup */file_skip/date_skip > This is probably because you use an older version of the metamath program, which did not have the top_date_skip option. If it's not a hassle, then install the newest version of the program. Else, using /date_skip is ok: it will not check date consistencies in "Contributed ...", but if you entered them carefully, this is no problem. > How long is the character line in set.mm, it looks like 79 characters > long, is that right? Seems like an unusual choice for the length. I > understand about high in the tree I think, e.g in ((A = B) -> (C = (D + F)) > the -> is high and the D+F is low. > Yes, 79. I think 80 is standard and metamath's convention is 79 maybe because the 80th is actually a non-printable "line break" character, or something like that? You got it right for the "high" operators. I have to add that I wrote earlier "break after the binary operator" while Norm told me he prefers "break before"; there is no universal convention. A more general philosophical question: is there some thing about how "it > must be deduction form all the way down" in the sense that if I do some > proof A in non-deduction form and then B relies on A then B cannot be in > deduction form. Does this mean it's important to build the whole tree in > deduction form? I have the proofs arearect and areaquad and I guess I would > need to go back and put them in deduction form, which maybe isn't so hard. > I think the above exchanges show that closed and deduction forms are more applicable, while inference forms are less applicable. So go directly for the deduction form (unless the proof is short enough that you can prove the closed form). I think you can state more general rules like the one you wrote. For arearect and areaquad, I would say: wait until you need the deduction form. Benoit -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8287d9fa-143e-4d23-9158-4a896c93c08b%40googlegroups.com.
