A few minimizations

[tirix]

Following discussions in #3790, I made a few experiments for a metamath-knife based minimizer (metamath/metamath-knife#156).

These are the results of a few trials on randomly chosen theorems.

[GinoGiotto]

Oh wow, that's actually very interesting.

If you manage to make it faster than metamath-exe I'm probably going to use your version heavily.

[benjub]

Your wrote in metamath/metamath-knife#156 that your minimizer does not check axiom usage. Did you check that the minimizations in this PR do not introduce new axioms or df-cl* dependences ?

[tirix]

Did you check that the minimizations in this PR do not introduce new axioms or df-cl* dependences ?

I've manually checked the axiom usage from the output of metamath-knife -X, there is no difference. You're right the tool currently does not guarantee this, so for now one should use it with caution.

Note however that metamath-knife -X does not check df-cl*. I don't think that the script I'm using for minimizing with metamath-exe (the one in the script directory) checks for them either. The line is:

minimize */allow */no_new ax-*

If you manage to make it faster

I have not run an actual benchmark yet, it's better to do so when it's feature-complete. I believe the -M option of metamath-knife is much faster for shorter theorems, but looses its advantage for longer ones.

[avekens]

Did you check that the minimizations in this PR do not introduce new axioms or df-cl* dependences ?

I've manually checked the axiom usage from the output of metamath-knife -X, there is no difference. You're right the tool currently does not guarantee this, so for now one should use it with caution.

I also checked it for regsumsupp manually, and can confirm @tirix's statement in this single case.

Note however that metamath-knife -X does not check df-cl*. I don't think that the script I'm using for minimizing with metamath-exe (the one in the script directory) checks for them either. The line is:

minimize */allow */no_new ax-*

df-cl* means df-clab df-cleq df-clel only, not other definition with this prefix, e.g., df-clim?

[benjub]

df-cl* means df-clab df-cleq df-clel only, not other definition with this prefix, e.g., df-clim?

You're correct. Sorry for the potential confusion.

[wlammen]

FYI. There seem to be minor problems with the syntax definition hints. One shortening just omits a weq from the theorem list. This should be investigated further, but perhaps not in this PR.

[wlammen]

This is in TA's mathbox. The proof shrinks from 65 down to 63 lines. No change in Syntax, Axioms and Definitions usage.

[wlammen]

No change in Syntax, Axioms and Definitions usage. Proof length reduced from52 to 41 lines.

[wlammen]

The proof size shrinks from 44 down to 41 lines. No change in Syntax, Axioms and Definitions usage.

[wlammen]

This shortening is insignificant. For some reason a weq is spared from the list of used theorems in the new proof, even though = is used between setvars. Otherwise I see no change. I checked the proof lines optically line by line, and saw no difference whatsoever. No change in proof byte count. MM accepts and verifies both proofs alike.

[GinoGiotto]

For some reason a weq is spared from the list of used theorems in the new proof, even though = is used between setvars.

Can you provide a step number which uses equality between setvars? I looked a bit into the proof and so far I only found equality between classes (therefore making wceq sufficient and weq not needed).

[wlammen]

Step 7 velsn: (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧)
One can obviously always convert a set to a class, so 𝑦 = 𝑧 is also an equality between classes.

[benjub]

Indeed, class y and class z were already proved in earlier steps, so that is reused, and only wceq is needed, not weq.

[wlammen]

It is in my eyes a matter of taste, whether you always interpret a formula 𝑦 = 𝑧 as an equality between sets (weq), and in case you need this equality as one between classes (wceq), or if it is delivered as such, you need a conversion step. See the comment of weq: However, logically weq is considered to be a primitive syntax. Otherwise you silently apply the overload as a kind of hidden knowlwdge to switch between the possible primitives back and forth without control, or lets better say: proof step. This has no practical implications, as the result is always the same. In the end it is a matter of one's liking, I'd say.

[benjub]

My above comment describes the modified proof. It is only a description.

[wlammen]

The proof shrinks from 74 to 73 lines. No change in Syntax, Axioms and Definitions usage.

[wlammen]

The theorem under focus here is zrhpsgnelbas. Its proof length shrinks from 31 down to 30 lines. Interestingly, the Syntax Definition Hints in the new proof do not list cgrp any more. Why? Both proofs contain a line (𝑅 ∈ Ring → 𝑅 ∈ Grp) , so my expectation is that it is listed in the new proof, too. The used Axioms and Definitions are the same. The MM verifier accepts both proofs.

[benjub]

If you look at both proofs with all steps (MM> sh pr zrhpsgnelbas/ALL), you see that the old proof needs to prove that Grp is a class in order to prove that R e. Grp is a formula. It is needed when used as syl3anc.1. In the new proof, that formula appears as mulgcld.3, where it is not necessary to prove that R e. Grp is a formula.

[wlammen]

Syntax Definition cvv is not listed in the Syntax Definition hints any more. And in fact the class of all sets is not used in the new proof. On the other hand cfn is also not listed in the new proof. That is weird, since this line ((𝐹:𝐼⟶ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉) → (𝐹 supp 0) ∈ Fin) appears in the proof. The proof length shrinks from 38 to 34 lines. No change in the Axioms or Definitions list.

[benjub]

Probably the same reason as above.

[wlammen]

The proof size shrinks from 48 to 41 lines. In the list of Syntax Definitions hints wn is not listed any longer. This is explicable since the operator NOT does not appear in the proof any more. The list of Axioms and Definitions do not change.

[wlammen]

The theorem under focus here is frlmphllem. Its proof size shrinks from 54 to 52 lines. No change in Syntax Hints, Axioms or Definitions.

[icecream17]

This is the only mention of syntax hints in the mpe home page:

I think the syntax hints only show what syntaxes are needed to rederive the (hidden) syntax steps in the proof -- equivalent to the syntax labels explicitly written between the parentheses of a compressed proof.

For example https://us.metamath.org/mpeuni/re0m0e0.html does not display the syntax hint "wi" because you don't need to construct a "wi" for any substitution in the proof.

[icecream17]

based on wlammen's comments there are no differences in axioms or definitions

[tirix]

Thanks for the careful check.

I've now added a constraint which will ensure that no additional axiom is introduced, and I hope I can do the same for distinct variable conditions.

The fact that the new proof requires less syntax axioms is probably a good sign, showing that something has been saved.

[wlammen]

As @icecream17 and @benjub already found out it is not necessary for the Syntax Definition Hints to completely reference the symbols appearing on the web page of a proof. If only I had read the instructions carefully...
That said, a casual visitor might share my expectations and wonder where s/he can find an explanatory index of the symbols presented to him (or why there are entries missing).
Thanks for giving me an explanation.

[benjub]

As @icecream17 and @benjub already found out it is not necessary for the Syntax Definition Hints to completely reference the symbols appearing on the web page of a proof. If only I had read the instructions carefully... That said, a casual visitor might share my expectations and wonder where s/he can find an explanatory index of the symbols presented to him (or why there are entries missing). Thanks for giving me an explanation.

You're right. Maybe the sentences at the bottom of each theorem webpage should be more uniform:

• Colors of variables:
• This proof depends on syntax axioms:
• This proof depends on non-syntax axioms:
• This proof depends on definitions:
• This theorem is referenced in the proofs:

?

[GinoGiotto]

• This proof depends on syntax axioms:
• This proof depends on non-syntax axioms:

This might be misleading. With formal axioms we care about direct and indirect usage, but with syntactic ones we want to show direct usage only (for example wfrlem14 indirectly depends on wex, but we don't want to show it because the ∃ symbol doesn't appear in the HTML proof steps).

[benjub]

This might be misleading. With formal axioms we care about direct and indirect usage, but with syntactic ones we want to show direct usage only (for example wfrlem14 indirectly depends on wex, but we don't want to show it because the ∃ symbol doesn't appear in the HTML proof steps).

Good point. Then, should we say "This proof references the syntax axioms: ..." (or "uses") ?

[GinoGiotto]

Good point. Then, should we say "This proof references the syntax axioms: ..." (or "uses") ?

I'd say "uses" is better, because that's exactly what it does. The wff and class labels listed in the compressed proof are the ones used to substitute a metavariable with an expression. When a step has the same expression of the statement being used, there is no need for any intermediate syntax step, and that's the reason why "wi" doesn't appear in us.metamath.org/mpeuni/re0m0e0.html despite the fact that we see the implication symbol in the proof.

[benjub]

I'd say "uses" is better, because that's exactly what it does.

I think it's also more explicit, but I wanted to keep the last line ("This theorem is referenced by:"). Then, that last line should also be changed to "is used by".

[wlammen]

If you find shortenings using tools not fully trusted by now, add them as a NEW version, so people can compare the versions and verify nothing bad is introduced. After a short verification period, the new version may replace the previous one.

[GinoGiotto]

I think it's also more explicit, but I wanted to keep the last line ("This theorem is referenced by:"). Then, that last line should also be changed to "is used by".

I think "This theorem is used by.." is more consistent with "SHOW USAGE <label>", since the information presented in the HTML webpage matches the output of that command (then to be even more explicit we could say "is directly used by..", since at first I was uncertain myself if that was meant to be direct or indirect usage). The word "referenced" sounds a bit vague and out of place to me, but this is somewhat subjective so I'm not going to push this too much.

[wlammen]

@tirix Are you going to merge this pull request? Is there a reason for still waiting? I could open one for the truly shortened theorems on my behalf.

[tirix]

Are you going to merge this pull request? Is there a reason for still waiting?

I did not notice @icecream17's approval, but this is the only one, for example you did not approve.
You were asking for creating "NEW" versions and to be honest I don't really see the reason for that: either the proofs pass our requirements or they don't. And I think they do. So you're OK to merge as-is?

I could open one for the truly shortened theorems on my behalf.

What do you mean with truly shortened theorems?

[wlammen]

Except the one where just a weq was removed without a shorter sequence of proof bytes. I would spare that one.

The NEW versions were meant as a means of convincing others that shortenings are valid and introduce nothing contradicting our rules, such as added axioms. I do not need these any more, as I copied the proofs from github, compiled them to web pages and compared them side by side with the current ones.

[GinoGiotto]

Not sure if my approval counts, but to me this is good as is.

A note: I'm not 100% sure whether the metamath-exe minimizer produces proofs that change wff steps only (like weq in this PR). In the past I made a PR series minimizing the whole main of set.mm and nobody mentioned it, so maybe such cases are purposely discarded. The only thing I'm sure about is that if the searchMethod flag is set to 1 then the minimizer will produce such changes.