metamath.exe - added "/extract" to "write source"

130 views
Skip to first unread message

Norman Megill

unread,
Sep 4, 2020, 11:04:01 PM9/4/20
to Metamath
The amount of material in set.mm has grown quite large and may be overwhelming for someone who just wants to see what is needed to prove a particular theorem of interest.

Organizing set.mm with section headings and splitting it into modules help but only partially address the problem.  "show trace_back" does show only the earlier theorems that are needed, but it isn't user friendly in the sense that it can be easily browsed, and it doesn't aggregate the traces of multiple statements.

In metamath version 0.192 ( http://us2.metamath.org/index.html#mmprog ), "write source" has a new qualifier, "/extract <label-list>", which will create a self-contained database containing exactly and only the axioms and theorems needed to prove <label-list>, as well as the section headings relevant to them.  For example, after "read set.mm",

    MM> write source xyz.mm /extract exmid,canth

will extract everything needed to prove exmid and canth, and nothing more.  (See "help search" for the format of <label-list>.  For example, "/extract ax-mp~stoic4b" will extract all of propositional calculus.)

A possible use for this is to create a miniature local website for the extracted xyz.mm, which can be used as a self study guide, for example.  To do this, download metamathsite.zip from the Metamath Home Page, unzip it, create the subdirectory mpeuni, and copy the content of the mpegif subdirectory as well as xyz.mm to it.  Assuming the metamath program is in your path, run from inside the mpeuni directory

metamath "read xyz.mm" \
    "write theorem_list /alt_html /show_lemmas" \
    "show statement */alt_html"  \
    "exit"


Some notes:

1. A "~ <label>" in a comment may sometimes refer to a theorem that no longer exists in the extracted database.  When this happens, it is converted to a link to the corresponding page on us.metamath.org.

2. If you do "write source xyz.mm /extract *" i.e. extract everything, it doesn't reproduce set.mm exactly although it's functionally equivalent.  This is because it extracts the statements individually then uses them to reconstruct the output file, discarding unrelated content.  (There are some interesting differences such as orphan $c's, redundant $d's, and headers deleted because there are no statements between them and the next same- or higher-level header.)  However, "verify proof *" and "verify markup */f" will pass, and the output of "write theorem_list /a/s" will be identical.

3. File inclusion markup ("$( Begin $[...") and $j comments are currently not included.  If people need these, I could try to put them in, but it would take some work to figure out which ones are relevant to the extracted statements.  However, the output .mm is primarily intended for read-only display purposes rather than development.

4. If you are puzzled about why an apparently unrelated earlier theorem is included, use the "/to" option of "show trace_back".

Alexander van der Vekens

unread,
Sep 5, 2020, 2:46:44 AM9/5/20
to Metamath
That's sound really great! I will try this new feature soon, using the friendship theorem as "root"...

Glauco

unread,
Sep 5, 2020, 5:08:08 PM9/5/20
to Metamath
> In metamath version 0.192 ( http://us2.metamath.org/index.html#mmprog ), "write source" has a new qualifier, "/extract <label-list>",
> which will create a self-contained database containing exactly and only the axioms and theorems needed to prove <label-list>  
> A possible use for this is to create a miniature local website for the extracted xyz.mm, which can be used as a self study guide

Very nice feature

Glauco

Norman Megill

unread,
Sep 5, 2020, 5:56:58 PM9/5/20
to Metamath
On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der Vekens wrote:
That's sound really great! I will try this new feature soon, using the friendship theorem as "root"...
 
Good choice. I was curious so I added it (temporarily) here:

http://us2.metamath.org/ocat/friendship/mmtheorems.html

Who would have known that it depends on Stoic logic? :)

I wrote about something similar that included the /extract functionality (but with a much more ambitious goal in mind) in 2014:

https://groups.google.com/g/metamath/c/hrtD9_wAcHM/m/fHL85-Hx5usJ

set.mm was put on GitHub about 6 months later, addressing some of the issues I brought up, and the idea of extract/merge was put on hold. But I've always felt /extract could provide insight about a particular theorem, and if nothing else would give you an idea of what background you need to understand it fully.

Norm
 

Mario Carneiro

unread,
Sep 5, 2020, 6:19:34 PM9/5/20
to metamath
The Metamath -> MM0 importer already contains a feature for selecting which target theorems you want, so it has the same effect as using /extract on the source database first and then importing it. I've been using numbers for example theorems like dirith or pnt in my talks. I wonder what is the maximum fraction of set.mm you can get by /extracting a single theorem...?

Mario


--
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/718e5102-91c9-4215-94c0-50fb53387b70n%40googlegroups.com.

Alexander van der Vekens

unread,
Sep 6, 2020, 2:59:28 AM9/6/20
to Metamath
On Saturday, September 5, 2020 at 11:56:58 PM UTC+2 Norman Megill wrote:
On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der Vekens wrote:
That's sound really great! I will try this new feature soon, using the friendship theorem as "root"...
 
Good choice. I was curious so I added it (temporarily) here:

http://us2.metamath.org/ocat/friendship/mmtheorems.html

Who would have known that it depends on Stoic logic? :)
 
Really impressive: so the friendship theorem depends on about 6500 theorems (of about 25000 in main set.mm, that is about one fourth!). And it depends only on about 300 theorems about graph theory itself. It will be exiting to analyse these dependencies in more detail... 

Norman Megill

unread,
Sep 6, 2020, 9:20:29 AM9/6/20
to Metamath
On Saturday, September 5, 2020 at 6:19:34 PM UTC-4 di.... gmail.com wrote:
The Metamath -> MM0 importer already contains a feature for selecting which target theorems you want, so it has the same effect as using /extract on the source database first and then importing it. I've been using numbers for example theorems like dirith or pnt in my talks. I wonder what is the maximum fraction of set.mm you can get by /extracting a single theorem...?

I did this for all theorems in set.mm, and below are the 63 requiring > 8000 $p's.  It looks like dirith uses the most in terms of $p count.   I didn't save the extracted .mms, but re-running it on 3 of them, dirith.mm has 6994793 bytes, fouriersw.mm has 7026106 bytes, and pnt.mm has 5665034 bytes.  For comparison, the current set.mm has 36616 $p,  2587 $a, and 39486525 bytes.  BTW $a includes both |- and syntax statements, so the number of axioms and definitions is about half the $a count.

 8019 $p  557 $a  pntlemp
 8024 $p  557 $a  pntleml
 8030 $p  620 $a  dchrisum0flblem2
 8032 $p  620 $a  dchrisum0flb
 8033 $p  559 $a  areacirc
 8041 $p  622 $a  dchrmusum2
 8049 $p  557 $a  pnt3
 8049 $p  596 $a  meascnbl
 8049 $p  600 $a  coinflippvt
 8051 $p  557 $a  pnt2
 8053 $p  557 $a  pnt
 8075 $p  596 $a  omssubadd
 8076 $p  560 $a  etransclem23
 8077 $p  616 $a  dchrisum0lem2a
 8080 $p  616 $a  dchrisum0lem2
 8114 $p  608 $a  dstfrvclim1
 8145 $p  624 $a  dchrvmasumlem3
 8149 $p  624 $a  dchrvmasumiflem1
 8172 $p  628 $a  dchrisum0fno1
 8187 $p  554 $a  fourierdlem111
 8237 $p  620 $a  dchrisum0lem3
 8244 $p  568 $a  etransclem46
 8248 $p  604 $a  omsmeas
 8271 $p  620 $a  rpvmasumlem
 8278 $p  552 $a  fourierdlem103
 8278 $p  552 $a  fourierdlem104
 8313 $p  562 $a  stirling
 8334 $p  564 $a  stirlingr
 8417 $p  554 $a  fourierdlem112
 8431 $p  630 $a  dchrvmasumiflem2
 8447 $p  640 $a  dchrpt
 8455 $p  574 $a  etransclem47
 8465 $p  554 $a  fourierdlem113
 8480 $p  554 $a  fourierdlem114
 8481 $p  554 $a  fourierdlem115
 8482 $p  554 $a  fourierclimd
 8482 $p  554 $a  fourierd
 8483 $p  554 $a  fourier
 8483 $p  554 $a  fourierclim
 8483 $p  554 $a  fouriercnp
 8484 $p  554 $a  fouriercn
 8486 $p  554 $a  fourier2
 8498 $p  632 $a  dchrvmasumif
 8517 $p  574 $a  etransclem48
 8542 $p  576 $a  etransc
 8563 $p  556 $a  fouriersw
 8595 $p  654 $a  sumdchr2
 8603 $p  654 $a  dchrhash
 8604 $p  654 $a  sumdchr
 8641 $p  658 $a  sum2dchr
 8653 $p  684 $a  sitgaddlemb
 9313 $p  678 $a  rpvmasum2
 9331 $p  678 $a  dchrisum0re
 9428 $p  682 $a  dchrisum0
 9429 $p  682 $a  dchrisumn0
 9429 $p  682 $a  rpvmasum
 9430 $p  682 $a  dchrmusumlem
 9430 $p  682 $a  dchrvmasumlem
 9431 $p  682 $a  dchrmusum
 9431 $p  682 $a  dchrvmasum
 9502 $p  684 $a  rplogsum
 9505 $p  684 $a  dirith2
 9506 $p  684 $a  dirith

Norm

Glauco

unread,
Jun 24, 2022, 8:19:00 AMJun 24
to Metamath
Is it possible to automatically remove all comments from the extracted theory?

I need to build "small" theories for unit testing my code.

I can, of course, pipeline the /extract step with a subsequent /removeComments step (if the "remove comment" feature is present in metamath.exe)


Thanks in advance
Glauco

Glauco

unread,
Jul 10, 2022, 9:52:17 AMJul 10
to Metamath
May be some code could be written, as an alternative to /extract  (it extracts some statements that are not needed and, in some cases, it does not extract some syntactic axioms that would be useful for proof assistants).

In the meanwhile, this regexp works well in VSCode, to remove all comments (replace it with an empty string)

\$\((.|\n)+?\$\)


Then this regexp

^$\n

can be used to remove empty lines and get a "compact" theory.


Glauco
Reply all
Reply to author
Forward
0 new messages