On Monday, January 13, 2020 at 5:51:18 AM UTC-5, Alexander van der Vekens wrote: > > As far as I can remember, idi was *inserted* by 'minimize' in some cases, > and I had to remove it manually. Unfortunately, I do not know when and in > which context this appeared, but I think the concerned theorem was not > marked as "usage discouraged"... > Maybe there was an error which was fixed meanwhile - I will come back to > this if it happens again. >
There are situations where idi will temporarily shorten an inefficient proof during 'minimize', showing up in its 'decreased' list at the beginning of the run. This can happen when the proof has 2 different subproofs for the same fact, with the idi attaching the shorter subproof to its hypothesis. But (unless you are using discouraged theorems) the idi itself should be removed later in the minimize run. If you see an idi remaining (even after 'minimize * /override'), let me know and I'll look at it. > > Looking for idi in the current version of set.mm, there are a lot of > "idi"s in the proofs of the theorems Glauco provided in December (in his > mathbox)! Since they are very long, I fear that 'minimize' will take a long > time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran > some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to > 10757 steps (567 to 520 essential steps). "idi" was removed by this > minimization, so everything is fine. > Yes, I am aware of this and am looking at what we will have to do in order to 'minimize' some of the larger new proofs since the last run. Unfortunately some are over an order of magnitude larger than our previous run 2 years ago. 'minimize' isn't going to be feasible on the longest proofs unless we refactor them by breaking out some lemmas or maybe add definitional hypotheses for very long repeated subexpressions. This might be a good idea anyway so a human can understand them. I'm currently looking at what will be needed for a new global run with the help of savask's formula (and maybe will ask for his help). In any case, idi itself is likely only a tiny contributor to the size of those proofs, so in those cases it actually serves as a useful "canary" to remind us the proof needs minimization. BTW an idi itself can be removed with a quick 'minimize xxx' where xxx is the theorem attached to the idi hypothesis, if people are bothered by it, but the rest of the proof should still be minimized someday. Norm -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7e12f2d7-9e50-464e-9699-3d428ce0e2cf%40googlegroups.com.
