I agree that both dummylink and idi should not be deleted or discouraged. While mmj2 should normally detect and collapse reused steps, I don't know if this behavior should be relied upon, and if a proof assistant finds a proof using idi then that is just as good, since it produces the right proof as t -> +oo (after a minimize run), so the tool should not be limited to avoid idi.
On Sun, Jan 12, 2020 at 9:06 PM David A. Wheeler <[email protected]> wrote: > This is really about mmj2. I'm trying to update the mmj2 tutorial. > > I found that you start up mmj2 with this: > h1::reiteration.1 |- ph > qed:1: |- ph > > A control-U will automatically prove that using idi: > h1::reiteration.1 |- ph > qed:1:idi |- ph > $= ( reiteration.1 idi ) ABC $. > This is actually the one time when mmj2 will not use auto #-marking, because it cannot make the qed step the same as the h step, even though that's logically what it should do. The proof worksheet format doesn't support this although the underlying metamath proof does. In any case, this appears to be working as intended: theorem "reiteration" is literally identical to idi so it's good that mmj2 found it. If idi were blocked here it would have to do some more convoluted thing similar to what the tutorial proposes, such as applying ax-mp to id. > mmj2 already has a RunParms which prevents use of dummylink. It currently > says: > ProofAsstUnifySearchExclude,biigb,xxxid,dummylink > I think I can bring it all the way down to *just* dummylink. > The first was renamed biigb -> dfbi1gb -> dfbi1ALT whose > use is discouraged anyway, and xxxid doesn't exist any more. > For the rest we're using the "New usage is discouraged", which > is easier to maintain anyway. > I'll take a PR for this, but as mentioned above I don't think idi should be on the exclude list. Mario -- 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/CAFXXJSvpLDrHVGB5vrNn1tDBHZ19r27iQ0b15nOvLhej7aYqoQ%40mail.gmail.com.
