> Now I want to create this set_simplified.mm file. Mario Carneiro suggests to use a ""metamath aware" slicer". Is there such a slicer already created?
Yes, there is already such slicer, you do the following: READ set.mm WRITE SOURCE 2p2e4.mm /EXTRACT 2p2e4 This creates a working .mm file that contains only the 619 theorems needed for 2p2e4, the necessary axioms, and the other technical stuff (latex definitions, variables, constants ecc..). Il Sab 6 Apr 2024, 00:56 Anarcocap-socdem <[email protected]> ha scritto: > Thank you for all the answers, they are quite informative. > > Now I want to create this set_simplified.mm file. Mario Carneiro suggests > to use a ""metamath aware" slicer". Is there such a slicer already created? > I guess it is not as easy as just deleting, from set.mm, the subtheorems > that are not needed for 2p2e4. I guess that quite a few other steps need to > be taken in order to ensure the set_simplified.mm works properly. > > Could somebody give me a hand on this project? > > Thanks! > > On Wednesday, April 3, 2024 at 1:15:41 AM UTC+2 [email protected] wrote: > >> On Tue, Apr 2, 2024 at 6:56 PM Anarcocap-socdem <[email protected]> >> wrote: >> >>> Thank you very much for the answer. >>> >>> Let us see if I understand this: >>> >>> Let us assume I take the 619 different subtheorems used in 2p2e4 (I get >>> this number, 619, by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). These 619 >>> subtheorems can be listed by doing show trace_back 2p2e4. The total number >>> of steps of these 619 subtheorems is 12178 (again, this number is obtained >>> by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). >>> >>> So, is it correct to say the following: >>> >>> - I can create a new file, let us call it set_simplified.mm, which >>> corresponds to taking set.mm, and only keeping the 619 subtheorems used >>> in the proof of 2p2e4. >>> - I can run python3 mmverify.py set_simplified.mm --logfile set.log to >>> check that the proof is correct. mmverify.py has about 690 lines. >>> >>> So, with 12178 steps, plus 690 lines, I can get a full proof of 2p2e4. >>> All these steps could be written in a pdf file (long, but not unreasonably >>> long). >>> >>> Is this correct? Or maybe the way I have defined set_simplified.mm is >>> "too simplified"? >>> >> >> Yes, that is basically correct. Strictly speaking though it is "too >> simplified", because it doesn't account for statement types other than $p / >> $a : >> >> * ${ , $} - obviously we need these for grouping a statement with its >> hypotheses >> * $e - (hypotheses) these are "attached" to each theorem and usually >> directly precede them, although sometimes they can be in the same scope as >> an earlier theorem and shared across multiple theorems >> * $d - (disjoint variable conditions) these are also hypothesis-like in >> their scoping pattern and semantics >> * $v, $f - (variable declarations) for set.mm these are basically >> global, but there is still a well defined notion of "use" of a variable: >> just look for its token in any of the 619 subtheorems. If you see it then >> it must be declared, otherwise it can be dropped. >> * $c - (constant declarations) These are global, and have the same kind >> of "use" as variables: if you see it in the $p ... $= or $a ... $. text >> then it must be declared first. >> >> For all these reasons, you probably want to use a "metamath aware" slicer >> for constructing these *_simplified.mm databases. But this is all very >> straightforward and will not add much on top of the 619 theorems you >> identified. None of these count as "steps" though toward the 12178 step >> count; these are for proof steps (I don't know whether syntax steps are >> included or omitted in the count), and the best you can say about its >> relation to the simplified.mm file is that every step requires at least >> one character so set_simplified.mm should be at least 12178 characters >> and probably more because of theorem statements, delimiters, formatting, >> and comments if you are keeping them. >> >> In general, no this process will not produce long proofs. In fact it's >> about as short as we know how to make them, since this is taking full >> advantage of metamath's abstraction and reuse mechanisms, and the library >> itself is optimized for overall proof size. However you can find some >> inefficiencies in this process because set.mm is trying to prove more >> than just 2+2 = 4 so it will prove things in "unnecessary" generality that >> becomes pure overhead once you cut literally everything else out. So it's >> likely that after extracting such a database you can run minimizers over >> the code and get still more savings. >> >> >>> On Monday, April 1, 2024 at 10:48:46 PM UTC+2 [email protected] wrote: >>> >>>> > 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated >>>> that "A longest path back to an axiom from 2 + 2 = 4 is *184 layers* >>>> deep". However, if I run show trace_back 2p2e4 /count_steps, it is >>>> stated that "The maximum path length is 84". Is there a typo somewhere? (84 >>>> != 184). >>>> >>>> Note that that statistic is one of those that will go out of date >>>> quickly due to changes in the library structure. So you should not expect >>>> it to be exact, unless we have an automated mechanism for keeping it up to >>>> date, and we don't currently. However, there is one major change between >>>> when that text was written and now which significantly decreased most of >>>> the numbers quoted, which is the isolation of the real numbers from their >>>> construction. 2+2 = 4 is a theorem very close to the axioms of real >>>> numbers, so it was reduced from something depending on the entire stack of >>>> set theory and the construction, down to just a few direct axiom >>>> applications (plus still a bunch of set theory because of the use of df-ov >>>> "operation value" for expressing the + function, defined in the set theory >>>> section). >>>> >>>> In order to get something closer to the "true" original numbers, you >>>> should replace "ax-mulcom $a ... $." with ax-mulcom $p ... $= <apply >>>> axmulcom> $. and similarly for all the other axioms in the same section. >>>> This will allow metamath-exe to see that uses of these axioms actually >>>> depend on a big stack of other lemmas when calculating statistics like max >>>> depth and full-expansion theorem counts. >>>> >>>> > 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a >>>> total of 619 different subtheorems are used. The statement and subtheorems >>>> have a total of 12178 actual steps (...) The proof would have 5887862241803 >>>> =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is >>>> the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess >>>> that 12178 steps refers to the case in which we take the axioms of the >>>> complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms >>>> of the complex numbers, starting from ZFC. But I am not 100% sure, and I >>>> would like to have confirmation of that. >>>> >>>> No, this is not about that. Metamath theorems are able to refer to >>>> previous theorems multiple times, in multiple concrete instantiations. That >>>> is, a theorem is really a "theorem schema" over the assignments to the wff >>>> and class variables. If you wanted to perform the same proof in pure first >>>> order logic, you would have to redo the proof for every choice of those wff >>>> variables. So the statistic here (also calculated by metamath-exe) is >>>> working out an approximation to the (exponential) speedup this >>>> accomplishes, by seeing how many steps would have been taken if you had to >>>> replay each use of each theorem. Effectively, you can think of this as >>>> treating every metamath theorem as a macro which expands to a proof >>>> containing more macro references, and if we macro-expand everything all >>>> that remains are direct references to the axioms. It's easy to get >>>> exponential growth in this process, since theorem 2 can use theorem 1 >>>> twice, theorem 3 uses theorem 2 twice and so on. Of course the metamath >>>> library is not quite so pathological as that, but the nature of the process >>>> is still exponential, where the base is related to the density of >>>> converging paths in the DAG of theorem references. >>>> >>>> > 3. Is there some way to print/export to file the 12178 steps, and >>>> even the 5.9 x 10^12 steps, all at once? I ask this since running show >>>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the >>>> subtheorems, not the steps themselves. And I have been unable to find a >>>> command that gives the full number of steps, all at the same time. >>>> >>>> As far as I know, no. Both of these numbers are calculated by the >>>> metamath-exe tool, using the command "SHOW TRACE_BACK 2p2e4 /COUNT_STEPS". >>>> Internally, it only creates and manipulates the numbers, it doesn't >>>> actually perform the expansion (which would take exponentially long just to >>>> output). For the former number (12178 steps), an approximation to this is >>>> to just "show proof *" which will print all proofs, or look at the entire >>>> metamath web site on disk, which contains every step of every theorem. The >>>> 12178 steps are a subset of those, and you can get metamath-exe to print >>>> out all of the relevant theorems using "show trace_back 2p2e4" alone. >>>> >>>> That said, it is certainly possible to calculate the actual 5.9 x 10^12 >>>> steps if you are interested in such a programming project. But be aware >>>> that the steps can also get pretty large in the process (I think also >>>> exponential in general). Although I'm sure your terabyte drive has better >>>> things to do... >>>> >>>> Mario Carneiro >>>> >>>> On Mon, Apr 1, 2024 at 9:44 AM Anarcocap-socdem < >>>> [email protected]> wrote: >>>> >>>>> Hello, I am trying to understand 2p2e4, as an excuse to understand >>>>> metamath better. >>>>> >>>>> I have a few questions: >>>>> >>>>> 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated >>>>> that "A longest path back to an axiom from 2 + 2 = 4 is *184 layers* >>>>> deep". However, if I run show trace_back 2p2e4 /count_steps, it is >>>>> stated that "The maximum path length is 84". Is there a typo somewhere? >>>>> (84 >>>>> != 184). >>>>> 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a >>>>> total of 619 different subtheorems are used. The statement and >>>>> subtheorems >>>>> have a total of 12178 actual steps (...) The proof would have >>>>> 5887862241803 >>>>> =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is >>>>> the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess >>>>> that 12178 steps refers to the case in which we take the axioms of the >>>>> complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms >>>>> of the complex numbers, starting from ZFC. But I am not 100% sure, and I >>>>> would like to have confirmation of that. >>>>> 3. Is there some way to print/export to file the 12178 steps, and even >>>>> the 5.9 x 10^12 steps, all at once? I ask this since running show >>>>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the >>>>> subtheorems, not the steps themselves. And I have been unable to find a >>>>> command that gives the full number of steps, all at the same time. >>>>> >>>>> Thank you for your work on this great project. >>>>> >>>>> -- >>>>> 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/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com >>>>> <https://groups.google.com/d/msgid/metamath/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>> -- >>> 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/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > 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/6300ff6f-9d28-468a-9716-589787a2e2e4n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/6300ff6f-9d28-468a-9716-589787a2e2e4n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAPKSAW6%2BbQzh4SajAs0AYAKpoxX50W_hA4nAvzFLA30pVyV1zA%40mail.gmail.com.
