mmj2: Unification failure in derivation proof step

[Brian Larson]

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

[Mario Carneiro]

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.

--
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.

[Brian Larson]

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.

[Mario Carneiro]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4e690e6b-8aa7-4c16-b309-9a3779dbaa00n%40googlegroups.com.