Bottom-up prover adds unnecessary disjoints

[BTernaryTau]

{"srcs":[{"typ":"Web","fileName":"","url":"https://us.metamath.org/metamath/set.mm","readInstr":"ReadAll","label":"vtocl2","resetNestingLevel":true,"allLabels":[]}],"descr":"","varsText":"","disjText":"","stmts":[{"label":"vtocl2d2.1","typ":"e","isGoal":false,"cont":"|- ( ph -> A e. V )","jstfText":""},{"label":"vtocl2d2.2","typ":"e","isGoal":false,"cont":"|- ( ph -> B e. W )","jstfText":""},{"label":"vtocl2d2.3","typ":"e","isGoal":false,"cont":"|- ( ph -> ( ( x = A /\\ y = B ) -> ( ps <-> ch ) ) )","jstfText":""},{"label":"vtocl2d2.4","typ":"e","isGoal":false,"cont":"|- ( ph -> ps )","jstfText":""},{"label":"1","typ":"p","isGoal":false,"cont":"|- ( ph -> ( y = B -> ps ) )","jstfText":"vtocl2d2.4 : a1d"},{"label":"2","typ":"p","isGoal":false,"cont":"|- ( ( ph /\\ y = B ) -> ps )","jstfText":"vtocl2d2.4 : adantr"},{"label":"3","typ":"p","isGoal":false,"cont":"|- ( ( ph /\\ x = A /\\ y = B ) -> ( ps <-> ch ) )","jstfText":"vtocl2d2.3 : 3impib"},{"label":"4","typ":"p","isGoal":false,"cont":"|- ( ( ( ph /\\ x = A ) /\\ y = B ) -> ( ps <-> ch ) )","jstfText":"3 : 3expa"},{"label":"5","typ":"p","isGoal":false,"cont":"|- ( ( ph /\\ x = A ) -> ( ( y = B -> ps ) <-> ( y = B -> ch ) ) )","jstfText":"4 : pm5.74da"},{"label":"6","typ":"p","isGoal":false,"cont":"|- ( ph -> ( y = B -> ch ) )","jstfText":""},{"label":"7","typ":"p","isGoal":false,"cont":"|- ( ( ph /\\ y = B ) -> ch )","jstfText":"6 : imp"},{"label":"8","typ":"p","isGoal":false,"cont":"|- ( ( ph /\\ y = B ) -> ( ps <-> ch ) )","jstfText":"2 7 : 2thd"},{"label":"9","typ":"p","isGoal":false,"cont":"|- ( ph -> ( y = B -> ( ps <-> ch ) ) )","jstfText":"8 : ex"},{"label":"vtocl2d2","typ":"p","isGoal":true,"cont":"|- ( ph -> ch )","jstfText":""}]}

Steps to reproduce:

• Load the latest version of set.mm
• Import the above JSON
• Use the bottom-up prover on the goal statement, allowing new disjoints but not new steps
• Apply the only option

Resulting disjoints:

ph,x
ph,y
ph,A
ch,x
ch,y
ch,A
x,B
y,B
A,B

Expected disjoints:

ph,y
ch,y
y,B

[expln]

Thanks for submitting this bug. I can reproduce it.

[expln]

This bug is fixed on dev.

[BTernaryTau]

Looks like this change introduced a new bug. The bottom-up prover now sometimes suggests theorems with disjoints that make the justification invalid.

Steps to reproduce:

• Add ( E. x E. y x = y -> x = y ) as the goal
• Add ( x = y -> x = y ) as the step above the goal
• Use the bottom-up prover on the goal statement, allowing new disjoints but not new steps

The latest release doesn't give any results, but the dev version gives exlimivv as an option even though it's invalid.

[BTernaryTau]

Found an example that's buggy in both v18 and dev, but in different ways.

{"srcs":[{"typ":"Web","fileName":"","url":"https://us.metamath.org/metamath/set.mm","readInstr":"StopBefore","label":"cbv3","resetNestingLevel":true,"allLabels":[]}],"descr":"","varsText":"","disjText":"ps,y\nch,x\nph,x,y","stmts":[{"label":"qed.1","typ":"e","isGoal":false,"cont":"|- F/ y ( ph -> ps )","jstfText":"cbv1v.2 cbv1v.3 : nfim1"},{"label":"qed.2","typ":"e","isGoal":false,"cont":"|- F/ x ( ph -> ch )","jstfText":"cbv1v.1 cbv1v.4 : nfim1"},{"label":"qed.3","typ":"e","isGoal":false,"cont":"|- ( x = y -> ( ( ph -> ps ) -> ( ph -> ch ) ) )","jstfText":"3 : a2d"},{"label":"1","typ":"p","isGoal":false,"cont":"|- ( A. x ( ph -> ps ) -> A. y ( ph -> ch ) )","jstfText":""},{"label":"qed","typ":"p","isGoal":true,"cont":"|- ( ph -> ( A. x ps -> A. y ch ) )","jstfText":""}]}

Using the bottom-up prover in dev only shows cbvalivw as an option, even though cbv3v also works and has fewer disjoints. Applying this option works correctly.

Using the bottom-up prover in v18 correctly shows cbv3v as an option (though not cbvalivw), but applying it then results in the disjoints for cbvalivw being applied instead of those for cbv3v.

[expln]

Looks like this change introduced a new bug. The bottom-up prover now sometimes suggests theorems with disjoints that make the justification invalid.

You are right. It was a newly introduced bug. Luckily it was easy to fix and I've already fixed it on dev.

Found an example that's buggy in both v18 and dev, but in different ways.

There are two things:

1. Incorrect disjoints in v18 - this is the same bug you've described in the first comment in this issue. It is already fixed on dev.
2. v18 finds cbv3v which has lesser number of disjoints, but dev finds cbvalivw with bigger number of disjoints - this is not a bug, this is how mm-lamp currently works. mm-lamp stops immediately as it finds any proof for the statement being proved. So the result depends on in which order mm-lamp iterates over all assertions. In v18, there is no any specific order of assertions (v18 iterates over entries of a hash map, so the order is close to random, but stable for the given set of frame labels). It just happened that cbv3v was placed before cbvalivw and mm-lamp v18 found it first. But in dev, I recently fixed the order - 1) number of essentials hypotheses, 2) declaration order (Unify prefers mathbox theorems over identical core set.mm theorems (e.g. frege27 and id) #163). So now in dev cbvalivw precedes cbv3v because of number of essential hypotheses.

I am not sure, maybe ordering by number of essential hypotheses doesn't make sense, and it is better to order by number of disjoints first. What do you think?

[BTernaryTau]

I'm not experienced enough to know which option is better, so I'd say just keep it as is unless someone else has an opinion.

(In general what I want is for mm-lamp to show me all options that aren't strictly worse than an alternative across their necessary hypotheses, disjoints, and axioms. I assume that'd be a large feature request though.)

[expln]

I created an issue to implement this in the future #169. Currently I am working on something else, but this feature of showing more options also looks very useful.

[expln]

This fix is available in version 19.