Change definitions of the "shift" function and of the "subword" function

[benjub]

I propose to (eventually) amend the definitions df-shift and df-substr as follows:

${
$d f x y $.
$( Define the translate of a function (or relation) on complex numbers by a
   given number.  (The name "shift" is historical: its first applications were
   for sequences and translates by integers.) $)
   df-shift $a |- shift =
                 ( f e. _V , x e. CC |- ( f o. ( y e. CC |-> ( y - x ) ) ) ) $.
$}

${
$d w b $.
$( Define the function that gives a subword of a word between the two given
   indices.  (The symbol "substr" is for "substring", since both the terms
   "(sub)word" and "(sub)string" are widely used.) $)
   df-substr $a |- substr = ( w e. _V , b e. ( NN0 X. NN0 ) |->
                                ( ( w |` ( ..^ ` b ) ) shift ( 1st ` b ) ) ) $.
$}

(I thought of this after reviewing #2890.)

df-shift: simpler than the current version (formula is less complex, has one fewer dummy variable and no df-opab), and also clearer, since the value is explicitly a composed relation (o.). As a corollary, this would simplify some existing theorems (e.g., proving that the shift function is indeed a function, etc.). Unless I'm overlooking some special case, the value is precisely the same.

df-substr: simpler than the current version (formula is less complex, has one fewer dummy variable and, no df-if, df-dom, df-subset, etc.), and also clearer: it is explicitly defined for indices in NN0. The value changes in one way: if one asks for a longer subword, then the returned value is simply truncated (whereas currently, the returned value is the empty set). To me, this change is for the better, and would probably allow to remove some hypotheses in later theorems (and I seem to recall that that's the behavior of most common programming languages? --- at least the "safe" ones, not C).

Cost of the changes: For df-shift, since the value is not changed, the modifications would be rather localized, and not too large. For df-substr, on the other hand, this would need more work, since the value changes, and many theorems use that definition. The value of df-prefix, for instance, would also change. That's why I wrote "eventually" at the beginning. But probably, most of the affected theorems have an $e-hypothesis or an antecedent stating that the subword/prefix is not going beyond the word, so they would remain true, and at worst would have superfluous hypotheses.

[avekens]

Regarding the shift operation, I am dispassionate: The only theorems of section "The "shift" operation" which are used beyond this section are ~shftfn, ~shftval, ~shftval4, ~shftcan1, ~seqshft, and these should be valid (without modification)  also for the alternate definition.

[avekens]

Regarding the substring operation, I have an ambivalent opinion: I would appreciate if b e. ( NN0 X. NN0 ) was used instead of b e. ( ZZ X. ZZ ) (I never understood the advantage of the latter: It can make sense if the substring operation is applied not to a word, but to a function over an arbitrary integer range. But is there actually any application for that?). Furthermore, the usage of the shift operation is more elegant indeed.

On the other hand, I have no good feeling about an upper bound of the subwords beyond the length of the word: this would mean that ( W substr <. A , ( # ` W ) >.) = ( W substr <. A ,( ( # ` W ) + X ) >. ) for any 0 <_ X. The main impact, however, might be that ~ swrdlen (( # ` ( S substr <. F , L >. ) ) = ( L - F )) would not hold anymore if ( # ` S ) < L. This is not a problem as long as L e. ( 0 ... ( # ` S ) ) is assumed (as actually in ~swrdlen), but then I see no advantage/application of the alternate definition.

By the way, in Java there will be an IndexOutOfBoundsException if the "endIndex is larger than the length of this String object".

[avekens]

Another question concerning the substring operation is about "junk theorems" using the behaviour for out-of-domain arguments specific for set.mm (see also the Google group discussion https://groups.google.com/g/metamath/c/GQmelsKtaWQ/m/G1PqaOXJFQAJ).

Should a theorem ( -. ( S e. _V /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( S substr <. F , L >. ) = (/) ) (or ( -. ( S e. _V /\ ( F e. NN0 /\ L e. NN0 ) )) be provided? In general, such a theorem could be provided for each definition based on a maps-to expression. If yes, should it be tagged by "(New usage is discouraged.)")?

As an application, ~swrdlend could be shortend to ( L <_ F -> ( W substr <. F , L >. ) = (/) ) (would this also become a "junk theorem" then?), as a lot of additional theorems with conclusion ( W substr <. F , L >. ) = (/). See, for example,

swrdnnn0nd $p |- ( ( S e. Word V /\ -. ( F e. NN0 /\ L e. NN0 ) ) -> ( S substr <. F , L >. ) = (/) )

@benjub asked rightly in PR #2941 if S e. Word V can be removed (and it could if the above mentioned "junk theorems" were available).

Are there any objections about such theorems? Following Norm's remarks in the above mentioned Google group discussion, such "junk theorems" should be acceptable.

[benjub]

Thanks. So the question of what substr should return when one asks for a subword which ends after the end of the word does not have a clear answer. The definition I gave in the first post above is simpler but gives, for instance, that the prefix of length 99 of "smurf" is "smurf", and not "set.mm's official undefined value", the empty set. This has both advantages and drawbacks (also, one could ask the same question for subwords beginning at negative indices). If one wants to return the empty set, then one can simply add an if to my above proposal. To me, simplicity of the definition should be the prevailing criterion, but I haven't looked at the consequences in this particular case enough.

As for your question regarding "junk theorems", they happen when a definition is used outside of its intended domain (the term "junk" is subjective, so necessarily, "intended" is also subjective).

I would say that your example ( L <_ F -> ( W substr <. F , L >. ) = (/) ) is not a junk theorem, since it can be used when W is a word and L and F are natural numbers (these hypotheses are removed simply for convenience).

I would say, refrain from adding junk theorems, unless they permit some substantial simplifications. Again, "junk" and "substantial" are subjective terms, so this is a judgment call. If they are added, it should be mentioned in the comment (e.g., "this depends on our conventions...", "avoid depending on this implementation detail...", etc.).