Discourage usage of theorems relying on ax-13 #3896
Conversation
|
If I count correctly, there are about 300 new "Discourage" tags, and about 80 of the affected theorems are not used by other theorems. As proposed in #3879, these 80 theorems could be renamed without much effort so that they can be identified as "use ax-13 but are not used" theorems easily (this can be done in a separate PR if there is an agreement which should be discussed in #3879). |
For a proposal regarding comments, see my comment in #3879. |
|
I haven't been following the ax-13 reduction enough to have an especially firm set of opinions, but generally it makes sense to me and it seems like we end up with enough theorems which use distinct variables and enough theorems which use distinctors that we demonstrate both techniques. Beyond that, I think I better defer to the comments at #3879 including some numbers on how much certain things are used. As for the details, it would be easier for me to work with these theorems in the future if the comment of the discouraged theorem said why it is discouraged. Ideally, this would point to another theorem and say something like "Most usages should prefer ~ xxxx which has an additional distinct variable constraint but which uses fewer axioms". I don't know what people think is practical here. But even something boilerplate like "Discouraged because it uses ax-13" which could be copy-pasted without further elaboration would, I would think, be an improvement over not saying anything. |
|
Ok, I can add comments and cross references here. What phrasing would satisfy you the most? I was thinking: Usage of this theorem is discouraged because it depends on ~ ax-13 . Use the weaker ~ xxx if possible. Note that not all theorems have a weaker version (because they are not needed), so most of the time only the first sentence would be present. |
|
I added comments and references to weaker versions. Contrary to what I initially thought, most theorems depending on ax-13 have one, so it took me some time to check and report them all. I haven't always used boilerplate sentences because in some occurrences they sounded either redundant or out of place, so I revised the wording from time to time. The case of rgen2 vs rgen2a is special and I used a stronger language there (rgen2a was used more than 200 times before my PR series, but now it's not used anywhere anymore). I also added a few $j tags and removed ax-13 from disjxun. |
Thanks! This helps significantly. I guess comments so far seem to be positive and it seems like we've given people time to weigh in, so I'll mark this as approved. Feel free to use your judgement about whether to merge it now or seek further discussion. |
There was a problem hiding this comment.
OK for now, but the resuls of the discussions of issue #3896 should be incorporated later. For example, I would like to propagate the original contributors to the new theorems which should be used instead of the discouraged theorems, as proposed on March 27.
Can you open a separate issue for this? I would like to close #3879 after this PR gets merged since a tool to automatically notice new ax-13 usage is implemented. |
I don't have write access. I'd say wait 12 hours max and then merge if nobody says anything. |
Hope I'm not jumping the gun by 11 hours but seems like this is ready to merge. As usual, if people still see problems, open a new issue or pull request. |
|
See #3902 for a fix to failures I'm seeing on develop after merging this. |
Based on comments from multiple people, it seems that the discouragement mechanism is the preferred tool to address #3879. Therefore in this PR I add discouragement tags to every theorem in main relying on ax-13.
This is just the first step. If this PR lands, in the following ones I will add cross references, a few missing $j tags, revise comments appropriately and maybe rename some theorems for consistency, but those following developments will depend on what will be the result of this PR.
I also removed ax-13 from iresn0n0, which I noticed while I was scanning theorems.