Add minimizer functionality

[tirix]

Adds a minimal functioning minimizer, which:

• has the basic necessary structure
• sometimes actually provides a shorter compressed proof
• does not crash

To-do list:

• ignore "discouraged theorem"
• check for additional distinct variable requirements
• check for axiom usage
• provide steps, compressed proof size
• apply good heuristics for choosing shorter step
• save updated database (the resulting proof is simply dumped to the standard output in MMP format)
• complete significantly faster than metamath-exe for longer theorems
• perform forward and backward passes (only a forward pass is performed)

Usage: -M command line switch.

[tirix]

@digama0 would you like to review this?
I'm interested in any feedback!

[savask]

That's really great. This finally made me install the Rust toolchain and try metamath-knife :-)

I tried it on the recent large 3cubeslem3l theorem, minimization succeeded in 557899ms, which is fairly good for a theorem of that size.

I don't know Rust so can't really comment on the code, but let me still make several remarks, maybe you'll find them useful.

Compressed proof
The metamath-exe save proof 3cubeslem3l /compressed command still has managed to shave off quite a few bytes from the proof, so it seems that metamath-knife doesn't order theorem labels used in the proof according to their usage (theorems which are used more often should go first).

Minimize_with
Correct me if I'm wrong, but it seems that right now your algorithm loops through all steps, and for each step it loops through all theorems (subject to some restrictions). Metamath-exe does it in a different order, the outer loop goes though all theorems, and the inner loop (which is really a subroutine called minimize_with) goes though all the steps in the proof.

This has two advantages, first you can implement the /allow_growth option easily, which makes the "minimizer" use some theorem even if it makes the proof larger. The second advantage is a possible cumulative proof minimization. Suppose in a proof steps 10, 20, 30 use theoremX and this theorem isn't used in other steps. You try to minimize with theoremY and it so happens, that it works for steps 10, 20 and 30, but only after replacing the final occurrence of theoremX by theoremY in step 30 the proof gets shorter. In your current approach (as far as I understand it!), the minimizer won't use theoremX in steps 10 and 20, and when it would try to use it in step 30, it would probably also gloss over it - because steps 10 and 20 will still reference theoremX and step 30 will reference theoremY, and that is an additional label in the referenced theorems list.

As another example, suppose steps 10, 20, 30 all reference step 5 but theoremY allows to get rid of this dependence. Only after you replace theoremX with theoremY in 10, 20 and 30 at the same time, step 5 can be removed to shorten the proof.

Optimizations
There's one optimization I've discussed with Norm and which was implemented in metamath-exe (but not merged...) metamath/metamath-exe#94 There's a description, but tldr is that one computes the list of constants used in the proof and theorem hypotheses, and tries to minimize only with those theorems which only use constants from this set. This is essentially an additional filter alongside axiom usage and it often reduces the number of candidate theorems significantly.

I'm a bit rusty on the metamath-exe internals, but if I recall correctly the biggest burden besides looping through all theorems and all steps, was computing the compressed proof to actually check if it got smaller. I can't quite understand if you're doing the same in your algo, but often you can avoid computing the compressed proof over and over again if, for example, you're able to remove some theorem from the theorem list, or if the referenced theorems list doesn't change but some steps were removed.

Deep minimization
There's some freedom in the way steps are arranged in the proof. For example, it may happen that steps 10 and 20 can be interchanged in the MMP format without breaking anything (they may correspond to independent subtrees, for example). This gives an opportunity for deeper minimization. Suppose you're trying to minimize step 10 with some theorem. Usually this theorem is allowed to use only steps 1, 2, ..., 9 as hypotheses, but we know that step 20 is also allowed in theory, it just so happens that it's placed later in the proof. So it might be possible to shorten the whole proof if step 20 is moved to an earlier position, so step 10 can reference it.

One can precompute "allowed steps" for each step beforehand, and use those as potential hypotheses when trying to match a theorem to a step. Updating this structure shouldn't be too hard, but I guess that's a feature for minimizers of the future :-)

[tirix]

Thank you @savask for your encouraging and detailed feedback!

Compressed proof
The metamath-exe save proof 3cubeslem3l /compressed command still has managed to shave off quite a few bytes from the proof, so it seems that metamath-knife doesn't order theorem labels used in the proof according to their usage (theorems which are used more often should go first).

I believe metamath_knife uses the same knapsack algorithm as metamath-exe. The algorithm first counts how many references there are to a proof step, pulls all the hypotheses first, but then the knapsack might reorder, as it will use labels sorted by length.

Minimize_with
Correct me if I'm wrong, but it seems that right now your algorithm loops through all steps, and for each step it loops through all theorems (subject to some restrictions). Metamath-exe does it in a different order, the outer loop goes though all theorems, and the inner loop (which is really a subroutine called minimize_with) goes though all the steps in the proof.

Yes you're right! I'll try swapping the order of the loops.

Optimizations
If I recall correctly the biggest burden besides looping through all theorems and all steps, was computing the compressed proof to actually check if it got smaller. I can't quite understand if you're doing the same in your algo.

I'm actually not recomputing the compressed proof in the current algo. I find alternatives, and only estimate they could lead to a shorter proof... this is very random right now! Actually recomputing the compressed proof and actually comparing proof lengths is going to be my next step. I checked a few proofs and from what I saw there were very few alternative proofs to check (a handful per proof, if any), so my guess was that the performance impact would be minimal.

Deep minimization

When attempting to minimize a step, I currently consider all steps previously proved, in the current proof order.
Maybe one easy way to go towards this "deep minimization" would be to consider all steps up to the step where the current step is first referenced. In many cases that might be the next step, but in some cases that might indeed be much later. This is not the absolute best, but it would already complicate the minimization algorithm. Maybe for later!

[savask]

I believe metamath_knife uses the same knapsack algorithm as metamath-exe.

Right, but there seems to be some difference still. Here's the proof of txomap minimized by metamath-knife:

Proof

      ( vz wcel wss wa cfv vc va vb cima ctx cxp wrex wral wceq simp-6l simpllr
      co cv syl2anc simplr wfn opex fnmpoi ctopon ad6antr toponss xpss12 simprl
      cop fnfvima mp3an2i simp-4r wf ffn 3syl fimaproj imass2 ad2antll eqsstrrd
      3eltr3d xpeq1 eleq2d sseq1d anbi12d xpeq2 rspc2ev syl112anc wb eltx mpbid
      r19.21bi ad4ant13 r19.29vva wfun mpofun fvelima adantl r19.29a ralrimiva
      mpan mpbird ) AHDUNZKLUOVBUGZUKVCZULVCZUMVCZUPZUGZXLXGUHZUIZUMLUQULKUQZUK
      XGURZAXPUKXGAXIXGUGZUIZUFVCZHUJZXIUSZXPUFDXSXTDUGZUIZYBUIZXTBVCZCVCZUPZUG
      ZYHDUHZUIZXPBCIJYEYFIUGZUIZYGJUGZUIZYKUIZFYFUNZKUGZGYGUNZLUGZXIYQYSUPZUGZ
      UUAXGUHZXPYPAYLYRAXRYCYBYLYNYKUTZYEYLYNYKVAZUBVDYPAYNYTUUDYMYNYKVEZUCVDYP
      YAHYHUNZXIUUAHMNUPZVFZYPYHUUHUHZYIYAUUGUGBCMNYFFUJZYGGUJZVNZHUEUUKUULVGVH
      ZYPYFMUHZYGNUHZUUJYPIMVIUJZUGZYLUUOAUURXRYCYBYLYNYKRVJUUEYFIMVKVDZYPJNVIU
      JZUGZYNUUPAUVAXRYCYBYLYNYKSVJUUFYGJNVKVDZYFMYGNVLVDYOYIYJVMUUHYHHXTVOVPYD
      YBYLYNYKVQYPBCMNFGHYFYGUEYPAMOFVRFMVFUUDPMOFVSVTYPANEGVRGNVFUUDQNEGVSVTUU
      SUVBWAZWEYPUUAUUGXGUVCYJUUGXGUHYOYIYHDHWBWCWDXOUUBUUCUIXIYQXKUPZUGZUVDXGU
      HZUIULUMYQYSKLXJYQUSZXMUVEXNUVFUVGXLUVDXIXJYQXKWFZWGUVGXLUVDXGUVHWHWIXKYS
      USZUVEUUBUVFUUCUVIUVDUUAXIXKYSYQWJZWGUVIUVDUUAXGUVJWHWIWKWLAYCYKCJUQBIUQZ
      XRYBAUVKUFDADIJUOVBUGZUVKUFDURZUDAUURUVAUVLUVMWMRSBCDIJUUQUUTUFWNVDWOWPWQ
      WRXRYBUFDUQZAHWSXRUVNBCMNUUMHUEWTUFXIDHXAXEXBXCXDAKOVIUJZUGLEVIUJZUGXHXQW
      MTUAULUMXGKLUVOUVPUKWNVDXF $.

And now after applying save proof txomap /compressed to the metamath-knife output:

Proof

      ( vc va vb vz cima ctx co wcel cxp wss wrex wral cfv wceq simp-6l simpllr
      cv wa syl2anc simplr wfn opex fnmpoi ctopon ad6antr toponss xpss12 simprl
      cop fnfvima mp3an2i simp-4r wf ffn 3syl fimaproj imass2 ad2antll eqsstrrd
      3eltr3d xpeq1 eleq2d sseq1d anbi12d xpeq2 rspc2ev syl112anc wb eltx mpbid
      r19.21bi ad4ant13 r19.29vva wfun mpofun fvelima adantl r19.29a ralrimiva
      mpan mpbird ) AHDUJZKLUKULUMZUFVBZUGVBZUHVBZUNZUMZXLXGUOZVCZUHLUPUGKUPZUF
      XGUQZAXPUFXGAXIXGUMZVCZUIVBZHURZXIUSZXPUIDXSXTDUMZVCZYBVCZXTBVBZCVBZUNZUM
      ZYHDUOZVCZXPBCIJYEYFIUMZVCZYGJUMZVCZYKVCZFYFUJZKUMZGYGUJZLUMZXIYQYSUNZUMZ
      UUAXGUOZXPYPAYLYRAXRYCYBYLYNYKUTZYEYLYNYKVAZUBVDYPAYNYTUUDYMYNYKVEZUCVDYP
      YAHYHUJZXIUUAHMNUNZVFYPYHUUHUOZYIYAUUGUMBCMNYFFURZYGGURZVNZHUEUUJUUKVGVHY
      PYFMUOZYGNUOZUUIYPIMVIURZUMZYLUUMAUUPXRYCYBYLYNYKRVJUUEYFIMVKVDZYPJNVIURZ
      UMZYNUUNAUUSXRYCYBYLYNYKSVJUUFYGJNVKVDZYFMYGNVLVDYOYIYJVMUUHYHHXTVOVPYDYB
      YLYNYKVQYPBCMNFGHYFYGUEYPAMOFVRFMVFUUDPMOFVSVTYPANEGVRGNVFUUDQNEGVSVTUUQU
      UTWAZWEYPUUAUUGXGUVAYJUUGXGUOYOYIYHDHWBWCWDXOUUBUUCVCXIYQXKUNZUMZUVBXGUOZ
      VCUGUHYQYSKLXJYQUSZXMUVCXNUVDUVEXLUVBXIXJYQXKWFZWGUVEXLUVBXGUVFWHWIXKYSUS
      ZUVCUUBUVDUUCUVGUVBUUAXIXKYSYQWJZWGUVGUVBUUAXGUVHWHWIWKWLAYCYKCJUPBIUPZXR
      YBAUVIUIDADIJUKULUMZUVIUIDUQZUDAUUPUUSUVJUVKWMRSBCDIJUUOUURUIWNVDWOWPWQWR
      XRYBUIDUPZAHWSXRUVLBCMNUULHUEWTUIXIDHXAXEXBXCXDAKOVIURZUMLEVIURZUMXHXQWMT
      UAUGUHXGKLUVMUVNUFWNVDXF $.

You can see that the label ordering is different ( vz wcel ... before re-compression and vc va ... after), and the proof re-compressed by metamath-exe is 2 bytes shorter. Note that the theorems labels block inside ( ) has the same length, so the shortening doesn't come from some line packing effects.

On the larger theorem 3cubeslem3l the difference was several lines.