Hi Igor, I haven't tried the proof myself, a little short on time right now, but I have doubts about why you are trying to prove F(a) = 4 or F(b). It seems to me this is given, an hypothesis, right?
Regards, Jorge On Wed, Oct 16, 2024 at 8:41 AM Igor Ieskov <[email protected]> wrote: > Hi Glauco, > > > Yes, this answers my question. Thank you very much. Also I found this > thread <https://groups.google.com/g/metamath/c/1T18-hzCw5E/m/Igpc2gWFBAAJ> > contains other shortcuts used in the video. > > > I don’t have much experience with mmj2. I used it to repeat proofs from > David’s video tutorials, but not for creating my own proofs. > > > - > > Igor > > > On Tuesday, October 15, 2024 at 11:50:12 PM UTC+2 Glauco wrote: > >> Hi Igor, >> >> with regard to your question, yamma, for now, is similar to mmj2. Do you >> have some experience with mmj2? >> >> I tend to proof backwards, thus yamma may have a bias toward this >> approach. >> >> Did you see this simple video? >> >> https://www.youtube.com/watch?v=N7W0VBsbOcQ >> >> As you can see, when it has to prove >> >> |- E. x x e. { 1 } >> >> if you hit ctrl+space , intellisense shows you the labels that are more >> likely to move you in the right direction. >> >> The one I chose is the 6th one, that is ceqsexv2d (intellisense details >> clearly show me that's the one I'm looking for) >> >> I would not be able to know it myself, so it saves me some search time. >> >> eximii , the first one suggested, is not the right one, but I can easily >> see why it's, in general, a good candidate for the given statement >> >> HTH >> Glauco >> >> >> >> Il giorno lunedì 14 ottobre 2024 alle 22:48:36 UTC+2 [email protected] >> ha scritto: >> >>> Thank you Glauco and Mario for helpful answers. I will need some time to >>> analyze and understand everything you wrote. >>> >>> >>> For now, I have one question. Glauco, you mentioned that you developed >>> this proof using Yamma. Can you explain at a high level what steps you’ve >>> done in Yamma to come up with such a proof? I am asking for the proof >>> of |- ( F ` a ) = 4. No need to explain how to set up Yamma, it can be >>> found in its readme >>> <https://github.com/glacode/yamma/blob/master/README.md>. I am more >>> interested in how much of this proof was constructed by Yamma and how much >>> was manual work. I didn’t have time yet to try to prove this in Yamma, but >>> I will surely try. So, what I think would be interesting for me (and >>> probably for others) is a high level list of actions you’ve done to create >>> this proof. For example: >>> >>> >>> 1) put all required hypotheses and the goal statement to Yamma. >>> >>> 2) I know that for such kind of proofs elrab assertion is usually used, >>> so type its name in and unify (press CTRL+U). New steps appeared. >>> >>> 3) … >>> >>> >>> I will be very surprised if you’ve just provided the hypotheses and the >>> goal statement and Yamma found everything else! >>> >>> >>> Sorry, if I am requesting too much. You can respond as high level or >>> detailed depending on how much free time you have. I am asking because I >>> tried to prove this using mm-lamp. Since I don’t know set.mm assertions >>> well, I just searched for assertions which I thought could be used in the >>> proof and tried to combine them somehow. I am interested in how you came up >>> with this proof (how much automation you used and how much your experience >>> with set.mm). >>> >>> >>> BTW, it is Igor writing :) >>> >>> >>> - >>> >>> Igor >>> >>> >>> On Monday, October 14, 2024 at 5:05:35 PM UTC+2 Glauco wrote: >>> >>>> Below is a full contradiction derived. >>>> >>>> >>>> It's amazing to see how ChatGPT can understand set.mm even though I >>>> guess there's not much content, when compared to other subjects. >>>> >>>> Here's a brief "conversation" (not perfect, but close...): >>>> >>>> https://chatgpt.com/share/670d3203-1d2c-8010-bb5b-2e4105fc5379 >>>> >>>> >>>> >>>> h1::temp4.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>>> 2::pnfex |- +oo e. _V >>>> 3::preq1 |- ( a = +oo -> { a , b } = { +oo , b } ) >>>> 4:3:eqeq2d |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } = >>>> { a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) ) >>>> 5:2,4,1:vtocl |- { x e. RR | ( F ` x ) = 4 } = { +oo , b } >>>> 6:2:prid1 |- +oo e. { +oo , b } >>>> 7:6,5:eleqtrri |- +oo e. { x e. RR | ( F ` x ) = 4 } >>>> 8::elrabi |- ( +oo e. { x e. RR | ( F ` x ) = 4 } -> +oo e. >>>> RR ) >>>> 9:7,8:ax-mp |- +oo e. RR >>>> 10::pnfnre2 |- -. +oo e. RR >>>> qed:9,10:pm2.24ii |- F. >>>> >>>> $= ( cpnf cr wcel wfal cv cfv c4 wceq crab cpr pnfex prid1 preq1 eqeq2d >>>> vtocl >>>> eleqtrri elrabi ax-mp pnfnre2 pm2.24ii ) >>>> FGHZIFAJBKLMZAGNZHUFFFDJZOZUHFUIPQU >>>> HCJZUIOZMUHUJMCFPUKFMULUJUHUKFUIRSETUAUGAFGUBUCUDUE $. >>>> >>>> >>>> $d a x >>>> $d a b >>>> $d F a >>>> >>>> Il giorno lunedì 14 ottobre 2024 alle 16:25:31 UTC+2 [email protected] >>>> ha scritto: >>>> >>>>> That's the first part of the proof. The second part of the proof is to >>>>> show a contradiction from this, because +oo is in the RHS but not the LHS >>>>> of that equality. >>>>> >>>>> On Mon, Oct 14, 2024 at 3:24 PM Glauco <[email protected]> wrote: >>>>> >>>>>> I think I got it. Thank you very much for the insight. >>>>>> >>>>>> h1::temp4.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>>>>> 2::pnfex |- +oo e. _V >>>>>> 3::preq1 |- ( a = +oo -> { a , b } = { +oo , b } ) >>>>>> 4:3:eqeq2d |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } = { >>>>>> a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) ) >>>>>> qed:2,4,1:vtocl |- { x e. RR | ( F ` x ) = 4 } = { +oo , b } >>>>>> >>>>>> $= ( cv cfv c4 wceq cr crab cpr cpnf pnfex preq1 eqeq2d vtocl ) >>>>>> AFBGHIAJKZCFZDF >>>>>> ZLZIRMTLZICMNSMIUAUBRSMTOPEQ $. >>>>>> >>>>>> $d a x >>>>>> $d a b >>>>>> $d F a >>>>>> >>>>>> >>>>>> Il giorno lunedì 14 ottobre 2024 alle 15:02:42 UTC+2 Glauco ha >>>>>> scritto: >>>>>> >>>>>>> Hi Mario, >>>>>>> >>>>>>> I'm sure you're right, and in fact I would use a class A and >>>>>>> something like ph -> A e. V as an additional hyp. >>>>>>> >>>>>>> But I cannot reproduce the contradiction off the top of my head; it >>>>>>> would be interesting to see it, to gain a deeper understanding. >>>>>>> >>>>>>> Can you please show a short proof? (do you proof something like +oo >>>>>>> e. RR ? ) >>>>>>> >>>>>>> Thank you >>>>>>> Glauco >>>>>>> >>>>>>> >>>>>>> Il giorno lunedì 14 ottobre 2024 alle 14:28:43 UTC+2 >>>>>>> [email protected] ha scritto: >>>>>>> >>>>>>>> It's not safe to make an assumption of the form |- { x e. RR | ( F >>>>>>>> ` x ) = 4 } = { a , b } because the variables a,b are implicitly >>>>>>>> universally quantified in the hypothesis, which means you can prove a >>>>>>>> contradiction from it. (Consider what happens if you use vtocl on the >>>>>>>> hypothesis to replace a by +oo.) You should either use class >>>>>>>> variables A,B as I indicated, or add a context ph -> before every >>>>>>>> assumption (which is *not* assumed to be disjoint from a,b). >>>>>>>> >>>>>>>> On Mon, Oct 14, 2024 at 2:12 PM Glauco <[email protected]> >>>>>>>> wrote: >>>>>>>> >>>>>>>>> I take it back, you can get away with { x | ( F ` x ) = 4 } , >>>>>>>>> here's the proof (but for your larger goal, I doubt it's enough) >>>>>>>>> >>>>>>>>> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) >>>>>>>>> ) - ( ( 2 x. k ) x. x ) ) + l ) ) >>>>>>>>> h2::temp3.2 |- { x | ( F ` x ) = 4 } = { a , b } >>>>>>>>> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >>>>>>>>> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = >>>>>>>>> 4 ) ) >>>>>>>>> 5::vex |- a e. _V >>>>>>>>> 6::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2 >>>>>>>>> ) ) - ( ( 2 x. k ) x. x ) ) + l ) ) >>>>>>>>> 7:1,6:nfcxfr |- F/_ x F >>>>>>>>> 8::nfcv |- F/_ x a >>>>>>>>> 9:7,8:nffv |- F/_ x ( F ` a ) >>>>>>>>> 10:9:nfeq1 |- F/ x ( F ` a ) = 4 >>>>>>>>> 11:10,5,4:elabf |- ( a e. { x | ( F ` x ) = 4 } <-> ( F ` a ) >>>>>>>>> = 4 ) >>>>>>>>> 12::vex |- a e. _V >>>>>>>>> 13:12:prid1 |- a e. { a , b } >>>>>>>>> 14:13,2:eleqtrri |- a e. { x | ( F ` x ) = 4 } >>>>>>>>> qed:14,11:mpbi |- ( F ` a ) = 4 >>>>>>>>> >>>>>>>>> $= ( cv cfv c4 wceq cab wcel cpr vex cr c2 co cmul prid1 cexp cmin >>>>>>>>> caddc nfmpt1 >>>>>>>>> eleqtrri cmpt nfcxfr nfcv nffv nfeq1 fveq2 eqeq1d elabf mpbi ) >>>>>>>>> DIZAIZCJZKLZA >>>>>>>>> >>>>>>>>> >>>>>>>>> MZNUPCJZKLZUPUPEIZOUTUPVCDPZUAHUFUSVBAUPAVAKAUPCACAQBIZUQRUBSTSRVETSUQTSUCSF >>>>>>>>> IUDSZUGGAQVFUEUHAUPUIUJUKVDUQUPLURVAKUQUPCULUMUNUO $. >>>>>>>>> >>>>>>>>> $d a x >>>>>>>>> >>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 13:53:35 UTC+2 Glauco ha >>>>>>>>> scritto: >>>>>>>>> >>>>>>>>>> Since the >>>>>>>>>> >>>>>>>>>> $d F x >>>>>>>>>> >>>>>>>>>> constraint would conflict with your F definition, here is an >>>>>>>>>> alternative version >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> h1::temp3.1 |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 >>>>>>>>>> ) ) - ( ( 2 x. k ) x. x ) ) + l ) ) >>>>>>>>>> h2::temp3.2 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>>>>>>>>> 3::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >>>>>>>>>> 4:3:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) >>>>>>>>>> = 4 ) ) >>>>>>>>>> 5::nfcv |- F/_ x a >>>>>>>>>> 6::nfcv |- F/_ x RR >>>>>>>>>> 7::nfmpt1 |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ >>>>>>>>>> 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) ) >>>>>>>>>> 8:1,7:nfcxfr |- F/_ x F >>>>>>>>>> 9:8,5:nffv |- F/_ x ( F ` a ) >>>>>>>>>> 10:9:nfeq1 |- F/ x ( F ` a ) = 4 >>>>>>>>>> 11:5,6,10,4:elrabf |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( >>>>>>>>>> a e. RR /\ ( F ` a ) = 4 ) ) >>>>>>>>>> 12::vex |- a e. _V >>>>>>>>>> 13:12:prid1 |- a e. { a , b } >>>>>>>>>> 14:13,2:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 } >>>>>>>>>> 15:14,11:mpbi |- ( a e. RR /\ ( F ` a ) = 4 ) >>>>>>>>>> qed:15:simpri |- ( F ` a ) = 4 >>>>>>>>>> >>>>>>>>>> $= ( cv cr wcel cfv c4 wceq crab wa nfcv c2 co cmul cpr vex prid1 >>>>>>>>>> eleqtrri cexp >>>>>>>>>> cmin caddc cmpt nfmpt1 nfcxfr nffv nfeq1 fveq2 eqeq1d elrabf >>>>>>>>>> mpbi simpri ) D >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> IZJKZURCLZMNZURAIZCLZMNZAJOZKUSVAPURUREIZUAVEURVFDUBUCHUDVDVAAURJAURQZAJQAUT >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> MAURCACAJBIZVBRUESTSRVHTSVBTSUFSFIUGSZUHGAJVIUIUJVGUKULVBURNVCUTMVBURCUMUNUO >>>>>>>>>> UPUQ $. >>>>>>>>>> >>>>>>>>>> $d a x >>>>>>>>>> >>>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 13:42:45 UTC+2 Glauco ha >>>>>>>>>> scritto: >>>>>>>>>> >>>>>>>>>>> Hi Jorge, >>>>>>>>>>> >>>>>>>>>>> with Yamma you get something like this (I doubt you can get >>>>>>>>>>> away with { x | ( F ` x ) = 4 }, for instance ( F ` +oo ) is >>>>>>>>>>> not "well-defined" ) >>>>>>>>>>> >>>>>>>>>>> ``` >>>>>>>>>>> $theorem temp3 >>>>>>>>>>> >>>>>>>>>>> * comments >>>>>>>>>>> >>>>>>>>>>> h1::temp3.1 |- { x e. RR | ( F ` x ) = 4 } = { a , b } >>>>>>>>>>> 2::fveq2 |- ( x = a -> ( F ` x ) = ( F ` a ) ) >>>>>>>>>>> 3:2:eqeq1d |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a >>>>>>>>>>> ) = 4 ) ) >>>>>>>>>>> 4:3:elrab |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( >>>>>>>>>>> a e. RR /\ ( F ` a ) = 4 ) ) >>>>>>>>>>> 5::vex |- a e. _V >>>>>>>>>>> 6:5:prid1 |- a e. { a , b } >>>>>>>>>>> 7:6,1:eleqtrri |- a e. { x e. RR | ( F ` x ) = 4 } >>>>>>>>>>> 8:7,4:mpbi |- ( a e. RR /\ ( F ` a ) = 4 ) >>>>>>>>>>> qed:8:simpri |- ( F ` a ) = 4 >>>>>>>>>>> >>>>>>>>>>> $= ( cv cr wcel cfv c4 wceq crab wa cpr vex prid1 eleqtrri fveq2 >>>>>>>>>>> eqeq1d elrab >>>>>>>>>>> mpbi simpri ) >>>>>>>>>>> CFZGHZUCBIZJKZUCAFZBIZJKZAGLZHUDUFMUCUCDFZNUJUCUKCOPEQUIUFAUCG >>>>>>>>>>> UGUCKUHUEJUGUCBRSTUAUB $. >>>>>>>>>>> >>>>>>>>>>> $d F x >>>>>>>>>>> $d a x >>>>>>>>>>> ``` >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Il giorno lunedì 14 ottobre 2024 alle 12:40:47 UTC+2 >>>>>>>>>>> [email protected] ha scritto: >>>>>>>>>>> >>>>>>>>>>>> I wanted to check how far I can get in formalizing this problem >>>>>>>>>>>> and its solution. But I stuck in the very beginning. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Firstly, I formalized the initial conditions as Mario suggested: >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> hyp1: |- 0 < k >>>>>>>>>>>> >>>>>>>>>>>> hyp2: |- 0 < l >>>>>>>>>>>> >>>>>>>>>>>> hyp3: |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k >>>>>>>>>>>> ) x. x ) ) + l ) ) >>>>>>>>>>>> >>>>>>>>>>>> hyp4: |- { x | ( F ` x ) = 4 } = { a , b } >>>>>>>>>>>> >>>>>>>>>>>> hyp5: |- ( ( ( a - b ) ^ 2 ) + ( ( ( F ` a ) - ( F ` b ) ) ^ 2 >>>>>>>>>>>> ) ) = ( 6 ^ 2 ) >>>>>>>>>>>> >>>>>>>>>>>> hyp6: |- ( ( ( a ^ 2 ) + ( ( F ` a ) ^ 2 ) ) + ( ( b ^ 2 ) + ( >>>>>>>>>>>> ( F ` b ) ^ 2 ) ) ) = c >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> I used { a , b } instead of { A , B } because then I can >>>>>>>>>>>> easily prove |- a e. _V, which is used in the proof below. >>>>>>>>>>>> Also, as I understand, a and b represent x-coordinates of the >>>>>>>>>>>> corresponding >>>>>>>>>>>> points. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Next, I wanted to simplify hyp5, by proving that F(a) = F(b) = >>>>>>>>>>>> 4, so the hyp5 would be |- ( ( a - b ) ^ 2 ) = ( 6 ^ 2 ). But >>>>>>>>>>>> that’s where I am stuck. I can prove |- [ a / x ] ( F ` x ) = 4 >>>>>>>>>>>> which looks a right direction to move in: >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> 1| | vex | |- a e. _V >>>>>>>>>>>> >>>>>>>>>>>> 2| 1 | prid1 | |- a e. { a , b } >>>>>>>>>>>> >>>>>>>>>>>> 3| | hyp4 | |- { x | ( F ` x ) = 4 } = { a , b } >>>>>>>>>>>> >>>>>>>>>>>> 4| 3 | eleq2i | |- ( a e. { x | ( F ` x ) = 4 } <-> a e. { a >>>>>>>>>>>> , b } ) >>>>>>>>>>>> >>>>>>>>>>>> 5| 2,4 | mpbir | |- a e. { x | ( F ` x ) = 4 } >>>>>>>>>>>> >>>>>>>>>>>> 6| | df-clab | |- ( a e. { x | ( F ` x ) = 4 } <-> [ a / x >>>>>>>>>>>> ] ( F ` x ) = 4 ) >>>>>>>>>>>> >>>>>>>>>>>> 7| 5,6 | mpbi | |- [ a / x ] ( F ` x ) = 4 >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> But I still cannot prove |- ( F ` a ) = 4. Any suggestions >>>>>>>>>>>> what approaches I can try to prove this? >>>>>>>>>>>> >>>>>>>>>>>> On Sunday, July 28, 2024 at 11:54:47 PM UTC+2 [email protected] >>>>>>>>>>>> wrote: >>>>>>>>>>>> >>>>>>>>>>>>> On Sun, Jul 28, 2024 at 11:43 PM Glauco <[email protected]> >>>>>>>>>>>>> wrote: >>>>>>>>>>>>> >>>>>>>>>>>>>> I maybe wrong, but my feeling is that what Jagra calls A , in >>>>>>>>>>>>>> Mario's translation is actually < A , 4 > (or < A, F(A) > , if >>>>>>>>>>>>>> you >>>>>>>>>>>>>> prefer). >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> I meant it to be interpreted as <A, F(A)>, and part of the >>>>>>>>>>>>> proof would be showing that F(A) = 4 so that the rest of the >>>>>>>>>>>>> statement >>>>>>>>>>>>> simplifies. (But that would seem to be part of the proof, not the >>>>>>>>>>>>> formalization of the statement, if we want to read it literally.) >>>>>>>>>>>>> >>>>>>>>>>>>> -- >>>>>>>>> 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/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com >>>>>>>>> <https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>>>>> . >>>>>>>>> >>>>>>>> -- >>>>>> 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/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%40googlegroups.com >>>>>> <https://groups.google.com/d/msgid/metamath/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>> . >>>>>> >>>>> -- > 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/0466031a-8f6f-4d1d-8a69-8ff2351dc4f6n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/0466031a-8f6f-4d1d-8a69-8ff2351dc4f6n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAAoC84xyvx4%2BkFEHrGY3XmiTf4LoJXvFDuHDgXg3A7M%2BnXzbmw%40mail.gmail.com.
