Shortened proofs 7

[GinoGiotto]

Continuation of #3127. Proof minimizer ran between the 6000th and the 7000th theorems that don't have a proof modification is discouraged label in their comment.

No new axiom dependencies are introduced. For evidence I recommend to scan my min-all branch instead of this pull request, so that you'll have it already checked for all commits up to shortened proofs 22 which will be the 36th pull request of this series. Axiom usage is recommended to be compared to my develop branch, to be sure that any change is caused only by my minimizations.

This series will finish at shortened proofs 25.5 which will correspond to the end of main (so deprecated sections and mathboxes are excluded). My computer will end the job in about 3-5 days from now.

At the moment, axiom dependencies can be scanned using metamath.exe, but it's quite slow, in the future I recommend using metamath-knife which has in preparation a much faster tool which will be available soon.

I can also upload in my fork the result of the axiom scan if you consider it as valid evidence, although I think your own scan of min-all is probably more valuable. In general any suggestion on how to present the evidence is welcome.

For more info you may be insterested in consulting the discussion here #3150

[david-a-wheeler]

Thanks so much for doing this! +1.

[david-a-wheeler]

I didn't review the changes in detail, but the approach seems sound.

[wlammen]

I did a manual review, and it took me more than 2 hrs to roughly assess the changes in each theorem. Often they are about using a deduction version vs. its tautological form. In many cases the overall proof logic is just a bit streamlined. And in a few instances replacements were not so obvious, but finally turned out to be possible given the axiom list of the original theorem.

I am not going to do that again. I simply cannot afford to spend all my spare time verifying these commits. Unless the PR will get smaller, say covering some 20 odd theorems, a manual control and visual check nothing bad had happened will not occur on my side again. If nobody else chimes in, we are reduced to trust GinoGiotto he did not make a mistake.

[david-a-wheeler]

wlammen said:

I did a manual review, and it took me more than 2 hrs to roughly assess the changes in each theorem. ...

First, thank you SO MUCH for checking in detail, that's greatly appreciated.

Humans are notoriously hard to predict :-), but I find that the best predictor is past behavior. So if @GinoGiotto did fine on past simplifications, the odds are good for future ones.

I think it'd be wise to double-check that no new axioms were added. This takes about an hour of computer time (1/2 an hour each to compute before & after), but almost no human time, and it's human time that's expensive. Think someone should do that? I'm happy to accept @GinoGiotto 's word that he did that (if he said he did). I could do it myself, if no one else wants to do that.

My understanding is that the assumptions & final goals aren't being changed by these shortenings, it's just shortening the proofs themselves (without adding new axioms). The proofs are checked mechanically (by multiple verifiers), so as long as results still pass the verifiers, I think it's fine to accept them.

[GinoGiotto]

I'm happy to accept @GinoGiotto 's word that he did that (if he said he did). I could do it myself, if no one else wants to do that.

Yes, I checked axiom dependencies from shortened proofs 7 up to shortened proofs 20.5, but I still haven't checked between shortened proofs 21 and shortened proofs 22. I plan to scan between shortened proofs 21 and shortened proofs 25.5 all in one go after my computer will end the job (btw my computer needed 2 hours instead of 30 min to make the scan, I'm not sure if that's because I'm running the minimizer at the same time or if I just have a slower computer).

The only differences that I found were in 5 theorems and they were all reductions in axiom dependencies, so the proof minimizer could also be used as an axiom usage minimizer (although a very inefficient one since it only found 5 theorems out of 14500).

You can check the differences in this commit I just made to show this b0445ac.

If you scan min-all by yourself the result might differ from mine because I still haven't checked between shortened proofs 21 and shortened proofs 22, but since I'm scanning the set.mm database from top to bottom, your result should (at least) be identical to mine from the first theorem of main up to ussval, which is the last theorem scanned in min20.5.

[avekens]

Just had a quick look - no conspicuousness detected.

[avekens]

In my opinion, @GinoGiotto can continue his work. It's almost the same as done before (global minimizations coordinated by Norm), and the only "risk" is to introduce new axiom dependencies, as discussed before. I think the measures to minimize this risk are sufficient, and the dependencies from axioms becomes less important when the theorems become more advanced. Maybe it becomes interesting again after the provision of the axioms for real and complex numbers. but starting with part 7 at the latest, dependencies on axioms needs not be checked anymore.