Minimizer doesn't find simple shortening

[GinoGiotto]

I'm using set.mm at commit 02d887a.

This is more like a question rather than an issue because it's hard to tell if this is supposed to happen or not, anyway I find this to be an interesting test case.

In main there is this theorem:

    $d y z A $.  $d x B $.  $d x y z $.  $d ph z $.  $d B z $.
    $( Interchange class substitution and restricted existential quantifier.
       (Contributed by NM, 15-Nov-2005.)  (Revised by NM, 18-Aug-2018.) $)
    sbcrex $p |- ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) $=
      ( wnfc wrex wsbc wb nfcv sbcrext ax-mp ) CDFACEGBDHABDHCEGICDJABCDEKL $.

In the mathbox of Stefan O'Rear there is this theorem:

  ${
    $d y z A $.  $d x B $.  $d x y z $.  $d ph z $.  $d B z $.
    $( Interchange class substitution and restricted existential quantifier.
       (Contributed by NM, 15-Nov-2005.)  (Proof shortened by Andrew Salmon,
       29-Jun-2011.)  Obsolete as of 18-Aug-2018.  Use ~ sbcrex instead.
       (New usage is discouraged.)  (Proof modification is discouraged.) $)
    sbcrexgOLD $p |- ( A e. V ->
                 ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) ) $=
      ( vz wrex wsb wsbc dfsbcq2 wceq rexbidv nfcv nfs1v nfrex weq sbequ12 sbie
      cv vtoclbg ) ACEHZBGIABGIZCEHZUBBDJABDJZCEHGDFUBBGDKGTDLUCUECEABGDKMUBUDB
      GUCBCEBENABGOPBGQAUCCEABGRMSUA $.
  $}

We can notice that sbcrexgOLD is simply a version of sbcrex with an antecedent, therefore sbcrexgOLD can be proven from sbcrex:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> r set.mm
Reading source file "set.mm"... 43771335 bytes
43771335 bytes were read into the source buffer.
The source has 208947 statements; 2798 are $a and 41505 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> pr sbcrexgOLD /ove
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT sbcrexgOLD"):
$d y A $.  $d x B $.  $d x y $.
170795 sbcrexgOLD $p |- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [.
      A / x ]. ph ) ) $= ... $.
Note:  The proof you are starting with is already complete.
>>> ?Warning: Modification of this statement's proof is discouraged.
MM-PA> del all
The entire proof was deleted.
1    sbcrexgOLD=? $? |- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [.
                                                                A / x ]. ph ) )
MM-PA> as 1 a1i
3      a1i.1=?        $? |- ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x
                                                                        ]. ph )
MM-PA> as 3 sbcrex
MM-PA> impr all
A proof of length 1 was found for step 7.
A proof of length 1 was found for step 6.
A proof of length 1 was found for step 5.
A proof of length 1 was found for step 4.
A proof of length 1 was found for step 3.
A proof of length 3 was found for step 2.
A proof of length 15 was found for step 1.
Steps 1 and above have been renumbered.
CONGRATULATIONS!  The proof is complete.  Use SAVE NEW_PROOF to save it.
Note:  The Proof Assistant does not detect $d violations.  After saving
the proof, you should verify it with VERIFY PROOF.
MM-PA> save ne /compr /ove
>>> ?Warning: You are overwriting a proof whose modification is discouraged.
The new proof of "sbcrexgOLD" has been saved internally.
Remember to use WRITE SOURCE to save changes permanently.
MM-PA> sh ne /compr
Proof of "sbcrexgOLD":
---------Clip out the proof below this line to put it in the source file:
      ( wrex wsbc wb wcel sbcrex a1i ) ACEGBDHABDHCEGIDFJABCDEKL $.
---------The proof of "sbcrexgOLD" (58 bytes) ends above this line.
MM-PA> exi
Exiting the Proof Assistant.  Type EXIT again to exit Metamath.
MM> ver pr sbcrexgOLD
sbcrexgOLD
MM>

We can also use improve all to find this shorter proof:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> r set.mm
Reading source file "set.mm"... 43771335 bytes
43771335 bytes were read into the source buffer.
The source has 208947 statements; 2798 are $a and 41505 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> pr sbcrexgOLD /over
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT sbcrexgOLD"):
$d y A $.  $d x B $.  $d x y $.
170795 sbcrexgOLD $p |- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [.
      A / x ]. ph ) ) $= ... $.
Note:  The proof you are starting with is already complete.
>>> ?Warning: Modification of this statement's proof is discouraged.
MM-PA> del all
The entire proof was deleted.
1    sbcrexgOLD=? $? |- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [.
                                                                A / x ]. ph ) )
MM-PA> improve all /3
Pass 1:  Trying to match cut-free statements...
Pass 2:  Trying to match all statements, with cut-free hypothesis matches...
A proof of length 25 was found for step 1.
Steps 1 and above have been renumbered.
CONGRATULATIONS!  The proof is complete.  Use SAVE NEW_PROOF to save it.
Note:  The Proof Assistant does not detect $d violations.  After saving
the proof, you should verify it with VERIFY PROOF.
MM-PA> save ne /compr /over
>>> ?Warning: You are overwriting a proof whose modification is discouraged.
The new proof of "sbcrexgOLD" has been saved internally.
Remember to use WRITE SOURCE to save changes permanently.
MM-PA> sh ne /compr
Proof of "sbcrexgOLD":
---------Clip out the proof below this line to put it in the source file:
      ( wrex wsbc wb wcel sbcrex a1i ) ACEGBDHABDHCEGIDFJABCDEKL $.
---------The proof of "sbcrexgOLD" (58 bytes) ends above this line.
MM-PA> exi
Exiting the Proof Assistant.  Type EXIT again to exit Metamath.
MM> ver pr sbcrexgOLD
sbcrexgOLD
MM>

However if I use the minimizer then it doesn't find it:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> r set.mm
Reading source file "set.mm"... 43771335 bytes
43771335 bytes were read into the source buffer.
The source has 208947 statements; 2798 are $a and 41505 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> pr sbcrexgOLD /over
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT sbcrexgOLD"):
$d y A $.  $d x B $.  $d x y $.
170795 sbcrexgOLD $p |- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [.
      A / x ]. ph ) ) $= ... $.
Note:  The proof you are starting with is already complete.
>>> ?Warning: Modification of this statement's proof is discouraged.
MM-PA> minimize * /allow * /no ax-*
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
No shorter proof was found.
(Other mathboxes were not checked.  Use / INCLUDE_MATHBOXES to include them.)
MM-PA>

Axiom usage of sbcrexgOLD is the same as sbcrex, so this isn't the reason. The verifier does not complain about $d violations so it doesn't appear they are the problem either. I tried to move sbcrexgOLD out of the mathbox and remove the discouragment labels. Still nothing. So the question is why the minimizer doesn't notice this trivial shortening?

[tirix]

My guess would be that the minimizer does not know a1i, and does not even know what is an antecedent.
It only searches for exact matches.

[GinoGiotto]

I admit I'm ignorant about how the minimizer works. But isn't a1i just a simple rule of inference? And doesn't the minimizer replace rules of inference as well?

Here is an example:

$c |- wff ( ) | $.
$v A B C $.

wa $f wff A $.
wb $f wff B $.
wc $f wff C $.
wbar $a wff ( A | B ) $.

ax-1 $a |- ( ( A | A ) | B ) $.

${
  ax-inf1.1 $e |- ( ( B | B ) | C ) $.
  ax-inf1 $a |- ( ( ( B | B ) | C ) | ( B | B ) ) $.
$}

${
  ax-inf2.1 $e |- ( ( ( B | B ) | C ) | ( B | B ) ) $.
  ax-inf2 $a |- ( C | C ) $.
$}

${
  ax-inf3.1 $e |- ( ( B | B ) | C ) $.
  ax-inf3.2 $e |- ( C | C ) $.
  ax-inf3 $a |- ( ( ( B | B ) | C ) | ( B | B ) ) $.
$}

$( First theorem. (New usage is discouraged.) $)
th1 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) )  $= ( wbar ax-1 ax-inf1 ) ACCDBDZAGEF $.

$( Second theorem. $)
th2 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) )  $= ( wbar ax-1 ax-inf1 ax-inf2 ax-inf3 ) ACCDBDZAIECICICIEFGH $.

Theorems th1 and th2 are identical, but th2 has a longer proof, using more rules of inference than it needs. Let's see if the minimizer can find the shortening:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> r min.mm /
Reading source file "min.mm"... 755 bytes
755 bytes were read into the source buffer.
The source has 22 statements; 5 are $a and 2 are $p.
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.01 s.
No errors were found.
MM> prove th2
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT th2"):
22 th2 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) ) $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> minimize * /allow * /no ax-*
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "th2" decreased from 58 to 33 bytes using "ax-inf1".
Scanning backward through statements...
Proof of "th2" decreased from 58 to 33 bytes using "ax-inf1".
The forward scan results were used.
MM-PA> sh ne /compressed
Proof of "th2":
---------Clip out the proof below this line to put it in the source file:
  ( wbar ax-1 ax-inf1 ) ACCDBDZAGEF $.
---------The proof of "th2" (33 bytes) ends above this line.
MM-PA>

In this case the minimizer found the shortening, so the diagnosis doesn't seem related to the fact that a1i is a rule of inference, nor to the fact that exact matches are needed, since I created th2 in a way that doesn't do so. What am I missing?

[tirix]

You're right.

Then I suppose someone would need to dig into the way the minimizer is implemented to understand why this minimization is not found.

[david-a-wheeler]

I haven't dug through the minimizer implementation, but IIRC, Norm thought of the minimizer as a useful heuristic; he didn't expect the code to find "all" minimizations. So I'm unsurprised some simple shortenings are missed.

That said, if we can improve the minimizer, that'd be great.

[jkingdon]

That said, if we can improve the minimizer, that'd be great.

A change that makes it slower kinda has to be a separate option or separate tool or something. At least the way I use it, and I think maybe people in general.

[GinoGiotto]

A change that makes it slower kinda has to be a separate option or separate tool

Exactly, I'd prefer to have the ability to choose an arbitrary depth rather than sticking with the settings someone else chosed for me. If metamath-knife can provide a minimizer with a better performance it might be strategically convenient to attempt it there.

[icecream17]

I think I know why it didn't find it:

#170
In the failed case, one basically has to introduce two new theorems: ax-1 and in1, while in the passed test case, ax-1 already exists

In essence, when trying theorem in1, it checks only subproofs, and doesn't include previous theorems or axioms, and so doesn't find ax-1.