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 Le jeudi 14 novembre 2019 16:54:45 UTC+1, Norman Megill a écrit : > > You're welcome. :) Norm > > On Wednesday, November 13, 2019 at 10:23:09 AM UTC-5, Olivier Binda wrote: >> >> 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 >> >> >> Le samedi 2 novembre 2019 00:33:58 UTC+1, Norman Megill a écrit : >>> >>> 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. >>>> >>>> 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: >>>>> >>>>> Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? >>>>> >>>>> fsumshft.5 [image: |-] [image: (][image: j] [image: =] [image: (][image: >>>>> k] [image: -] [image: K][image: )] [image: ->] [image: A] [image: =] >>>>> [image: >>>>> B][image: )] >>>>> 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 >>>>> >>>> -- 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/239d5123-b154-4708-b07e-395c2a560df4%40googlegroups.com.
