This reminds me of another kind of analysis which I would like to do at some point, which I think amounts to a slightly generalized version of your analysis (most likely with even more blowup in the search space...).
If we think of a metamath proof as a tree of theorem applications, then we can identify commonly occurring subtrees. A subtree here would be some root theorem (which may occur as a step anywhere in the containing theorem), and then some choice of lemmas leading into it, and some lemmas leading to those lemmas and so on, where you can choose to cut the tree off at any hypothesis to get a leaf. For example, the test1 example corresponds to the subtree eqeltri(-, fvex()), but we could also look for e.g. eqeltri(0re(), -) or eqeltri(0re(), eqtri(-, -)) or any other subtree structure like that. Once we have a subtree structure, we can uniquely reconstruct the theorem as the "most general unifier" of the applications. For example eqeltri(0re(), eqtri(-, -)) corresponds to the theorem: $e |- 0 = A $e |- A = B $p |- B e. RR (This is probably not a common occurrence; I haven't actually done the analysis.) It's a bit more expensive of an analysis than looking for proof sequences (which correspond roughly to right-leaning subtrees) since you have to actually parse the proof into a tree/dag, but I still wonder about what things you could find. On Wed, Jul 6, 2022 at 9:08 AM savask <[email protected]> wrote: > >That's great, but I do not really know how to get this theorem (including > its proof) from the sequence ["fvex","eqeltri"]. How does the > reverse-engineering work in mmj2? > > The sequence of labels "fvex", "eqeltri" is the sequence of essential > steps in the compressed proof of our theorem. For example in metamath.exe: > > MM>show proof test1/lemmon > 6 test1.1 $e |- A = ( F ` B ) > 9 fvex $p |- ( F ` B ) e. _V > 10 6,9 eqeltri $p |- A e. _V > > To deduce the theorem from the sequence of labels in mmj2, I do as follows > (note that there might be a better way). Start with a clean proof: > > 10:: > qed:: |- ph > > Then set the theorem in 10 to eqeltri and unify with Ctrl-U: > > !d1:: |- &C1 = &C2 > !d2:: |- &C2 e. &C3 > 10:d1,d2:eqeltri |- &C1 e. &C3 > qed:: |- ph > > Now set the theorem in !d2 to fvex and unify: > > !d1:: |- &C1 = ( &C5 ` &C4 ) > d2::fvex |- ( &C5 ` &C4 ) e. _V > 10:d1,d2:eqeltri |- &C1 e. _V > qed:: |- ph > > Fill in the meta variables: > > !d1:: |- A = ( F ` B ) > d2::fvex |- ( F ` B ) e. _V > 10:d1,d2:eqeltri |- A e. _V > qed:: |- ph > > Finally, set step 10 to qed and rename all unproven steps to hypotheses > (only !d1 in our case): > > h1::test1.1 |- A = ( F ` B ) > d2::fvex |- ( F ` B ) e. _V > qed:1,d2:eqeltri |- A e. _V > > $= ( test1.1 cfv cvv fvex eqeltri ) ABCEFDBCGH $. > > For some reason mmj2 puts test1.1 into the label list, so it must be > removed. We have a theorem with one essential hypothesis |- A = ( F ` B ) > and conclusion |- A e. _V. The proof is $= ( cfv cvv fvex eqeltri ) > ABCEFDBCGH $. > > -- > 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/38398358-b9c1-4977-a7d8-acc44a631773n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/38398358-b9c1-4977-a7d8-acc44a631773n%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/CAFXXJSt2WpTQWFVYgUDLnwFiHwvjBU8XrQoETWSB_XB0QwDZzg%40mail.gmail.com.
