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'].
On Wednesday, November 23, 2022 at 5:37:50 PM UTC+1 [email protected] wrote: > 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/67854b0b-7324-40e5-9143-6135ddd35794n%40googlegroups.com.
