idi not removed on minimization

[avekens]

Now I got again a situation in which ~idi was added to a proof during minimization:

Theorem with original proof:

$( The closed (internal binary) operations for a set.  (Contributed by AV,
   20-Jan-2020.) $)
clintopval $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) ) $=
  ( vm wcel cclintop cfv cxp cmap co cv cintop cvv cmpt wceq df-clintop a1i
  wa id oveq12d eqtrd adantl jca intopval syl adantr elex ovex fvmptd eqidd
  ) ABDZAEFAAAGZHIZULUJCACJZUMKIZULLELECLUNMNUJCOPUJUMANZQUNAAKIZULUOUNUPNU
  JUOUMAUMAKUORZUQSUAUJUPULNZUOUJUJUJQURUJUJUJUJRZUSUBAABBUCUDUETABUFULLDUJ
  AUKHUGPUHUJULUIT $.

---

1 df-clintop $a |- clIntOp = ( m e. _V |-> ( m intOp m ) )
2 1 a1i $p |- ( M e. V -> clIntOp = ( m e. _V |-> ( m intOp m ) ) )
3 id $p |- ( m = M -> m = M )
4 id $p |- ( m = M -> m = M )
5 3,4 oveq12d $p |- ( m = M -> ( m intOp m ) = ( M intOp M ) )
6 5 adantl $p |- ( ( M e. V /\ m = M ) -> ( m intOp m ) = ( M intOp M ) )
7 id $p |- ( M e. V -> M e. V )
8 id $p |- ( M e. V -> M e. V )
9 7,8 jca $p |- ( M e. V -> ( M e. V /\ M e. V ) )
10 intopval $p |- ( ( M e. V /\ M e. V ) -> ( M intOp M ) = ( M ^m ( M X.
M ) ) )
11 9,10 syl $p |- ( M e. V -> ( M intOp M ) = ( M ^m ( M X. M ) ) )
12 11 adantr $p |- ( ( M e. V /\ m = M ) -> ( M intOp M ) = ( M ^m ( M X. M
) ) )
13 6,12 eqtrd $p |- ( ( M e. V /\ m = M ) -> ( m intOp m ) = ( M ^m ( M X. M
) ) )
14 elex $p |- ( M e. V -> M e. _V )
15 ovex $p |- ( M ^m ( M X. M ) ) e. _V
16 15 a1i $p |- ( M e. V -> ( M ^m ( M X. M ) ) e. _V )
17 2,13,14,16 fvmptd $p |- ( M e. V -> ( clIntOp M ) = ( M ^m ( M X. M ) ) ) 18 eqidd $p |- ( M e. V -> ( M ^m ( M X. M ) ) = ( M ^m ( M X. M ) ) ) 19 17,18 eqtrd $p |- ( M e. V -> ( clIntOp M ) = ( M ^m ( M X. M ) ) )

Proof after min *:

  ( vm wcel cclintop cfv cxp cmap co wceq wi cintop cvv cmpt df-clintop a1i
  cv id oveq12d intopval anidms sylan9eqr elex ovex fvmptd idi ) ABDZAEFAAA
  GZHIZJKUGCACQZUJLIZUIMEMECMUKNJUGCOPUJAJZUGUKAALIZUIULUJAUJALULRZUNSUGUMU
  IJAABBTUAUBABUCUIMDUGAUHHUDPUEUF $.

---

1 df-clintop $a |- clIntOp = ( m e. _V |-> ( m intOp m ) )
2 1 a1i $p |- ( M e. V -> clIntOp = ( m e. _V |-> ( m intOp m ) ) )
3 id $p |- ( m = M -> m = M )
4 id $p |- ( m = M -> m = M )
5 3,4 oveq12d $p |- ( m = M -> ( m intOp m ) = ( M intOp M ) )
6 intopval $p |- ( ( M e. V /\ M e. V ) -> ( M intOp M ) = ( M ^m ( M X.
M ) ) )
7 6 anidms $p |- ( M e. V -> ( M intOp M ) = ( M ^m ( M X. M ) ) )
8 5,7 sylan9eqr $p |- ( ( M e. V /\ m = M ) -> ( m intOp m ) = ( M ^m ( M X.
M ) ) )
9 elex $p |- ( M e. V -> M e. _V )
10 ovex $p |- ( M ^m ( M X. M ) ) e. _V
11 10 a1i $p |- ( M e. V -> ( M ^m ( M X. M ) ) e. _V )
12 2,8,9,11 fvmptd $p |- ( M e. V -> ( clIntOp M ) = ( M ^m ( M X. M ) ) ) 13 12 idi $p |- ( M e. V -> ( clIntOp M ) = ( M ^m ( M X. M ) ) )

Running min * again didn't help, I had to remove the line 13 by hand. No discouraged theorems were used.

@nmegill could you have a look at it, please? If you need the whole context of the theorem, please wait for my next PR. I used Metamath - Version 0.180 10-Dec-2019.

[avekens]

Running min * again for ~clintopval with new version Version 0.181 12-Feb-2020 does not add ~idi anymore! Let's wait for the global minimization action if new cases come up.

[nmegill]

I apologize for not answering sooner. It seems I had a very large number of emails that day and somehow this got overlooked.

Whenever this kind of problem occurs, we can narrow down what's happening by doing the minimizations one at a time and looking at what happened to the proof.

Here is the end of the original proof ('show new_proof/renumber').

...
17   eqtrd.1=fvmptd   $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )
18   eqtrd.2=eqidd    $p |- ( M e. V -> ( M ^m ( M X. M ) ) = ( M ^m ( M X. M ) ) )
19 clintopval=eqtrd $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )

Notice that the eqtrd/eqidd chain is redundant. The forward 'minimize' scan
tries idi early in the scan. After 'minimize idi' we have:

...
17   idi.1=fvmptd     $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )
18 clintopval=idi   $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )

Above you can see that idi was legitimately used to shorten the proof. While this may seem counterintuitive since idi is inherently inefficient, the original proof was even more inefficient.

Later on in the scan, fvmptd eventually matches the idi output at step 18. After 'minimize fvmptd', idi goes away:

...
17 clintopval=fvmptd $p |- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )

The only situation I have seen where idi would not be removed is when the statement matching the idi output, fvmptd in this case, has a usage discouraged tag. (This has happened in the past.)
In that case, idi would remain in the proof. To check whether this is the case, you can add the '/override' qualifier to 'minimize'; but don't save the proof before checking that the minimizations used were desired ones.

Whether the Nov. 29 bug affected this is hard to say without further investigation, but it may be possible. In any case it doesn't seem to be a problem now.

[avekens]

Thank you very much, Norm, for your valuable explanations, and don't worry - the case wasn't urgent. But the next time I know now how to analyse in such a situation.

By the way, I checked with metamath.exe version Version 0.180 10-Dec-2019, and the problem did not occur anymore even with this old version. Maybe other changes in set.mm are responsible...

[avekens]

I had again a case where idi was introduced by minimze, and is not removed on following minimize calls. Here the original proof of theorem ~wspthnon:

1 breq2          $p |- ( w = W -> ( f ( A ( SPathsOn ` G ) B ) w <-> f ( A ( SPathsOn ` G ) B ) W ) )
2 1 exbidv       $p |- ( w = W -> ( E. f f ( A ( SPathsOn ` G ) B ) w <-> E. f f ( A ( SPathsOn ` G ) B ) W ) )
3 wwlknon.v      $e |- V = ( Vtx ` G )
4 3 iswspthsnon  $p |- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w }
5 2,4 elrab2     $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )
6 biid           $p |- ( ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )
7 5,6 bitri      $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )

After calling minimize, I got:

1 breq2          $p |- ( w = W -> ( f ( A ( SPathsOn ` G ) B ) w <-> f ( A ( SPathsOn ` G ) B ) W ) )
2 1 exbidv       $p |- ( w = W -> ( E. f f ( A ( SPathsOn ` G ) B ) w <-> E. f f ( A ( SPathsOn ` G ) B ) W ) )
3 wwlknon.v      $e |- V = ( Vtx ` G )
4 3 iswspthsnon  $p |- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w }
5 2,4 elrab2     $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )
6 5 idi          $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )

I will not remove the idi step manually and provide this theorem with its proof using idi with my next PR. If anybody is interested can investigate on this case further.

[digama0]

@avekens Can you produce a minimal test case demonstrating the issue?

[avekens]

Here is the complete theorem (together with two theorems this theorem depends on) which should work with the current set.mm):

${
$d G a b g n $. $d N a b g n w $.
wwlksonvtxTEST.v $e |- V = ( Vtx ` G ) $.
wwlksonvtxTEST $p |- ( W e. ( A ( N WWalksNOn G ) C )
-> ( A e. V /\ C e. V ) ) $=
( vg vn vb vw va wcel cn0 cvv wa cvtx cfv cv wceq cwwlksnon pm3.2i rgen2w
co wral wi fvex cc0 cwwlksn crab df-wwlksnon fveq2 adantl el2mpt2cl ax-mp
jca eleq2i anbi12i biimpri simpl2im ) FABDCUAUDUDMZDNMCOMPZACQRZMZBVCMZPZ
AEMZBEMZPZHSZQRZOMZVLPZHOUEINUEVAVBVFPUFVMIHNOVLVLVJQUGZVNUBUCIHJNOVKVKAB
OUHKSZRLSTISZVORJSTPKVPVJUIUDUJVCVCUAOFDCLKHILJUKVJCTZVKVCTZVRPVPDTVQVRVR
VJCQULZVSUPUMUNUOVIVFVGVDVHVEEVCAGUQEVCBGUQURUSUT $.

$d A a b f w $.  $d B a b f w $.  $d G a b f w $.  $d N a b f w $.
$d V a b f w $.  $d a b f g n w $.
iswspthsnonTEST $p |- ( A ( N WSPathsNOn G ) B )
                  = { w e. ( A ( N WWalksNOn G ) B ) |
                      E. f f ( A ( SPathsOn ` G ) B ) w } $=
  ( vn va vb wcel cvv wa co cv crab wceq wn c0 cn0 cwwspthsnon cspthson cfv
  vg wbr wex cwwlksnon 0ov cvtx cmpt2 df-wspthsnon mpt2ndm0 oveqd wwlksnon0
  id intnanrd syl rabeqdv rab0 syl6eq 3eqtr4a wspthsnon adantr adantl eqtrd
  wi eqid ex a1d pm2.61i wral wal wwlksonvtxTEST pm2.24d impcom alnex sylib
  alrimiv ralrimiva rabeq0 sylibr eqtr4d oveq12 breqd exbidv rabeqbidv ovex
  simprl simprr rabex a1i ovmpt2d ecase ) FUALEMLNZBGLZCGLZNZBCFEUBOZOZDPZA
  PZBCEUCUDZOZUFZDUGZABCFEUHOZOZQZRWOSZBCTOZTWTXIBCUIZXJWSTBCIUEJKUEPZUJUDZ
  XNXAXBJPZKPZXMUCUDOUFDUGAXOXPIPXMUHOOQUKUBFEUAMADUEIJKULUMUNZXJXIXFATQTXJ
  XFAXHTXJWOWRNZSXHTRXJWOWRXJUPUQBCEFGHUOURUSXFAUTVAVBWRSZWTTXIWOXSWTTRZVGW
  OXSXTWOXSNZWTBCJKGGXAXBXOXPXCOZUFZDUGZAXOXPXGOZQZUKZOZTYAWSYGBCWOWSYGRZXS
  AMDEFGJKHVCZVDUNXSYHTRWOJKYFYGBCGGYGVHUMVEVFVIXJXTXSXJWTXKTXQXLVAVJVKXSXF
  SZAXHVLXITRXSYKAXHXSXBXHLZNZXESZDVMYKYMYNDYLXSYNYLWRYNBCEFGXBHVNVOVPVSXED
  VQVRVTXFAXHWAWBWCXRJKBCGGYFXIWSMWOYIWRYJVDXOBRXPCRNZYFXIRXRYOYDXFAYEXHXOB
  XPCXGWDYOYCXEDYOYBXDXAXBXOBXPCXCWDWEWFWGVEWOWPWQWIWOWPWQWJXIMLXRXFAXHBCXG
  WHWKWLWMWN $.

$d W f w $.
wspthnonTEST $p |- ( W e. ( A ( N WSPathsNOn G ) B )
                 <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) ) $=
  ( vw cwwspthsnon co wcel cwwlksnon cv cspthson cfv wbr wex wa wb wceq idi
  breq2 exbidv iswspthsnonTEST elrab2 ) GABEDJKKZLGABEDMKKZLCNZGABDOPKZQZCR
  ZSTUIINZUJQZCRULIGUHUGUMGUAUNUKCUMGUIUJUCUDIABCDEFHUEUFUB $.

$}

[avekens]

Curiously, appending or inserting these theorems into the current set.mm, minimize applied to wspthnonTEST will remove the idi step! Therefore, my previously observed behaviour depends on the context. I will keep a copy of my current set.mm, which I can provide for you (how?).

[digama0]

Minimization is an important part of the bug isolation process. It's not just about getting me the information needed to replicate, because ideally the test case should end up in the metamath-exe test suite and a megabytes long unit test is not good.

[avekens]

Maybe the reason why minimize did not remove the idi step was the (superfluous) hypothesis

wwlknon.v $e |- V = ( Vtx ` G ) $.

After I removed it, there is no idi step after minimization anymore. Here the output:
MM-PA> sh n/lem/ren
1 breq2 $p |- ( w = W -> ( f ( A ( SPathsOn G ) B ) w <-> f ( A ( SPathsOn G ) B ) W ) )
2 1 exbidv $p |- ( w = W -> ( E. f f ( A ( SPathsOn G ) B ) w <-> E. f f ( A ( SPathsOn G ) B ) W ) )
3 eqid $p |- ( Vtx G ) = ( Vtx G )
4 3 iswspthsnon $p |- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G
) B ) | E. f f ( A ( SPathsOn G ) B ) w } 5 2,4 elrab2 $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn G ) B ) W ) )
6 biid $p |- ( ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A (
SPathsOn G ) B ) W ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn G ) B ) W ) )
7 5,6 bitri $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N
WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) W ) )

MM-PA> min */V/i
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Reverting "a1ii": Uncompressed steps: old = 172, new = 167
but compressed size: old = 224 bytes, new = 232 bytes
Proof of "wspthnon" decreased from 224 to 215 bytes using "idi".
Proof of "wspthnon" decreased from 172 to 128 steps using "idi".
Proof of "wspthnon" decreased from 215 to 180 bytes using "elrab2".
Proof of "wspthnon" decreased from 128 to 95 steps using "elrab2".
Scanning backward through statements...
Proof of "wspthnon" decreased from 224 to 180 bytes using "elrab2".
Proof of "wspthnon" decreased from 172 to 95 steps using "elrab2".
Forward vs. backward: 180 vs. 180 bytes; 95 vs. 95 steps
The forward scan results were used.

MM-PA> sh n/lem/ren
1 breq2 $p |- ( w = W -> ( f ( A ( SPathsOn G ) B ) w <-> f ( A ( SPathsOn G ) B ) W ) )
2 1 exbidv $p |- ( w = W -> ( E. f f ( A ( SPathsOn G ) B ) w <-> E. f f ( A ( SPathsOn G ) B ) W ) )
3 eqid $p |- ( Vtx G ) = ( Vtx G )
4 3 iswspthsnon $p |- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G
) B ) | E. f f ( A ( SPathsOn G ) B ) w } 5 2,4 elrab2 $p |- ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn G ) B ) W ) )