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
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/1372dfc6-e629-4f15-bf64-63147fae132dn%40googlegroups.com.
example.mm
Description: application/freemind
