Revision of structure theorems (3)

[avekens]

As discussed in issue #3235, the new usage of the definitions df-* for slots in extensible structures is discouraged now. It was possible to replace most of the former usages by new/existing theorems not depending on the hard-coded values for the indices.
For this, new auxiliary theorems (*ndxn*, slots*) were provided. There are 40 of these auxiliary theorems in set.mm now, 26 of them are used more than once (and therefore surely pay off). This number is far less then the maximum 190 (number of proper pairs of numbers 1 to 20, which are currently used as slot indices).

As a result, the usage of the definitions df-* could be reduced from 159 to 39 (the OLD theorems excluded): except df-base, df-plusg and df-sca, each definition is only used by the two basic theorems *id and *ndx now (df-base is used by ~baseval and ~bj-endbase, df-plusg by ~grpstr and ~bj-endcomp, and df-sca by ~bj-isrvec additionally - the ~bj-* theorems can and should be revised later).

As a side effect, the number of usages of the *ndx theorems could be reduced from 141 to 103 (not counting the OLD theorems and the auxiliary theorems *ndxn*, *ndxlt*, *ndxnn, slots*). This is a first step in direction of the second part of issue #3235, to reduce and discourage the usage of the *ndx theorems (outside of subsection 7.1.2).

I commited the changes regarding each definition separately, so that a detailed review should be done commit by commit.

[avekens]

As a result, the usage of the definitions df-* could be reduced from 159 to 39 (the OLD theorems excluded): except df-base, df-plusg and df-sca, each definition is only used by the two basic theorems *id and *ndx now (df-base is used by ~baseval and ~bj-endbase, df-plusg by ~grpstr and ~bj-endcomp, and df-sca by ~bj-isrvec additionally - the ~bj-* theorems can and should be revised later).

~bj-endbase and ~bj-endcomp seem to be already revised accordingly meanwhile, so only ~bj-isrvec is left.

[digama0]

I would like to push back a little on not ever making use of the slot numbers, because proving that a structure is well formed is done most efficiently by proving that its fields are ordered numerically. Not doing this causes the proof to go from O(n) to O(n^2) in size.

[avekens]

I would like to push back a little on not ever making use of the slot numbers, because proving that a structure is well formed is done most efficiently by proving that its fields are ordered numerically. Not doing this causes the proof to go from O(n) to O(n^2) in size.

Are you talking about the *str theorems, like ~catstr: { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } Struct <. 1 , ; 1 5 >. ? The proofs for such theorems are based on ~strle* (and ~strleun), and these theorems require the indices to be ordered (actually to be positive integers). Such preconditions could be provided by theorems like ~basendxltplendx and ~plendxnn. I propose we continue the discussion about the *str theorems in issue #3235.

On the other hand, there are already theorems which must be proven by quadratically many inequalities of the form ( E ` ndx ) =/= ( F ` ndx ). See, for example, ~cnfldfun, which is just Fun CCfld, and since CCfld is a structure with 8 slots, the proof for ~cnfldfun requires (8 * (8 - 1)) / 2 = 28 inequalities of the form ( E ` ndx ) =/= ( F ` ndx ), and actually contains all of these inequalities. Many of them are provided already as separate theorems in this PR, so I assume the proof of ~cnfldfun can be massively shortened.

With my next PR, I will concentrate on theorems not being *str theorems, which can be revised not to use *ndx theorems directly (like ~cnfldfun). Additional candidates are ~ttgval and ~rescabs, which can be shortened using the mostly already existing theorems ndxndx.