On Friday, February 14, 2020 at 8:01:47 AM UTC-5, Thierry Arnoux wrote: > > If ~ footex and ~ mideulem are too long, I may split them into smaller > lemmas, and then run minimize on the smaller lemmas. >
That would be the preferred thing to do, because it means that we won't have the problem in the future. As a rule of thumb, the time for 'save proof .../compressed/time' should ideally be less than roughly 10 sec. There is definitely some faster-than-linear growth in time vs. proof length going on (even for just 'save proof../compressed'), which I'm trying to understand the cause of, but I don't think I will be able to speed it up before this 'minimize' project is done. > > Alternatively, since geometry is a rather closed domain, we know only the > theorems from predicate logic and elementary geometry (and basic set > theory) are needed to be considered. Is there a way to do that? > You can specify a single statement range in the 'minimize' argument e.g. 'minimize ax-1~ax-ac /a * /n ax-*' (multiple ranges separated by commas aren't implemented yet, it's on my todo list). The minimization can thus be done in several pieces. Although this won't account for interactions due to scan order (i.e. the difference between the forward scan and reverse scan), they typically aren't that great and not worth worrying about in individual cases like this. That said, if you could break up those proofs, it would be great. 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/48fc4405-c3ac-4e76-8da2-5a269b0f1783%40googlegroups.com.
