Discourage use of df-base and other structure definitions

[tirix]

In general we want the real "Slot" values (1 for Base, 2 for +g, etc.) to be hidden and not directly used. Instead, only the corresponding symbols should be used (Base, +g, etc.)

That's the reason why basendx usage is discouraged. However currently only basendx is in this case.

We should follow the same model and discourage new usages of the following theorems:

• plusgndx
• mulrndx
• starvndx
• scandx
• vscandx
• ipndx
• tsetndx
• plendx
• ocndx
• dsndx
• unifndx
• homndx
• ccondx
• itvndx
• lngndx

The corresponding df- slot definitions also make those slot identifiers public. So for the same reason, I would suggest to discourage new usage of the corresponding definitions:

• df-base
• df-plusg
• df-mulr
• df-starv
• df-sca
• df-vsca
• df-ip
• df-tset
• df-ple
• df-ocomp
• df-ds
• df-unif
• df-hom
• df-cco
• df-itv
• df-lng
• df-edgf

[david-a-wheeler]

The goal of hiding makes sense, theorems shouldn't depend on the specific definition of "base". But it should be possible to add a new use of Base without having to say they're using something discouraged.

Currently if you added df-base to the set of discouraged definitions, I think you'd end up with problems with many other theorems such as wunfunc.

[digama0]

wunfunc is special, I don't think it is a problem to exempt it. I am more worried about lmodstr et al, these proofs explicitly rely on the numeric values because they use total ordering in order to show that the slots are pairwise disjoint (which would require quadratically many lemmas otherwise).

[david-a-wheeler]

wunfunc is special, I don't think it is a problem to exempt it. I am more worried about lmodstr et al, these proofs explicitly rely on the numeric values because they use total ordering in order to show that the slots are pairwise disjoint (which would require quadratically many lemmas otherwise).

Can we instead provide proofs that (certain) slots are disjoint, and then let all other proofs reuse those proofs? It'd be a pain to to do that for all cases, but I imagine that only a small subset need to be proved that way. I presume that the other proofs only need to know that they're disjoint, and that they don't care about the actual values.

[digama0]

No, this proof methodology is already about as streamlined as it can be. There is a single theorem which encapsulates the assertion "slots {A,B,C,D,E} are disjoint", and everything else involving structures on those slots can use it, but when you want to add slot F you need a new such assertion. Those assertions are exactly the *str theorems, and to prove them you either need a ton of theorems like B != E, or you need to unfold the numeric value so that you can prove A<B<C<D<E.

[tirix]

But it should be possible to add a new use of Base without having to say they're using something discouraged

New usage is still possible, it is only discouraged. This just means that any new usage will be noticed and reviewed as part of the change of the discouraged file.

It's also completely possible to use Base without referring to either df-base or basendx. For example, ressbas does not use it, neither does ressval2 or ressval.

Those assertions are exactly the *str theorems

Yes, those *str theorems will of course still need to unfold the numeric values, and for that use those theorems or definitions which are discouraged. I'm not a fan of adding quadraticly many B!=E type theorems like basendxnplusgndx.

[jkingdon]

I'm not a fan of adding quadraticly many B!=E type theorems like basendxnplusgndx.

If this is our choice we need some kind of explicit statement that it is OK to get at indexes in this situation.

Merely marking something as discouraged, without a statement about why or what the exceptions are, is pretty daunting for contributors who want to build on what is there. At least, it was for me when I first started intuitionizing extensible structure theorems.

It may be slightly beyond the scope of this issue, but is the vision to adopt the (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) idiom from iset.mm (as seen in theorems like https://us.metamath.org/ileuni/strslfv.html and a bunch of others)? Last I looked that would be the most obvious way to get rid of usage of the indexes (except for the exceptions discussed above, of course).