feat: upstream more List lemmas (#4856)

src/Init/Core.lean

@@ -1107,6 +1107,7 @@ inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α 
 /-! # Subtype -/
 
 namespace Subtype
+
 theorem existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 

src/Init/Data.lean

@@ -36,3 +36,4 @@ import Init.Data.Channel
 import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
+import Init.Data.Subtype

src/Init/Data/List.lean

@@ -12,3 +12,5 @@ import Init.Data.List.Attach
 import Init.Data.List.Impl
 import Init.Data.List.TakeDrop
 import Init.Data.List.Notation
+import Init.Data.List.Range
+import Init.Data.List.Nat

src/Init/Data/List/Attach.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.List.Lemmas
+import Init.Data.Subtype
 
 namespace List
 
@@ -44,3 +45,155 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   | nil, hL' => rfl
   | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
   exact go L h'
+
+@[simp] theorem attach_nil : ([] : List α).attach = [] := rfl
+
+@[simp]
+theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) :
+    @pmap _ _ p (fun a _ => f a) l H = map f l := by
+  induction l
+  · rfl
+  · simp only [*, pmap, map]
+
+theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂}
+    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
+  induction l with
+  | nil => rfl
+  | cons x l ih => rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]
+
+theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
+    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
+  induction l
+  · rfl
+  · simp only [*, pmap, map]
+
+theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
+    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun a h => H _ (mem_map_of_mem _ h) := by
+  induction l
+  · rfl
+  · simp only [*, pmap, map]
+
+theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
+    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
+  rw [attach, attachWith, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl
+
+theorem attach_map_coe (l : List α) (f : α → β) :
+    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
+  rw [attach, attachWith, map_pmap]; exact pmap_eq_map _ _ _ _
+
+theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
+  attach_map_coe _ _
+
+@[simp]
+theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
+  (attach_map_coe _ _).trans l.map_id
+
+theorem countP_attach (l : List α) (p : α → Bool) : l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+  simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]
+
+@[simp]
+theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a :=
+  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
+
+@[simp]
+theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
+  | ⟨a, h⟩ => by
+    have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
+    rcases this with ⟨⟨_, _⟩, m, rfl⟩
+    exact m
+
+@[simp]
+theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
+    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
+  simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
+
+@[simp]
+theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by
+  induction l
+  · rfl
+  · simp only [*, pmap, length]
+
+@[simp]
+theorem length_attach (L : List α) : L.attach.length = L.length :=
+  length_pmap
+
+@[simp]
+theorem pmap_eq_nil {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by
+  rw [← length_eq_zero, length_pmap, length_eq_zero]
+
+@[simp]
+theorem attach_eq_nil (l : List α) : l.attach = [] ↔ l = [] :=
+  pmap_eq_nil
+
+theorem getLast_pmap (p : α → Prop) (f : ∀ a, p a → β) (l : List α)
+    (hl₁ : ∀ a ∈ l, p a) (hl₂ : l ≠ []) :
+    (l.pmap f hl₁).getLast (mt List.pmap_eq_nil.1 hl₂) =
+      f (l.getLast hl₂) (hl₁ _ (List.getLast_mem hl₂)) := by
+  induction l with
+  | nil => apply (hl₂ rfl).elim
+  | cons l_hd l_tl l_ih =>
+    by_cases hl_tl : l_tl = []
+    · simp [hl_tl]
+    · simp only [pmap]
+      rw [getLast_cons, l_ih _ hl_tl]
+      simp only [getLast_cons hl_tl]
+
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
+    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons hd tl hl =>
+    rcases n with ⟨n⟩
+    · simp only [Option.pmap]
+      split <;> simp_all
+    · simp only [hl, pmap, Option.pmap, getElem?_cons_succ]
+      split <;> rename_i h₁ _ <;> split <;> rename_i h₂ _
+      · simp_all
+      · simp at h₂
+        simp_all
+      · simp_all
+      · simp_all
+
+theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
+    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (get?_mem H) := by
+  simp only [get?_eq_getElem?]
+  simp [getElem?_pmap, h]
+
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
+    (hn : n < (pmap f l h).length) :
+    (pmap f l h)[n] =
+      f (l[n]'(@length_pmap _ _ p f l h ▸ hn))
+        (h _ (getElem_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
+  induction l generalizing n with
+  | nil =>
+    simp only [length, pmap] at hn
+    exact absurd hn (Nat.not_lt_of_le n.zero_le)
+  | cons hd tl hl =>
+    cases n
+    · simp
+    · simp [hl]
+
+theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
+    (hn : n < (pmap f l h).length) :
+    get (pmap f l h) ⟨n, hn⟩ =
+      f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
+        (h _ (get_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
+  simp only [get_eq_getElem]
+  simp [getElem_pmap]
+
+theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι)
+    (h : ∀ a ∈ l₁ ++ l₂, p a) :
+    (l₁ ++ l₂).pmap f h =
+      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
+        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
+  induction l₁ with
+  | nil => rfl
+  | cons _ _ ih =>
+    dsimp only [pmap, cons_append]
+    rw [ih]
+
+theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : List α)
+    (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
+    ((l₁ ++ l₂).pmap f fun a ha => (List.mem_append.1 ha).elim (h₁ a) (h₂ a)) =
+      l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
+  pmap_append f l₁ l₂ _

src/Init/Data/List/Basic.lean

@@ -611,7 +611,7 @@ If `l` is initially larger than `n`, just return `l`.
 -/
 def rightpad (n : Nat) (a : α) (l : List α) : List α := l ++ replicate (n - length l) a
 
-/-! ### reduceOption-/
+/-! ### reduceOption -/
 
 /-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/
 @[inline] def reduceOption {α} : List (Option α) → List α :=
@@ -1168,11 +1168,15 @@ theorem findSome?_cons {f : α → Option β} :
   | [], n => n
   | a :: l, n => bif p a then n else go l (n + 1)
 
+@[simp] theorem findIdx_nil {α : Type _} (p : α → Bool) : [].findIdx p = 0 := rfl
+
 /-! ### indexOf -/
 
 /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
 def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
+@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl
+
 /-! ### findIdx? -/
 
 /-- Return the index of the first occurrence of an element satisfying `p`. -/

src/Init/Data/List/Control.lean

@@ -227,6 +227,8 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
 instance : ForIn m (List α) α where
   forIn := List.forIn
 
+@[simp] theorem forIn_eq_forIn [Monad m] : @List.forIn α β m _ = forIn := rfl
+
 @[simp] theorem forIn_nil [Monad m] (f : α → β → m (ForInStep β)) (b : β) : forIn [] b f = pure b :=
   rfl