Open GinoGiotto opened 9 months ago
My guess would be that the minimizer does not know a1i
, and does not even know what is an antecedent.
It only searches for exact matches.
I admit I'm ignorant about how the minimizer works. But isn't a1i
just a simple rule of inference? And doesn't the minimizer replace rules of inference as well?
Here is an example:
$c |- wff ( ) | $. $v A B C $. wa $f wff A $. wb $f wff B $. wc $f wff C $. wbar $a wff ( A | B ) $. ax-1 $a |- ( ( A | A ) | B ) $. ${ ax-inf1.1 $e |- ( ( B | B ) | C ) $. ax-inf1 $a |- ( ( ( B | B ) | C ) | ( B | B ) ) $. $} ${ ax-inf2.1 $e |- ( ( ( B | B ) | C ) | ( B | B ) ) $. ax-inf2 $a |- ( C | C ) $. $} ${ ax-inf3.1 $e |- ( ( B | B ) | C ) $. ax-inf3.2 $e |- ( C | C ) $. ax-inf3 $a |- ( ( ( B | B ) | C ) | ( B | B ) ) $. $} $( First theorem. (New usage is discouraged.) $) th1 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) ) $= ( wbar ax-1 ax-inf1 ) ACCDBDZAGEF $. $( Second theorem. $) th2 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) ) $= ( wbar ax-1 ax-inf1 ax-inf2 ax-inf3 ) ACCDBDZAIECICICIEFGH $.
Theorems th1
and th2
are identical, but th2
has a longer proof, using more rules of inference than it needs. Let's see if the minimizer can find the shortening:
Metamath - Version 0.198 7-Aug-2021 Type HELP for help, EXIT to exit. MM> r min.mm / Reading source file "min.mm"... 755 bytes 755 bytes were read into the source buffer. The source has 22 statements; 5 are $a and 2 are $p. 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% .................................................. All proofs in the database were verified in 0.01 s. No errors were found. MM> prove th2 Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. You will be working on statement (from "SHOW STATEMENT th2"): 22 th2 $p |- ( ( ( A | A ) | ( ( C | C ) | B ) ) | ( A | A ) ) $= ... $. Note: The proof you are starting with is already complete. MM-PA> minimize * /allow * /no ax-* Bytes refer to compressed proof size, steps to uncompressed length. Scanning forward through statements... Proof of "th2" decreased from 58 to 33 bytes using "ax-inf1". Scanning backward through statements... Proof of "th2" decreased from 58 to 33 bytes using "ax-inf1". The forward scan results were used. MM-PA> sh ne /compressed Proof of "th2": ---------Clip out the proof below this line to put it in the source file: ( wbar ax-1 ax-inf1 ) ACCDBDZAGEF $. ---------The proof of "th2" (33 bytes) ends above this line. MM-PA>
In this case the minimizer found the shortening, so the diagnosis doesn't seem related to the fact that a1i
is a rule of inference, nor to the fact that exact matches are needed, since I created th2
in a way that doesn't do so. What am I missing?
You're right.
Then I suppose someone would need to dig into the way the minimizer is implemented to understand why this minimization is not found.
I'm using set.mm at commit 02d887a.
This is more like a question rather than an issue because it's hard to tell if this is supposed to happen or not, anyway I find this to be an interesting test case.
In main there is this theorem:
In the mathbox of Stefan O'Rear there is this theorem:
We can notice that
sbcrexgOLD
is simply a version ofsbcrex
with an antecedent, thereforesbcrexgOLD
can be proven fromsbcrex
:We can also use
improve all
to find this shorter proof:However if I use the minimizer then it doesn't find it:
Axiom usage of
sbcrexgOLD
is the same assbcrex
, so this isn't the reason. The verifier does not complain about $d violations so it doesn't appear they are the problem either. I tried to movesbcrexgOLD
out of the mathbox and remove the discouragment labels. Still nothing. So the question is why the minimizer doesn't notice this trivial shortening?