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

[avekens]

Although #4283 is a helpful improvement related to this issue, the initial questions remain open:

• should a (new!) usage of the theorems *ndx be discouraged, that means, the "(New usage is discouraged.)" tag should be added (analogously to ~basendx)?
• should a (new!) usage of the definitions for slots be discouraged, that means, the "(New usage is discouraged.)" tag should be added?

In my opinion, the definitions and the *ndx theorems should only be used in section 7.1 (or even in subsections 7.1.1 and 7.1.2 only). This is a kind of "package scope", such as known in the Java programming language. Furthermore, the definitions should only be used to prove the theorems *ndx, *id and ress*. This would justify to add the "(New usage is discouraged.)" tag , as proposed by @tirix.

Currently, of course, this is not the case in set.mm. We should, however, try to reach the above stated conventions as much as possible, revising the concerned theorems accordingly.

For example, we can remove the dependency of ~prdsval on ~df-hom by using ~homid (which is and will not be discouraged) instead (I will prove this in my next PR).

Another approach is to provide helper theorems, as already discussed above, and partially already available in set.mm (~basendxnplusgndx , ~plusgndxnmulrndx, ~ basendxnmulrndx, ~slotsbhcdif). Such theorems do not only help to ensure the proposed encapsulation, but also can shorten the corresponding proofs: for example, the proof of ~rescco can be shortened using ~slotsbhcdif (I will provide this in my next PR, too). So we do not need theorems for all combinations of slots in advance, as criticised above, but only on demand (if a corresponding transformation has to be done in a proof anyway).

I'll try to find other cases of proofs which can be modified to obey the above stated conventions. If we can eliminate, or at least significantly reduce the usage of the definitions and *ndx theorems outside of section 7.1, then we should make these conventions "official" by adding them to our conventions in section 17.1.

[avekens]

By the way, there are slot definitions outside of section 7.1.:

Section 15.1 "Definition and Tarski's Axioms of Geometry":

• df-itv $a |- Itv = Slot ; 1 6 $.
• df-lng $a |- LineG = Slot ; 1 7 $.

Subsection 16.1.1 "The edge function extractor for extensible structures"

• df-edgf $a |- .ef = Slot ; 1 8 $.

Subsection 20.6.15 "Models of formal systems" (Mario's Mathbox!)

• df-muv $a |- mUV = Slot 7 $.
• df-mfsh $a |- mFresh = Slot 8 $.
• df-mevl $a |- mEval = Slot 9 $.

Either these definitions (and related basic theorems) should be moved to subsection 7.1.2, or the "encapsulation rules" should apply to the sections which contain the definitions of slots.

To have all definitions of slots in section 7.1.2 would also be helpful to get a complete overview of all defined slots, and to avoid gaps or overlappings in the numbering, as we currently have (slot 7 is missing in main, slots 8 and 9 are defined twice!).

[jkingdon]

Although #4283 is a helpful improvement related to this issue, the initial questions remain open:

Sounds like the thing to do is merge that (well, giving a little more time for further objections or desired changes) but leave this issue open. I've removed the "fixes" from the pull request.

[avekens]

With PR #4291, I started to reduce the usage of definitions of slots (which are obviously index-dependent) and index-dependent theorems for extensible structures. After this usage is minimized, the definitions and *ndx can be tagged with "(New usage is discouraged.)", as proposed by @tirix .

The results of #4291 show that, in many cases, df- can be replaced by id, which almost always results in shorter proofs!

Furthermore, it seems that the proofs of the ress* theorems can also be made independent of the definitions of slots, so that only the theorems *ndx and *id should directly depend on the definitions of the slots.

[avekens]

By the way, I would like to restructure subsection "7.1.1 Basic definitions" by splitting up this subsection into subsubsections, one for each definition. Then the depencies of the definitions and the related theorems shall become clearer.

For these subsubsections, I would propose the same ordering as given in the list of the new classes (which differs a little bit from the ordering of the definitions):

7.1.1.1 Extensible structures as structures with components (Struct) 7.1.1.2 Structure component indices (ndx) 7.1.1.3 Substitution of components (sSet) 7.1.1.4 Slots (Slot) 7.1.1.5 Base sets (Base) 7.1.1.6 Base set restrictions (|`s)