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/45d2c28b-d7de-46b2-909c-82e0903242c9n%40googlegroups.com.
