Conventions

[benjub]

Align conventions following discussions in #3542 and #3562.

edit: I introduced an extra commit which I then reverted, so better reviewed globally, not by commit.

[GinoGiotto]

As I mentioned in #3542 (comment) #3542 (comment) ALT should be clarified as well.

Currently the conventions about ALT say:

Alternate (ALT) proofs. If a different proof is shorter or clearer but uses more or stronger axioms, we make that proof an "alternate" proof (marked with an ALT label suffix), even if this alternate proof was formalized first. We then make the proof that requires fewer axioms the main proof. Alternate proofs can also occur in other cases when an alternate proof gives some particular insight. Their comment should begin with "Alternate proof of ~ xxx " followed by a description of the specificity of that alternate proof. There can be multiple alternates. Alternate (*ALT) theorems should have "(Proof modification is discouraged.) (New usage is discouraged.)" in their comment and should follow the main statement, so that people reading the text in order will see the main statement first. The alternate and main statement comments should use hyperlinks to refer to each other.

The way I interpret this is that ALT is for alternative proofs only, not for alternative versions (it starts with Alternate (ALT) proofs, not Alternate (ALT) versions, also it's quite obvious by reading the rest of the paragraph). The issue is that ALT is actually used in main for alternative versions as well. Examples: sbequ1 and sbequ1ALT, max1 and max1ALT, meetcom and meetcomALT.

So either the conventions get changed to include alternative versions for the ALT suffix as well (note that in this case ALT and ALTV would overlap in mathboxes), or all ALT theorems in main that are not alternative proofs should be renamed with a more specific suffix as this PR is proposing in the ALTV section (based on a quick look in main it doesn't seem there are that many ALT variants, so it would be feasable).

[wlammen]

We can decide here on how these suffixes are used in future. If there are a few existing instances that deviate from the rules described here, then they can be updated in another pull request. So: the meaning of the ALT suffix given here is exactly how I used it in the past. I have not used the ALTV suffix before (at least I cannot remember), so I have no strong opinion about it. Limiting it to mathboxes is fine for me.

[wlammen]

Fine for me

[benjub]

So, which of Gino's alternatives should we choose :

• keep the existing conventions saying that *ALT should be used only when statements are identical (except possibly for DVs ?), hence find labels for sbequ1ALT, max1ALT, meetcomALT, and maybe others;
• update the conventions for *ALT with an exception like "it may happen that the statement is also slightly different, but close enough that we consider it mainly an alternate proof" ?

No strong opinions. A meta-convention we should try to follow is that conventions should be not too long, nor too numerous (i.e., no gratuitous conventions). I think the current situation is fine, but it's just a safeguard to keep in mind.

[GinoGiotto]

I'm still not super happy about this. Following this convention proposal the name chvarfv would suggest the addition of a non-free hypothesis to remove a $d condition and the addition of another $d condition to drop axiom usage to chvar, but in reality chvarfv and chvar differ by a $d condition only (their hypothesis are identical). So following your conventions update the appropriate name for chvarfv would be chvarv, but that's already taken so it can't be that.

To be clear here is how it is currently in the webpage:

• chvar is the "base version".
• chvarv differs from the base version by replacing a non-free hypothesis with a $d condition between $\Psi$ and x.
• chvarfv differs from the base version by adding a $d condition between x and y (without replacing anything).

I think with this new proposal the f and v suffixes would interact between each other in a convoluted way. The current conventions are more clear about this: the v and f suffixes are simply the inverse of each other, one adds a $d condition to remove a non-free hyp while the other adds a non-free hyp to remove a $d, I can easily recognise what to expect in the statement just by looking at the label.

[benjub]

No labeling scheme can be completely systematic and consistent if we don't want labels to be basically as long as the statements themselves. That's why many of these conventions use the adverb "sometimes".

In a given theorem ~xxx, there can be multiple natural DV conditions to add, so ~xxxv won't be unambiguous. Similarly, one may consider multiple natural nonfreeness conditions, so ~xxxf won't be unambiguous either.

The practice of suffixing a "v" when adding a DV condition is simple, and is followed by many existing theorems. Again, one does not necessarily add a DV condition in order to remove a nonfreeness hypothesis, but sometimes it can be in order to use fewer axioms.

I propose we stay like this at least for now.

[jkingdon]

I agree with No labeling scheme can be completely systematic especially in a context like metamath where we want labels to be short and memorable. I don't think I have much of an opinion about the proposed change here - it strikes me as maybe a bit longer than it needs to be and maybe gets too much into details which don't need to be covered here, but I'm not sure it would really cause problems either.

[GinoGiotto]

• keep the existing conventions saying that *ALT should be used only when statements are identical (except possibly for DVs ?), hence find labels for sbequ1ALT, max1ALT, meetcomALT, and maybe others;

I personally prefer this one more, because it keeps ALT and ALTV separated from each other. Also I agree with you that being a different version is a vague notion, and so that it would be better to clarify in the suffix how two versions are different instead of putting them in a big bucket. I offer myself to collect all the exceptions in main and open an issue with a list to discuss the renaming.

[icecream17]

Incidentally the section with the old proofs of substitution (using the old definition, like sbequALT) can be removed I think, since the section is unused now

[benjub]

• keep the existing conventions saying that *ALT should be used only when statements are identical (except possibly for DVs ?), hence find labels for sbequ1ALT, max1ALT, meetcomALT, and maybe others;

I personally prefer this one more, because it keeps ALT and ALTV separated from each other. Also I agree with you that being a different version is a vague notion, and so that it would be better to clarify in the suffix how two versions are different instead of putting them in a big bucket. I offer myself to collect all the exceptions in main and open an issue with a list to discuss the renaming.

Ok, then we can choose other labels for the few remaining exceptions, and we can do this progressively in future PRs.

[benjub]

Incidentally the section with the old proofs of substitution (using the old definition, like sbequALT) can be removed I think, since with further changes the section is unused

Or maybe you can indicate in the head comment of that section something to the effect that this is a temporary section that originated from work related to the revision of df-sb, and that it is due for deletion one year after that work was done; that is, this section is obsolete as of 31-May-2023. Or something like that.

[avekens]

• keep the existing conventions saying that *ALT should be used only when statements are identical (except possibly for DVs ?), hence find labels for sbequ1ALT, max1ALT, meetcomALT, and maybe others;

I personally prefer this one more, because it keeps ALT and ALTV separated from each other. Also I agree with you that being a different version is a vague notion, and so that it would be better to clarify in the suffix how two versions are different instead of putting them in a big bucket. I offer myself to collect all the exceptions in main and open an issue with a list to discuss the renaming.

Ok, then we can choose other labels for the few remaining exceptions, and we can do this progressively in future PRs.

I would also prefer this variant.

• Instead of the suffix ALT, we can use the label fragment "asb" (for "alternate substitution") in section "Alternate definition of substitution"
• Why not use simply ~max1alt instead of ~may1ALT
• ~meetcomALT is very critical, because it is used in the proof of ~meetcom. Maybe we can call it ~meetcomlem?

[wlammen]

What bothers me a bit is that there is no progress here. Is the suggested wording an improvement over the current situation? If so, we can perhaps accept it as is, and tweak it in follow-up pulls. Who is in favor of this? I am.

[benjub]

What bothers me a bit is that there is no progress here. Is the suggested wording an improvement over the current situation? If so, we can perhaps accept it as is, and tweak it in follow-up pulls. Who is in favor of this? I am.

I just needed time to finish my work week, and I think now it's good to merge.