*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
<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
--
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/9cd36b07-2ca3-47b5-98f7-e476018a3aa8%40googlegroups.com.
