metamath.exe - added "/extract" to "write source"
164 views
Skip to first unread message
Norman Megill
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".
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
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
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
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
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
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
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
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
Jun 24, 2022, 8:19:00 AM6/24/22
to Metamath
Is it possible to automatically remove all comments from the extracted theory?
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
Jul 10, 2022, 9:52:17 AM7/10/22
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