Closed BTernaryTau closed 9 months ago
Thanks for submitting this bug. I can reproduce it.
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:
The latest release doesn't give any results, but the dev version gives exlimivv
as an option even though it's invalid.
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
.
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 (https://github.com/expln/metamath-lamp/issues/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?
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.)
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.
Steps to reproduce:
Resulting disjoints:
Expected disjoints: