Proposal: Mark dummylink & idi with "(New usage is discouraged.)"

[David A. Wheeler]

I propose that dummylink & idi be marked with
"(New usage is discouraged.)".

As noted in the text,
they should normally never appear in a completed proof.
Marking them this way will prevent them from being
automatically used, and I think that's usually what is wanted.
The normal mmj2 invocation has special case stuff to
avoid its invocation, but that was created before we
had the marking "(New usage is discouraged.)".
Of course, someone can specifically *force* its use, but
then it will noticed as such.

I noticed this while trying to update the mmj2 tutorial.

Does that seem reasonable?

--- David A. Wheeler

[Norman Megill]

I don't think it's necessarily because both of these will automatically be removed with 'minimize'.

While I may be the only one to do so, I have used dummylink to build proofs in MM-PA to work around the "backwards only" method it requires.  Making it 'discouraged' will be a nuisance that I'll have to override.  dummylink is also used by the eimm program (see Metamath Home Page) to import partial mmj2 proofs into MM-PA.

As for idi, I don't really care - mmj2 used to make use of it but I don't think it does anymore.  As far as I am concerned, we can delete idi unless someone has a use for it.

Norm

[Jim Kingdon]

On January 12, 2020 3:25:13 PM PST, "David A. Wheeler" <dwhe...@dwheeler.com> wrote:
>I propose that dummylink & idi be marked with
>"(New usage is discouraged.)".

Makes sense to me. I'm not thinking of any disadvantages.

[Benoit]

This was proposed in PR #1105. There is an ensuing discussion.

Benoît

[Norman Megill]

On Sunday, January 12, 2020 at 7:09:17 PM UTC-5, Norman Megill wrote:

As for idi, I don't really care - mmj2 used to make use of it but I don't think it does anymore.  As far as I am concerned, we can delete idi unless someone has a use for it.
 

Alan Sare's tool "completeusersproof" appears to make use of idi, at least it appears in his C code and is referenced extensively in the program comments.   Although this program probably has a very small user base, I think we should leave in idi and also not mark it discouraged so that proofs generated by the code won't be rejected.  Any idi usage in the generated proofs will be removed by 'minimize'.

My overall opinion then is that neither dummylink nor idi should be discouraged or deleted.  Do you have any other reason for discouraging them?

Norm

[David A. Wheeler]

On Sun, 12 Jan 2020 16:09:16 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> I don't think it's necessarily because both of these will automatically be

> removed with 'minimize'. ...

Okay, how about marking just idi with "(New usage is discouraged.)"?
I *do* refer to idi in a tutorial, and it's useful in some cases, I just
don't want it to be automatically matched.

Details below.

--- David A. Wheeler


========= DETAILS =========================

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 $.

I think we want to avoid automatic use of dummylink and idi;
someone should specifically *request* it (by referring to its reference).

> As for idi, I don't really care - mmj2 used to make use of it but I don't
> think it does anymore. As far as I am concerned, we can delete idi unless
> someone has a use for it.

I specifically mentioned in my tutorial using idi to copy a statement
so it can then be edited. So there's a *use* for it, I just don't want
it used unintentionally.

> While I may be the only one to do so, I have used dummylink to build proofs
> in MM-PA to work around the "backwards only" method it requires. Making it
> 'discouraged' will be a nuisance that I'll have to override. dummylink is
> also used by the eimm program (see Metamath Home Page) to import partial
> mmj2 proofs into MM-PA.

Ok, I didn't realize that was a nuisance. Never mind.

Can we just mark idi as "(New usage is discouraged.)" then?
I presume we don't want people to use it unless they *mean* to use it,
and your use only uses dummylink.

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.

[David A. Wheeler]

On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> >
> Alan Sare's tool "completeusersproof" appears to make use of idi, at least
> it appears in his C code and is referenced extensively in the program
> comments. Although this program probably has a very small user base, I
> think we should leave in idi and also not mark it discouraged so that
> proofs generated by the code won't be rejected. Any idi usage in the
> generated proofs will be removed by 'minimize'.

We could just ask people to use 'minimize' before submitting proofs generated
by that tool.

But if that's not convincing enough, that's fine.
I couldn't think of a reason *not* to do this, but I didn't know about those
other situations. You learn something every day!!

If idi won't be marked like this, I'll probably propose to Mario
that this RunParms.txt line:
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
be changed to:
ProofAsstUnifySearchExclude,dummylink,idi
I think that for mmj2 users it would have a similar effect.

--- David A. Wheeler

[Norman Megill]

I'm unclear about what prompted this and why it is considered a problem.  I don't see why we should care whether someone wants to use dummylink or idi for whatever reason.  They are harmless, and all they do is make the proof slightly less efficient.  It is a trivial and temporary cosmetic issue that will go away when 'minimize' is run.  I would prefer not to have 'discouraged' tags, because it will make these a nuisance to use in the occasional cases where they are useful.

BTW the eimm program generates a script for MM-PA that uses 'assign' commands to rebuild a partial proof from an mmj2 worksheet, using dummylink to connect isolated subproofs in the mmj2 proof.  If dummylink is 'discouraged', the proof building will corrupted unless the user first issues a global 'set discouragement off', defeating the purpose of 'discouraged'.  And it will be another thing for the user to learn or be unpleasantly surprised by.

Benoit mentioned an earlier discussion in PR#1105 where a 'minimize' did not remove idi, and it was because of 'discouraged' tags in theorems referenced by the proof.  Normally this will not be an issue - if a theorem is 'discouraged', it normally shouldn't be used in a new proof to begin with.  But in any case, 'minimize' has '/override' that will allow it to try 'discouraged' theorems, and that is fine to use as long as you carefully inspect what it did.

On Sunday, January 12, 2020 at 9:15:44 PM UTC-5, David A. Wheeler wrote:

On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill wrote:
> >
> Alan Sare's tool "completeusersproof" appears to make use of idi, at least
> it appears in his C code and is referenced extensively in the program
> comments.   Although this program probably has a very small user base, I
> think we should leave in idi and also not mark it discouraged so that
> proofs generated by the code won't be rejected.  Any idi usage in the
> generated proofs will be removed by 'minimize'.

We could just ask people to use 'minimize' before submitting proofs generated
by that tool.

The redundant idi's will be removed when we run a global minimization, so it's not strictly necessary.  They don't take up much space in the proof.  More importantly, I don't know how the tool works, and having a discouraged idi might unnecessarily increase risk of something going wrong, like with eimm.

In any case, of course it is nice when people 'minimize' before they submit, and I encourage people to do that.  But a long time ago I asked people to do that and got complaints it was too much trouble.  So I've given up on that.  So we do global minimizations to take care of it. 

Norm
 

[David A. Wheeler]

On January 12, 2020 11:04:54 PM EST, Norman Megill <n...@alum.mit.edu> wrote:
>I'm unclear about what prompted this and why it is considered a
>problem.

No problem, you answered my question. No change in set.mm is fine. Carry on!

--- David A.Wheeler

[Mario Carneiro]

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 <dwhe...@dwheeler.com> 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

[Alexander van der Vekens]

As far as I can remember, idi was *inserted*  by 'minimize' in some cases, and I had to remove it manually. Unfortunately, I do not know when and in which context this appeared, but I think the concerned theorem was not marked as "usage discouraged"...

Maybe there was an error which was fixed meanwhile - I will come back to this if it happens again.

Looking for idi in the current version of set.mm, there are a lot of "idi"s in the proofs of the theorems Glauco provided in December (in his mathbox)! Since they are very long, I fear that 'minimize' will take a long time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to 10757 steps (567 to 520 essential steps). "idi" was removed by this minimization, so everything is fine.

[Norman Megill]

On Monday, January 13, 2020 at 5:51:18 AM UTC-5, Alexander van der Vekens wrote:

As far as I can remember, idi was *inserted*  by 'minimize' in some cases, and I had to remove it manually. Unfortunately, I do not know when and in which context this appeared, but I think the concerned theorem was not marked as "usage discouraged"...

Maybe there was an error which was fixed meanwhile - I will come back to this if it happens again.

There are situations where idi will temporarily shorten an inefficient proof during 'minimize', showing up in its 'decreased' list at the beginning of the run.  This can happen when the proof has 2 different subproofs for the same fact, with the idi attaching the shorter subproof to its hypothesis.  But (unless you are using discouraged theorems) the idi itself should be removed later in the minimize run.  If you see an idi remaining (even after 'minimize * /override'), let me know and I'll look at it.
 

Looking for idi in the current version of set.mm, there are a lot of "idi"s in the proofs of the theorems Glauco provided in December (in his mathbox)! Since they are very long, I fear that 'minimize' will take a long time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to 10757 steps (567 to 520 essential steps). "idi" was removed by this minimization, so everything is fine.

Yes, I am aware of this and am looking at what we will have to do in order to 'minimize' some of the larger new proofs since the last run.  Unfortunately some are over an order of magnitude larger than our previous run 2 years ago.  'minimize' isn't going to be feasible on the longest proofs unless we refactor them by breaking out some lemmas or maybe add definitional hypotheses for very long repeated subexpressions.  This might be a good idea anyway so a human can understand them.  I'm currently looking at what will be needed for a new global run with the help of savask's formula (and maybe will ask for his help).

In any case, idi itself is likely only a tiny contributor to the size of those proofs, so in those cases it actually serves as a useful "canary" to remind us the proof needs minimization.  BTW an idi itself can be removed with a quick 'minimize xxx' where xxx is the theorem attached to the idi hypothesis, if people are bothered by it, but the rest of the proof should still be minimized someday.

Norm

[Benoit]

On Monday, January 13, 2020 at 4:19:16 PM UTC+1, Norman Megill wrote:

On Monday, January 13, 2020 at 5:51:18 AM UTC-5, Alexander van der Vekens wrote:

As far as I can remember, idi was *inserted*  by 'minimize' in some cases, and I had to remove it manually. Unfortunately, I do not know when and in which context this appeared, but I think the concerned theorem was not marked as "usage discouraged"...

Maybe there was an error which was fixed meanwhile - I will come back to this if it happens again.

There are situations where idi will temporarily shorten an inefficient proof during 'minimize', showing up in its 'decreased' list at the beginning of the run.  This can happen when the proof has 2 different subproofs for the same fact, with the idi attaching the shorter subproof to its hypothesis.  But (unless you are using discouraged theorems) the idi itself should be removed later in the minimize run.  If you see an idi remaining (even after 'minimize * /override'), let me know and I'll look at it.

I encountered this also (a minimization introducing idi but not removing it).  This was probably due to a small bug of minimize_with in the versions around 0.178--0.179 (for it to work properly, you had to save the proof, exit MM-PA, then re-enter it and minimize).  Norm has corrected this bug, and indeed I didn't see this behavior again.

Benoît

[Glauco]

Il giorno lunedì 13 gennaio 2020 11:51:18 UTC+1, Alexander van der Vekens ha scritto:

Looking for idi in the current version of set.mm, there are a lot of "idi"s in the proofs of the theorems Glauco provided in December (in his mathbox)! Since they are very long, I fear that 'minimize' will take a long time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to 10757 steps (567 to 520 essential steps). "idi" was removed by this minimization, so everything is fine.

I use idi as a useful tool when writing a proof. It allows to create a "smart" copy of an already proven statement, that may be several lines above the current line.

Using idi I create (just above the current line) a copy of the far away statement (let's say you need to look at it carefully, or you need to copy paste pieces of that statement).

A copy paste with a comment could be used, but idi has a number of advantages (the most important, mmj2 automatically updates its step reference if you renumber all the proof).

I should never reference those idi steps, I should always reference the step number of the "original" (far away) statement, but sometimes the autocomplete grabs the idi step, instead of the original one.

When the proof is done, the plan is to search for any accidental actual use of the idi steps and remove them from the proof (I guess sometimes one slips under the radar...)

Glauco