*> That's awesome, thanks for organizing this!*
I second that. Thank you Saveliy for continuing this initiative! I also was able to prove abaeqb. Similarly to Thierry’s proof, my proof also introduced a disjoint condition for a and b, whereas the task has disjoints showing that a and b should be non-disjoint. I spent some time trying to find another proof which will not require this additional disjoint for a and b, but I could not find it. On the one hand, as I understand, requiring a and b to be disjoint, means that we cannot substitute the same set for a and b simultaneously. Please correct me if I am wrong. For example, with this new disjoint we will not be able to “apply” this theorem to the statement |- ( ph -> A. x e. B A. x e. B ( x .o. x ) e. B ). Also the original d-conditions look like it was made deliberately that a and b should not be disjoint. On the other hand, it was mentioned that “beware of possible problems in the statements (especially in the d-conditions)”. Saveliy, could you please comment on that (is it legal to add a disjoint for a and b and what was your intention)? *> do you use some automation (tactics) to do substitutions into the identity, like deriving step 23 of your MPP file? Or you simply remember the movements by heart?* *> That auto-transformation we mention, is what? Do you mind explaining?* These are all good questions. I used mm-lamp, and it has some automation to prove such steps (no need to write any code, it is available out of the box). I want to record a video with some explanations on how I proved abaeqb. This is a good example for me to demonstrate automation capabilities of mm-lamp. Will it not break any rules of this initiative, if I show how to prove abaeqb? On Monday, December 2, 2024 at 6:12:07 PM UTC+1 Thierry Arnoux wrote: > On 02/12/2024 17:52, Jorge Agra wrote: > > That auto-transformation we mention, is what? Do you mind explaining? > > > For example MMJ2 is able to automatically expand this proof snippet from > just the last step: > 9::oveq1 |- ( b = Y -> ( b .o. ( X .o. Y ) ) = ( Y .o. ( X .o. Y ) ) ) > 10:9:oveq2d |- ( b = Y -> ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) ) = ( ( > X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) ) > 11::id |- ( b = Y -> b = Y ) > !12:10,11:eqeq12d |- ( b = Y -> ( ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) > ) = b <-> ( ( X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) = Y ) ) > > All it needs is the exclamation mark before the label and once the Unify > command is called (Ctrl-U), it will generate all 3 steps above. > > Yamma does not have this and I manually fill in `eqeq12d` among a short > list. Then it will automatically find `id` as it is a one-step proof. I > have to choose `oveq1d` over a short list (the first theorem in the list is > often the correct one), and finally it find `oveq1` automatically. > > MMJ2's auto-transformation is mentioned here: > https://github.com/digama0/mmj2/blob/c8dd05548139c7003220caedde65a7abe44a00bf/CHGLOG.TXT#L47 > > > -- 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 visit https://groups.google.com/d/msgid/metamath/6ab2306f-fda2-45b5-91b5-96951e725f76n%40googlegroups.com.
