Revision of structure theorems (4) #4397
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* auxiliary slots* and *ndxn* theorems extracted from proofs of ~rescabs, ~cnfldfun, ~ttgval: ~tsetndxnstarvndx, ~slotsdifplendx, ~slotsdifdsndx, ~slotsdifunifndx, ~lngndxnitvndx * proofs of ~rescabs, ~cnfldfun, ~ttgval shortened and independent of *ndx theorems.
* proofs of ~setsmsbas, ~setsmsds, ~zlmds, ~zlmtset shortend and independent of *ndx theorems by using already existing slot*/*ndxn* theorems.
* auxiliary *ndxn* theorems extracted from proofs of ~thlbas, ~thlle: ~basendxnocndx , ~plendxnocndx * proofs of ~thlbas, ~thlle shortened and independent of *ndx theorems.
* auxiliary slotsdif* theorems extracted from proofs of ~srasca, ~sravsca, ~prstcleval, ~prstcocval: ~slotsdifipndx , ~slotsdifplendx2, ~slotsdifocndx * proofs of ~srasca, ~sravsca, ~prstcleval, ~prstcocval shortened and independent of *ndx theorems.
* proofs of ~odubas, ~setsmsds, ~matvsca shortend and independent of *ndx theorems by using already existing *ndxn* theorems.
|
@avekens Just in case you did not notice it: This PR has conflicts that need to be resolved (for some days now). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As discussed in issue #3235, the new usage of the theorems
*ndxfor the hard-coded indices of 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. All proofs were shortened by these replacements.For this, some additional new auxiliary theorems (
*ndxn*,slots*) were provided. These new theorems are extracts of former proofs without exception, so there should be no objection to them. There are 46 of these auxiliary theorems in set.mm now, 35 of them are used more than once (and therefore surely pay off). This number is still 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 theorems
*ndxis restricted to the basic theorems*ndxnn(7),*ndxlt*(12),*ndxn*(58) andslots*(42), and the*strtheorems showing that a structure is well formed (see also comments in #4377), except five deprecated theorems ~1strstr, ~2strstr, ~grpbasex, ~grpplusx, ~indistpsx.By this PR, the main tasks of issue #3235 (discouragement of the df-* definitions of slots and *ndx theorems for extensible structures) is done. There are, however, some details to be clarified/adjusted (e.g., how to proceed with the
*strtheorems, and how to adjust the comments provided with #4283), which I will descibe in #3235 in more detail (and solve them in a subsequent PR).