From 6fb4f5e024f64b430895103f71c860d34c1f3aa9 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 12 Feb 2024 21:30:54 +0900 Subject: [PATCH] refactor: move theorems about lists from mathlib `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. I removed the `simp` priority and `nolint` attribute from `modifyHead_modifyHead` because we don't need them anymore. We need these theorems to prove `String.splitOn_of_valid`. See https://github.com/leanprover-community/batteries/pull/756. Co-authored-by: Kim Morrison --- Batteries/Data/List/Lemmas.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index fd82629a8a..6deb2f1873 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -17,6 +17,10 @@ open Nat @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by simp [Array.mem_def] +/-! ### isEmpty -/ + +theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;> simp [isEmpty] + /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @@ -34,6 +38,11 @@ theorem get?_inj apply getElem?_inj h₀ h₁ simp_all +/-! ### modifyHead -/ + +@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) : + (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead] + /-! ### modifyNth -/ @[simp] theorem modifyNth_nil (f : α → α) (n) : [].modifyNth f n = [] := by cases n <;> rfl