Open GinoGiotto opened 1 year ago
The option seems reasonable to me, although I'm not planning on working on it any time soon. I will review a PR which implements it. The design looks a bit ad-hoc / inextensible (I'm sure you can come up with more variations on this command and maybe we will be doing this again later), but I will leave rethinking / overhauling the system to one of the newer alternatives.
As mentioned in the GitHub issue[^1^], with the
/MAY_GROW
option it's possible to utilize the minimizer as an axiom usage minimizer. Some of my pull requests[^2^][^3^][^4^] show that this approach can lead to meaningful results.However, the drawback of this method is that the minimizer often produces "garbage" modified proofs that are neither shorter nor eliminate any axiom dependency. Consequently, I find myself needing to tediously filter only the valuable edits, which consumes a lot of time.
To address this issue, I propose the addition of a new option for the minimizer. Its implementation would limit the edits to only when some dependencies at choice are eliminated as a result (so no garbage edits would occour). Below I present how this addition would combine with the other commands. I'm not attached to this formatting particularly, feel free to propose your alternative ideas (or different option names).
/IF_DROP
The
/IF_DROP <label-match>
option means: "Modify the proof only when at least one of the labels in<label-match>
has been removed in the proof dependencies". In most cases we would be interested in removing axioms, so/IF_DROP ax-*
would be the most common use. Regardless the user can use it against undesirable theorems and definitions as well.Here is how this addition would behave with some option combinations:
Edit proofs if replacements are both shorter and less dependent on axioms. This is a rare occurrence, so it's probably not very useful.
Edit proofs when axiom dependencies are reduced, regardless of the length of new proofs. This would be the basic useful form.
Edit proofs when axiom dependencies are reduced, regardless of the length of new proofs. Additionally, allow the introduction of new definitions within the proof, which provides a better fine-tuning compared to the previous combination.
As mentioned by @benjub in the Metamath mailing list[^5^], by proving a few statements in main with distinct variable conditions, then most other theorems can drop ax-13 without adding any new dv conditions. This is where the axiom minimizer becomes handy, as it could automatically axiom-reduce those non-dv proofs, thereby speeding up the process:
The combination with
/FORBID
ensures that any replacement would never use ax-13, therefore providing the desired behaviour (in practice/FORBID
makes it more likely to find a specific axiom reduction, because we are forcing it to choose our route in case of interchangeable possibilities, see https://github.com/metamath/metamath-exe/pull/154#issue-1797005295 for a basic example)./IF_DROP_OR_SHORTER
Minimization requires a significant amount of computing power, so we might aim to make the most of our time. In that case we could use a refined option
/IF_DROP_OR_SHORTER <label-match>
. This one would make an edit if either any of the written labels dropped (regardless of the proof length) or if the proof is shorter. This way we would maximize the outcome for the time spent for the process (note: in this case the/MAY_GROW
option would have no effect).Some side thoughts
As explained by Norman Megill[^6^],
/NO_NEW_AXIOMS_FROM ax-*
(when accompanied by/ALLOW_NEW_AXIOMS *
) does not introduce new axioms, but can utilize different ones if they are already part of the proof. In contrast,/FORBID
avoids any dependency from<label-match>
, regardless of their presence in the proof. The latter option effectively forces the minimizer to eliminate dependencies from a proof if enough allowed replacements exist.Therefore I disagree with the first note of
/FORBID
when consultingMM> help minimize
in metamath-exe[^7^]: I think/FORBID
is useful and shouldn't be deprecated. If the minimizer will be used as an axiom reducer, I would propose revising or removing that note, as/FORBID
would be exactly what is needed.One could also add an option to create a log file of axiom reductions for the corresponding proof edits. This way the user would be facilitated when consulting the reasons behind those particular changes.
I'm aware that this whole proposal goes against the "don't add anything" rule for metamath-exe, but I believe this small addition would be useful to speed up some routine processes in the long term. If you think this is worth giving consideration, I'll already be very grateful for it.
Regards
Gino
[^1^]: GitHub issue about ax-13: https://github.com/metamath/set.mm/issues/3183 [^2^]: Pull request removing ax-11 and ax-13: https://github.com/metamath/set.mm/pull/3189 [^3^]: Pull request removing ax-pow: https://github.com/metamath/set.mm/pull/3222 [^4^]: Pull request removing ax-13: https://github.com/metamath/set.mm/pull/3274 [^5^]: Benjub Google Groups discussion: https://groups.google.com/g/metamath/c/1wi1s6qBYqY/m/FPkPsd5oAwAJ [^6^]: Norman Megill's explanation: https://groups.google.com/g/metamath/c/f-L91-1jI24/m/3KJnGa8qCgAJ [^7^]: Help section about /FORBID: https://github.com/metamath/metamath-exe/blob/16ca0310abff69ff9c3777cb336ea69213f01f79/src/mmhlpb.c#L1296C1-L1299