Analysis of full 'minimize' run on set.mm

[Norman Megill]

All jobs from 101 to 158 have completed.  Many thanks to all who contributed CPU time!  Jobs 159 and 160 are still running, but we will handle those manually later.  Therefore we are ready to start the final analysis.

I put all of the logs except 159 and 160 here:  http://us2.metamath.org/downloads/min2020-logs.zip

Other links for reference:
'minimize' scripts: http://us2.metamath.org/downloads/min2020-jobs.zip
Job status:  https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ
Estimates vs. actual run times:  https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ
2018 'minimize' scripts:  http://us2.metamath.org/downloads/min2018-jobs.zip
2018 logs:  http://us2.metamath.org/downloads/min2018-logs.zip

Before performing the final minimize run, we need to make sure it will do what we expect.  Below are some greps I used to flag some unusually large size reductions that we probably want to look at.  (The 'uniq' is to get rid of identical lines from the forward and backward 'minimize' scans.  I also edited out some duplicates where the 'from' number was different for the two scans, as well as a couple that I will take care of myself.)  If anyone identifies other suspicious minimizations (with better grep ranges, manual inspection of the logs, etc.), please post here.

Many of the suspect cases are in various mathboxes, and it would be best if mathbox users review the minimizations done on their mathboxes.

We should edit set.mm to prevent unwanted minimizations rather than editing the final minimize job, so that we don't have to do this same analysis for next year's run.  For example, ~ eqeq1dALT should have "(Proof modification is discouraged.)" in its description to prevent overwriting its proof with ~ eqeq1d.

I'm not sure what the best way to maintain the results of the analysis.  Google Documents is a possibility, but I've never used it; someone else would have to volunteer to set it up and post instructions for people like me.  Alternately, I could maintain a fixed post that I edit as people respond to this post, like I did for the job status - maybe I'll start off doing that.

In the end I'd like to have each minimization accompanied by a recommendation e.g.

    job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using "mptfzshft".
      Resolution: ok (NM)

    job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using "eqeq1d".
      Resolution: discourage proof modification of eqeq1dALT (WL)

The initials would indicate who analyzed the case and, if not ok, who will make the modification to set.mm.

Norm



$ grep '[0-9]... to [1-3].. bytes' job*.log | uniq
job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using "mptfzshft".

$ grep '[2-9].. to [4-9]. bytes' job*.log | uniq
job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using "ncolcom".
job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using "gsumsnd".
job109.log:Proof of "fz0hash" decreased from 207 to 98 bytes using "hashfz0".
job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using "grpbase".
job132.log:Proof of "euhash1" decreased from 514 to 93 bytes using "hashen1".
job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using "ioodvbdlimc1lem

$ grep 'to [1-3]. bytes' job*.log | uniq
job101.log:Proof of "bj-bi3ant" decreased from 84 to 21 bytes using "bi3antOLD".
job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using "eqeq1d".
job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
job102.log:Proof of "frege53aid" decreased from 58 to 33 bytes using "com12".
job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using "ifbieq12d".
job102.log:Proof of "mplrcl" decreased from 170 to 38 bytes using "strov2rcl".
job103.log:Proof of "frege24" decreased from 55 to 19 bytes using "rp-frege24".
job103.log:Proof of "hashssle" decreased from 447 to 19 bytes using "hashss".
job103.log:Proof of "tsor2" decreased from 55 to 39 bytes using "imori".
job104.log:Proof of "aevALT" decreased from 90 to 14 bytes using "aev".
job104.log:Proof of "frege25" decreased from 55 to 20 bytes using "rp-frege25".
job104.log:Proof of "tsor3" decreased from 59 to 39 bytes using "imori".
job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using "gsumsnfd".
job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using "perpdragALT".
job108.log:Proof of "leimnltd" decreased from 50 to 19 bytes using "lensymd".
job108.log:Proof of "orcomdd" decreased from 60 to 31 bytes using "syl6".
job109.log:Proof of "bj-bisym" decreased from 39 to 18 bytes using "bisymOLD".
job109.log:Proof of "fseq0hash" decreased from 88 to 16 bytes using "ffzohash".
job109.log:Proof of "symgfixfvh" decreased from 116 to 32 bytes using "fvtresfn".
job110.log:Proof of "bj-hbsb3" decreased from 50 to 15 bytes using "hbsb3".
job110.log:Proof of "bj-nfs1" decreased from 42 to 14 bytes using "nfs1".
job110.log:Proof of "frege55aid" decreased from 30 to 14 bytes using "bicom1".
job110.log:Proof of "sbequ8ALT" decreased from 72 to 15 bytes using "sbequ8".
job111.log:Proof of "frege55b" decreased from 138 to 15 bytes using "equcomi".
job112.log:Proof of "equsb3ALT" decreased from 96 to 15 bytes using "equsb3".
job112.log:Proof of "rp-simp2" decreased from 33 to 14 bytes using "simp2".
job113.log:Proof of "rp-simp2-frege" decreased from 39 to 34 bytes using "rp-a1i".
job114.log:Proof of "cleqf" decreased from 59 to 35 bytes using "nfcrii".
job114.log:Proof of "vdgfrgra0" decreased from 495 to 17 bytes using "vdfrgra0".
job115.log:Proof of "AnelBC" decreased from 61 to 32 bytes using "nelir".
job115.log:Proof of "nfnfcALT" decreased from 89 to 15 bytes using "nfnfc".
job116.log:Proof of "rexbidvaALT" decreased from 26 to 20 bytes using "rexbidva".
job116.log:Proof of "sbceq1ddi2" decreased from 105 to 38 bytes using "sbceq1ddi".
job116.log:Proof of "wl-equsal" decreased from 86 to 18 bytes using "equsal".
job117.log:Proof of "adant423" decreased from 56 to 39 bytes using "sylancom".
job117.log:Proof of "frege39" decreased from 56 to 34 bytes using "rp-frege2i".
job117.log:Proof of "rexbidvALT" decreased from 25 to 19 bytes using "rexbidv".
job118.log:Proof of "pirp2" decreased from 72 to 30 bytes using "elrpii".
job119.log:Proof of "rp-frege2ii" decreased from 47 to 37 bytes using "rp-frege2i".
job120.log:Proof of "eleq2dALT" decreased from 165 to 17 bytes using "eleq2d".
job120.log:Proof of "frege57aid" decreased from 58 to 11 bytes using "bi2".
job120.log:Proof of "impel" decreased from 61 to 35 bytes using "syl2anr".
job120.log:Proof of "rp-frege2iii" decreased from 51 to 32 bytes using "rp-frege2ii".
job122.log:Proof of "cbvald" decreased from 41 to 34 bytes using "nfvd".
job123.log:Proof of "ex3" decreased from 53 to 35 bytes using "3impa".
job124.log:Proof of "3expc" decreased from 26 to 16 bytes using "exp31".
job124.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1".
job124.log:Proof of "frege58bcor" decreased from 64 to 16 bytes using "spsbim".
job125.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using "dveeq2".
job125.log:Proof of "tgiooss" decreased from 218 to 17 bytes using "rerest".
job125.log:Proof of "wl-sb6nae" decreased from 63 to 13 bytes using "sb4b".
job126.log:Proof of "adantlllr" decreased from 47 to 21 bytes using "adantl3r".
job126.log:Proof of "ax12a2" decreased from 55 to 26 bytes using "ax12v".
job127.log:Proof of "absnpncand" decreased from 148 to 21 bytes using "abs3difd".
job127.log:Proof of "ad5ant1345" decreased from 54 to 21 bytes using "adantl3r".
job127.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using "ax16nf".
job130.log:Proof of "bf-frege55a" decreased from 73 to 23 bytes using "bj-frege55lem2a".
job130.log:Proof of "bj-csbprc" decreased from 157 to 15 bytes using "csbprc".
job130.log:Proof of "nn0ge2m1nnALT" decreased from 172 to 17 bytes using "nn0ge2m1nn".
job131.log:Proof of "bf-frege55cor1a" decreased from 74 to 14 bytes using "bicom1".
job131.log:Proof of "ccat2s1fvwALT" decreased from 477 to 21 bytes using "ccat2s1fvw".
job131.log:Proof of "wl-sbal1" decreased from 97 to 15 bytes using "sbal1".
job132.log:Proof of "4an31" decreased from 67 to 37 bytes using "sylanb".
job132.log:Proof of "frege52b" decreased from 42 to 16 bytes using "sbequi".
job132.log:Proof of "wl-sbal2" decreased from 97 to 15 bytes using "sbal2".

[Mario Carneiro]

Job 160 is done, after 99.7 hours of CPU time. (I think it was done yesterday, but I got confused with the state of the process and didn't want to mess with it.)

It found one lemma, saving 5 bytes.

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/67c66042-7193-4eec-abd2-db9e3d0364ca%40googlegroups.com.

[Alexander van der Vekens]

 Hi Norm, I had a look at the first two blocks. See my remarks/recommendations below.

Alexander

On Friday, February 21, 2020 at 4:28:24 AM UTC+1, Norman Megill wrote:

$ grep '[0-9]... to [1-3].. bytes' job*.log | uniq
job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using "mptfzshft".

 ~frprodshft (contributed in Jan 2018, used 2 times) is in SF's mathbox, ~mptfzshft (contributed in Aug 2019) is in main set. I think both should be kept, shortening proof of frprodshft (will still have 13 essential lines) should be OK.

$ grep '[2-9].. to [4-9]. bytes' job*.log | uniq
job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using "ncolcom".

Both contibuted by TA, he should decide (From my point of view shortening is OK)

job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using "gsumsnd".

  ~gsumsn2 (contributed in Jan 2017, used only once) is in TA's mathbox, ~gsumsnd (contributed in Jan 2019) is in main set. I think ~gsumsn2 could be deleted, replaced by ~gsumsnd in proof of ~esumsn.

Maybe the tags for ~gsumsnd could be changed to "(Contributed by TA, 30-Jan-2017.)  (Proof shortened by AV, 11-Dec-2019.) $)" after the deletion of ~gsumsn.

job109.log:Proof of "fz0hash" decreased from 207 to 98 bytes using "hashfz0".

 ~fz0hash(contributed in Jun 2018, used 3 times) and ~hashfz0 (contributed in Jul 2018) both in main set. I think both should be kept, shortening proof of ~fz0hash is OK.

job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using "grpbase".

 ~signswbase (contributed in Sep 2018, used 6 times) is in TA's mathbox, ~grpbase (contributed in Aug 2013) is in main set. I think both should be kept, shortening proof of ~signswbase is OK.

 

job132.log:Proof of "euhash1" decreased from 514 to 93 bytes using "hashen1".

  ~euhash1 (contributed in Feb 2018, used only once) and ~hashen1 (contributed in Apr 2019) both in main set. I think both should be kept, shortening proof of ~euhash1 is OK.

job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using "ioodvbdlimc1lem

 ~fourierdlem45 (contributed in Dec 2019, not used!), ~ioodvbdlimc1lem does not exist (cut off at the end?), only ~ioodvbdlimc1lem1 and ~ioodvbdlimc1lem2 all in GS's mathbox. I think  ~fourierdlem45 could be deleted (but GS has to decide). 

[Norman Megill]

Thanks.  Looking at the end of the log file, it seems the job didn't complete.  99.7 hrs seems like an unusual number - could there have been a 100 hr timeout?

  Scanning forward through statements...
  Proof of "mideulem" decreased from 7532 to 7527 bytes using "ad2antrr".
  359212.21user 5.68system 99:48:42elapsed 99%CPU (0avgtext+0avgdata 1864856maxresident)k
  0inputs+40outputs (0major+667317minor)pagefaults 0swaps

BTW each printf in metamath.exe has an fflush(stdout) after it, so presumably there is no buffering that would truncate the log.

Anyway, DAW recently started running job160 in parallel as a backup.  Since your forward 'minimize' scan didn't complete, your run tells us it will take more than 200 hrs.  In any case, for the purpose of set.mm, Thierry has broken up ~mideulem into 3 theorems, and we can minimize those separately.  Therefore at this point the only purpose of completing job 160 is to get an actual time to compare to the 403-hr estimate to help future estimates.  You don't need to restart your run.  We'll let DAW run his for weeks, if he is willing, and see what comes through.

Norm

[David A. Wheeler]

On Fri, 21 Feb 2020 06:54:38 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> We'll let DAW run his for
> weeks, if he is willing, and see what comes through.

Indeed.

I suggest that anyone who's run this minimization on Linux
report their bogomips. There are a long list of flaws
with the bogomips measure (hence the name),
but it's an estimate of CPU speed that's really easy to get.

You can find this value by running this:
grep bogomips /proc/cpuinfo

I see 8 copies of this (one for each of the 8 CPUs):
bogomips : 5799.99

--- David A. Wheeler

[Alexander van der Vekens]

 Hi Norm, I had a look at many entries of the third block. The remaining entries should be reviewed by others. See my remarks/recommendations below.

Alexander

On Friday, February 21, 2020 at 4:28:24 AM UTC+1, Norman Megill wrote:

$ grep 'to [1-3]. bytes' job*.log | uniq
job101.log:Proof of "bj-bi3ant" decreased from 84 to 21 bytes using "bi3antOLD".
job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using "eqeq1d".

"eqeq1dALT" should be tagged with "(Proof modification is discouraged.)"

job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
job102.log:Proof of "frege53aid" decreased from 58 to 33 bytes using "com12".
job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using "ifbieq12d".

ifeq123d in GS's mathbox: usage should be replaced by ifbieq12d, and ifeq123d should be
deleted afterwards (see my remark within the comment)

job102.log:Proof of "mplrcl" decreased from 170 to 38 bytes using "strov2rcl".

used 6 times, shortening OK, both should be kept

job103.log:Proof of "frege24" decreased from 55 to 19 bytes using "rp-frege24".
job103.log:Proof of "hashssle" decreased from 447 to 19 bytes using "hashss".

hashssle in GS's mathbox: usage (2 times) should be replaced by hashss,
and hashssle should be deleted afterwards 

job103.log:Proof of "tsor2" decreased from 55 to 39 bytes using "imori".

job104.log:Proof of "aevALT" decreased from 90 to 14 bytes using "aev".

"aevALT" should be tagged with "(Proof modification is discouraged.)"

job104.log:Proof of "frege25" decreased from 55 to 20 bytes using "rp-frege25".
job104.log:Proof of "tsor3" decreased from 59 to 39 bytes using "imori".

job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using "gsumsnfd".

gsumsndf in AV's mathbox: usage (only once) should be replaced by gsumsnfd,
and gsumsndf should be deleted afterwards

job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using "perpdragALT".
job108.log:Proof of "leimnltd" decreased from 50 to 19 bytes using "lensymd".

leimnltd in GS's mathbox: not used, should be deleted

job108.log:Proof of "orcomdd" decreased from 60 to 31 bytes using "syl6".

orcomdd in GM's mathbox: usage (2 times) should be replaced by hashss
and hashssle should be deleted afterwards, or both should be kept, shortening OK 

job109.log:Proof of "bj-bisym" decreased from 39 to 18 bytes using "bisymOLD".
job109.log:Proof of "fseq0hash" decreased from 88 to 16 bytes using "ffzohash".

Identical, one of them can be replaced by the other and removed afterwards

job109.log:Proof of "symgfixfvh" decreased from 116 to 32 bytes using "fvtresfn".

usage of symgfixfvh should be replaced by fvtresfn and removed afterwards

job110.log:Proof of "bj-hbsb3" decreased from 50 to 15 bytes using "hbsb3".
job110.log:Proof of "bj-nfs1" decreased from 42 to 14 bytes using "nfs1".
job110.log:Proof of "frege55aid" decreased from 30 to 14 bytes using "bicom1".
job110.log:Proof of "sbequ8ALT" decreased from 72 to 15 bytes using "sbequ8".

"sbequ8ALT" should be tagged with "(Proof modification is discouraged.)"

job111.log:Proof of "frege55b" decreased from 138 to 15 bytes using "equcomi".
job112.log:Proof of "equsb3ALT" decreased from 96 to 15 bytes using "equsb3".

"equsb3ALT" should be tagged with "(Proof modification is discouraged.)"

job112.log:Proof of "rp-simp2" decreased from 33 to 14 bytes using "simp2".
job113.log:Proof of "rp-simp2-frege" decreased from 39 to 34 bytes using "rp-a1i".
job114.log:Proof of "cleqf" decreased from 59 to 35 bytes using "nfcrii".
job114.log:Proof of "vdgfrgra0" decreased from 495 to 17 bytes using "vdfrgra0".

Identical, vdgfrgra0 can be deleted (is not used anyway)

job115.log:Proof of "AnelBC" decreased from 61 to 32 bytes using "nelir".
job115.log:Proof of "nfnfcALT" decreased from 89 to 15 bytes using "nfnfc".

"nfnfcALT" should be tagged with "(Proof modification is discouraged.)"

job116.log:Proof of "rexbidvaALT" decreased from 26 to 20 bytes using "rexbidva".

"nfnfcALT" should be tagged with "(Proof modification is discouraged.)"
("rexbida" in comment should be replaced by "rexbidva")

job116.log:Proof of "sbceq1ddi2" decreased from 105 to 38 bytes using "sbceq1ddi".

Identical, sbceq1ddi2 can be deleted (is not used anyway)

job116.log:Proof of "wl-equsal" decreased from 86 to 18 bytes using "equsal".
job117.log:Proof of "adant423" decreased from 56 to 39 bytes using "sylancom".
job117.log:Proof of "frege39" decreased from 56 to 34 bytes using "rp-frege2i".
job117.log:Proof of "rexbidvALT" decreased from 25 to 19 bytes using "rexbidv".

"rexbidvALT" should be tagged with "(Proof modification is discouraged.)"

job118.log:Proof of "pirp2" decreased from 72 to 30 bytes using "elrpii".
job119.log:Proof of "rp-frege2ii" decreased from 47 to 37 bytes using "rp-frege2i".
job120.log:Proof of "eleq2dALT" decreased from 165 to 17 bytes using "eleq2d".

"eleq2dALT" should be tagged with "(Proof modification is discouraged.)"

job120.log:Proof of "frege57aid" decreased from 58 to 11 bytes using "bi2".
job120.log:Proof of "impel" decreased from 61 to 35 bytes using "syl2anr".
job120.log:Proof of "rp-frege2iii" decreased from 51 to 32 bytes using "rp-frege2ii".
job122.log:Proof of "cbvald" decreased from 41 to 34 bytes using "nfvd".

used 15 times, shortening OK, both should be kept

job123.log:Proof of "ex3" decreased from 53 to 35 bytes using "3impa".
job124.log:Proof of "3expc" decreased from 26 to 16 bytes using "exp31".
job124.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1".

"dral1ALT" should be tagged with "(Proof modification is discouraged.)"

job124.log:Proof of "frege58bcor" decreased from 64 to 16 bytes using "spsbim".
job125.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using "dveeq2".

"dveeq2ALT" should be tagged with "(Proof modification is discouraged.)"

job125.log:Proof of "tgiooss" decreased from 218 to 17 bytes using "rerest".

tgiooss in GS's mathbox: usage (3 times) should be replaced by rerest,
and tgiooss should be deleted afterwards 

job125.log:Proof of "wl-sb6nae" decreased from 63 to 13 bytes using "sb4b".
job126.log:Proof of "adantlllr" decreased from 47 to 21 bytes using "adantl3r".
job126.log:Proof of "ax12a2" decreased from 55 to 26 bytes using "ax12v".
job127.log:Proof of "absnpncand" decreased from 148 to 21 bytes using "abs3difd".

absnpncand in GS's mathbox: usage (2 times) should be replaced by abs3difd,
and absnpncand should be deleted afterwards 

job127.log:Proof of "ad5ant1345" decreased from 54 to 21 bytes using "adantl3r".
job127.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using "ax16nf".
job130.log:Proof of "bf-frege55a" decreased from 73 to 23 bytes using "bj-frege55lem2a".
job130.log:Proof of "bj-csbprc" decreased from 157 to 15 bytes using "csbprc".
job130.log:Proof of "nn0ge2m1nnALT" decreased from 172 to 17 bytes using "nn0ge2m1nn".

"nn0ge2m1nnALT" should be tagged with "(Proof modification is discouraged.)"

job131.log:Proof of "bf-frege55cor1a" decreased from 74 to 14 bytes using "bicom1".
job131.log:Proof of "ccat2s1fvwALT" decreased from 477 to 21 bytes using "ccat2s1fvw".

"ccat2s1fvwALT" should be tagged with "(Proof modification is discouraged.)"

[Glauco]

job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using "ioodvbdlimc1lem

 ~fourierdlem45 (contributed in Dec 2019, not used!), ~ioodvbdlimc1lem does not exist (cut off at the end?), only ~ioodvbdlimc1lem1 and ~ioodvbdlimc1lem2 all in GS's mathbox. I think  ~fourierdlem45 could be deleted (but GS has to decide). 

~ fourierdlem45 was originally intended as a specific lemma for ~ fourierd , but later on it was replaced by ioodvbdlimc1lem1 in order to prove ~ ioodvbdlimc1 , that will probably be useful on its own.

I suggest to apply the minimization, in order to save space ( but I plan to remove ~ fourierdlem45 in a future commit, with the proper renumbering of other lemmas )

Thanks for your analysis

Glauco

[fl]

How many bytes saved eventually?

-- 

FL

[Norman Megill]

Thank you, Alexander and Glauco.  I'd like to hear from Benoit and Wolf who have a number of theorems in these lists.  After that I'll organize it into the final list of actions we'll take. (I will probably do the necessary editing of set.mm myself to prevent confusion or conflict.)

Here are some more ALT cases (with duplicates removed):

$ grep 'using ".*ALT"' j*g
job116.log:Proof of "climf" decreased from 873 to 872 bytes using "rexbidvALT".   <- use rexbidv instead
job147.log:Proof of "fourierdlem65" decreased from 9585 to 9567 bytes using "rexbidvALT".   <- use rexbidv instead

$ grep 'Proof of "ALT" decr' j*g
job119.log:Proof of "ismgmALT" decreased from 199 to 151 bytes using "elab2g".    <- Alexander:   I assume this is ok to do?

Norm

[Benoit]

I think that the *ALT and *OLD theorems appearing in the list (and those I quoted earlier in this thread) can be given both discouragement tags. This will take care of most of "my" cases (and others).  I can do it if Norm wants.  As for the other minimizations of theorems of the form bj-* in this list, it's better to add a proof modif discouragement tag.  I can also do it if Norm prefers.

Benoît

[Norman Megill]

Thanks.  I'll take care of adding the discouragement tags.  I just wanted agreement that it is the correct thing to do.

Norm

[Alexander van der Vekens]

On Saturday, February 22, 2020 at 9:27:56 PM UTC+1, Norman Megill wrote:

Thank you, Alexander and Glauco.  I'd like to hear from Benoit and Wolf who have a number of theorems in these lists.  After that I'll organize it into the final list of actions we'll take. (I will probably do the necessary editing of set.mm myself to prevent confusion or conflict.)

Here are some more ALT cases (with duplicates removed):

$ grep 'using ".*ALT"' j*g
job116.log:Proof of "climf" decreased from 873 to 872 bytes using "rexbidvALT".   <- use rexbidv instead

 "rexbidvALT" is only used in the backward scan, but the result of the forward scan is used. Therefore, I think that there is nothing to to here.

job147.log:Proof of "fourierdlem65" decreased from 9585 to 9567 bytes using "rexbidvALT".   <- use rexbidv instead

$ grep 'Proof of "ALT" decr' j*g
job119.log:Proof of "ismgmALT" decreased from 199 to 151 bytes using "elab2g".    <- Alexander:   I assume this is ok to do?

Yes, it's OK to minimize the proof using elab2g. And no tags are required.

[Thierry Arnoux]

Hi all,

Here are my remarks to the results of the minimizations:

> job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using "grpbase".

Ok

> job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using "gsumsnd".

It looks like my version was anterior to Alexander, but Alexander’s is more powerful. Anyway only one version shall be kept, as they are identical, so I suggest to remove gsumsn2.

> job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using "gsumsnfd".

The ‘f’ version replaces distinct variable restriction. Is the shortening legit? (Does it not reintroduce the distinct variables?)

> job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using "ncolcom".

I probably have proved ~ncolne2 when ~ncolcom did not exist yet. The minimization is legit, and maybe ~ncolne2 could be simplified out.

> job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using "ifbieq12d".

There is already a note from AV noting that ifeq123d shall be replaced by ifbieq12d

> job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using "perpdragALT".

I think even though longer, the proof for perpdragALT was interesting (it does not require the extra set variable ‘x’) and I wanted to keep it. It shall have been marked “Proof modification discouraged” and “New usage discouraged”, though.

BR,
_
Thierry

[Norman Megill]

All minimization runs are now incorporated into set.mm.  The total size reduction of set.mm was 217484 bytes.  set.mm now contains 2684 fewer lines.

Notes:  (1) The byte count above is for set.mm on Linux.  On Windows, the reduction was 220168 bytes because of the extra byte in the CR/LF line termination.  (2)  Thierry broke up the large proof in job160 into smaller lemmas and minimized them separately, so I didn't include job160 in the total.

Many thanks to the following people who donated CPU time for these runs:

Thierry Arnoux
Mario Carneiro
heiphohmia
Giovanni Mascellani
David Starner
Alexander van der Vekens
David A. Wheeler

Also, thanks to the people on this thread who analyzed the results for suspicious minimizations.  The numbers above reflect the adjustments that were made as a result of that analysis.

Norm

[Norman Megill]

And thanks to Saveliy Skresanov for providing the script preparejobs.sh that made the process of creating the jobs much easier, and to David A. Wheeler for writing the jobs script to automate the process of launching the jobs.

Norm