Yes, you can certainly state that as a subgoal in mmj2 (with a &C1 work variable) and try to prove it, and when you get to the end and know what it has been assigned to you can edit the theorem statement to use the correct value.
On Sun, Jul 28, 2024 at 10:03 PM jagra <[email protected]> wrote: > Thank you for feedback. > > Your last comment touched a very relevant point. > > From a tooling perspective, mmj2 for instance, do you think it would be > possible to replace the ? for a &C1 and work on some proof elaboration > steps that will produce the value for &C1, eventually promoting it to a > hyp? > > Best regards. > > On Sunday, July 28, 2024 at 7:24:41 PM UTC+1 [email protected] wrote: > >> I would do something like this (which is not exactly metamath syntax but >> not too hard to write precisely): >> >> 0 < k, >> 0 < l, >> F = (x e. RR |-> k*x^2 - 2*k*x + l), >> { x | F(x) = 4 } = {A, B}, >> (A - B)^2 + (F(A) - F(B))^2 = 6 >> |- (A^2 + F(A)^2) + (B^2 + F(B)^2) = ? >> >> although to actually prove it you have to first fill in the ? with the >> answer. >> >> On Sun, Jul 28, 2024 at 8:07 PM jagra <[email protected]> wrote: >> >>> Understand this is not a common, and probably not even wanted, topic on >>> this group. >>> >>> Trying to translate to metamath a simple problem from AIMO train >>> dataset, just out of curiosity. >>> >>> The problem statement is: >>> >>> Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ >>> intersects the line $y = 4$ at two points $A$ and $B$. These points are >>> distance 6 apart. What is the sum of the squares of the distances from $A$ >>> and $B$ to the origin? >>> >>> Trying to come up a direct construction of the conditions and statement >>> to prove and blocking, from my ignorance most certainly, on some >>> embarassing road blocks. >>> >>> >>> 1. Define function y=4 >>> 2. Define parabola function in terms of k and l >>> 3. Connect 1 & 2 with points A and B >>> 4. Define distance between A and B >>> 5. Define the goal in terms of A and B >>> >>> Really understand this is probably a basic question and I'm offsetting >>> my due dilligence, so, no problem if no one takes the time to answer this :) >>> >>> Best regards, >>> Jorge Agra >>> >>> -- >>> 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/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%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/b3b85824-1085-470e-848a-45e2b751f267n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b3b85824-1085-470e-848a-45e2b751f267n%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/CAFXXJSttL%3DnoQMZpmrn5F%3DeJp78P690Q7Nx%2B9ssW06RQ2zWC%2BQ%40mail.gmail.com.
