Let me try to make to some more clarifications.
First, some of the hypotheses you mention such as:
> Line 63231: fvmptdf.2 $e |- ( ( ph /\ x = A ) -> B e. V ) $.
> Line 63232: fvmptdf.3 $e |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B ->
ps ) ) $.
> Line 77808: oe0lem.1 $e |- ( ( ph /\ A = (/) ) -> ps ) $.
do not have consequents of the form A = B or ( ps <-> ch ). Maybe this was
an oversight, but to be clear these aren't part of the discussion, and the
ph is definitely appropriate for them. We are specifically discussing the
use of implicit substitution hypotheses and whether they should routinely
have the ph. Aside from the 4 cases mentioned in the thread "When to use a
"ph ->" antecedent in a deduction form" (one of which is implicit
substitution), normally ph should always be used as an antecedent in a
deduction form.
Recall fsumshft:
fsumrev.1 $e |- ( ph -> K e. ZZ ) $.
fsumrev.2 $e |- ( ph -> M e. ZZ ) $.
fsumrev.3 $e |- ( ph -> N e. ZZ ) $.
fsumrev.4 $e |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) $.
fsumshft.5 $e |- ( j = ( k - K ) -> A = B ) $.
fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K )
... ( N + K ) ) B ) $= ... $.
fsumshft.5 is used to provide an alternate (implicit substitution) version
of the explicit substitution version, which would be
fsumrev.1 $e |- ( ph -> K e. ZZ ) $.
fsumrev.2 $e |- ( ph -> M e. ZZ ) $.
fsumrev.3 $e |- ( ph -> N e. ZZ ) $.
fsumrev.4 $e |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) $.
fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K )
... ( N + K ) ) [_ ( k - K ) / j ]_ A ) $= ... $.
The implicit and explicit substitution versions can be derived from each
other and are duals. In the explicit substitution version, all hypotheses
have a ph as desired. Thus the lack of ph on fsumshft.5 does not weaken
the theorem intrinsically (as would the omission of ph elsewhere).
The reason we usually use implicit substitution is that most of the time it
results in shorter proofs.
fsumshft.5 is used to let us show that A and B are substitution instances
of the same formula using simple equality theorems. While we could add ph
to allow us to do extra work with the hypothesis, the need for such extra
work is the exception rather than the rule. In most cases the ph is
redundant and masks the intended purpose - it is no longer just the simple
substitution that was intended but becomes something else.
Another example:
nn0indd.1 $e |- ( x = 0 -> ( ps <-> ch ) ) $.
nn0indd.2 $e |- ( x = y -> ( ps <-> th ) ) $.
nn0indd.3 $e |- ( x = ( y + 1 ) -> ( ps <-> ta ) ) $.
nn0indd.4 $e |- ( x = A -> ( ps <-> et ) ) $.
nn0indd.5 $e |- ( ph -> ch ) $.
nn0indd.6 $e |- ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta ) $.
nn0indd $p |- ( ( ph /\ A e. NN0 ) -> et ) $= ... $.
Do we really want this to be:
nn0indd.1 $e |- ( ( ph /\ x = 0 ) -> ( ps <-> ch ) ) $.
nn0indd.2 $e |- ( ( ph /\ x = y ) -> ( ps <-> th ) ) $.
nn0indd.3 $e |- ( ( ph /\ x = ( y + 1 ) ) -> ( ps <-> ta ) ) $.
nn0indd.4 $e |- ( ( ph /\ x = A ) -> ( ps <-> et ) ) $.
nn0indd.5 $e |- ( ph -> ch ) $.
nn0indd.6 $e |- ( ( ( ph /\ y e. NN0 ) /\ th ) -> ta ) $.
nn0indd $p |- ( ( ph /\ A e. NN0 ) -> et ) $= ... $.
Not only does the statement of the theorem become longer, to me this
visually obscures the intended substitutional purpose of nn0indd.1 through
nn0indd.4, and most proofs using it would be slightly longer in order to
ignore the redundant ph. Maybe an occasional proof could use one of the
extra ph antecedents to do some extra work at that point rather than
elsewhere in the proof, but I don't think it is common enough to make up
for the longer proofs needed everywhere else.
I'm not opposed to adding the ph on occasion where it offers a benefit such
as shorter proofs overall. Some of the examples you show are used for that
purpose, and there is no reason to change those.
However, I don't think it is something we should do routinely without a
reason. In particular, I think it would be a mistake to massively retrofit
existing theorems by adding ph; I am pretty sure this would result in an
unnecessary growth in set.mm size.
Norm
On Monday, November 4, 2019 at 3:22:30 AM UTC-5, Alexander van der Vekens
wrote:
>
> 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]> 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/c716614b-aab3-421c-971a-ea956dc9dbc0%40googlegroups.com.
