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) b → SatisfiesM (motive (↑i + 1)) (f b as[i]))
:
SatisfiesM (motive as.size) (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) b → SatisfiesM (motive (↑i + 1)) (f b as[i]))
{i j : Nat}
{b : β}
(h₁ : j ≤ as.size)
(h₂ : as.size ≤ i + j)
(H : motive j b)
:
SatisfiesM (motive as.size) (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 : Nat → Prop)
(h0 : motive 0)
(p : Fin as.size → β → Prop)
(hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun (x : β) => p i x ∧ motive (↑i + 1)) (f as[i]))
:
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 α)
:
theorem
Array.SatisfiesM_anyM
{m : Type → Type u_1}
{α : Type u_2}
[Monad m]
[LawfulMonad m]
(p : α → m Bool)
(as : Array α)
(start stop : Nat)
(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)
@[irreducible]
theorem
Array.SatisfiesM_anyM.go
{m : Type → Type u_1}
{α : Type u_2}
[Monad m]
[LawfulMonad m]
(p : α → m Bool)
(as : Array α)
(tru : Prop)
(fal : Nat → Prop)
{stop j : Nat}
(hj' : j ≤ stop)
(hstop : stop ≤ as.size)
(h0 : fal j)
(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 stop) (anyM.loop p as stop hstop j)
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) b → SatisfiesM (motive ↑i) (f as[i] b))
:
SatisfiesM (motive 0) (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) b → SatisfiesM (motive ↑i) (f as[i] b))
{i : Nat}
{b : β}
(hi : i ≤ as.size)
(H : motive i b)
:
SatisfiesM (motive 0) (foldrM.fold f as 0 i hi b)
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)
(h0 : motive 0)
(p : (i : Nat) → β → i < as.size → Prop)
(hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun (x : β) => p i x h ∧ motive (i + 1)) (f i as[i] h))
:
theorem
Array.SatisfiesM_mapFinIdxM.go
{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)
(hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun (x : β) => p i x h ∧ motive (i + 1)) (f i as[i] h))
{bs : Array β}
{i j : Nat}
{h : i + j = as.size}
(h₁ : j = bs.size)
(h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h)
(hm : motive j)
:
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 β)
(motive : Nat → Prop)
(h0 : motive 0)
(p : (i : Nat) → β → i < as.size → Prop)
(hs : ∀ (i : Nat) (h : i < as.size), motive i → SatisfiesM (fun (x : β) => p i x h ∧ motive (i + 1)) (f i as[i]))
:
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_modifyM
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(a : Array α)
(i : Nat)
(f : α → m α)
:
theorem
List.filterM_toArray
{m : Type → Type u_1}
{α : Type}
[Monad m]
[LawfulMonad m]
(l : List α)
(p : α → m Bool)
:
theorem
List.filterRevM_toArray
{m : Type → Type u_1}
{α : Type}
[Monad m]
[LawfulMonad m]
(l : List α)
(p : α → m Bool)
:
theorem
List.filterMapM_toArray
{m : Type u_1 → Type u_2}
{α β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : List α)
(f : α → m (Option β))
:
theorem
List.flatMapM_toArray
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : List α)
(f : α → m (Array β))
:
theorem
List.mapFinIdxM_toArray.go
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : List α)
(f : (i : Nat) → α → i < l.length → m β)
(i : Nat)
(acc : Array β)
(inv : i + acc.size = l.length)
:
Array.mapFinIdxM.map l.toArray f i acc.size inv acc = toArray <$> mapFinIdxM.go l f (drop acc.size l) acc ⋯
theorem
List.mapIdxM_toArray.go
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(l : List α)
(f : Nat → α → m β)
(bs : List α)
(acc : Array β)
(inv : bs.length + acc.size = l.length)
:
mapFinIdxM.go l (fun (i : Nat) (a : α) (h : i < l.length) => f i a) bs acc inv = mapIdxM.go f bs acc
theorem
Array.toList_filterM
{m : Type → Type u_1}
{α : Type}
[Monad m]
[LawfulMonad m]
(a : Array α)
(p : α → m Bool)
:
theorem
Array.toList_filterRevM
{m : Type → Type u_1}
{α : Type}
[Monad m]
[LawfulMonad m]
(a : Array α)
(p : α → m Bool)
:
theorem
Array.toList_filterMapM
{m : Type u_1 → Type u_2}
{α β : Type u_1}
[Monad m]
[LawfulMonad m]
(a : Array α)
(f : α → m (Option β))
: