chore(Foundations/Relation/Confluence): cleanup - #855
Conversation
| lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a := | ||
| Std.Symm.symm a b |
There was a problem hiding this comment.
This one seems worth deprecating
There was a problem hiding this comment.
i've done so, though i'm not sure the line @[deprecated Relation.ReflGen.stdSymm (since := "2026-09-03")] is exactly correct since that instance doesn't exactly reproduce the signature of the result, is there a better way?
There was a problem hiding this comment.
Is this an appropriate place to use the new deprecated +typeChanged flag?
|
For some historical context here. At the time I initially added these the state of Mathlib was
so I added these in a consistent style. Now that these are no longer the case, could we just deprecate some (most?) of these entirely? Edit: From Eric's comments I remember now that Mathlib doesn't have the various |
| theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := | ||
| EqvGen.reflGen_le_eqvGen r _ _ h | ||
|
|
||
| theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := by | ||
| induction h <;> grind | ||
| theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := | ||
| EqvGen.transGen_le_eqvGen r _ _ h | ||
|
|
||
| theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := by | ||
| induction h <;> grind | ||
| theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := | ||
| EqvGen.reflTransGen_le_eqvGen r _ _ h | ||
|
|
||
| theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := by | ||
| induction h <;> grind | ||
| theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := | ||
| EqvGen.symmGen_le_eqvGen r _ _ h |
There was a problem hiding this comment.
These ones look perhaps worth keeping for dot notation (and upstreaming to mathlib), but could maybe become aliases. I'd probably argue that the to_ should be dropped from the name.
There was a problem hiding this comment.
Mathlib has other pairs of theorems like Relation.reflGen_le_reflTransGen and Relation.ReflGen.to_reflTransGen that this matches, so if to_ were to be dropped, it should be coordinated with these I guess?
(There also seems to be a bit of disagreement on if both versions are really needed for dot notation, see this discussion)
There was a problem hiding this comment.
i've left them as-is for the moment, lmk if that's appropriate. in particular i'm not sure how to alias them since the signature is slightly different.
thomaskwaring
changed the title
|
@chenson2018 i see, that makes a lot of sense. since it's being discussed i've gone ahead and updated the naming conventions throughout, aligned with the mathlib |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I think the only outstanding question is about deprecation procedures, so I'll approve and feel free to merge once that is settled.
|
okay great, thanks. working with deprecations / aliases is a little new to me so i might have to defer to your and @eric-wieser's opinions on that — the current status looks okay to my eyes. |
3 participants
Several proofs in
Foundations/Relations/Confluencecan be vastly simplified using results from Mathlib — possibly some results could be deleted entirely, though evidently the Mathlib equivalents are not particularly discoverable. I have also fixed some naming conventions, with deprecation labels for the old names.