'minimize_with' command in metamath.exe
66 views
Skip to first unread message
Norman Megill
Sep 21, 2019, 10:20:35 PM9/21/19
to Metamath
1. Changes to 'minimize_with'
As noted on the 10-Aug-2019 news item on the Most Recent Proofs page
http://us2.metamath.org/mpeuni/mmrecent.html
the behavior of the 'minimize' command has been changed.
Before the change, 'minimize *' with no qualifiers could add dependencies on new axioms if it made the proof shorter. This is was dangerous in some cases, for example if in the original proof we went out of our way to avoid the Axiom of Choice. Earlier, we recommended the use of 'minimize * / no_new_axioms_from ax-*' for everyday use to prevent this, but sometimes people would forget and use the more dangerous 'minimize *'.
For maximum safety, the new philosophy is to prevent introducing dependence on any new axioms (actually any new $a statement) unless specifically allowed by qualifiers. A new qualifier, '/allow_new_axioms', is now needed to allow dependence on any additional $a's. Usually we don't care about dependence on new definitions or syntax, and to allow all $a's except axioms proper, the new recommendation is to use
MM-PA> minimize_with * / allow_new_axioms * / no_new_axioms_from ax-*
for everyday use, which can be abbreviated
MM-PA> min */a */n ax-*
(although in scripts, it may be best to use the full command names for robustness against future ambiguity). In many cases, this command and the unqualified
MM-PA> min *
will produce the same results, so don't worry about it too much if you forget the qualifiers, but occasionally the qualified command might result in a shorter proof through the use of new definitional and syntax $a's. The main thing, though, is that an unqualified 'min *' is always safe to use now, unlike before.
When you don't care at all about possible dependence on additional axioms, you can use
MM-PA> min */a *
which in some cases might produce a shorter proof with more axiom dependencies. This obviously should not used for bulk minimization but only for specific proofs where you know additional axiom dependencies are not an issue.
'help miinimize' describes the new qualifier behavior (although there are some wording issues pointed out by Benoit that I will be improving). The Metamath book unfortunately omitted a description of the 'undo' and 'redo' commands ('help undo'), so be aware of them. In particular, 'undo' will revert a 'minimize' command and 'redo' will restore it, which is occasionally useful for comparing before and after results with 'show new_proof /compressed', or for experimenting with different qualifiers.
2. Policies for proof minimization
In the past we have occasionally run the entire set.mm through minimization, and that will probably happen again at some point in the future when there is a volunteer with the necessary CPU resources. I've had a vague goal to do it once a year, but in the past it's typically been once every few years.
In the meantime, shorter proofs can benefit everyone incrementally with smaller file size and slightly faster run times of various functions. Benoit mentioned that he has reduced the size of new mathbox proofs up to 40% occasionally. So we encourage (but do not require) that people minimize their proofs when it is not too much trouble to do so. (A decade or so ago I tried to make it a requirement, and several mathbox contributors didn't like that.)
Regarding the minimization of other people's work, our policy has been to allow anyone to minimize proofs in other people's mathboxes without notice since it rarely causes problems. A case where it is natural to do so is after adding a new propositional calculus theorem that is expected to shorten many proofs throughout set.mm. In all cases, when 'minimize' results in shorter proofs, we don't add or change any "(Proof shortened by...)" tags since there was little manual labor or ingenuity involved.
Benoit has updated his script for bulk minimization ('scripts/min.cmd' on GitHub set.mm develop) to accommodate the new 'minimize' behavior.
Norm
As noted on the 10-Aug-2019 news item on the Most Recent Proofs page
http://us2.metamath.org/mpeuni/mmrecent.html
the behavior of the 'minimize' command has been changed.
Before the change, 'minimize *' with no qualifiers could add dependencies on new axioms if it made the proof shorter. This is was dangerous in some cases, for example if in the original proof we went out of our way to avoid the Axiom of Choice. Earlier, we recommended the use of 'minimize * / no_new_axioms_from ax-*' for everyday use to prevent this, but sometimes people would forget and use the more dangerous 'minimize *'.
For maximum safety, the new philosophy is to prevent introducing dependence on any new axioms (actually any new $a statement) unless specifically allowed by qualifiers. A new qualifier, '/allow_new_axioms', is now needed to allow dependence on any additional $a's. Usually we don't care about dependence on new definitions or syntax, and to allow all $a's except axioms proper, the new recommendation is to use
MM-PA> minimize_with * / allow_new_axioms * / no_new_axioms_from ax-*
for everyday use, which can be abbreviated
MM-PA> min */a */n ax-*
(although in scripts, it may be best to use the full command names for robustness against future ambiguity). In many cases, this command and the unqualified
MM-PA> min *
will produce the same results, so don't worry about it too much if you forget the qualifiers, but occasionally the qualified command might result in a shorter proof through the use of new definitional and syntax $a's. The main thing, though, is that an unqualified 'min *' is always safe to use now, unlike before.
When you don't care at all about possible dependence on additional axioms, you can use
MM-PA> min */a *
which in some cases might produce a shorter proof with more axiom dependencies. This obviously should not used for bulk minimization but only for specific proofs where you know additional axiom dependencies are not an issue.
'help miinimize' describes the new qualifier behavior (although there are some wording issues pointed out by Benoit that I will be improving). The Metamath book unfortunately omitted a description of the 'undo' and 'redo' commands ('help undo'), so be aware of them. In particular, 'undo' will revert a 'minimize' command and 'redo' will restore it, which is occasionally useful for comparing before and after results with 'show new_proof /compressed', or for experimenting with different qualifiers.
2. Policies for proof minimization
In the past we have occasionally run the entire set.mm through minimization, and that will probably happen again at some point in the future when there is a volunteer with the necessary CPU resources. I've had a vague goal to do it once a year, but in the past it's typically been once every few years.
In the meantime, shorter proofs can benefit everyone incrementally with smaller file size and slightly faster run times of various functions. Benoit mentioned that he has reduced the size of new mathbox proofs up to 40% occasionally. So we encourage (but do not require) that people minimize their proofs when it is not too much trouble to do so. (A decade or so ago I tried to make it a requirement, and several mathbox contributors didn't like that.)
Regarding the minimization of other people's work, our policy has been to allow anyone to minimize proofs in other people's mathboxes without notice since it rarely causes problems. A case where it is natural to do so is after adding a new propositional calculus theorem that is expected to shorten many proofs throughout set.mm. In all cases, when 'minimize' results in shorter proofs, we don't add or change any "(Proof shortened by...)" tags since there was little manual labor or ingenuity involved.
Benoit has updated his script for bulk minimization ('scripts/min.cmd' on GitHub set.mm develop) to accommodate the new 'minimize' behavior.
Norm
savask
Sep 22, 2019, 11:32:46 AM9/22/19
to Metamath
So we encourage (but do not require) that people minimize their proofs when it is not too much trouble to do so.
Perhaps it is a bit off-topic for this thread, but I think it's worth suggesting anyway.
Maybe there should be a "tutorial" page for contributing to set.mm which will explain all the steps required and some tips/suggestions (like minimizing your proof before contributing it to set.mm)? I imagine a set-by-step explanation, showing how to transfer the statement and the proof of your theorem into set.mm, how to comment it correctly, how to minimize the proof, wrap/unwrap and so on.
It seems to me that set.mm accumulated a baggage of rules and conventions (some of which are, of course, covered in the "Conventions and Style" page), so having a definite first guide will make contributing more "user-friendly" and will encourage correct behavior, like minimizing theorems or writing detailed comments.
Maybe there should be a "tutorial" page for contributing to set.mm which will explain all the steps required and some tips/suggestions (like minimizing your proof before contributing it to set.mm)? I imagine a set-by-step explanation, showing how to transfer the statement and the proof of your theorem into set.mm, how to comment it correctly, how to minimize the proof, wrap/unwrap and so on.
It seems to me that set.mm accumulated a baggage of rules and conventions (some of which are, of course, covered in the "Conventions and Style" page), so having a definite first guide will make contributing more "user-friendly" and will encourage correct behavior, like minimizing theorems or writing detailed comments.
David A. Wheeler
Sep 22, 2019, 12:39:08 PM9/22/19
to savask, Metamath
On September 22, 2019 11:32:46 AM EDT, savask <sav...@yandex.ru> wrote:
>Perhaps it is a bit off-topic for this thread, but I think it's worth
>suggesting anyway.
>Maybe there should be a "tutorial" page for contributing to set.mm
>which
>will explain all the steps required and some tips/suggestions (like
>minimizing your proof before contributing it to set.mm)? I imagine a
>set-by-step explanation, showing how to transfer the statement and the
>proof of your theorem into set.mm, how to comment it correctly, how to
>minimize the proof, wrap/unwrap and so on.
We do have a getting started wiki page, right here:
>Perhaps it is a bit off-topic for this thread, but I think it's worth
>suggesting anyway.
>Maybe there should be a "tutorial" page for contributing to set.mm
>which
>will explain all the steps required and some tips/suggestions (like
>minimizing your proof before contributing it to set.mm)? I imagine a
>set-by-step explanation, showing how to transfer the statement and the
>proof of your theorem into set.mm, how to comment it correctly, how to
>minimize the proof, wrap/unwrap and so on.
https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing
It doesn't have everything you suggested, but I think it shouldn't be hard to add. Please do!
That page is not as prominent as perhaps it should be. Suggestions on how to make that happen are also welcome.
--- David A.Wheeler
Benoit
Sep 22, 2019, 12:47:13 PM9/22/19
to Metamath
I was planning to add the "encouragement" to minimize proofs on the page
I think that this page, together with the page it links to,
https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing
is very useful. It is always open on my desktop when I work on set.mm.
Benoit
savask
Sep 22, 2019, 1:24:43 PM9/22/19
to Metamath
I completely missed the wiki page and CONTRIBUTING.md file (probably because I couldn't see them in http://us2.metamath.org:88/mpeuni/mmset.html).
They both answer many questions I thought were not covered anywhere, so I guess they serve as a guide.
I would still like a tutorial with examples, but I don't dare making one, since I'm not a regular contributor. In any case, some contributing technicalities most probably won't stop a person who already managed to prove something in metamath, and materials you linked answer most questions anyway.
Benoit
Sep 22, 2019, 2:05:46 PM9/22/19
to Metamath
On Sunday, September 22, 2019 at 7:24:43 PM UTC+2, savask wrote:
I completely missed the wiki page and CONTRIBUTING.md file (probably because I couldn't see them in http://us2.metamath.org:88/mpeuni/mmset.html).
Good point, maybe a link could be added to the contributing.md file on the mmset.html page (I'll make a proposal in my next PR). Note that the Metamath home page has a FAQ section with a question "How can I contribute to Metamath", and the answer has a link to github.com/metamath/set.mm . Granted, this is not very direct.
Benoit
Norman Megill
Sep 22, 2019, 4:57:30 PM9/22/19
to Metamath
I added links to "How can I contribute to Metamath?" ( http://us2.metamath.org/index.html#contribute ) near the top of these pages:
http://us2.metamath.org/mpeuni/mmset.html
http://us2.metamath.org/mpeuni/mmrecent.html
I also added links to the wiki https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing and CONTRIBUTING.md under "How can I contribute to Metamath?".
Hopefully this will address most of your concerns. Feel free to enhance the wiki if you wish.
Norm
http://us2.metamath.org/mpeuni/mmset.html
http://us2.metamath.org/mpeuni/mmrecent.html
I also added links to the wiki https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing and CONTRIBUTING.md under "How can I contribute to Metamath?".
Hopefully this will address most of your concerns. Feel free to enhance the wiki if you wish.
Norm
David A. Wheeler
Sep 23, 2019, 12:20:46 AM9/23/19
to savask, Metamath
On September 22, 2019 1:24:42 PM EDT, savask <sav...@yandex.ru> wrote:
>I completely missed the wiki page and CONTRIBUTING.md file (probably
>because I couldn't see them in
>http://us2.metamath.org:88/mpeuni/mmset.html
>).
>They both answer many questions I thought were not covered anywhere, so
>I
>guess they serve as a guide.
>
>I would still like a tutorial with examples
You might find these 2 video tutorials that I created useful:
>I completely missed the wiki page and CONTRIBUTING.md file (probably
>because I couldn't see them in
>http://us2.metamath.org:88/mpeuni/mmset.html
>).
>They both answer many questions I thought were not covered anywhere, so
>I
>guess they serve as a guide.
>
>I would still like a tutorial with examples
https://m.youtube.com/watch?v=Rst2hZpWUbU
https://m.youtube.com/watch?v=vE3v175cMKM
--- David A.Wheeler
savask
Sep 23, 2019, 12:37:21 AM9/23/19
to Metamath
You might find these 2 video tutorials that I created useful:
Thanks, I saw those a few years ago :-) They were very useful.
Also, they are featured at http://us2.metamath.org:88/index.html#mmj2 so it was not hard to find them by exploring Metamath website.
I added links to "How can I contribute to Metamath?" ( http://us2.metamath.org/index.html#contribute ) near the top of these pages:
http://us2.metamath.org/mpeuni/mmset.html
http://us2.metamath.org/mpeuni/mmrecent.html
Great, now it's a lot easier to find contributing tips.
Reply all
Reply to author
Forward
0 new messages