Strange behaviour of Metamath

[Gino Giotto]

Hello, I decided to report this event here since I'm not sure if this is a true bug or just a result of my inexperience.

So I made a simple file called "example.mm" that I attached in this email.

This file contains only one theorem, called "th" which has an incorrect proof.

Now when I verify that proof with "verify proof *" it seems that Metamath doesn't notice the mistake, here is the complete log sequence:

---------------------------------------------------------------------------------------------------------------

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read example.mm
Reading source file "example.mm"... 122 bytes
122 bytes were read into the source buffer.
The source has 7 statements; 2 are $a and 1 are $p.
SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> VERIFY PROOF *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
MM> show proof th /lemmon /all
1 ax             $a axiom
2 1 mp           $a thesis
MM> 

--------------------------------------------------------------------------------------------------------------------------------

But if I enter the proof assistant, it detects that something is wrong:

--------------------------------------------------------------------------------------------------------------------------------

MM> prove th
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
?Error in step 2:  Could not simultaneously unify the hypotheses of "mp":
    $|$ hypothesis $|$
with the following statement list:
    $|$ axiom $|$
(The $|$ tokens are internal statement separation markers)
Zapping targets so we can proceed (but you should exit the Proof Assistant and
fix this problem)
(This may take a while; please wait...)
Step 1 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
You will be working on statement (from "SHOW STATEMENT th"):
7 th $p thesis $= ... $.
Note:  The proof you are starting with is already complete.

MM-PA> show new_proof /lemmon /all
1 ax             $a hypothesis
                  = axiom
2 1 mp           $a thesis
MM-PA>

----------------------------------------------------------------------------------------------------------------------------------------

And then it contradicts itself stating that the proof is already complete, which can't be true, since it contains mistakes.

My question is why the command "verify proof *" doesn't notice that the proof is incorrect? Is this a bug or it is supposed to behave this way?

Regards 

Gino

[Benoit]

That looks like a real bug.  The python verifier mmverify.py correctly rejects the proof:

  $ python3 mmverify.py example.mm --verbosity 20

gives

  __main__.MMError: Proof stack entry ['axiom'] does not match essential hypothesis ['hypothesis'].

[Gino Giotto]

Thanks for the answer, so I should report it on github?

[Benoit]

On Thursday, November 24, 2022 at 9:58:06 PM UTC+1 ginogiott...@gmail.com wrote:

Thanks for the answer, so I should report it on github?

Yes please.