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/a450dc13-57c7-471c-9f41-bd484341363cn%40googlegroups.com.
