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.
