On Monday, January 13, 2020 at 4:19:16 PM UTC+1, Norman Megill wrote: > > 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. >
I encountered this also (a minimization introducing idi but not removing it). This was probably due to a small bug of minimize_with in the versions around 0.178--0.179 (for it to work properly, you had to save the proof, exit MM-PA, then re-enter it and minimize). Norm has corrected this bug, and indeed I didn't see this behavior again. Benoît -- 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/02fa0060-262c-4a43-bc0d-fdb8bb96e93c%40googlegroups.com.
