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]> 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]. > 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/CAFXXJStDjCi%2BdMCMfbf9UeukORAApd_5a4CmQJ%3DzsHS%3Ddj7Rrg%40mail.gmail.com.
