Bootstrapping theorems about arrays #
This file contains some theorems about Array and List needed for Std.List.Basic.
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) b → SatisfiesM (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) b → SatisfiesM (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.foldl_induction
{α : Type u_1}
{β : Type u_2}
{as : Array α}
(motive : Nat → β → Prop)
{init : β}
(h0 : motive 0 init)
{f : β → α → β}
(hf : ∀ (i : Fin (Array.size as)) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i]))
:
motive (Array.size as) (Array.foldl f init as 0)
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 (Array.size as) → β → Prop)
(hs : ∀ (i : Fin (Array.size as)), motive ↑i → SatisfiesM (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 : Type → Type 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 : Nat → Prop)
(h0 : fal start)
(hp : ∀ (i : Fin (Array.size as)),
↑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 (Array.size as))) (Array.anyM p as start stop)
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 : Nat}
{j : Nat}
(hj' : j ≤ stop)
(hstop : stop ≤ Array.size as)
(h0 : fal j)
(hp : ∀ (i : Fin (Array.size as)),
↑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) (Array.anyM.loop p as stop hstop j)
theorem
Array.SatisfiesM_anyM_iff_exists
{m : Type → Type 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 ≤ ↑i → ↑i < stop → SatisfiesM (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.contains_def
{α : Type u_1}
[DecidableEq α]
{a : α}
{as : Array α}
:
Array.contains as a = true ↔ a ∈ as
instance
Array.instDecidableMemArrayInstMembershipArray
{α : Type u_1}
[DecidableEq α]
(a : α)
(as : Array α)
: