New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore: de-mathlib lots of Data/List/Lemmas.lean #98
chore: de-mathlib lots of Data/List/Lemmas.lean #98
Conversation
okay, I made mostly style and golfing changes, but also some renames. For I will merge shortly if there are no objections. |
Also just realized there's some |
if the attributes can be added after the fact in mathlib (which I think is the case), then it's fine to remove the comments. The mathlib4 PR will have standalone |
c359d52
to
f05bb95
Compare
Notably incorporates leanprover-community/batteries#98 and leanprover-community/batteries#109. leanprover-community/batteries#98 moves a number of lemmas from Mathlib to Std, so the bump requires deleting them in Mathlib. I did check on each lemma whether its attributes were kept in the move (and gave attribute markings in Mathlib if they were not present in Std), but a reviewer may wish to re-check. `List.mem_map` changed statement from `b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a` to `b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b`. Similarly for `List.exists_of_mem_map`. This was a deliberate change, so I have simply adjusted proofs (many become simpler, which supports the change). I also deleted `List.mem_map'`, `List.exists_of_mem_map'`, which were temporary versions in Mathlib while waiting for this change (replacing their uses with the unprimed versions). Also, the lemma `sublist_nil_iff_eq_nil` seems to have been renamed to `sublist_nil` during the move, so I added an alias for the old name. (another issue fixed during review by @digama0) ~~`List.Sublist.filter` had an argument change from explicit to implicit. This appears to have been an oversight (cc @JamesGallicchio). I have temporarily introduced `List.Sublist.filter'` with the argument explicit, and replaced Mathlib uses of `Sublist.filter` with `Sublist.filter'`. Later we can fix the argument in Std, and then delete `List.Sublist.filter'`.~~
I believe all the statements are pulled from mathlib4 identically.
Main weirdness is Std had a
mem_map
lemma with a conclusion that is in some sense backwards from what would generally be preferred. Mathlib has amem_map'
for porting, so I moved themem_map'
lemma here. We might want to deprecatemem_map
.Depends on #97.