Sorry, but maybe my comments were more confusing than helpful for the discussion:
On Sunday, December 13, 2020 at 4:54:33 PM UTC+1 Norman Megill wrote: > It looks like my proposal wouldn't be welcomed, so I will abandon it. As > for keeping a list of minimized theorems, I'm not really in favor of that > either; it would be one more thing to maintain that people will forget or > neglect. > > As for mathboxes, we've never had a rule about people minimizing proofs in > other people's mathboxes, or even finding shorter proofs manually, adding > credit and creating a *OLD for the original (and still keeping everything > in the mathbox). In the past we've done this often, and I always welcomed > it. Indeed, there are well over 100 "(Proof shortened by [someone > else]...)" tags currently in mathboxes. And if we add, say, a new variation > of syl* in main that shortens 50 proofs, we typically apply it to all of > them including ones in mathboxes, without consulting the mathbox owners. > > What would be the reason someone would not want a proof in their mathbox > minimized? I could see a few cases where the proof is still being worked on > and minimization would create a merge conflict, but I think that is rare. > Most people, once they have a proof (a minimum requirement for the PR > checks to pass), go on to the next and only occasionally go back and revise > the proof. If a mathbox user doesn't want a proof to be touched because it > is still being modified, the tag "(Proof modification is discouraged.)" can > be added temporarily until it is finished. > I did not (intend to) say that it should be forbidden to shorten proofs in other's mathboxes, especially by using "minimize-with". Manual shortenings in other's mathboxes should be marked by the *OLD convention, as described, but I don't duplicate theorems and mark one of them as OLD in my own mathbox, although I put the tag "Proof shortened by[myself].." to the comment in such cases. I only was concerned about maintaining additional tags in my mathbox as initially proposed, but since the proposal is abandon, there is no problem anymore. > > In any case, I strongly encourage people to minimize all proofs they > submit, whether in their mathbox or not. An informal rule to minimize > proofs when importing to main is nice, but it can't be enforced and I doubt > it will always be followed. > I fully agree. > On Saturday, December 12, 2020 at 3:42:36 AM UTC-5 Alexander van der > Vekens wrote: > >> 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 shouldn't have happened. 'minimize_with' does not consider other > mathboxes unless '/include_mathboxes' is specified. Is that what you used, > or is this a bug I should investigate? > Yes, I used '/include_mathboxes' intentionally. > As for moving theorems out of mathboxes, we have often done that when a > theorem is needed for another mathbox. Typically we simply move the theorem > to main at an appropriate place (I use 'show trace_back' to help identify > where it should best go) and add an entry to the list at the top of set.mm, > but we don't necessarily notify the mathbox owner. Sometimes a name change > is needed e.g. the "bj-" prefix would be removed or a new name is chosen > that better conforms to our informal conventions; this is also documented > in the same list entry at the top of set.mm. > Usually, I move theorems I use in my mathbox to main set.mm by myself, exactly as described. Benoît's therorems are a little bit special, so I wanted to ask him for the right way/place where to move them. > BTW that fact that someone else's mathbox theorem shortens a proof isn't > necessarily a good reason to move it to main. E.g. there are many trivial > variants of existing propositional calculus theorems in some mathboxes that > may, by coincidence, slightly shorten a proof elsewhere in set.mm, but > that doesn't necessarily mean we should move it out of the mathbox if it > doesn't "pay for itself" in terms of shortening many proofs. > Besides Benoît's therorem(s), there where two theorems of Glauco's mathbox which shortened my proofs. I moved one of them (~ffnd) to main set.mm, because I think it is meaningful/helpul (deduction version of already existing ~ffn). The second one (~fnvinran ) I did not move, because it was exactly the same as an existing theorem (~ ffvelrnda ), having a shorter label only. > 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. > I don't think this happens enough to be concerned with much. The global > minimization will handle it, and in individual cases it can be dealt with > manually. When proposing moving a new basic logic theorem to set.mm, most > people will determine what proofs can be minimized with it as > justification, and then will perform those minimizations. > If we continue to perform global minimizations, there is no problem. My only concern were theorems being marked as "minimized" which are not minimized (anymore). > > 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)? >> > > This isn't practical because for a very large proof, 'minimize_with' may > take days to run. > Yes, I see - large proof would cause problems. In general, large proofs are problematic (difficult to understand/maintain, containing parts which could be useful as theorems by themselves, etc.). In my opinion proofs should usually not contain more than 100 (essential) steps, and maybe not more than 500 steps in extraordinary cases. Parts of large proofs should be extracted as separate theorems (if general enough) or as lemmata. But this is another topic to be discussed separately... > 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/3e8fad6c-89dd-4b79-b5ce-26485c2ca6fbn%40googlegroups.com.
