Finding lemmata which minimize set.mm

[savask]

In the post repeatedly re-proven statements David A. Wheeler found statements which appear in different proofs again and again. I decided to search for "repeatedly re-proven lemmata", i.e. sequences of theorem labels which often appear as sub-proofs in other theorems.

The rough algorithm is as follows. Say, we want to find lemmata with k steps. We take a compressed proof of some theorem T, and check all k-step subsequences L of its proof. We count a subsequence valid if

1) All its steps reference theorem labels (not a hypothesis and not a step marked with Z);
2) All its steps correspond to |- statements (to avoid counting syntax builder subproofs as lemmata);
3) L leaves exactly one theorem on the proof stack provided it is supplied with enough hypotheses (i.e. L is indeed a subproof, so subsequences like "0re, 0re" are not counted);
4) At least one of the theorems used in the subsequence L is used exactly once in the proof of T (otherwise minimizing with L would append an additional theorem label to the compressed proof of T, and likely that wouldn't minimize the proof).

Next we find all valid subsequences, and give each one a score by the formula (length - 1)*(number of theorems where it occurs). This gives an approximation to the number of saved bytes.

I did this search in set.mm for subsequences of lengths from 2 to 7, took top 20 of each length and combined into the following list:

https://gist.github.com/savask/13649ae9f1114544dd3d79f3ba01622f

The first component of each tuple is the subsequence and the second is its score.

For example, the first line is (["fvex","eqeltri"],791). By reverse-engineering the associated statement in mmj2 we get a reasonable theorem

${
  test1.1 $e |- A = ( F ` B ) $.
  test1 $p |- A e. _V $=
    ( cfv cvv fvex eqeltri ) ABCEFDBCGH $.
$}

If we take the line (["0re","1re","elicc2i"],88) we get

${
  test2 $p |- ( C e. ( 0 [,] 1 ) <-> ( C e. RR /\ 0 <_ C /\ C <_ 1 ) ) $=
    ( cc0 c1 0re 1re elicc2i ) BCADEF $.
$}

This is a version of elicc2i specialized to the unit interval. Apparently it is used quite often.

There are some mysterious proof subsequences in set.mm, for example consider (["toponunii","restid","ax-mp","eqcomi"],93). When expanded it gives

${
  test3.1 $e |- A e. C $.
  test3.2 $e |- A e. ( TopOn ` B ) $.
  test3 $p |- A = ( A |`t B ) $=
    ( crest co wcel wceq toponunii restid ax-mp eqcomi ) ABFGZAACHNAIDACBBAEJKLM $.
$}

This looks like a theorem with a completely useless hypothesis test3.1, but believe me or not, it does appear in some proofs, for example, in cncfcn1 (one can shorten its proof from 172 to 116 bytes using test3). If we correct the statement a little bit, we get a saner theorem

${
  test4.1 $e |- A e. ( TopOn ` B ) $.
  test4 $p |- A = ( A |`t B ) $=
  ( crest co ctopon wcel wceq toponunii restid ax-mp eqcomi cfv ) ABDEZAABFMZGNAHCAOBBACIJKL $.
$}

Which also minimizes the proof of cncfcn1 but this time to 98 bytes.

There are 120 proof sequences in the list I linked above, and surely not all of them deserve to be set.mm theorems (although many might indeed save byte usage, though I haven't been able to run a full minimize run with theorems test1-test4 as it's too resource intensive for my computer). I'm not an active set.mm contributor, so I don't know which theorems look reasonable, how to name them, where to put them in set.mm etc. If anyone is interested in this, I encourage them to take any theorem they like from the
list (including test1-test4) and add them into set.mm - no reference to me or the list is needed.

I would be glad to hear your opinions and suggestions.

[David A. Wheeler]

> On Jul 5, 2022, at 1:18 PM, savask <sav...@yandex.ru> wrote:
>
> In the post repeatedly re-proven statements David A. Wheeler found statements which appear in different proofs again and again. I decided to search for "repeatedly re-proven lemmata", i.e. sequences of theorem labels which often appear as sub-proofs in other theorems.

Awesome! Just like my approach that you cited, I think of such lists as an *indicator* of potential new theorems to add. Specific theorems should be created, then added or rejected on their own terms.

That said, I think adding *some* such theorems can help shorten some proofs. They can also simplify creating some proofs - tools can automatically detect when those patterns are matched & use them directly.

--- David A. Wheeler

[Alexander van der Vekens]

For example, the first line is (["fvex","eqeltri"],791). By reverse-engineering the associated statement in mmj2 we get a reasonable theorem

${
  test1.1 $e |- A = ( F ` B ) $.
  test1 $p |- A e. _V $=
    ( cfv cvv fvex eqeltri ) ABCEFDBCGH $.
$}

That's great, but I do not really know how to get this theorem (including its proof) from the sequence  ["fvex","eqeltri"]. How does the reverse-engineering work in mmj2?

[savask]

>That's great, but I do not really know how to get this theorem (including its proof) from the sequence  ["fvex","eqeltri"]. How does the reverse-engineering work in mmj2?

The sequence of labels "fvex", "eqeltri" is the sequence of essential steps in the compressed proof of our theorem. For example in metamath.exe:

MM>show proof test1/lemmon
 6 test1.1       $e |- A = ( F ` B )
 9 fvex          $p |- ( F ` B ) e. _V
10 6,9 eqeltri   $p |- A e. _V

To deduce the theorem from the sequence of labels in mmj2, I do as follows (note that there might be a better way). Start with a clean proof:

10::
qed::             |- ph

Then set the theorem in 10 to eqeltri and unify with Ctrl-U:

!d1::              |- &C1 = &C2
!d2::              |- &C2 e. &C3
10:d1,d2:eqeltri   |- &C1 e. &C3
qed::             |- ph

Now set the theorem in !d2 to fvex and unify:

!d1::              |- &C1 = ( &C5 ` &C4 )
d2::fvex           |- ( &C5 ` &C4 ) e. _V
10:d1,d2:eqeltri   |- &C1 e. _V
qed::             |- ph

Fill in the meta variables:

!d1::              |- A = ( F ` B )
d2::fvex           |- ( F ` B ) e. _V
10:d1,d2:eqeltri   |- A e. _V
qed::             |- ph

Finally, set step 10 to qed and rename all unproven steps to hypotheses (only !d1 in our case):

h1::test1.1       |- A = ( F ` B )
d2::fvex           |- ( F ` B ) e. _V
qed:1,d2:eqeltri   |- A e. _V

$=  ( test1.1 cfv cvv fvex eqeltri ) ABCEFDBCGH $.

For some reason mmj2 puts test1.1 into the label list, so it must be removed. We have a theorem with one essential hypothesis  |- A = ( F ` B ) and conclusion |- A e. _V. The proof is $=  ( cfv cvv fvex eqeltri ) ABCEFDBCGH $.

[Mario Carneiro]

This reminds me of another kind of analysis which I would like to do at some point, which I think amounts to a slightly generalized version of your analysis (most likely with even more blowup in the search space...).

If we think of a metamath proof as a tree of theorem applications, then we can identify commonly occurring subtrees. A subtree here would be some root theorem (which may occur as a step anywhere in the containing theorem), and then some choice of lemmas leading into it, and some lemmas leading to those lemmas and so on, where you can choose to cut the tree off at any hypothesis to get a leaf. For example, the test1 example corresponds to the subtree eqeltri(-, fvex()), but we could also look for e.g. eqeltri(0re(), -) or eqeltri(0re(), eqtri(-, -)) or any other subtree structure like that.

Once we have a subtree structure, we can uniquely reconstruct the theorem as the "most general unifier" of the applications. For example eqeltri(0re(), eqtri(-, -)) corresponds to the theorem:

$e |- 0 = A

$e |- A = B

$p |- B e. RR

(This is probably not a common occurrence; I haven't actually done the analysis.)

It's a bit more expensive of an analysis than looking for proof sequences (which correspond roughly to right-leaning subtrees) since you have to actually parse the proof into a tree/dag, but I still wonder about what things you could find.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/38398358-b9c1-4977-a7d8-acc44a631773n%40googlegroups.com.

[Alexander van der Vekens]

@savask thanks a lot for your detailed explanation how reverse engineering can be performed with mmj2. Following your "tutorial", I was able to create my first theorem (from No. 6 of your list):

h1::Test.1        |- ( ph -> X e. A )
h2::Test.2        |- ( ph -> th )
h3::Test.3        |- ( ph -> ta )
h4::Test.4        |- ( x = X -> ( ps <-> th ) )
h5::Test.5        |- ( x = X -> ( ch <-> ta ) )
d5:4,5:anbi12d   |- ( x = X -> ( ( ps /\ ch ) <-> ( th /\ ta ) ) )
d4:d5:rspcev       |- ( ( X e. A /\ ( th /\ ta ) ) -> E. x e. A ( ps /\ ch ) )
qed:1,2,3,d4:syl12anc
                   |- ( ph -> E. x e. A ( ps /\ ch ) )

with $d A x $. $d X x $.  $d ta x $. $d th x $.

But is this a useful theorem? Although it looks inconspicuous, I have run the minimize script looking for proofs using ~rspcev (there are more than 5000 of them), and stopped the script after more than 100 proofs were found which could be minimized by using the new theorem. This shows that there is a high potential that such theorems can be useful for a lot of minimizations.

[savask]

>But is this a useful theorem?

I personally don't think it is a very enlightening theorem, and I agree with David's comment that items in the list should be considered only as indicators of potential theorems.

I'm not sure there's a way to tell if a theorem is interesting automatically, but I can supplement the list with numbers of essential hypotheses for each suggested lemma. That way things like ["latjle12","syl13anc","mpbi2and"] with 9 essential hypotheses can be avoided.

[Benoit]

That's great, savask !  The list should be a good indicator of which lemmas to add.  The number of essential hypotheses could modulate it, as you proposed.  I'll try to have a look at them.  Right now, I see a few which are within propositional calculus, which should probably be added (I think, 7 in the first 24).  If you cut the list at the 24th, you have all the ones with score above 200, and all the ones with only two essential steps.  It could be a good idea to look at these first.

As for the useless hypothesis in test3 versus test4, it is probably due to shared subproofs: the proof of test3 is shorter, and in proofs containing it as a subproof, what corresponds to the hypothesis test3.1 was already proved for another subproof anyway, so the proof could as well use it with no extra cost.

Benoît

[savask]

Here's the list supplemented with the number of essential hypotheses (second column): https://gist.github.com/savask/dce5b48b7317e8144635fda09e983fae There are quite a few theorems with 0-1 hypotheses even among the ones with long proofs, so maybe it's worth looking at these first.

Jim Kingdon added theorem test4 to set.mm (thanks!), and as calculated by Alexander, a subsequent minimize_with run saved 2577 bytes. Theorem test4 was "inspired" by test3, which had score 93 in the table, so the savings were almost 30-fold of what was expected.

[Alexander van der Vekens]

To have the number of essential hypotheses available is very useful and interesting. I will have a closer look at the items no. 23, 27, 34/48 of the list (they require no hypotheses and contain interesting combinations of theorems). Unless the corresponding proofs look too awkward, and if they really help to shorten proofs significantly, I will add them to set.mm (together with the theorem corresponding to item no.6 which I mentioned before, although it has many hypotheses - maybe this could serve as example of the usefulness of such theorems).

[Benoit]

I'm just thinking of two things:

* Adding one of the theorems in the list may change the score of the others: for instance, the recently added theorem corresponding to

  93    2    ["toponunii","restid","ax-mp","eqcomi"]

probably changes the score of

  124    2    ["restid","ax-mp","eqcomi"]

which may not make it in the updated list anymore.  Maybe between these two, it would have been better to add only the latter, instead of only the former.

* As you said, there should still be some pondering before adding a theorem, even with a high score.  A possibility is that a theorem appears in this list because a proof pattern occurs often.  It could be that this proof pattern can be shortened in other ways, but if the theorem in the list is added, the resulting shortened proofs will not allow this kind of proof inspection.  Of course it's not specific to the present list: the more lemmas are used in a proof, the more difficult a global minimization is.  It's not necessarily bad, and there's always a balance to find.  Actually, I would generally prefer more reused lemmas, making for an often clearer proof, over a shorter but more cryptic proof.  I guess this has similarities with using a high-level language versus completely optimized but obscure assembly code.

Benoît

[savask]

>As you said, there should still be some pondering before adding a theorem, even with a high score.

I think the main criterion should be whether the suggested theorem makes any mathematical sense. For example, no. 6 from the list doesn't make any sense to me, and it's definitely not a theorem which would come to my mind when formalizing a proof. Thus I would argue against adding it to set.mm even if it saves a few kilobytes of the database size, since it would hinder readability of set.mm proofs.

On the other hand, test4 (now toponrestid in set.mm) looks like a reasonable lemma which was often re-proven over and over. Finding these kinds of lemmata is, I think, the ultimate goal.

> A possibility is that a theorem appears in this list because a proof pattern occurs often.  It could be that this proof pattern can be shortened in other ways, but if the theorem in the list is added, the resulting shortened proofs will not allow this kind of proof inspection.  Of course it's not specific to the present list: the more lemmas are used in a proof, the more difficult a global minimization is.

Perhaps a better solution then would be to run full minimize on affected theorems instead of minimize_with, so we can give metamath.exe a chance to shorten the proof in other ways before applying a new lemma?

[Benoit]

On Saturday, July 9, 2022 at 4:43:50 PM UTC+2 savask wrote:

On the other hand, test4 (now toponrestid in set.mm) looks like a reasonable lemma which was often re-proven over and over.

My first point above was about that particular example: now that the theorem corresponding to

  93    2    ["toponunii","restid","ax-mp","eqcomi"]

is in set.mm as "toponrestid", the score of

  124    2    ["restid","ax-mp","eqcomi"]

will probably drop and maybe it won't make it to your list anymore.  Maybe it would have been better to add only the theorem corresponding to that former suproof, rather than only toponrestid. (Maybe both will still make it, I can't tell; my point is that if only one makes it, then maybe it should not be toponrestid but the other one.)

 

Perhaps a better solution then would be to run full minimize on affected theorems instead of minimize_with, so we can give metamath.exe a chance to shorten the proof in other ways before applying a new lemma?

 

Unfortunately, "minimize_with" only sees "obvious minimizations", and I was thinking of more global minimizations using different proof methods.  I admit this is vague.  All this is to say that, indeed, human inspection is important concerning potential new additions, as you wrote.

Benoît

[Alexander van der Vekens]

On Saturday, July 9, 2022 at 4:05:20 PM UTC+2 Benoit wrote:

* As you said, there should still be some pondering before adding a theorem, even with a high score.  A possibility is that a theorem appears in this list because a proof pattern occurs often.  It could be that this proof pattern can be shortened in other ways, but if the theorem in the list is added, the resulting shortened proofs will not allow this kind of proof inspection.  Of course it's not specific to the present list: the more lemmas are used in a proof, the more difficult a global minimization is.  It's not necessarily bad, and there's always a balance to find.  Actually, I would generally prefer more reused lemmas, making for an often clearer proof, over a shorter but more cryptic proof.  I guess this has similarities with using a high-level language versus completely optimized but obscure assembly code.

 

Yes, I can confirm that Benoît's concerns are right: I reconstructed the followig theorem for list no. 34 ["2re","2pos","pm3.2i"]  (no. 48 is nearly the same) as I announced:

  2posre $p |- ( 2 e. RR /\ 0 < 2 ) $=
      ( c2 cr wcel cc0 clt wbr 2re 2pos pm3.2i ) ABCDAEFGHI $.

But this is only the expanded form of ~2rp, and looking at proofs using `2 e. RR` and `0 < 2` (i.e., ~2re and ~2pos), such proofs can be shortened more elegantly making use of `2 e. RR*`. For example, the proof of ~amgm2 can be shortened by using ~lemuldiv2d instead of ~lemuldiv2 (this must have been done manually, minimize_with did not shorten anything). Since ~2pos is not needed/used anymore, a new theorem ~2posre would not help to shorten this proof further. Furthermore, using  ~lemuldiv2d better fits to our preferred "deduction style". Therefore, I will not add  ~2posre to set.mm (but will contribute the shortened proofs of ~amgm2 and a few others with my next PR).

 

[Alexander van der Vekens]

On Saturday, July 9, 2022 at 6:41:27 PM UTC+2 Alexander van der Vekens wrote:

But this is only the expanded form of ~2rp, and looking at proofs using `2 e. RR` and `0 < 2` (i.e., ~2re and ~2pos), such proofs can be shortened more elegantly making use of `2 e. RR*`.

Sorry, I mean `2 e. RR+` of course.