Documentation

Batteries.Data.Array.Monadic

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 α} (motive : NatβProp) {init : β} (h0 : motive 0 init) {f : βαm β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) bSatisfiesM (motive (i + 1)) (f b as[i])) :
SatisfiesM (motive as.size) (Array.foldlM f init as)
@[irreducible]
theorem Array.SatisfiesM_foldlM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} (motive : NatβProp) {f : βαm β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) bSatisfiesM (motive (i + 1)) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j as.size) (h₂ : as.size i + j) (H : motive j b) :
SatisfiesM (motive as.size) (Array.foldlM.loop f as as.size i j b)
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 : NatProp) (h0 : motive 0) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive iSatisfiesM (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]) (Array.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]) (Array.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) (Array.mapM f as)
theorem Array.SatisfiesM_anyM {m : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (as : Array α) (start : Nat) (stop : Nat) (hstart : start min stop as.size) (tru : Prop) (fal : NatProp) (h0 : fal start) (hp : ∀ (i : Fin as.size), i < stopfal iSatisfiesM (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)) (Array.anyM p as start stop)
@[irreducible]
theorem Array.SatisfiesM_anyM.go {m : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (as : Array α) (tru : Prop) (fal : NatProp) {stop : Nat} {j : Nat} (hj' : j stop) (hstop : stop as.size) (h0 : fal j) (hp : ∀ (i : Fin as.size), i < stopfal iSatisfiesM (fun (x : Bool) => bif x then tru else fal (i + 1)) (p as[i])) :
SatisfiesM (fun (res : Bool) => bif res then tru else fal stop) (Array.anyM.loop p as stop hstop j)
theorem Array.SatisfiesM_anyM_iff_exists {m : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (as : Array α) (start : Nat) (stop : Nat) (q : Fin as.sizeProp) (hp : ∀ (i : Fin as.size), start ii < stopSatisfiesM (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) (Array.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 α} (motive : NatβProp) {init : β} (h0 : motive as.size init) {f : αβm β} (hf : ∀ (i : Fin as.size) (b : β), motive (i + 1) bSatisfiesM (motive i) (f as[i] b)) :
SatisfiesM (motive 0) (Array.foldrM f init as)
@[irreducible]
theorem Array.SatisfiesM_foldrM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {as : Array α} (motive : NatβProp) {f : αβm β} (hf : ∀ (i : Fin as.size) (b : β), motive (i + 1) bSatisfiesM (motive i) (f as[i] b)) {i : Nat} {b : β} (hi : i as.size) (H : motive i b) :
SatisfiesM (motive 0) (Array.foldrM.fold f as 0 i hi b)
theorem Array.SatisfiesM_mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.sizeαm β) (motive : NatProp) (h0 : motive 0) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive iSatisfiesM (fun (x : β) => p i x 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, h arr[i]) (as.mapIdxM f)
theorem Array.SatisfiesM_mapIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.sizeαm β) (motive : NatProp) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive iSatisfiesM (fun (x : β) => p i x motive (i + 1)) (f i as[i])) {bs : Array β} {i : Nat} {j : Nat} {h : i + j = as.size} (h₁ : j = bs.size) (h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i, h bs[i]) (hm : motive j) :
SatisfiesM (fun (arr : Array β) => motive as.size ∃ (eq : arr.size = as.size), ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1, h arr[i_1]) (Array.mapIdxM.map as f i j h bs)
theorem Array.size_modifyM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : αm α) :
SatisfiesM (fun (x : Array α) => x.size = a.size) (a.modifyM i f)