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 -- 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/19033d18-f2a5-461e-bd48-52f089c9d8f0%40googlegroups.com.
