feat: list lemmas (#11626)

Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext.



Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>

Mathlib/Data/List/Basic.lean

@@ -397,6 +397,18 @@ theorem cons_eq_append_iff {a b c : List α} {x : α} :
 @[deprecated] alias append_right_cancel := append_cancel_right -- deprecated since 2024-01-18
 #align list.append_right_cancel List.append_cancel_right
 
+@[simp] theorem append_left_eq_self {x y : List α} : x ++ y = y ↔ x = [] := by
+  rw [← append_left_inj (s₁ := x), nil_append]
+
+@[simp] theorem self_eq_append_left {x y : List α} : y = x ++ y ↔ x = [] := by
+  rw [eq_comm, append_left_eq_self]
+
+@[simp] theorem append_right_eq_self {x y : List α} : x ++ y = x ↔ y = [] := by
+  rw [← append_right_inj (t₁ := y), append_nil]
+
+@[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = [] := by
+  rw [eq_comm, append_right_eq_self]
+
 theorem append_right_injective (s : List α) : Injective fun t ↦ s ++ t :=
   fun _ _ ↦ append_cancel_left
 #align list.append_right_injective List.append_right_injective
@@ -487,6 +499,9 @@ theorem replicate_left_injective (a : α) : Injective (replicate · a) :=
   (replicate_left_injective a).eq_iff
 #align list.replicate_left_inj List.replicate_left_inj
 
+@[simp] theorem head_replicate (n : ℕ) (a : α) (h) : head (replicate n a) h = a := by
+  cases n <;> simp at h ⊢
+
 /-! ### pure -/
 
 theorem mem_pure {α} (x y : α) : x ∈ (pure y : List α) ↔ x = y := by simp
@@ -540,6 +555,9 @@ theorem reverse_cons' (a : α) (l : List α) : reverse (a :: l) = concat (revers
   simp only [reverse_cons, concat_eq_append]
 #align list.reverse_cons' List.reverse_cons'
 
+theorem reverse_concat' (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse := by
+  rw [reverse_append]; rfl
+
 -- Porting note (#10618): simp can prove this
 -- @[simp]
 theorem reverse_singleton (a : α) : reverse [a] = [a] :=
@@ -771,6 +789,9 @@ theorem getLast?_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?)
 
 /-! ### head(!?) and tail -/
 
+@[simp] theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by
+  cases x <;> simp at h ⊢
+
 theorem head!_eq_head? [Inhabited α] (l : List α) : head! l = (head? l).iget := by cases l <;> rfl
 #align list.head_eq_head' List.head!_eq_head?
 
@@ -1349,6 +1370,33 @@ theorem take_one_drop_eq_of_lt_length' {l : List α} {n : ℕ} (h : n < l.length
 
 #align list.ext List.ext
 
+-- TODO one may rename ext in the standard library, and it is also not clear
+-- which of ext_get?, ext_get?', ext_get should be @[ext], if any
+alias ext_get? := ext
+
+theorem ext_get?' {l₁ l₂ : List α} (h' : ∀ n < max l₁.length l₂.length, l₁.get? n = l₂.get? n) :
+    l₁ = l₂ := by
+  apply ext
+  intro n
+  rcases Nat.lt_or_ge n <| max l₁.length l₂.length with hn | hn
+  · exact h' n hn
+  · simp_all [Nat.max_le, get?_eq_none.mpr]
+
+theorem ext_get?_iff {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ n, l₁.get? n = l₂.get? n :=
+  ⟨by rintro rfl _; rfl, ext_get?⟩
+
+theorem ext_get_iff {l₁ l₂ : List α} :
+    l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩ := by
+  constructor
+  · rintro rfl
+    exact ⟨rfl, fun _ _ _ ↦ rfl⟩
+  · intro ⟨h₁, h₂⟩
+    exact ext_get h₁ h₂
+
+theorem ext_get?_iff' {l₁ l₂ : List α} : l₁ = l₂ ↔
+    ∀ n < max l₁.length l₂.length, l₁.get? n = l₂.get? n :=
+  ⟨by rintro rfl _ _; rfl, ext_get?'⟩
+
 @[deprecated ext_get]
 theorem ext_nthLe {l₁ l₂ : List α} (hl : length l₁ = length l₂)
     (h : ∀ n h₁ h₂, nthLe l₁ n h₁ = nthLe l₂ n h₂) : l₁ = l₂ :=

Mathlib/Data/List/Infix.lean

@@ -70,6 +70,11 @@ theorem infix_rfl : l <:+: l :=
 theorem prefix_concat (a : α) (l) : l <+: concat l a := by simp
 #align list.prefix_concat List.prefix_concat
 
+theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} :
+    l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂ := by
+  simpa only [← reverse_concat', reverse_inj, reverse_suffix] using
+    suffix_cons_iff (l₁ := l₁.reverse) (l₂ := l₂.reverse)
+
 #align list.infix_cons List.infix_cons
 #align list.infix_concat List.infix_concat
 #align list.is_prefix.trans List.IsPrefix.trans
@@ -211,6 +216,27 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
     fun e => e.symm ▸ take_prefix _ _⟩
 #align list.prefix_iff_eq_take List.prefix_iff_eq_take
 
+theorem prefix_take_iff {x y : List α} {n : ℕ} : x <+: y.take n ↔ x <+: y ∧ x.length ≤ n := by
+  constructor
+  · intro h
+    constructor
+    · exact List.IsPrefix.trans h <| List.take_prefix n y
+    · replace h := h.length_le
+      rw [length_take, Nat.le_min] at h
+      exact h.left
+  · intro ⟨hp, hl⟩
+    have hl' := hp.length_le
+    rw [List.prefix_iff_eq_take] at *
+    rw [hp, List.take_take]
+    simp [min_eq_left, hl, hl']
+
+theorem concat_get_prefix {x y : List α} (h : x <+: y) (hl : x.length < y.length) :
+    x ++ [y.get ⟨x.length, hl⟩] <+: y := by
+  use y.drop (x.length + 1)
+  nth_rw 1 [List.prefix_iff_eq_take.mp h]
+  convert List.take_append_drop (x.length + 1) y using 2
+  rw [← List.take_concat_get, List.concat_eq_append]; rfl
+
 theorem suffix_iff_eq_drop : l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length l₁) l₂ :=
   ⟨fun h => append_cancel_left <| (suffix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
     fun e => e.symm ▸ drop_suffix _ _⟩
@@ -442,7 +468,7 @@ theorem nth_le_tails (l : List α) (n : ℕ) (hn : n < length (tails l)) :
   · simp
   · cases n
     · simp [nthLe_cons]
-    · simpa[nthLe_cons] using IH _ _
+    · simpa [nthLe_cons] using IH _ _
 #align list.nth_le_tails List.nth_le_tails
 
 @[simp]
@@ -452,7 +478,7 @@ theorem nth_le_inits (l : List α) (n : ℕ) (hn : n < length (inits l)) :
   · simp
   · cases n
     · simp [nthLe_cons]
-    · simpa[nthLe_cons] using IH _ _
+    · simpa [nthLe_cons] using IH _ _
 #align list.nth_le_inits List.nth_le_inits
 end deprecated
 
@@ -510,4 +536,17 @@ theorem mem_of_mem_suffix (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂ :=
   hl.subset hx
 #align list.mem_of_mem_suffix List.mem_of_mem_suffix
 
+theorem IsPrefix.ne_nil {x y : List α} (h : x <+: y) (hx : x ≠ []) : y ≠ [] := by
+  rintro rfl; exact hx <| List.prefix_nil.mp h
+
+theorem IsPrefix.get_eq {x y : List α} (h : x <+: y) {n} (hn : n < x.length) :
+    x.get ⟨n, hn⟩ = y.get ⟨n, hn.trans_le h.length_le⟩ := by
+  obtain ⟨_, rfl⟩ := h
+  exact (List.get_append n hn).symm
+
+theorem IsPrefix.head_eq {x y : List α} (h : x <+: y) (hx : x ≠ []) :
+    x.head hx = y.head (h.ne_nil hx) := by
+  cases x <;> cases y <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢
+  all_goals (obtain ⟨_, h⟩ := h; injection h)
+
 end List