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 Le mercredi 30 octobre 2019 07:24:51 UTC+1, Alexander van der Vekens a écrit : > > > > 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. > -- 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/aeeb7d07-705c-4012-a910-3baee5f2ef6f%40googlegroups.com.
