Array

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

theorem Array.scanlM.loop_toList {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : Array α} {start : Nat} {acc : Array β} [Monad m] [LawfulMonad m] {f : β → α → m β} {stop : Nat} (h : stop ≤ as.size) : toList <$> loop f init as start stop h acc = do let __do_lift ← List.scanlM f init (List.take (stop - start) (List.drop start as.toList)) pure (acc.toList ++ __do_lift)

theorem Array.scanlM_eq_scanlM_toList {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} : scanlM f init as = List.toArray <$> List.scanlM f init as.toList

@[simp]

theorem Array.toList_scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} : toList <$> scanlM f init as = List.scanlM f init as.toList

theorem Array.scanrM.loop_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : Array α} {stop : Nat} {acc : Array β} [Monad m] [LawfulMonad m] {f : α → β → m β} {start : Nat} {h : start ≤ as.size} : toList <$> loop f init as start stop h acc = do let __do_lift ← List.scanrM f init (List.take (start - stop) (List.drop stop as.toList)) pure (__do_lift ++ acc.toList.reverse)

theorem Array.scanrM_eq_scanrM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} : scanrM f init as = List.toArray <$> List.scanrM f init as.toList

@[simp]

theorem Array.toList_scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} : toList <$> scanrM f init as = List.scanrM f init as.toList

theorem Array.scanlM_extract {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {start stop : Nat} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} : scanlM f init (as.extract start stop) = scanlM f init as start stop

theorem Array.scanrM_extract {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop start : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Array α} : scanrM f init (as.extract stop start) = scanrM f init as start stop

@[simp]

theorem Array.scanlM_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] {f : β → α → m β} {start stop : Nat} : scanlM f init #[] start stop = pure #[init]

theorem Array.scanrM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] {f : α → β → m β} {start stop : Nat} : scanrM f init #[] start stop = pure #[init]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Array.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 : Array α₁} : scanlM g init (map f as) = scanlM (fun (x1 : β) (x2 : α₁) => g x1 (f x2)) init as

theorem Array.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 : Array α₁} : scanrM g init (map f as) = scanrM (fun (a : α₁) (b : β) => g (f a) b) init as

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

Array.scanl

theorem Array.scanl_eq_scanl_toList {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α} : scanl f init as = (List.scanl f init as.toList).toArray

@[simp]

theorem Array.toList_scanl {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α} : (scanl f init as).toList = List.scanl f init as.toList

@[simp]

theorem Array.size_scanl {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β) (as : Array α) : (scanl f init as).size = as.size + 1

theorem Array.scanl_empty {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β) : scanl f init #[] = #[init]

theorem Array.scanl_singleton {β : Type u_1} {α : Type u_2} {init : β} {a : α} {f : β → α → β} : scanl f init #[a] = #[init, f init a]

@[simp]

theorem Array.scanl_ne_empty {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β} : scanl f init as ≠ #[]

@[simp]

theorem Array.scanl_eq_singleton_iff {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β} (c : β) : scanl f init as = #[c] ↔ c = init ∧ as = #[]

@[simp]

theorem Array.getElem_scanl {β : Type u_1} {α : Type u_2} {i : Nat} {init : β} {f : β → α → β} {as : Array α} (h : i < (scanl f init as).size) : (scanl f init as)[i] = foldl f init (as.take i)

theorem Array.getElem?_scanl {β : Type u_1} {α : Type u_2} {a : β} {l : Array α} {i : Nat} {f : β → α → β} : (scanl f a l)[i]? = if i ≤ l.size then some (foldl f a (l.take i)) else none

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

theorem Array.getElem?_scanl_zero {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β} : (scanl f init as)[0]? = some init

theorem Array.getElem_scanl_zero {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β} : (scanl f init as)[0] = init

theorem Array.getElem?_succ_scanl {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {i : Nat} {f : β → α → β} : (scanl f init as)[i + 1]? = (scanl f init as)[i]?.bind fun (x : β) => Option.map (fun (y : α) => f x y) as[i]?

theorem Array.getElem_succ_scanl {β : Type u_1} {α : Type u_2} {i : Nat} {b : β} {as : Array α} {f : β → α → β} (h : i + 1 < (scanl f b as).size) : (scanl f b as)[i + 1] = f (scanl f b as)[i] as[i]

theorem Array.scanl_push {β : Type u_1} {α : Type u_2} {f : β → α → β} {init : β} {a : α} {as : Array α} : scanl f init (as.push a) = (scanl f init as).push (f (foldl f init as) a)

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

@[simp]

theorem Array.back_scanl {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α} : (scanl f init as).back ⋯ = foldl f init as

theorem Array.back_scanl? {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α} : (scanl f init as).back? = some (foldl f init as)

Array.scanr

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

theorem Array.scanr_eq_scanr_toList {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α} : scanr f init as = (List.scanr f init as.toList).toArray

@[simp]

theorem Array.toList_scanr {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α} : (scanr f init as).toList = List.scanr f init as.toList

@[simp]

theorem Array.size_scanr {α : Type u_1} {β : Type u_2} {f : α → β → β} (init : β) (as : Array α) : (scanr f init as).size = as.size + 1

theorem Array.scanr_empty {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β} : scanr f init #[] = #[init]

@[simp]

theorem Array.scanr_ne_empty {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α} : scanr f init as ≠ #[]

theorem Array.scanr_push {α : Type u_1} {β : Type u_2} {a : α} {init : β} {f : α → β → β} {as : Array α} : scanr f init (as.push a) = (scanr f (f a init) as).push init

@[simp]

theorem Array.back_scanr {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α} : (scanr f init as).back ⋯ = init

theorem Array.back?_scanr {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α} : (scanr f init as).back? = some init

@[simp]

theorem Array.getElem_scanr {α : Type u_1} {β : Type u_2} {i : Nat} {b : β} {l : Array α} {f : α → β → β} (h : i < (scanr f b l).size) : (scanr f b l)[i] = foldr f b (l.drop i)

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

theorem Array.getElem_scanr_zero {α : Type u_1} {β : Type u_2} {init : β} {as : Array α} {f : α → β → β} : (scanr f init as)[0] = foldr f init as

theorem Array.getElem?_scanr_zero {α : Type u_1} {β : Type u_2} {init : β} {as : Array α} {f : α → β → β} : (scanr f init as)[0]? = some (foldr f init as)

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

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

theorem Array.scanl_extract {β : Type u_1} {α : Type u_2} {start stop : Nat} {init : β} {f : β → α → β} {as : Array α} : scanl f init (as.extract start stop) = scanl f init as start stop

theorem Array.scanr_extract {α : Type u_1} {β : Type u_2} {stop start : Nat} {init : β} {f : α → β → β} {as : Array α} : scanr f init (as.extract stop start) = scanr f init as start stop

theorem List.toArray_scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : List α} : toArray <$> scanlM f init as = Array.scanlM f init as.toArray

theorem List.toArray_scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : List α} : toArray <$> scanrM f init as = Array.scanrM f init as.toArray

theorem List.toArray_scanl {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : List α} : (scanl f init as).toArray = Array.scanl f init as.toArray

theorem List.toArray_scanr {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α} : (scanr f init as).toArray = Array.scanr f init as.toArray

@[simp]

theorem Subarray.scanlM_eq_scanlM_extract {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Subarray α} : scanlM f init as = Array.scanlM f init (as.array.extract as.start as.stop)

@[simp]

theorem Subarray.scanrM_eq_scanrM_extract {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Subarray α} : scanrM f init as = Array.scanrM f init (as.array.extract as.stop as.start)

@[simp]

theorem Subarray.scanl_eq_scanl_extract {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Subarray α} : scanl f init as = Array.scanl f init (as.array.extract as.start as.stop)

@[simp]

theorem Subarray.scanr_eq_scanr_extract {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Subarray α} : scanr f init as = Array.scanr f init (as.array.extract as.stop as.start)