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/cf66c75f-7131-4db4-ae49-64882e73912bn%40googlegroups.com.
