feat: add list function and lemmas

Batteries/Data/List/Basic.lean

@@ -10,6 +10,16 @@ namespace List
 
 /-! ## New definitions -/
 
+/-- Returns the longest common prefix of two lists. -/
+def commonPrefix [DecidableEq α] : (l₁ l₂ : List α) → List α
+  | [], _ => []
+  | _, [] => []
+  | a₁::l₁, a₂::l₂ =>
+    if a₁ = a₂ then
+      a₁ :: (commonPrefix l₁ l₂)
+    else
+      []
+
 /--
 Computes the "bag intersection" of `l₁` and `l₂`, that is,
 the collection of elements of `l₁` which are also in `l₂`. As each element

Batteries/Data/List/Lemmas.lean

@@ -19,6 +19,15 @@ namespace List
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
 
+/-! ### head and tail -/
+
+theorem head_cons_tail : ∀ (l : List α) (hne : l ≠ []), l.head hne :: l.tail = l
+  | _::_, _ => rfl
+
+theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) :
+    [l.head hne] = l := by
+  conv => rhs; rw [← head_cons_tail l hne, htl]
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -482,6 +491,83 @@ theorem Sublist.erase_diff_erase_sublist {a : α} :
 
 end Diff
 
+/-! ### prefix, suffix, infix -/
+
+theorem singleton_prefix_cons (a) : [a] <+: a :: l :=
+  (prefix_cons_inj a).mpr nil_prefix
+
+theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by
+  intro heq
+  simp [heq, nil_prefix] at h
+
+section
+
+variable [DecidableEq α]
+
+theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by
+  match l₁, l₂ with
+  | [],   _  => simp [commonPrefix]
+  | _::_, [] => simp [commonPrefix]
+  | a₁::l₁, a₂::l₂ =>
+    simp only [commonPrefix]
+    cases Decidable.em (a₁ = a₂)
+    · next h =>
+      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
+      apply commonPrefix_prefix_left
+    · next h =>
+      simp [h]
+
+theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by
+   match l₁, l₂ with
+  | [],   _  => simp [commonPrefix]
+  | _::_, [] => simp [commonPrefix]
+  | a₁::l₁, a₂::l₂ =>
+    simp only [commonPrefix]
+    cases Decidable.em (a₁ = a₂)
+    · next h =>
+      simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
+      apply commonPrefix_prefix_right
+    · next h =>
+      simp [h]
+
+theorem commonPrefix_append_append (p l₁ l₂ : List α) :
+    commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by
+  match p with
+  | []   => rfl
+  | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂
+
+theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p)
+    (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧
+      t₁.head? ≠ t₂.head? := by
+  constructor <;> intro h
+  · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1)
+    obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2)
+    cases Decidable.em (a₁ = a₂)
+    · subst a₂
+      simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂
+      simp only [cons_prefix_cons, true_and] at h
+      exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h
+    · next hne =>
+      simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂
+      simp [← h₁, ← h₂, hne]
+  · rw [h₁, h₂]
+    let ⟨ht₁, ht₂, hhd⟩ := h
+    obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁
+    obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂
+    simp only [head?_cons, ne_eq, Option.some.injEq] at hhd
+    rw [← ne_eq] at hhd
+    simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm]
+termination_by l₁.length
+decreasing_by
+  rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁
+    _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇
+  clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄
+    _₂₅ _₂₆ _₂₇
+  subst _l₁
+  simp
+
+end
+
 /-! ### drop -/
 
 theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)