@[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.val ≠ j)
:
@[simp]
@[simp]
theorem
Array.get?_set_ne
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
{j : Nat}
(v : α)
(h : i.val ≠ 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.val, isLt := (_ : j.val < Array.size (Array.set a i a[j.val])) }
(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.val], 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]
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.val + 1) b → SatisfiesM (motive i.val) (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.val + 1) b → SatisfiesM (motive i.val) (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.val + 1) b → motive i.val (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.val → SatisfiesM (fun x => p i x ∧ motive (i.val + 1)) (f i as[i]))
:
SatisfiesM
(fun arr => motive (Array.size as) ∧ ∃ eq, (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.val → SatisfiesM (fun x => p i x ∧ motive (i.val + 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 => motive (Array.size as) ∧ ∃ eq, (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.val → p i (f i as[i]) ∧ motive (i.val + 1))
:
motive (Array.size as) ∧ ∃ eq, (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, (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
@[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) }