question about fsumshft

[Olivier Binda]

Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? 

fsumshft.5

Is the same theorem with ( ph -> ( j = ( k-K ) -> A = B ) )  false ? or stupid ? or unnecessary ?

It looks stronger to me as I probably cannot prove it easily from fsumshtf

I am still grasping at all the subtleties of Metamath, so I may not understand something important here.

Could someone please enlighten me ?

Best regards,

Olivier

[Giovanni Mascellani]

Hi,

Il 28/10/19 22:18, Olivier Binda ha scritto:

> Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? 

I had your same question a few months ago, and of course Mario had an
answer for me:

https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Alexander van der Vekens]

I think the discussion mentioned by Giovanni is about a different case  - it's about "definitions", i.e. hypotheses in the form $e |- A = ... $. For example, look at ~ fmpt :

    fmpt.1 $e |- F = ( x e. A |-> C ) $.
    fmpt $p |- ( A. x e. A C e. B <-> F : A --> B ) $=

Here, "F" is defined as being (of the form) "( x e. A |-> C )", meaning that "F" could be replacd (at least in principle) by "( x e. A |-> C )" in the conclusion:
( A. x e. A C e. B <-> ( x e. A |-> C ) : A --> B )

No additional assumptions/prerequistes are requird (for which an antecedent "ph ->" would be needed) in this case. Mario explains this in https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ in more detail.

The present case, however, shows a different kind of hypotheses often used in deduction style (unfortunately not mentioned in the Metamath book or in http://us.metamath.org/mpegif/mmnatded.html ). It is a variant of hypotheses in the form $e |- ( x = Y -> A = B ) $., often also enhanced by the general antecedent ph: $e |- ( ( ph /\ x = Y ) -> A = B ) $.

Examples:

    gsumsn.b $e |- B = ( Base ` G ) $.
    gsumsn.s $e |- ( k = M -> A = C ) $.
    gsumsn $p |- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M } |-> A ) ) = C ) $=

    ...
    gsumsnd.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
    gsumsnd $p |- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C ) $=

These are abbreviations for substitutions (also called "implicit substitutions"), which could be written also as explicit substitutions: [_ M / k ]_ A = C (see also ~ csbied ). In other words, you can think of A as a class expression containing the setvar variable k, and B as a class expression containing the class variable M, so that A equals B after the substitution of k by M.

Example: replace M, A, C by the follwing expressions:

M := ( 2 + 5 )
A := ( k - 3 )
C := ( ( 2 + 5 ) - 3 )

Then ( k = M -> A = C ) is true.

In the case of ~ fsumshft mentioned by Olivier, j can be considered as being contained in A (A usually depends on j, because the summation is over j), and k can be considered as being contained in B (B usually depends on k, because the summation is over k), and the conclusion holds if A equals B after j is substituted by ( k - K ) within A.

Using explicit substitution the theorem ~ fsumshft

      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 ) $=

could also be written as  

      fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) [ ( k - K ) / j ] A ) $=

As a conclusion, the patterns $e |- ( x = Y -> A = B ) $. or $e |- ( ( ph /\ x = Y ) -> A = B ) $. for hypotheses are also allowed for deduction style theorems, and they could be considered as abbreviations for substitutions.

From my personal view I would recommend to use the pattern  $e |- ( ( ph /\ x = Y ) -> A = B ) $ only. Although this is not always necessary, it is often convenient to have all assumptions/prerequistes provided by ph available in a proof using such a theorem to show that A = B actually holds.

Alexander

[Olivier Binda]

Thanks a lot Giovanni and Alexander for the answers

In one of the proof that I must write, I have the asumption
|- ( ph -> ( j = ( k-K ) -> A = B ) ) where ph may be any wff

I would love to have $e |- ( ( ph /\ x = Y ) -> A = B ) $ as this would enable me to use fsumshift

Is there a trick to use fsumshift, as is in this situation  ?

Or is my only hope the deduiction theorem/or proving a version of fsumshift with the hypothesis

$e |- ( ( ph /\ x = Y ) -> A = B ) $ ?

Alexander, when you say  "the patterns $e |- ( x = Y -> A = B ) $. or $e |- ( ( ph /\ x = Y ) -> A = B ) $. for hypotheses are also allowed for deduction style theorems",

do you suggest that they are equivalent ? IMO, the first hypothesis is stronger than the second one.

[Norman Megill]

fsumshft.5 doesn't have a "ph ->" antecedent because its purpose is simply to specify that B is a substitution instance of A.  We sometimes call this "implicit substitution" as opposed to "explicit substitution", which would be B = [. ( k - K ) / j ]. A (or just using [. ( k - K ) / j ]. A in place of B instead of having a separate hypothesis).

Compare, for example, the implicit substitutions in first 4 hypotheses of the deduction form nn0indd.

In order to use a theorem with implicit substitution, the proof usually eliminates the implicit substitution hypotheses with a chain of equality and/or biconditional theorems.  The hypotheses are then completely eliminated, and ph is hardly ever needed to achieve that (if ever).  So we rarely bother to add a ph antecedent.  Offhand I can't recall a case where it would have helped in practice.

The primary reason we tend to use implicit substitution rather than explicit substitution is to obtain shorter proofs.  Note that (in this case) the variable j doesn't appear in B i.e. $d j B.  If instead we used [. ( k - K ) / j ]. A, we might have to use say reximd in place of reximdv, requiring a chain of nf* theorems to eliminate the "not free in" hypotheses and maybe making the proof longer.  Or, alternately, we could use intermediate dummy variables with cbv* + reximdv, also making the proof longer.

There are also theorems like sbcie to convert implicit to explicit.  Occasionally we have both versions of a theorem such as finds1 (implicit) vs. findes (explicit).  Note that the latter hasn't found a use yet.

Norm

[Olivier Binda]

I have not grasped what I wanted (yet). But Thanks to your 3 answers, I think that I understand a bit your point.
I will now have to ponder your answers a lot. There is a lot to think about in here for me. I'll try to get it (real hard, because I really really need this knowledge)

Many thanks for your answers and for the kind help :)

[Alexander van der Vekens]

Olivier, maybe an approach for your problem could be to transform B into an expression C which looks like A (except that it has ( k - K ) instead of j) and then apply ~ fsumshft:

...
5 ?              $? |- ( j = ( k - K ) -> A = C )
6 1,2,3,4,5 fsumshft  $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) C )
7 ?              $? |- ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> C = B )
8 7 sumeq2dv     $p |- ( ph -> sum_ k e. ( ( M + K ) ... ( N + K ) ) C = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
9 6,8 eqtrd      $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )

Example:
Assume there is the following hypothesis for your theorem: ph -> A. k e. NN0 B = ( X + ( 2 - ( k - K ) ) )

To prove ( ph -> sum_ j e. ( M ... N ) ( X + ( 2 - j ) ) = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) you can choose C = ( X + ( 2 - ( k - K ) ) ). Then you can prove step 7 in the template above

using the hypothesis, and afterwards you can prove step 5 easily, because it would become ( j = ( k - K ) -> ( X + ( 2 - j ) ) = ( X + ( 2 - ( k - K ) ) ) ).

Maybe this helps,

Alexander

[Alexander van der Vekens]

On Tuesday, October 29, 2019 at 10:46:39 PM UTC+1, Norman Megill wrote:

In order to use a theorem with implicit substitution, the proof usually eliminates the implicit substitution hypotheses with a chain of equality and/or biconditional theorems.  The hypotheses are then completely eliminated, and ph is hardly ever needed to achieve that (if ever).  So we rarely bother to add a ph antecedent.  Offhand I can't recall a case where it would have helped in practice.

Although the cases may be rare, they do exist (as Olivier`s case shows, and I had such cases, too - unfortunately, I do not exactly remember them). And it takes always a long time to find a proper solution. On the other way round, if we had an antecedent ( ph /\ ... ) in a hypothesis and we do not need it, it is a matter of about one second to apply ~ adantl to remove the ph and to continue.

Therefore, it should be a recommendation (not an obligation) to provide such hypotheses ( $e |- ( ( ph /\ x = Y ) -> A = B ) $. ) instead of $e |- ( x = Y -> A = B ) $. , as I proposed in my yesterdays post. As Olivier correctly stated, $e |- ( x = Y -> A = B ) $. is "stronger", i.e. more restrictive than $e |- ( ( ph /\ x = Y ) -> A = B ) $. - and I think we should preferably provide theorems with the weakest assumptions as possible.

[Olivier Binda]

After considering things through, I understand what Norman/Alexander/Giovani were saying : 
some hypothesis are just there to allow the theorem to do it's (verification) job. And are not really "needed", when you do an index shift in a sum, you apply a formula like k+->k+a to the index and it is the responsability of the theorem to propagate the changes in the formulas.
a e. ZZ is a necessary hypothesis to be allowed to do the transformation and, of course, the sum should be valid.

Also, "implicit" substitutions allow metamath to check the validity on a substitution but also do a lot more work than explicit substitution (there are equalities and transitivity involved).
So, IMO, theorems with implicit substitutions (they allow multiple steps to be done in one go) may be a lot better/more powerfull than the same theorem with an explicit substitution (which do a single step)... though, depending how the explicit substitution is done, it may allow to circumvent the limitations imposed on the implicit substitution crippled by the lack of (ph -> (but it will involve a lot of steps) 

Now, I concur with the opinion of Alexander.

Proving that |- sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + 1 ) = sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - 1 ) can be achieved 

through the implicit substitutions of fsumshift or explicit substitutions

But proving that |- ( x = 1 -> sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - ( x x. x ) )

CANNOT be proved by fsumshift, it may be proved by explicit substitutions (provided they allow the use of ( x = 1 -> ), but by using a lot more steps, which defeat the purpose of having a single theorem call prove the equality

In the opposite, fsumshift with e |-  ( ( ph /\\ k = ( j - k) ... ) -> in place of fsumshift.5 would allow us to prove this equality in a single theorem call.

So, I would suggest also that all deduction theorems should use    hypotheses like ( $e |- ( ( ph /\ x = Y ) -> A = B ) $. ) instead of $e |- ( x = Y -> A = B ) $ as, Alexander recommanded. 

Also, I believe that the example I gave is a concrete case usefull in the real world. (my aim is to enable average humans/students to use metamath to do regular classical maths)

Best regards and many thanks to you all.

Olivier 

[Thierry Arnoux]

Hi Olivier,

To illustrate Alexander's explanation with your example, I attach a proof of your statement in set.mm:

|- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 ... 3 ) ( ( 2 x. j ) - ( x x. x ) )

The main steps are following Alexander's model:

170::fsumshft         |- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ( ( 2 x. ( j - 1 ) ) + x ) )
210::                 |- ( x = 1 -> ( ( 0 + 1 ) ... ( 2 + 1 ) ) = ( 1 ... 3 ) )
510::                 |- ( ( x = 1 /\ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ) -> ( ( 2 x. ( j - 1 ) ) + x ) = ( ( 2 x. j ) - ( x x. x ) ) )
520:210,510:sumeq12dv |- ( x = 1 -> sum_ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ( ( 2 x. ( j - 1 ) ) + x ) = sum_ j e. ( 1 ... 3 ) ( ( 2 x. j ) - ( x x. x ) ) )
qed:170,520:eqtrd     |- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 ... 3 ) ( ( 2 x. j ) - ( x x. x ) ) )

BR,
_
Thierry

[Olivier Binda]

Thank you Thierry for the illustration.

You can indeed do that. I'm guessing that the first step uses fsumshft without antecedent, that are later added with ps |- (ph -> ps )

It helps but I am not sure that it will solve my issue : 

I'm writing an ide/system where the user will be provided with 

( ph -> ( j = ( k - K ) -> A = B ) )

where ph may be anything (it depends on what changes the user would have done in other parts of a statement) and so, the system would have to use first fsumshift, 

then add antecedents with ps |- (ph -> ps )

and then do the appropriate steps (without human intervention/help) that you did with mmj2 (I'm guessing)

It might be possible and your illustration shows the way.

I'll look into it. That would remove now, my need for a Mephistolus-friendly variant of fsumshift and also resolve the issues I would have in identical situations with other theorems.

Thank you for the tip :)

[Norman Megill]

On Wednesday, October 30, 2019 at 6:47:24 AM UTC-4, Olivier Binda wrote:

After considering things through, I understand what Norman/Alexander/Giovani were saying : 
some hypothesis are just there to allow the theorem to do it's (verification) job. And are not really "needed", when you do an index shift in a sum, you apply a formula like k+->k+a to the index and it is the responsability of the theorem to propagate the changes in the formulas.
a e. ZZ is a necessary hypothesis to be allowed to do the transformation and, of course, the sum should be valid.

Also, "implicit" substitutions allow metamath to check the validity on a substitution but also do a lot more work than explicit substitution (there are equalities and transitivity involved).
So, IMO, theorems with implicit substitutions (they allow multiple steps to be done in one go) may be a lot better/more powerfull than the same theorem with an explicit substitution (which do a single step)... though, depending how the explicit substitution is done, it may allow to circumvent the limitations imposed on the implicit substitution crippled by the lack of (ph -> (but it will involve a lot of steps) 

Now, I concur with the opinion of Alexander.

Proving that |- sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + 1 ) = sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - 1 ) can be achieved 

through the implicit substitutions of fsumshift or explicit substitutions

But proving that |- ( x = 1 -> sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - ( x x. x ) )

CANNOT be proved by fsumshift, it may be proved by explicit substitutions (provided they allow the use of ( x = 1 -> ), but by using a lot more steps, which defeat the purpose of having a single theorem call prove the equality

The implicit substitution hypothesis "fsumshft.5 $e |- ( j = ( k - K ) -> A = B ) $." is meant to let us show that B is the same as A with k - K substituted for j.  That is its only purpose, and that is why we normally keep it simple (no ph antecedent).

An attempt to use it for

|- ( x = 1 -> sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - ( x x. x ) )

tries to abuse this purpose, because sum_ j e. ( 1 .. 3 ) ( ( 2x. j ) - ( x x. x ) ) is not a substitution instance of sum_ k e. ( 0 .. 2 ) ( ( 2 x. k ) + x ) but involves things other than substitution.  Such a manipulation would normally be done elsewhere in the proof.

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.

This situation is analogous to our frequent use of definitional hypotheses such as |- A = ( B + C ).  This lets us use A to abbreviate the longer ( B + C ).  But we can't prove that |- A = ( C + B ) from this hypothesis.  We accept that, and normally we don't change it to "|- ( ph -> A = ( B + C ) )" to make the theorem more "general" since that would cause other proofs using the theorem to be slightly longer than necessary.

Norm

[Olivier Binda]

I believe that I see your point now.

fsumshift is an operation that should perform a single task : a shift of the index in a sum and not some magic (or it would confuse proofs/humans/reasoning).
After all, this is how I have been (correctly) using fsumshift in maths for the last 20 years,
so because there is a way to make a theorem "More powerfull" by slightly changing the way it is written is not a good reason to deform the theorem and it's purpose.

Got it. Thanks :)

In the process of proving Mephistolus theorems with metamath, I have to rethink how the Mephistolus theorem should be written, to perform good and sane maths.
before I try to prove them. Metamath is a wonderfull mentor.

[Norman Megill]

Getting back to your original question, we can prove fsumshft with your modified (weaker) fsumshft.5 starting from directly from fsumshft with the stronger fsumshft.5.  I show a proof here:

http://us2.metamath.org/mpeuni/fsumshftdOLD.html

To summarize the proof, we use csbeq1 at step 15 to eliminate the hypothesis fsumshft.5.  This converts the implicit substitution to an explicit substitution version of fsumshft at step 16.  Next we use cbvsumi at steps 18 and 25 to change the dummy variables x and y in the fsumshft conclusion to j and k.  Of particular interest is the use of csbied at step 30, which, using the new (weaker) hypothesis fsumshftd.5, results in [_ ( k - K ) / j ]_ A = B to get rid of the explicit substitution on A and result in B.

The proof is somewhat long.  Maybe someone can find a shorter proof or devise a library theorem to simplify this conversion.  But given its current size, this technique probably shouldn't be used routinely just to allow using fsumshftd.5 for things other than simple substitutions, unless the size savings in the target theorem's proof compensates for the size of the fsumshftd proof.

Norm

On Monday, October 28, 2019 at 5:18:40 PM UTC-4, Olivier Binda wrote:

[Norman Megill]

By using one less dummy variable, I found a shorter proof that might be easier to understand, updated at

http://us2.metamath.org/mpeuni/fsumshftd.html

To summarize the proof, we use csbeq1 at step 17 to eliminate the hypothesis fsumshft.5.  This converts the implicit substitution to an explicit substitution version of fsumshft at step 18.  Note that fsumshft requires $d j B, which is not satisfied when we substitute [_ ( k - K ) / j ]_ A for B.  So to avoid a dv conflict, we use dummy variable w instead of j.  We use cbvsumi at step 4 to change w in the fsumshft conclusion to j.  Of particular interest is the use of csbied at step 22, which, using the new (weaker) hypothesis fsumshftd.5, gives us [_ ( k - K ) / j ]_ A = B to get rid of the explicit substitution on A and result in B.

Norm

On Friday, November 1, 2019 at 1:27:50 PM UTC-4, Norman Megill wrote:

Getting back to your original question, we can prove fsumshft with your modified (weaker) fsumshft.5 starting from directly from fsumshft with the stronger fsumshft.5.  I show a proof here:

http://us2.metamath.org/mpeuni/fsumshftdOLD.html

To summarize the proof, we use csbeq1 at step 15 to eliminate the hypothesis fsumshft.5.  This converts the implicit substitution to an explicit substitution version of fsumshft at step 16.  Next we use cbvsumi at steps 18 and 25 to change the dummy variables x and y in the fsumshft conclusion to j and k.  Of particular interest is the use of sbcied at step 30, which, using the new (weaker) hypothesis fsumshftd.5, results in [_ ( k - K ) / j ]_ A = B to get rid of the explicit substitution on A and result in B.

[Alexander van der Vekens]

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..).

 

[Thierry Arnoux]

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 <meta...@googlegroups.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com.

<deduct_th_ph_eq_hyp.txt>

<deduct_th_eq_hyp.txt>

[Benoit]

> Therefore, I still would propose to recommend to use the form $e |- ( ( ph /\ x = ... ) -> ... ) $. in deduction style.

I agree. Plus, this is more systematic hence easier to remember.

> Already existing theorems need not to be rewritten

They need not but they could !

> (by the way, many of them have no "d" at the end..).

Since deduction form is the default for more advanced theorems, this makes sense.

Benoît

[Alexander van der Vekens]

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 <meta...@googlegroups.com> 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 meta...@googlegroups.com.

[Mario Carneiro]

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).

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3620ab9b-f405-43d2-821f-e15b56977eb0%40googlegroups.com.

[Alexander van der Vekens]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3620ab9b-f405-43d2-821f-e15b56977eb0%40googlegroups.com.

[Norman Megill]

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

[Alexander van der Vekens]

I think you convinced me that there are not many cases like fsumshft, and there are even less situations for such theorems in which the antecedent ph is useful in a hypothesis.

Therefore, we can end the discussion here. If I find a similar case in the future, I will revise the theorem/proof accordingly (because thanks to Norm I know how it can be done).

[Olivier Binda]

Many thanks for this post, Norman.

I am using it to prove fsumshftd from Mephistolus, by using fsumshft

I tried by myself (but had a distinct problem while using fsumsht with [_ / ]_  ... I understand now, why I need F/_ and not only distinct vars theorems
So, I started studying your proof (it helps me grow in metamath), I understood quite a few things along the way and I am really grateful

Many thanks for that answer.

:)

Olivier

[Norman Megill]

You're welcome. :)  Norm

[Olivier Binda]

Yesterday, I finally managed to prove fsumshift in Mephistolus (I could have coded something that allow me to adapt step by step (passthrough) a Metamath proof into a Mephistolus proof that is converted back into the exact same Metamath proof, but I chose instead to improve the math coverage of Mephistolus to enable it to do the proof with it's own set of tools.

This was really enlightening as I had to implement some support (I am really grateful for that, it helps Mephistolus grow a lot) for

F/
F/_
[_ / ]
[ / ]

changing bound variables...

And I finally made it yesterday evening.
Then, I tried using my shiny new fsumshift-enhanced theorem in Mephistolus with 2 antecedents and I had a bug
I fix the bug in the method that provide me dummy variables and all was working beautifully

It allowed me to get 49% of the proof converted to Metamath

/** proving that ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) */

done, and I stumbled into another obstacle, related to fsum1p :)

Actually, it is the exact same issue I had with fsumshift, so, by adapting Norm's proof to fsum1p to get a fsum1pd working, 

I should be good to go :)

But that is still going to be hard and take me a few days :)
Now that I have a beacon to follow, It might take me a few less days

Wish me luck ! ^^
Best regards,
Olivier