Documentation

Std.Data.Array.Monadic

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

The pure versions of these theorems are proved in Std.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 (Array.size as)) (b : β), motive (i) bSatisfiesM (motive (i + 1)) (f b as[i])) :
SatisfiesM (motive (Array.size as)) (Array.foldlM f init as 0)
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 (Array.size as)) (b : β), motive (i) bSatisfiesM (motive (i + 1)) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j Array.size as) (h₂ : Array.size as i + j) (H : motive j b) :
SatisfiesM (motive (Array.size as)) (Array.foldlM.loop f as (Array.size as) 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 (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive iSatisfiesM (fun (x : β) => p i x motive (i + 1)) (f as[i])) :
SatisfiesM (fun (arr : Array β) => motive (Array.size as) ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := 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 (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), SatisfiesM (p i) (f as[i])) :
SatisfiesM (fun (arr : Array β) => ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := 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 β) => Array.size arr = Array.size as) (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 (Array.size as)) (tru : Prop) (fal : NatProp) (h0 : fal start) (hp : ∀ (i : Fin (Array.size as)), 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 (Array.size as))) (Array.anyM p as start stop)
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 Array.size as) (h0 : fal j) (hp : ∀ (i : Fin (Array.size as)), 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 (Array.size as)Prop) (hp : ∀ (i : Fin (Array.size as)), start ii < stopSatisfiesM (fun (x : Bool) => x = true q i) (p as[i])) :
SatisfiesM (fun (res : Bool) => res = true ∃ (i : Fin (Array.size as)), 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 (Array.size as) init) {f : αβm β} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive (i + 1) bSatisfiesM (motive i) (f as[i] b)) :
SatisfiesM (motive 0) (Array.foldrM f init as (Array.size as))
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 (Array.size as)) (b : β), motive (i + 1) bSatisfiesM (motive i) (f as[i] b)) {i : Nat} {b : β} (hi : i Array.size as) (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 (Array.size as)αm β) (motive : NatProp) (h0 : motive 0) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive iSatisfiesM (fun (x : β) => p i x motive (i + 1)) (f i as[i])) :
SatisfiesM (fun (arr : Array β) => motive (Array.size as) ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } arr[i]) (Array.mapIdxM as 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 (Array.size as)αm β) (motive : NatProp) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive iSatisfiesM (fun (x : β) => p i x motive (i + 1)) (f i as[i])) {bs : Array β} {i : Nat} {j : Nat} {h : i + j = Array.size as} (h₁ : j = Array.size bs) (h₂ : ∀ (i : Nat) (h : i < Array.size as) (h' : i < Array.size bs), p { val := i, isLt := h } bs[i]) (hm : motive j) :
SatisfiesM (fun (arr : Array β) => motive (Array.size as) ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } arr[i]) (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 α) => Array.size x = Array.size a) (Array.modifyM a i f)