The issue is that the '. syntax is ambiguous, A = B '. can be interpreted as either "A = (B '.)" or "(A = B) '." . Syntax ambiguity in set.mm (and most metamath databases) is a big no-no, you can generally prove a contradiction from them, but because mmj2 parses formulas into trees ambiguous parses instead manifest as unification failures. My guess is that the expression you wrote as |- ( A = B '. <-> ( A = B ^. 1 ) ) is parsed using the A = (B '.) interpretation, but the instantiation of df-bl.tick would produce the (A = B) '. interpretation.
The short version of the ambiguity restriction as it applies to set.mm is that you are not allowed to have pure postfix operators without parentheses, which means both wtick and ctick are illegal, but wts and clts are fine. On Fri, Feb 2, 2024 at 8:33 AM Brian Larson <brianralphlar...@gmail.com> wrote: > 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 di....@gmail.com 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 <brianral...@gmail.com> >> 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 metamath+u...@googlegroups.com. >>> 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/4e690e6b-8aa7-4c16-b309-9a3779dbaa00n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4e690e6b-8aa7-4c16-b309-9a3779dbaa00n%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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs05DM_14YsvWsmdOaLVdzbPYbuQw%3DaQ0_gMMorqDZ%3DjQ%40mail.gmail.com.
