List of most frequently used assertions

[Kyle Wyonch]

Hello all,

I was wondering if it is possible to create a list of the most frequently used assertions in set.mm using the commands of the Metamath program.  I know that the description of syl has the next five most popularly referenced assertions, but I would like to extend this out to the next 100, or 1000 most referenced.

Thanks in advanced,

[Norman Megill]

There's no command to show such a list directly, but it can be constructed from information provided by the program.  There are many ways to do this (and maybe someone has a better way) but here is one way:

MM> open log usage.txt

MM> show usage *
Statement "a1ii" is not referenced in the proof of any statement.
  (None)
Statement "idi" is directly referenced in the proofs of 15 statements:
  opfi1uzind opfi1uzindOLD opphllem2 madjusmdetlem2 frege55lem2a fsovrfovd
  imo72b2lem0 ssmapsn fprodcnlem dvmptfprod dvnprodlem1 sge0f1o ovncvr2 pfxcl
  rngcifuestrc
Statement "wn" is directly referenced in the proofs of 7242 statements:
  con4i con4d pm2.21i pm2.21d pm2.21 pm2.24 pm2.18 pm2.18i pm2.18d notnotr
...

MM> close log

You can then grep for "referenced in the proof" in usage.txt, which will extract the lines with the usage numbers, then you can sort those lines.

If you don't want the syntax axioms like "wn", you can extract all non-syntax $a and $p labels from the output of "search * '|-'".  You can prefix this label list with "show usage " then use it as a command file for the "submit" command in metamath.exe,  instead of the "show usage *" command that I show above.

If you don't have a bash shell, the "tools" command provides processing functions that can accomplish what you need (extracting labels, sorting, etc.), if less efficiently.  Sometimes I use it just because unlike bash tools, there are no special characters to remember to escape (other than quotes inside of a quoted string) that can make matching set.mm graphics symbols tricky.

Whether to make an actual script as opposed to just typing in the commands is up to you, depending on whether this is a one-off effort.  Even if I planned to build a script, I would probably type them in first, saving everything to a log file, and use that to guide constructing a script once I'm happy with the output.

Norm

[Alexander van der Vekens]

  I think the list of the most commonly referenced assertion in set.mm, mentioned in the comment of ~syl, is not up-to-date anymore. Running show usage * for the mentioned assertion yields:

~ syl:  13447
~ eqid: 9597
~ syl2anc: 7420
~ adantr: 8858
~ syl3anc: 5432
~ ax-mp: 4726

~syl2anc and ~adantr changed places in the meantime.

And ~adantl is used 6401 times, ~simpr 5828 -> that would be places 5 and 6!

[Norman Megill]

Feel free to update the comment in your next PR. :)

[Alexander van der Vekens]

On Wednesday, July 21, 2021 at 3:31:19 PM UTC+2 Norman Megill wrote:

Feel free to update the comment in your next PR. :)

=> Done!