Unify prefers mathbox theorems over identical core set.mm theorems (e.g. frege27 and id)

[BTernaryTau]

I was originally going to title this "Unify should prefer non-mathbox theorems", but then I realized there are other ways to improve this behavior which might be better, like preferring theorems that aren't transitively discouraged or preferring theorems that introduce fewer axioms.

Steps to reproduce:

• Load the latest version of set.mm
• Add ( ph -> ph ) as the first step
• Unify

[BTernaryTau]

A similar issue: unify prefers using 3eqtr2ri (with the same justification 3 times) over eqcomi.

Steps to reproduce:

• Load the latest version of set.mm
• Add ( 6 + 1 ) = 7 as the goal
• Add 7 = ( 6 + 1 ) as the step above the goal
• Unify

Let me know if you want this split out into a separate bug.

[expln]

Hi @BTernaryTau,

No need to split out into a separate bug, I will handle these cases in this issue.

There is already an update on dev which resolves the second case. I noticed this behaviour some time ago and solved it by ordering assertions by number of hypotheses.

As of the first case, I will try to implement a solution similar to what you proposed - prefer assertions which are defined earlier. This is easier from the point of view of computation amount. However, this is not the same. If you see any issues with "prefer assertions which are defined earlier", please let me know.

Just as a side note. It is not possible to use the "transitively discouraged" approach because almost all theorems are "transitively discouraged". You may check this by copying the regex from "Regex to determine discouraged assertions by description" to "Regex to determine deprecated assertions by description", apply changes and use the explorer tab to find all "Transitively deprecated" theorems. You will see that there are a lot of such theorems. So this approach would not be selective enough.

Until this issue is resolved, if you don't want to use assertions from mathboxes at all, you may use the following approach:

1. Load set.mm and stop before mathbox. ( https://us.metamath.org/mpeuni/mathbox.html )
2. Extract your own mathbox into a separate file and load it as the second Metamath database.

However, this approach will not work if your mathbox depends on other mathboxes.

Thanks for submitting this issue and proposing possible solutions!

[BTernaryTau]

Just as a side note. It is not possible to use the "transitively discouraged" approach because almost all theorems are "transitively discouraged".

Somehow this completely slipped my mind. Thanks for reminding me!

Thanks for submitting this issue and proposing possible solutions!

Thank you for developing a wonderful metamath proof assistant!

[expln]

I changed in what order mm-lamp applies assertions. Now it applies them in the order:

1) assertions with smaller number of essential hypotheses first 2) among assertions with same number of essential hypotheses, the ones declared earlier are applied first.

This is already availabe on dev.

[expln]

This fix is available in version 19.