Why is ~ 4syl discouraged?
50 views
Skip to first unread message
Alexander van der Vekens
Jun 14, 2019, 10:06:03 AM6/14/19
to Metamath
Why is the theorem ~ 4syl discouraged? The comment says:
The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. Remember to update the Travis "discouraged" file if it gets used.
Actually, there are 191 uses of "4syl" in set.mm! So is there (still) a relevant impact on "minimize" or another reason why it is discouraged?
In my opinion this theorem is quite useful and therefore should be usable again (tag "(New usage is discouraged.)" should be removed).
Benoit
Jun 14, 2019, 10:35:07 AM6/14/19
to Metamath
On Friday, June 14, 2019 at 4:06:03 PM UTC+2, Alexander van der Vekens wrote:
Why is the theorem ~ 4syl discouraged? The comment says:The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. Remember to update the Travis "discouraged" file if it gets used.Actually, there are 191 uses of "4syl" in set.mm! So is there (still) a relevant impact on "minimize" or another reason why it is discouraged?
The reason is still the same: launch a "> minimize 4syl" on a long proof, and it will take a very long time. As Norm told me when I proposed to add 4syl, the "minimize" algorithm has something like exponential time complexity in the number of $e-hypotheses of the theorem to minimize with, and 4syl has four $e-hypotheses...
I agree that it is a useful theorem, but you can see manually if it is worth to launch a "minimize 4syl/override": if your proof already uses 3syl and chains it with a syl, for instance.
Benoit
Thierry Arnoux
Jun 14, 2019, 11:16:34 AM6/14/19
to meta...@googlegroups.com
Discouraged does not mean forbidden.
In this case, it is only there so that “minimize” does not use it.
You are still allowed to use it in your proofs. You will have to regenerate the “discouraged” file (and there will be even more use of 4syl!)
_
Thierry
In this case, it is only there so that “minimize” does not use it.
You are still allowed to use it in your proofs. You will have to regenerate the “discouraged” file (and there will be even more use of 4syl!)
_
Thierry
Jim Kingdon
Jun 14, 2019, 11:18:41 AM6/14/19
to 'Alexander van der Vekens' via Metamath
I use minimize_with * quite routinely (like, every time I prove something, usually). I haven't timed it with and without the discouraged tag on 4syl but that would be my benchmark.
This command is already pretty slow much of the time.
This command is already pretty slow much of the time.
Reply all
Reply to author
Forward
0 new messages