Results about monadic operations on Array, in terms of SatisfiesM.

The pure versions of these theorems are proved in Batteries.Data.Array.Lemmas directly, in order to minimize dependence on SatisfiesM.

theorem Array.SatisfiesM_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {init : β} {motive : Nat → β → Prop} {f : β → α → m β} (h0 : motive 0 init) (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])) : SatisfiesM (motive as.size) (foldlM f init as)

theorem Array.SatisfiesM_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {f : α → m β} {motive : Nat → Prop} {p : Fin as.size → β → Prop} (h0 : motive 0) (hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun (x : β) => p i x ∧ motive (↑i + 1)) (f as[i])) : SatisfiesM (fun (arr : Array β) => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (mapM f as)

theorem Array.SatisfiesM_mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {f : α → m β} {p : Fin as.size → β → Prop} (hs : ∀ (i : Fin as.size), SatisfiesM (p i) (f as[i])) : SatisfiesM (fun (arr : Array β) => ∃ (eq : arr.size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (mapM f as)

theorem Array.size_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (as : Array α) : SatisfiesM (fun (arr : Array β) => arr.size = as.size) (mapM f as)

theorem Array.SatisfiesM_anyM {m : Type → Type u_1} {α : Type u_2} {start stop : Nat} [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} (hstart : start ≤ min stop as.size) (tru : Prop) (fal : Nat → Prop) (h0 : fal start) (hp : ∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun (x : Bool) => bif x then tru else fal (↑i + 1)) (p as[i])) : SatisfiesM (fun (res : Bool) => bif res then tru else fal (min stop as.size)) (anyM p as start stop)

theorem Array.SatisfiesM_anyM_iff_exists {m : Type → Type u_1} {α : Type u_2} {start stop : Nat} [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} {q : Fin as.size → Prop} (hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun (x : Bool) => x = true ↔ q i) (p as[i])) : SatisfiesM (fun (res : Bool) => res = true ↔ ∃ (i : Fin as.size), start ≤ ↑i ∧ ↑i < stop ∧ q i) (anyM p as start stop)

theorem Array.SatisfiesM_foldrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {init : β} {motive : Nat → β → Prop} {f : α → β → m β} (h0 : motive as.size init) (hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)) : SatisfiesM (motive 0) (foldrM f init as)

theorem Array.SatisfiesM_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {f : (i : Nat) → α → i < as.size → m β} {motive : Nat → Prop} {p : (i : Nat) → β → i < as.size → Prop} (h0 : motive 0) (hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun (x : β) => p i x h ∧ motive (i + 1)) (f i as[i] h)) : SatisfiesM (fun (arr : Array β) => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : Nat) (h : i < as.size), p i arr[i] h) (as.mapFinIdxM f)

theorem Array.SatisfiesM_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} {f : Nat → α → m β} {p : (i : Nat) → β → i < as.size → Prop} {motive : Nat → Prop} (h0 : motive 0) (hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun (x : β) => p i x h ∧ motive (i + 1)) (f i as[i])) : SatisfiesM (fun (arr : Array β) => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : Nat) (h : i < as.size), p i arr[i] h) (mapIdxM f as)

theorem Array.size_mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : (i : Nat) → α → i < as.size → m β) : SatisfiesM (fun (arr : Array β) => arr.size = as.size) (as.mapFinIdxM f)

theorem Array.size_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : Nat → α → m β) : SatisfiesM (fun (arr : Array β) => arr.size = as.size) (mapIdxM f as)

theorem Array.size_modifyM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (i : Nat) (f : α → m α) : SatisfiesM (fun (x : Array α) => x.size = as.size) (as.modifyM i f)