Fixes compressed proof generation with essential hypotheses

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

Fixes compressed proof generation with essential hypotheses #28

Closed tirix closed 3 years ago

tirix commented 3 years ago

This shall fix issue #27 .

essentials are not added to the list of statements to be put in the parens,
instead, they are prepended to that list after it is output, so that they are found in later lookups,
there are cases where non-mandatory floating hypothesis are used. The corresponding statements are added to the parens list

The compressed proofs created with this new version are accepted by the Metamath program and MMJ2.

david-a-wheeler commented 3 years ago

@tirix - I trust your judgement. I have some personal family issues that, combined with work, are consuming my time at the moment. I hope to get back to this soon :-).

digama0 commented 3 years ago

The logic looks correct to me, so feel free to merge it once you have tested that it works to fix #27.

tirix commented 3 years ago

Thank you! It appears it does fix #27, both for very simple proofs like ~syl and more complex ones involving non-mandatory floating hypotheses.

To date, I've tested with various proofs of different complexity: ~syl, ~ellimc and ~numclwlk1lem2f1.