Skip to content
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.

Sign up for GitHub

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

Jump to bottom

refactor: move theorems about lists to batteries #12540

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+5 −23
Open

refactor: move theorems about lists to batteries #12540

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e086457
refactor: move theorems about lists to batteries
chabulhwi Apr 30, 2024
4fcf5e4
refactor: replace deprecated name with new one
chabulhwi Jun 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 0 additions & 12 deletions Mathlib/Data/List/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -601,10 +601,6 @@ theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) :

/-! ### empty -/

-- Porting note: this does not work as desired
-- attribute [simp] List.isEmpty

theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty]
#align list.empty_iff_eq_nil List.isEmpty_iff_eq_nil

/-! ### dropLast -/
Expand Down Expand Up @@ -904,14 +900,6 @@ theorem nthLe_cons {l : List α} {a : α} {n} (hl) :

end deprecated

-- Porting note: List.modifyHead has @[simp], and Lean 4 treats this as
-- an invitation to unfold modifyHead in any context,
-- not just use the equational lemmas.

-- @[simp]
@[simp 1100, nolint simpNF]
theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
(l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
#align list.modify_head_modify_head List.modifyHead_modifyHead

/-! ### Induction from the right -/
Expand Down
16 changes: 5 additions & 11 deletions Mathlib/Data/List/Infix.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,22 +294,16 @@ theorem prefix_take_le_iff {L : List (List (Option α))} (hm : m < L.length) :
simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]
#align list.prefix_take_le_iff List.prefix_take_le_iff

theorem cons_prefix_iff : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
constructor
· rintro ⟨L, hL⟩
simp only [cons_append] at hL
injection hL with hLLeft hLRight
exact ⟨hLLeft, ⟨L, hLRight⟩⟩
· rintro ⟨rfl, h⟩
rwa [prefix_cons_inj]
#align list.cons_prefix_iff List.cons_prefix_iff
#align list.cons_prefix_iff List.cons_prefix_cons

@[deprecated] alias cons_prefix_iff := cons_prefix_cons

protected theorem IsPrefix.map (h : l₁ <+: l₂) (f : α → β) : l₁.map f <+: l₂.map f := by
induction' l₁ with hd tl hl generalizing l₂
· simp only [nil_prefix, map_nil]
· cases' l₂ with hd₂ tl₂
· simpa only using eq_nil_of_prefix_nil h
· rw [cons_prefix_iff] at h
· rw [cons_prefix_cons] at h
simp only [List.map_cons, h, prefix_cons_inj, hl, map]
#align list.is_prefix.map List.IsPrefix.map

Expand All @@ -319,7 +313,7 @@ protected theorem IsPrefix.filterMap (h : l₁ <+: l₂) (f : α → Option β)
· simp only [nil_prefix, filterMap_nil]
· cases' l₂ with hd₂ tl₂
· simpa only using eq_nil_of_prefix_nil h
· rw [cons_prefix_iff] at h
· rw [cons_prefix_cons] at h
rw [← @singleton_append _ hd₁ _, ← @singleton_append _ hd₂ _, filterMap_append,
filterMap_append, h.left, prefix_append_right_inj]
exact hl h.right
Expand Down
Loading