I am currently workin within my Mathbox, and I found a minimization of one of my poofs (using minimize_with) using a theorem of Benoît's Mathbox (@Benoît: it's bj-eleq2w - can I move it (together with bj-eleq1w?) to main set.mm? Where is the right place for them?).
This example shows that there is a flaw in the approaches we discussed so far: what about minimization if a new theorem is added to main set.mm which would allow for a minimization of following theorems which were minimized before? The global run of "minimize_with" on the entire set.mm would detect and process such cases, but neither the marking proposed by Norm nor the list proposed by @savask nor my proposal would handle such cases. Maybe the program/script of my proposal could be extended to check for proofs which could be minimized by the new/modified theorems (and gives a hint to the contributor which proofs to minimize before the pull request can be accepted)? On Saturday, December 12, 2020 at 7:51:24 AM UTC+1 Alexander van der Vekens wrote: > I fully agree with Norm's demand that all theorems in set.mm (at least in > the main body of set.mm!) should be minimized, but I am of the same > opinion as @savask that tagging minimized/not minimized theorems as > proposed by Norm is not practicable and would make set.mm more clumsy. > > At least I would not be happy if I have to care for these tags in my > Mathbox (or allowing others to perform minimizations in my Mathbox, > although I always would welcome hints that there is a way to minimize a > proof in my Mathbox). I think we should restrict our attention/efforts to > main set.mm. > > For my part, I always minimize new/modified theorems (unless I do not > forget it unintentionally!) before I push them to the Git repository. Hints > as suggested by @savask would be a (small) step to achieve more quality > (with respect to minimization) and should be provided if this is possible > with little effort. Regarding a list to be maintained I am a little bit > sceptical if this was practical. > > What about checking for not minimized proofs while checking a Pull > Request? Of course a program/script has to be written for it. Such a > programm/script could look for all new/modified theorems (in main set.mm, > not being tagged with "(Proof modification is discouraged.)") and run > "minimize_with" for them. If the result is always "No shorter proof was > found", then the check is passed, otherwise the pull request should be > rejected. By this, each contributor is responsible for providing minimized > proofs only. > > Alexander > On Saturday, December 12, 2020 at 7:04:09 AM UTC+1 savask wrote: > >> I agree that minimization markers "add no value", so in my opinion they >> should be kept out of set.mm altogether. Maybe we can create a file >> "minimized_theorems" (something like "discouraged") which will be a list >> of, well, minimized theorems :-) Contributors won't have to set any tags or >> modify that file, but if someone decides to minimize a theorem, they will >> check that file and in case if the theorem wasn't processed earlier they >> will minimize it and add the name to the file. That way we will avoid >> additional bureaucratic burden of contributing to set.mm. >> >> The "minimize" command of metamath.exe can be made to skip minimization >> of theorems mentioned in the "minimized_theorems" file, so minimization >> volunteers will be able to minimize whole ranges of theorems in bulk, >> without doing double work. >> >> And speaking of making users minimize their theorems, I think most people >> need only a small reminder. Right now, after you complete a proof in >> metamath.exe, the program will remind you to do "SAVE NEW_PROOF" and >> "VERIFY PROOF". Perhaps a suggestion to minimize the proof can be added >> there as well? Same goes for mmj2, after a proof is finished and mmj2 >> compiles it to the compressed proof format, one can add an automatic >> comment suggesting the user to run "minimize" in metamath.exe. >> > -- 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/a913bf7e-4c16-4e1f-b295-7eb1739fd29bn%40googlegroups.com.
