@[simp]
@[simp]
@[simp]
@[simp]
theorem
Array.ugetElem_eq_getElem
{α : Type u_1}
(a : Array α)
{i : USize}
(h : USize.toNat i < Array.size a)
:
a[i] = a[USize.toNat i]
theorem
Array.get?_len_le
{α : Type u_1}
(a : Array α)
(i : Nat)
(h : Array.size a ≤ i)
:
a[i]? = none
theorem
Array.getElem_mem_data
{α : Type u_1}
{i : Nat}
(a : Array α)
(h : i < Array.size a)
:
a[i] ∈ a.data
theorem
Array.get?_eq_data_get?
{α : Type u_1}
(a : Array α)
(i : Nat)
:
Array.get? a i = List.get? a.data i
@[simp]
theorem
Array.getD_eq_get?
{α : Type u_1}
(a : Array α)
(n : Nat)
(d : α)
:
Array.getD a n d = Option.getD (Array.get? a n) d
theorem
Array.get!_eq_getD
{α : Type u_1}
{n : Nat}
[Inhabited α]
(a : Array α)
:
Array.get! a n = Array.getD a n default
@[simp]
theorem
Array.get!_eq_get?
{α : Type u_1}
{n : Nat}
[Inhabited α]
(a : Array α)
:
Array.get! a n = Option.getD (Array.get? a n) default
@[simp]
theorem
Array.back_eq_back?
{α : Type u_1}
[Inhabited α]
(a : Array α)
:
Array.back a = Option.getD (Array.back? a) default
@[simp]
theorem
Array.back?_push
{α : Type u_1}
{x : α}
(a : Array α)
:
Array.back? (Array.push a x) = some x
theorem
Array.back_push
{α : Type u_1}
{x : α}
[Inhabited α]
(a : Array α)
:
Array.back (Array.push a x) = x
theorem
Array.get?_push_lt
{α : Type u_1}
(a : Array α)
(x : α)
(i : Nat)
(h : i < Array.size a)
:
(Array.push a x)[i]? = some a[i]
theorem
Array.get?_push_eq
{α : Type u_1}
(a : Array α)
(x : α)
:
(Array.push a x)[Array.size a]? = some x
@[simp]
@[simp]
@[simp]
theorem
Array.get_set_ne
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
{j : Nat}
(v : α)
(hj : j < Array.size a)
(h : ↑i ≠ j)
:
@[simp]
@[simp]
theorem
Array.get?_set_ne
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
{j : Nat}
(v : α)
(h : ↑i ≠ j)
:
theorem
Array.get_set
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
(j : Nat)
(hj : j < Array.size a)
(v : α)
:
theorem
Array.swap_def
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
(j : Fin (Array.size a))
:
Array.swap a i j = Array.set (Array.set a i (Array.get a j)) { val := ↑j, isLt := (_ : ↑j < Array.size (Array.set a i a[↑j])) }
(Array.get a i)
theorem
Array.data_swap
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
(j : Fin (Array.size a))
:
theorem
Array.get?_swap
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
(j : Fin (Array.size a))
(k : Nat)
:
@[simp]
theorem
Array.swapAt_def
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
(v : α)
:
Array.swapAt a i v = (a[↑i], Array.set a i v)
theorem
Array.swapAt!_def
{α : Type u_1}
(a : Array α)
(i : Nat)
(v : α)
(h : i < Array.size a)
:
Array.swapAt! a i v = (a[i], Array.set a { val := i, isLt := h } v)
@[simp]
@[simp]
@[simp]
theorem
Array.getElem_pop
{α : Type u_1}
(a : Array α)
(i : Nat)
(hi : i < Array.size (Array.pop a))
:
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) b → SatisfiesM (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) b → SatisfiesM (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.foldr_induction
{α : Type u_1}
{β : Type u_2}
{as : Array α}
(motive : Nat → β → Prop)
{init : β}
(h0 : motive (Array.size as) init)
{f : α → β → β}
(hf : ∀ (i : Fin (Array.size as)) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b))
:
motive 0 (Array.foldr f init as (Array.size as))
theorem
Array.mapM_eq_mapM_data
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → m β)
(arr : Array α)
:
Array.mapM f arr = do
let __do_lift ← List.mapM f arr.data
pure { data := __do_lift }
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 : 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 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 : Nat → Prop)
(p : Fin (Array.size as) → β → Prop)
(hs : ∀ (i : Fin (Array.size as)), motive ↑i → SatisfiesM (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.mapIdx_induction
{α : Type u_1}
{β : Type u_2}
(as : Array α)
(f : Fin (Array.size as) → α → β)
(motive : Nat → Prop)
(h0 : motive 0)
(p : Fin (Array.size as) → β → Prop)
(hs : ∀ (i : Fin (Array.size as)), motive ↑i → p i (f i as[i]) ∧ motive (↑i + 1))
:
motive (Array.size as) ∧ ∃ (eq : Array.size (Array.mapIdx as f) = Array.size as),
∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.mapIdx as f)[i]
theorem
Array.mapIdx_induction'
{α : Type u_1}
{β : Type u_2}
(as : Array α)
(f : Fin (Array.size as) → α → β)
(p : Fin (Array.size as) → β → Prop)
(hs : ∀ (i : Fin (Array.size as)), p i (f i as[i]))
:
∃ (eq : Array.size (Array.mapIdx as f) = Array.size as),
∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.mapIdx as f)[i]
@[simp]
theorem
Array.size_mapIdx
{α : Type u_1}
{β : Type u_2}
(a : Array α)
(f : Fin (Array.size a) → α → β)
:
Array.size (Array.mapIdx a f) = Array.size a
@[simp]
theorem
Array.getElem_mapIdx
{α : Type u_1}
{β : Type u_2}
(a : Array α)
(f : Fin (Array.size a) → α → β)
(i : Nat)
(h : i < Array.size (Array.mapIdx a f))
:
(Array.mapIdx a f)[i] = f { val := i, isLt := (_ : i < Array.size a) } a[i]
@[simp]
theorem
Array.size_swap!
{α : Type u_1}
(a : Array α)
(i : Nat)
(j : Nat)
(hi : i < Array.size a)
(hj : j < Array.size a)
:
Array.size (Array.swap! a i j) = Array.size a
@[simp]
theorem
Array.size_reverse
{α : Type u_1}
(a : Array α)
:
Array.size (Array.reverse a) = Array.size a
theorem
Array.size_reverse.go
{α : Type u_1}
(as : Array α)
(i : Nat)
(j : Fin (Array.size as))
:
Array.size (Array.reverse.loop as i j) = Array.size as
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)
@[simp]
theorem
Array.size_modify
{α : Type u_1}
(a : Array α)
(i : Nat)
(f : α → α)
:
Array.size (Array.modify a i f) = Array.size a
@[simp]
theorem
Array.reverse_data
{α : Type u_1}
(a : Array α)
:
(Array.reverse a).data = List.reverse a.data
theorem
Array.reverse_data.go
{α : Type u_1}
(a : Array α)
(as : Array α)
(i : Nat)
(j : Nat)
(hj : j < Array.size as)
(h : i + j + 1 = Array.size a)
(h₂ : Array.size as = Array.size a)
(H : ∀ (k : Nat), List.get? as.data k = if i ≤ k ∧ k ≤ j then List.get? a.data k else List.get? (List.reverse a.data) k)
(k : Nat)
:
List.get? (Array.reverse.loop as i { val := j, isLt := hj }).data k = List.get? (List.reverse a.data) k
@[simp]
theorem
Array.size_ofFn_go
{α : Type u_1}
{n : Nat}
(f : Fin n → α)
(i : Nat)
(acc : Array α)
:
Array.size (Array.ofFn.go f i acc) = Array.size acc + (n - i)
@[simp]
theorem
Array.getElem_ofFn_go
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
(i : Nat)
{acc : Array α}
{k : Nat}
(hki : k < n)
(hin : i ≤ n)
(hi : i = Array.size acc)
(hacc : ∀ (j : Nat) (hj : j < Array.size acc), acc[j] = f { val := j, isLt := (_ : j < n) })
:
(Array.ofFn.go f i acc)[k] = f { val := k, isLt := hki }
@[simp]
theorem
Array.getElem_ofFn
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
(i : Nat)
(h : i < Array.size (Array.ofFn f))
:
(Array.ofFn f)[i] = f { val := i, isLt := (_ : i < n) }
theorem
Array.forIn_eq_data_forIn.loop
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(as : Array α)
(f : α → β → m (ForInStep β))
{i : Nat}
{h : i ≤ Array.size as}
{b : β}
{j : Nat}
:
j + i = Array.size as → Array.forIn.loop as f i h b = forIn (List.drop j as.data) b f
join #
@[simp]
theorem
Array.join_data
{α : Type u_1}
{l : Array (Array α)}
:
(Array.join l).data = List.join (List.map Array.data l.data)
append #
all #
theorem
Array.all_eq_true
{α : Type u_1}
(p : α → Bool)
(as : Array α)
:
Array.all as p 0 (Array.size as) = true ↔ ∀ (i : Fin (Array.size as)), p as[i] = true
theorem
Array.all_def
{α : Type u_1}
{p : α → Bool}
(as : Array α)
:
Array.all as p 0 (Array.size as) = List.all as.data p