List scan

Prove basic results about List.scanl, List.scanr, List.scanlM and List.scanrM.

List.scanlM and List.scanrM

theorem List.scanAuxM.go_eq_append_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {xs : List β} {last : α} {acc : List α} [Monad m] [LawfulMonad m] {f : α → β → m α} : go f xs last acc = (fun (x : List α) => x ++ acc) <$> scanAuxM f last xs

theorem List.scanAuxM_nil {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} [Monad m] {f : α → β → m α} : scanAuxM f init [] = pure [init]

theorem List.scanAuxM_cons {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} {x : β} {xs : List β} [Monad m] [LawfulMonad m] {f : α → β → m α} : scanAuxM f init (x :: xs) = do let __do_lift ← f init x let __do_lift ← scanAuxM f __do_lift xs pure (__do_lift ++ [init])

@[simp]

theorem List.scanlM_nil {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} [Monad m] [LawfulMonad m] {f : α → β → m α} : scanlM f init [] = pure [init]

@[simp]

theorem List.scanlM_cons {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} {x : β} {xs : List β} [Monad m] [LawfulMonad m] {f : α → β → m α} : scanlM f init (x :: xs) = do let __do_lift ← f init x let __do_lift ← scanlM f __do_lift xs pure (init :: __do_lift)

@[simp]

theorem List.scanrM_concat {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {xs : List α} {x : α} [Monad m] [LawfulMonad m] {f : α → β → m β} : scanrM f init (xs ++ [x]) = do let __do_lift ← f x init let __do_lift ← scanrM f __do_lift xs pure (__do_lift ++ [init])

@[simp]

theorem List.scanrM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] {f : α → β → m β} : scanrM f init [] = pure [init]

theorem List.scanlM_eq_scanrM_reverse {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [Monad m] {f : β → α → m β} : scanlM f init as = reverse <$> scanrM (flip f) init as.reverse

theorem List.scanrM_eq_scanlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [Monad m] [LawfulMonad m] {f : α → β → m β} : scanrM f init as = reverse <$> scanlM (flip f) init as.reverse

@[simp]

theorem List.scanrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [Monad m] [LawfulMonad m] {f : α → β → m β} : scanrM f init as.reverse = reverse <$> scanlM (flip f) init as

@[simp]

theorem List.scanlM_reverse {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [Monad m] {f : β → α → m β} : scanlM f init as.reverse = reverse <$> scanrM (flip f) init as

theorem List.scanlM_pure {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → β} {as : List α} : scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as = pure (scanl f init as)

theorem List.scanrM_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → β} {as : List α} : scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as = pure (scanr f init as)

theorem List.idRun_scanlM {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → Id β} {as : List α} : (scanlM f init as).run = scanl (fun (x1 : β) (x2 : α) => (f x1 x2).run) init as

theorem List.idRun_scanrM {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → Id β} {as : List α} : (scanrM f init as).run = scanr (fun (x1 : α) (x2 : β) => (f x1 x2).run) init as

@[simp]

theorem List.scanlM_map {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α₁ → α₂} {g : β → α₂ → m β} {as : List α₁} : scanlM g init (map f as) = scanlM (fun (x1 : β) (x2 : α₁) => g x1 (f x2)) init as

@[simp]

theorem List.scanrM_map {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α₁ → α₂} {g : α₂ → β → m β} {as : List α₁} : scanrM g init (map f as) = scanrM (fun (a : α₁) (b : β) => g (f a) b) init as

List.scanl and List.scanr

@[simp]

theorem List.length_scanl {β : Type u_1} {α : Type u_2} {init : β} {as : List α} {f : β → α → β} : (scanl f init as).length = as.length + 1

@[simp]

theorem List.scanl_nil {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} : scanl f init [] = [init]

@[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

theorem List.scanl_singleton {β : Type u_1} {α : Type u_2} {b : β} {a : α} {f : β → α → β} : scanl f b [a] = [b, f b a]

@[simp]

theorem List.scanl_ne_nil {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} : scanl f b l ≠ []

@[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 = []

@[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)

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

theorem List.take_scanl {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β) (as : List α) (i : Nat) : take (i + 1) (scanl f init as) = scanl f init (take i as)

theorem List.getElem?_scanl_zero {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} : (scanl f b l)[0]? = some b

theorem List.getElem_scanl_zero {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} : (scanl f b l)[0] = b

@[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

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

theorem List.getLast?_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} : (scanl f b l).getLast? = some (foldl f b l)

theorem List.tail_scanl {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β} (h : 0 < l.length) : (scanl f b l).tail = scanl f (f b (l.head ⋯)) l.tail

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]?

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]

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

theorem List.scanl_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {init : β} {f : β → γ → β} {g : α → γ} {as : List α} : scanl f init (map g as) = scanl (fun (acc : β) (x : α) => f acc (g x)) init as

theorem List.scanl_eq_scanr_reverse {β : Type u_1} {α : Type u_2} {init : β} {as : List α} {f : β → α → β} : scanl f init as = (scanr (flip f) init as.reverse).reverse

theorem List.scanr_eq_scanl_reverse {α : Type u_1} {β : Type u_2} {init : β} {as : List α} {f : α → β → β} : scanr f init as = (scanl (flip f) init as.reverse).reverse

@[simp]

theorem List.scanr_nil {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} : scanr f init [] = [init]

@[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_ne_nil {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} : scanr f b l ≠ []

theorem List.scanr_singleton {α : Type u_1} {β : Type u_2} {b : β} {a : α} {f : α → β → β} : scanr f b [a] = [f a b, b]

@[simp]

theorem List.length_scanr {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α} : (scanr f init as).length = as.length + 1

@[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 = []

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.getLast_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} (h : scanr f b l ≠ []) : (scanr f b l).getLast h = b

theorem List.getLast?_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} : (scanr f b l).getLast? = some b

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} {i : Nat} {b : β} {l : List α} {f : α → β → β} (h : i ≤ l.length) : drop i (scanr f b l) = scanr f b (drop i l)

@[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)

theorem List.getElem?_scanr {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {i : Nat} {f : α → β → β} : (scanr f b l)[i]? = if i < l.length + 1 then some (foldr f b (drop i l)) else none

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_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))

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

@[simp]

theorem List.scanl_reverse {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : List α} : scanl f init as.reverse = (scanr (flip f) init as).reverse

@[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

@[simp]

theorem List.length_partialSums {α : Type u_1} [Add α] [Zero α] {l : List α} : l.partialSums.length = l.length + 1

@[simp]

theorem List.partialSums_ne_nil {α : Type u_1} [Add α] [Zero α] {l : List α} : l.partialSums ≠ []

@[simp]

theorem List.partialSums_nil {α : Type u_1} [Add α] [Zero α] : [].partialSums = [0]

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

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

@[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

@[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

@[simp]

theorem List.take_partialSums {α : Type u_1} {i : Nat} [Add α] [Zero α] {l : List α} : take (i + 1) l.partialSums = (take i l).partialSums

@[simp]

theorem List.length_partialProds {α : Type u_1} [Mul α] [One α] {l : List α} : l.partialProds.length = l.length + 1

@[simp]

theorem List.partialProds_nil {α : Type u_1} [Mul α] [One α] : [].partialProds = [1]

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

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

@[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

@[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

@[simp]

theorem List.take_partialProds {α : Type u_1} {i : Nat} [Mul α] [One α] {l : List α} : take (i + 1) l.partialProds = (take i l).partialProds

flatten

theorem List.length_flatten_mem_partialSums_map_length {α : Type u_1} (L : List (List α)) : L.flatten.length ∈ (map length L).partialSums

theorem List.getElem_flatten_aux₁ {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) : findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1 < L.length

theorem List.getElem_flatten_aux₂ {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) : let j := findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1; have hj := ⋯; have k := i - (take j L).flatten.length; k < L[j].length

theorem List.getElem_flatten {α : Type u_1} (L : List (List α)) (i : Nat) (h : i < L.flatten.length) : L.flatten[i] = let j := findIdx (fun (x : Nat) => decide (x > i)) (map length L).partialSums - 1; have hj := ⋯; let k := i - (take j L).flatten.length; have hk := ⋯; L[j][k]

Indexing into a flattened list: L.flatten[i] equals L[j][k] where j is the sublist index and k is the offset within that sublist.

The indices are computed as:

• j is one less than where the cumulative sum first exceeds i
• k is i minus the total length of the first j sublists

This theorem states that these indices are in range and the equality holds.