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. Le jeudi 31 octobre 2019 13:55:27 UTC+1, Norman Megill a écrit : > > 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/ebc24b23-e6bd-434e-a335-eec502b4feb4%40googlegroups.com.
