Incorrect proof size

[GinoGiotto]

It seems metamath.exe is displaying an incorrect proof size according to @benjub and @avekens in this PR review. Although I haven't personally verified the observations, I thought it would be better to open an issue to ensure that this event is not forgotten, since the PR is likely to be closed soon.

[benjub]

I confess I do not remember. Maybe the files had not been rewrapped the same and counts are brittle ? I do not have the courage to dive into that again.

[digama0]

a standalone repro, or at least an exact version of set.mm, would be very helpful to diagnosing this.

[GinoGiotto]

I was about to post a long comment with all data and analysis of the event, but due to an unfortunate circumstance I lost it. Long story short @benjub is right. The command SHOW PROOF <label-match> /SIZE displays an incorrect amount because it adds the number of indentation spaces and new lines in the proof size, so different rewraps generate different counts. The count shown at the end of the output of SHOW PROOF <label-match> /COMPRESSED is the correct one (in fact this one doesn't change with different rewraps). To be specific SHOW PROOF <label-match> /COMPRESSED counts also the characters given by the label list, which may not be the most useful info, since usually we are interested only in the count of upper-case characters.

Anyway this is a short summary of a long analysis that I made, ask me any question if you want more info.

[benjub]

So your conclusion is that SHOW PROOF <label-match> / SIZE has a bug, correct ?

Its help says:

    / SIZE - Shows size of the proof in the source.  The size depends on
        how it was last SAVEd (compressed or normal).

If one is going to correct it, it would be better to have an implementation corresponding to:

    / SIZE - Shows total number of steps of the proof.

(the notion of "logical" or "essential" step does not always make sense anyway). The display after / COMPRESSED could also be clearer (and documented, which it is currently not:

    / NORMAL, / COMPRESSED, / EXPLICIT, / PACKED, / FAST,
        / OLD_COMPRESSION - These qualifiers are the same as for
        SAVE PROOF except that the proof is displayed on the screen in
        a format suitable for manual inclusion in a source file.  See
        HELP SAVE PROOF.

)

[GinoGiotto]

So your conclusion is that SHOW PROOF <label-match> / SIZE has a bug, correct ?

Yes. It clearly makes no sense to include indentation spaces and new lines into the size count of SHOW PROOF <label-match> / SIZE, so I think this command should be revisioned.

If one is going to correct it, it would be better to have an implementation corresponding to:

/ SIZE - Shows total number of steps of the proof.

To avoid confusion I think we can make it more clear by writing multiple values. Here is an example (with current version of set.mm):

MM> SHOW PROOF bezout / SIZE
The proof source for "bezout" has 905 total characters.
Excluding labels, the proof of "bezout" has 591 characters.
The proof of "bezout" has 368 total steps.
The proof of "bezout" has 47 essential steps.
Without repeated steps the proof of "bezout" has 45 essential steps.

• 905 characters includes labels, spaces between labels and parenthesis (this is equivalent to the number shown in SHOW PROOF bezout /COMPRESSED
• 591 characters counts the section with upper-case letters only, which is more useful for minimization.
• 368 steps includes wff and class steps (equivalent to what you would get with SHOW PROOF bezout /ALL or SHOW TRACE_BACK bezout /COUNT).
• 47 steps is the value derived from SHOW PROOF bezout /ESSENTIAL /RENUMBER
• 45 steps is the value reported in the bezout webpage which I believe is derived from SHOW PROOF bezout /LEMMON /ESSENTIAL /RENUMBER /NO_REPEATED_STEPS.

I personally find all those counts valuable for various reasons, so I would write all of them.

[GinoGiotto]

Actually I was assuming the proof was in the /COMPRESSED format, but my output wouldn't work for other ones. I think we could make it even more clear by doing something like this:

MM> SHOW PROOF bezout /COMPRESSED /SIZE 
The proof source for "bezout" has 905 total characters.
Excluding labels, the proof of "bezout" has 591 characters.
The proof of "bezout" has 368 total steps.
The proof of "bezout" has 47 essential steps.
Without repeated steps the proof of "bezout" has 45 essential steps.

MM> SHOW PROOF bezout /NORMAL /SIZE 
The proof source for "bezout" has 4756 total characters.
The proof of "bezout" has 1253 total steps.
The proof of "bezout" has 48 essential steps.
Without repeated steps the proof of "bezout" has 46 essential steps.

MM> SHOW PROOF bezout /EXPLICIT /SIZE 
The proof source for "bezout" has 10212 total characters.
The proof of "bezout" has 1253 total steps.
The proof of "bezout" has 48 essential steps.
Without repeated steps the proof of "bezout" has 46 essential steps.

MM> SHOW PROOF bezout /PACKED /SIZE 
The proof source for "bezout" has 1555 total characters.
The proof of "bezout" has 368 total steps.
The proof of "bezout" has 47 essential steps.
Without repeated steps the proof of "bezout" has 45 essential steps.

Currently, adding any format option like /NORMAL or /COMPRESSED with /SIZE doesn't change anything, which is a waste imo.