Thank you for the quick, and disappointing (as expected) answers. The problematic definition: $( Define Tick, Predicate ` ph '. <-> ( ph ^. 1 ) ` $) df-bl.tick $a |- ( ph '. <-> ( ph ^. 1 ) ) $.
Because tick is used as syntactic sugar, I can do without it. Unfortunately, I have other theorems whose proofs mmj2 won't unify, so were also proved using MM-PA. I forked the set.mm GitHub repo (brlarson) in preparation for contributing my small bit to the community. On Friday, February 2, 2024 at 5:49:07 AM UTC-6 [email protected] wrote: > That error message means that the theorem df-bl.tick has a statement that > does not match the expression |- ( A = B '. <-> ( A = B ^. 1 ) ) that you > have provided. It's difficult to say more without seeing the rest of the > code (and in particular, the definition of `df-bl.tick`). > > Q1: No, this is a fatal error, the proof is not correct as written. One > way you can try to clear things up is to delete the statement (just the |- > ( A = B '. <-> ( A = B ^. 1 ) ) part) and let mmj2 fill it in for you. The > only steps you can't delete are the hypotheses IIRC. > Q2: I think there isn't any centralized listing other than the source > code: > https://github.com/digama0/mmj2/blob/1cd95c1fe4435899c8575644fccb412dd77d79e4/src/main/java/mmj/pa/PaConstants.java#L2790-L2794 > > . In general you can search the repo for uses of the constant which might > have some additional clues about it, but most of them carry a decent amount > of explanation text which will be more helpful than looking at the code. > Q3: Yes, because set.mm only accepts completed proofs, and mmj2 will not > produce a completed proof (a block starting with $= at the bottom of the > file) until all unification errors are fixed and missing steps are filled > in. > > > On Thu, Feb 1, 2024 at 10:59 AM Brian Larson <[email protected]> > wrote: > >> I much enjoy using mmj2, and am often amazed at how its unification >> deduces a theorem to solve qed when I think I've got a couple more steps to >> go. However, sometimes I get failure in its final unification check. >> >> The error message: >> E-PA-0410 Theorem bl.tkeq: Step 100: Unification failure in derivation >> proof step df-bl.tick. The step's formula and/or its hypotheses could not >> be reconciled with the referenced Assertion. Try the Unify/Step Selector >> Search to find unifiable assertions for the step. >> --------------------------------------------------------- >> >> The culprit: >> 100::df-bl.tick |- ( A = B '. <-> ( A = B ^. 1 ) ) >> >> '. and ^. are modal logic operators which determine in which "world" >> variables and predicates made with them should be evaluated: A must equal >> B one thread period hence. >> >> Both operators can be applied to wffs or classes: >> $( Define ` ( ph ^. A ) ` as a wff $) >> wts $a wff ( ph ^. A ) $. >> >> $( Define ` ( A ^. B ) ` as a class $) >> clts $a class ( A ^. B ) $. >> >> $( Define ` ph '. ` as a wff $) >> wtick $a wff ph '. $. >> >> $( Define ` A '. ` as a class $) >> ctick $a class A '. $. >> >> For other theorems which encountered this problem, I used MM-PA, and then >> included such theorems in the ProofAsstUnifySearchExclude list. >> >> Q1) Is there some clever RunParamFile setting which will avoid the error? >> Q2) Where can the list of error codes like E-PA-0410 be found? >> Q3) Will the mmj2 check preclude such theorems from acceptance into >> set.mm? >> >> >> --Brian >> >> >> -- >> 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/e6bd6e24-9110-49cc-ac8b-08128a7828abn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/e6bd6e24-9110-49cc-ac8b-08128a7828abn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/4e690e6b-8aa7-4c16-b309-9a3779dbaa00n%40googlegroups.com.
