Although I tried already to filter the theorems, so that only relevant concerning substitution remain, I think there are still some in my list which should not be changed. Therefore, I agree with Mario that only those theorems which would shorten at least one proof should be considered to be revised. This could be done if such a theorem should be used in a new proof.
On Monday, November 4, 2019 at 8:12:17 AM UTC+1, Mario Carneiro wrote: > > There are only 19 theorems, as a few of them have multiple hypotheses and > are being double counted. > > But to me, this is not the relevant metric when it comes to analyzing the > impact of such a change. What matters is, of the 70 deduction theorems that > *don't* use a hypothesis in substitutions, how many uses do they > (collectively) have, and what percentage of those uses would get simpler > with the deduction? Consider that there is a theorem oveq1: |- ( A = B -> ( > A + C ) = ( B + C ) ), but no theorem |- ( ( ph /\ A = B ) -> ( A + C ) = ( > B + C ) ), so a proof that uses this would get one step longer (to either > use oveq1d + simpr or adantl + oveq1). I would guess that most uses fall > into this category, with only a small fraction going into the category that > is doing substitution and substantive steps separately rather than > simultaneously (at the cost of 5 or 6 steps). > > On Mon, Nov 4, 2019 at 1:00 AM 'Alexander van der Vekens' via Metamath < > [email protected] <javascript:>> wrote: > >> Hi Thierry, >> yes, you are right - the second list contains also theorems of the >> mathboxes. Here is the list containing only the 23 theorems of the main >> part. >> >> On Sunday, November 3, 2019 at 11:44:23 PM UTC+1, Thierry Arnoux wrote: >>> >>> Hi Alexander, >>> >>> For the second list, did you also restrict yourself to the main part of >>> set.mm ? >>> BR, >>> _ >>> Thierry >>> >>> Le 3 nov. 2019 à 23:38, 'Alexander van der Vekens' via Metamath < >>> [email protected]> a écrit : >>> >>> >>> >>> On Thursday, October 31, 2019 at 1:55:27 PM UTC+1, Norman Megill wrote: >>> >>>> >>>> We could add ph to every such hypothesis to make it more >>>> general-purpose, but 99% of the time it wouldn't be needed and would make >>>> all other proofs using it (as well as the theorem itself) slightly longer. >>>> >>>> Not to mention that it would be a huge retrofit to do this throughout >>>> set.mm. I will concede there may be a few cases where it would be >>>> advantageous to do things other than prove a simple substitution with the >>>> hypothesis, but overall I believe it is rare and does not justify adding >>>> ph >>>> everywhere. >>>> >>>> I tried to identify all the theorems in set.mm (excluding the >>> mathboxes) which would be concerned - I found about 70 of them (see >>> attachment deduct_th_eq_hyp.txt). On the other hand, there are about 50 >>> theorema in deduction form having the form $e |- ( ( ph /\ x = ... ) -> ... >>> ) $. (see attachment deduct_th_ph_eq_hyp.txt). So there is no big >>> difference. Therefore, I still would propose to recommend to use the form >>> $e |- ( ( ph /\ x = ... ) -> ... ) $. in deduction style. Already existing >>> theorems need not to be rewritten (by the way, many of them have no "d" at >>> the end..). >>> >>>> >>>> >>> -- >>> 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/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> <deduct_th_ph_eq_hyp.txt> >>> <deduct_th_eq_hyp.txt> >>> >>> -- >> 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] <javascript:>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/3620ab9b-f405-43d2-821f-e15b56977eb0%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/3620ab9b-f405-43d2-821f-e15b56977eb0%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/9d669e88-bd95-4379-bef0-71d79f999c53%40googlegroups.com.
