Documentation

Batteries.Data.List.Scan

List scan #

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

List.scanl #

source
@[simp]
theorem List.length_scanl {β : Type u_1} {α : Type u_2} {f : β → α → β} (b : β) (l : List α) :
(scanl f b l).length = l.length + 1
source
@[simp]
theorem List.scanl_nil {β : Type u_1} {α : Type u_2} {f : β → α → β} (b : β) :
scanl f b [] = [b]
source
@[simp]
theorem List.scanl_cons {β : Type u_1} {α : Type u_2} {b : β} {a : α} {l : List α} {f : β → α → β} :
scanl f b (a :: l) = b :: scanl f (f b a) l
source
theorem List.scanl_singleton {β : Type u_1} {α : Type u_2} {b : β} {a : α} {f : β → α → β} :
scanl f b [a] = [b, f b a]
source
@[simp]
theorem List.scanl_ne_nil {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} :
scanl f b l ≠ []
source
@[simp]
theorem List.scanl_iff_nil {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (c : β) :
scanl f b l = [c] ↔ c = b ∧ l = []
source
@[simp]
theorem List.getElem_scanl {α : Type u_1} {β : Type u_2} {i : Nat} {a : α} {l : List β} {f : α → β → α} (h : i < (scanl f a l).length) :
(scanl f a l)[i] = foldl f a (take i l)
source
theorem List.getElem?_scanl {α : Type u_1} {β : Type u_2} {a : α} {l : List β} {i : Nat} {f : α → β → α} :
(scanl f a l)[i]? = if i ≤ l.length then some (foldl f a (take i l)) else none
source
theorem List.take_scanl {α : Type u_1} {β : Type u_2} {f : α → β → α} (a : α) (l : List β) (i : Nat) :
take (i + 1) (scanl f a l) = scanl f a (take i l)
source
theorem List.getElem?_scanl_zero {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} :
(scanl f b l)[0]? = some b
source
theorem List.getElem_scanl_zero {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} :
(scanl f b l)[0] = b
source
@[simp]
theorem List.head_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : scanl f b l ≠ []) :
(scanl f b l).head h = b
source
theorem List.getLast_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : scanl f b l ≠ []) :
(scanl f b l).getLast h = foldl f b l
source
theorem List.getLast?_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} :
(scanl f b l).getLast? = some (foldl f b l)
source
theorem List.getElem?_succ_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {i : Nat} {f : β → α → β} :
(scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun (x : β) => Option.map (fun (y : α) => f x y) l[i]?
source
theorem List.getElem_succ_scanl {β : Type u_1} {α : Type u_2} {i : Nat} {b : β} {l : List α} {f : β → α → β} (h : i + 1 < (scanl f b l).length) :
(scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]
source
theorem List.scanl_append {β : Type u_1} {α : Type u_2} {b : β} {f : β → α → β} (l₁ l₂ : List α) :
scanl f b (l₁ ++ l₂) = scanl f b l₁ ++ (scanl f (foldl f b l₁) l₂).tail
source
theorem List.scanl_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ → β} {g : α → γ} (b : β) (l : List α) :
scanl f b (map g l) = scanl (fun (acc : β) (x : α) => f acc (g x)) b l

List.scanr #

source
@[simp]
theorem List.scanr_nil {α : Type u_1} {β : Type u_2} {f : α → β → β} (b : β) :
scanr f b [] = [b]
source
@[simp]
theorem List.scanr_ne_nil {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} :
scanr f b l ≠ []
source
@[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
source
theorem List.scanr_singleton {α : Type u_1} {β : Type u_2} {b : β} {a : α} {f : α → β → β} :
scanr f b [a] = [f a b, b]
source
@[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 = []
source
@[simp]
theorem List.length_scanr {α : Type u_1} {β : Type u_2} {f : α → β → β} (b : β) (l : List α) :
(scanr f b l).length = l.length + 1
source
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
source
@[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
source
theorem List.getLast_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} (h : scanr f b l ≠ []) :
(scanr f b l).getLast h = b
source
theorem List.getLast?_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} :
(scanr f b l).getLast? = some b
source
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
source
theorem List.drop_scanr {α : Type u_1} {β : Type u_2} {i : Nat} {b : β} {l : List α} {f : α → β → β} (h : i ≤ l.length) :
drop i (scanr f b l) = scanr f b (drop i l)
source
@[simp]
theorem List.getElem_scanr {α : Type u_1} {β : Type u_2} {i : Nat} {b : β} {l : List α} {f : α → β → β} (h : i < (scanr f b l).length) :
(scanr f b l)[i] = foldr f b (drop i l)
source
theorem List.getElem?_scanr {α : Type u_1} {β : Type u_2} {i : Nat} {b : β} {l : List α} {f : α → β → β} (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
source
theorem List.getElem_scanr_zero {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} :
(scanr f b l)[0] = foldr f b l
source
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)
source
theorem List.getElem?_scanr_of_lt {α : Type u_1} {β : Type u_2} {i : Nat} {b : β} {l : List α} {f : α → β → β} (h : i < l.length + 1) :
(scanr f b l)[i]? = some (foldr f b (drop i l))
source
theorem List.scanr_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → β} {g : γ → α} (b : β) (l : List γ) :
scanr f b (map g l) = scanr (fun (x : γ) (acc : β) => f (g x) acc) b l
source
@[simp]
theorem List.scanl_reverse {β : Type u_1} {α : Type u_2} {f : β → α → β} (b : β) (l : List α) :
scanl f b l.reverse = (scanr (flip f) b l).reverse
source
@[simp]
theorem List.scanr_reverse {α : Type u_1} {β : Type u_2} {f : α → β → β} (b : β) (l : List α) :
scanr f b l.reverse = (scanl (flip f) b l).reverse

partialSums/partialProd #

source
@[simp]
theorem List.length_partialSums {α : Type u_1} [Add α] [Zero α] {l : List α} :
l.partialSums.length = l.length + 1
source
@[simp]
theorem List.partialSums_ne_nil {α : Type u_1} [Add α] [Zero α] {l : List α} :
l.partialSums ≠ []
source
@[simp]
theorem List.partialSums_nil {α : Type u_1} [Add α] [Zero α] :
[].partialSums = [0]
source
theorem List.partialSums_cons {α : Type u_1} {a : α} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
(a :: l).partialSums = 0 :: map (fun (x : α) => a + x) l.partialSums
source
theorem List.partialSums_append {α : Type u_1} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l₁ l₂ : List α} :
(l₁ ++ l₂).partialSums = l₁.partialSums ++ map (fun (x : α) => l₁.sum + x) l₂.partialSums.tail
source
@[simp]
theorem List.getElem_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} (h : i < l.partialSums.length) :
l.partialSums[i] = (take i l).sum
source
@[simp]
theorem List.getElem?_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
l.partialSums[i]? = if i ≤ l.length then some (take i l).sum else none
source
@[simp]
theorem List.take_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] {l : List α} :
take (i + 1) l.partialSums = (take i l).partialSums
source
@[simp]
theorem List.length_partialProds {α : Type u_1} [Mul α] [One α] {l : List α} :
l.partialProds.length = l.length + 1
source
@[simp]
theorem List.partialProds_nil {α : Type u_1} [Mul α] [One α] :
[].partialProds = [1]
source
theorem List.partialProds_cons {α : Type u_1} {a : α} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
(a :: l).partialProds = 1 :: map (fun (x : α) => a * x) l.partialProds
source
theorem List.partialProds_append {α : Type u_1} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l₁ l₂ : List α} :
(l₁ ++ l₂).partialProds = l₁.partialProds ++ map (fun (x : α) => l₁.prod * x) l₂.partialProds.tail
source
@[simp]
theorem List.getElem_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} (h : i < l.partialProds.length) :
l.partialProds[i] = (take i l).prod
source
@[simp]
theorem List.getElem?_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
l.partialProds[i]? = if i ≤ l.length then some (take i l).prod else none
source
@[simp]
theorem List.take_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] {l : List α} :
take (i + 1) l.partialProds = (take i l).partialProds