search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

Generated compressed proofs include essential hypotheses #27

Closed tirix closed 3 years ago

tirix commented 3 years ago

When exporting a compressed proof in MMP format (-e option on the command line), metamath-knife includes the essential hypotheses.

For example, the file generated with metamath-knife -e syl includes the following compressed proof:

      ( syl.1 syl.2 wi a1i mpd ) ABCDBCFAEGH $.

This repeats the essential hypotheses syl.1 and syl.2 in the compressed proof.

When fed back to metamath-knife, this is not considered as an error. However, the metamath program complains with:

      ( syl.1 syl.2 wi a1i mpd ) ABCDBCFAEGH $.
        ^^^^^
Required hypotheses may not be explicitly declared.

and MMJ2 also complains:

E-LA-0113 Theorem sylALT: compressed proof contains required hypothesis within the parentheses. Label position within the compressed proof's parentheses = 1. Statement label = syl.1
tirix commented 3 years ago

The Metamath book states in Appendix B, Compressed Proofs:

An error message is given if (1) a label in the label list in parentheses does not refer to a previous $p or $a statement or a non-mandatory hypothesis of the statement being proved

tirix commented 3 years ago

Fixed with #28

The (re)generated proofs appear to be longer than the original set.mm proofs probably generated with the Metamath program or MMJ2, so there might be room for improvement, however this is not the scope of this issue.

digama0 commented 3 years ago

Do the generated proofs have a ragged right side? MMJ2 is using a knapsack algorithm to optimize the packing of the labels and make them look more "neat", and IIRC metamath.exe copied that implementation.

tirix commented 3 years ago

I'm keeping this issue, which I'd have categorized as a bug, closed, and I'm opening another one for an improvement of the compression algorithm. My answer is on that other thread. (TL;DR yes, there is a knapsack algorithm, but maybe it is limited)