I think it's indeed a good idea. I try to do these minimizations systematically with "scripts/min.cmd" when I move theorems to Main which look like utility theorems. So indeed we can recommend it.
As for marking these minimizations, I think this is not necessary. More generally, you mention the "history at the top of set.mm", but the initial goal was not, I think, to have a history (I'm starting another thread for that). Benoît On Sunday, December 5, 2021 at 11:51:47 AM UTC+1 Alexander van der Vekens wrote: > With PR #2345, I moved Glauco's theorem ovexd to the main part, and used > the minimize script to minimize all proofs using ovex or ovexi. There were > 435 proofs which could be shortened, see PR #2348). I can do the same for > fvexd. > > Maybe it would be a good idea that each time such a theorem is moved to > the main part (for other reasons, e.g. if it is used within another > mathbox), the minimize-script should be executed. We can mark this in the > history at the top of set.mm (maybe by adding "(m)" at the beginning or > the end of the notes) - a similar proposal for marking minimized theorems > was made already some time before. > > On Saturday, September 11, 2021 at 9:52:29 PM UTC+2 Norman Megill wrote: > >> On Wednesday, September 8, 2021 at 7:58:31 AM UTC-4 ookami wrote: >> >>> Norm once told me (several years ago!) that the threshold value is 7 >>> theorems: If the introduction of a convenience theorem affects this many or >>> more theorems, its value outperforms the downside of having more theorems.. >> >> >> That was a rough and probably outdated rule of thumb I sometimes used >> decades ago, especially early in set.mm development when I thought that >> 5 to 10 uses was an indication that the convenience theorem might be used >> more widely in the future. But as far as achieving a net shortening of >> set.mm, it depends on how many steps the new theorem saves in each >> proof. If it replaces a large section in the target proofs, as few as 2 or >> 3 uses could pay off. A convenience theorem saving one a1i step like this >> one may require dozens of uses. It is probably reasonable to expect that >> 447 uses would shorten set.mm. >> >> The only accurate way to find out is to do trial minimizations then keep >> or abandon the convenience theorem based whether there is a net size >> reduction. Since much of it can be done with scripts, it's usually not too >> time-consuming to do that, and I've done it quite often myself. >> >> Norm >> > -- 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/7de1b72a-cff2-4b72-9767-09ac314d75e4n%40googlegroups.com.
