I think mmj2 only ever uses wceq, because it "parses" formulas and using weq introduces an ambiguity into the resulting grammar. However metamath-exe's MINIMIZE will find shorter proofs using lemmas, and it treats syntax lemmas just like real lemmas, so it will "optimize" the proof to use weq. I think you shouldn't worry much about whether you produce one vs another, IMO having syntax lemmas was a mistake.
On Mon, Feb 12, 2024 at 7:14 PM jagra <agra.jo...@gmail.com> wrote: > Thanks both for the explanations. > > I had it working, but since the generated proofs were in some cases so > different from those in set.mm, I was trying to understand why. > > One of the things I noticed, and caused the differences I had, was > avoiding the use of $p statements in parsing rules. For instance, weq and > wceq seem to be similar, but weq is a $p while wceq is a $a, but they seem > to be basically equivalent when used in generated proof. > > Including weq creates in some cases, several distinct correct parsing > alternatives for the same statement, while using just $a rules (wceq > instead of weq) does not. Tested (only) with ax8, replacing the original > proof with one that contained a proof generated just from $a rules (from > base ax8 proof statements), and set.mm was verified without errors. > > The proof is bigger and I understand that's a concern always present, but, > other than that, do you see any problems with it? > > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/980d8c60-d073-4784-81c8-11a698612730n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/980d8c60-d073-4784-81c8-11a698612730n%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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvO1BXFcYRxVv96%2ByANDj8r_v7dZDhefRZ0auDmPA7xQQ%40mail.gmail.com.
