Thanks for the answer, so I should report it on github? Il giorno mercoledì 23 novembre 2022 alle 19:29:53 UTC+1 Benoit ha scritto:
> 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/2213b902-0a14-48aa-8c70-690c69dc9322n%40googlegroups.com.
