would fvexd be a bad idea?

[Glauco]

A theorem like

 |- ( ph -> ( F ` A ) e. _V )

would clearly be "redundant".

But it would save a LOT of a1i (and shorten many proofs, I guess)

And the autocomplete feature of mmj2 would take advantage of it (as far as I can tell, the current version doesn't add an a1i automagically).

Comments?

[Jim Kingdon]

As with things like 1cnd I think it is a matter of whether the convenience theorem would get used enough times to justify having it.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/756da4ff-316a-4861-bbaf-b100e108cdc8n%40googlegroups.com.

[ookami]

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..

Wolf Lammen

[Alexander van der Vekens]

Using Benoît's Minimize-Script scripts/min.cmd, I checked all 2743 proofs using fvex, and 447 of them can be minimized (by 2-10 bytes) by using fvexd. Therefore, Glauco's assumption that many proofs become shorter is true.

[Benoit]

scripts/min.cmd is due to Norm.  My modifications were very minor.  Indeed it is very useful.

Benoît

[Norman Megill]

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

[Alexander van der Vekens]

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.

[Benoit]

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

[Alexander van der Vekens]

With PR #2354, 451 proofs coud have been shortened using fvexd (set.mm became about 5 kB smaller)...