Documentation

Mathlib.Data.List.Scan

List scan #

Prove basic results about List.scanl and List.scanr.

List.scanl #

@[simp]
theorem List.length_scanl {α : Type u_1} {β : Type u_2} {f : βαβ} (b : β) (l : List α) :
(scanl f b l).length = l.length + 1
@[simp]
theorem List.scanl_nil {α : Type u_1} {β : Type u_2} {f : βαβ} (b : β) :
scanl f b [] = [b]
@[simp]
theorem List.scanl_ne_nil {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} :
scanl f b l []
@[simp]
theorem List.scanl_iff_nil {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} (c : β) :
scanl f b l = [c] c = b l = []
@[simp]
theorem List.scanl_cons {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {a : α} {l : List α} :
scanl f b (a :: l) = [b] ++ scanl f (f b a) l
theorem List.getElem?_scanl_zero {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} :
(scanl f b l)[0]? = some b
@[simp]
theorem List.getElem_scanl_zero {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} :
(scanl f b l)[0] = b
@[simp]
theorem List.head_scanl {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} (h : scanl f b l []) :
(scanl f b l).head h = b
theorem List.getElem?_succ_scanl {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} {i : } :
(scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun (x : β) => Option.map (fun (y : α) => f x y) l[i]?
@[deprecated List.getElem?_succ_scanl (since := "2025-02-21")]
theorem List.get?_succ_scanl {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} {i : } :
(scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun (x : β) => Option.map (fun (y : α) => f x y) l[i]?

Alias of List.getElem?_succ_scanl.

theorem List.getElem_succ_scanl {α : Type u_1} {β : Type u_2} {f : βαβ} {b : β} {l : List α} {i : } (h : i + 1 < (scanl f b l).length) :
(scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]

List.scanr #

@[simp]
theorem List.scanr_nil {α : Type u_1} {β : Type u_2} {f : αββ} (b : β) :
scanr f b [] = [b]
@[simp]
theorem List.scanr_ne_nil {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} :
scanr f b l []
@[simp]
theorem List.scanr_cons {α : Type u_1} {β : Type u_2} {b : β} {a : α} {l : List α} {f : αββ} :
scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l
@[simp]
theorem List.scanr_iff_nil {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} (c : β) :
scanr f b l = [c] c = b l = []
@[simp]
theorem List.length_scanr {α : Type u_1} {β : Type u_2} {f : αββ} (b : β) (l : List α) :
(scanr f b l).length = l.length + 1
theorem List.scanr_append {α : Type u_1} {β : Type u_2} {b : β} {f : αββ} (l₁ l₂ : List α) :
scanr f b (l₁ ++ l₂) = scanr f (foldr f b l₂) l₁ ++ (scanr f b l₂).tail
@[simp]
theorem List.head_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} (h : scanr f b l []) :
(scanr f b l).head h = foldr f b l
theorem List.tail_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} (h : 0 < l.length) :
(scanr f b l).tail = scanr f b l.tail
theorem List.drop_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} {i : } (h : i l.length) :
drop i (scanr f b l) = scanr f b (drop i l)
@[simp]
theorem List.getElem_scanr_zero {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} :
(scanr f b l)[0] = foldr f b l
theorem List.getElem?_scanr_zero {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} :
(scanr f b l)[0]? = some (foldr f b l)
theorem List.getElem_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} {i : } (h : i < (scanr f b l).length) :
(scanr f b l)[i] = foldr f b (drop i l)
theorem List.getElem?_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} {i : } (h : i < l.length + 1) :
(scanr f b l)[i]? = if i < l.length + 1 then some (foldr f b (drop i l)) else none
theorem List.getElem?_scanr_of_lt {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αββ} {i : } (h : i < l.length + 1) :
(scanr f b l)[i]? = some (foldr f b (drop i l))