mathlib documentation

data.array.lemmas

source
@[protected, instance]
def d_array.inhabited {n : ℕ} {α : fin n → Type u} [Π (i : fin n), inhabited (α i)] :
inhabited (d_array n α)
Equations
source
@[protected, instance]
def array.inhabited {n : ℕ} {α : Type u_1} [inhabited α] :
inhabited (array n α)
Equations
source
theorem array.to_list_of_heq {n₁ n₂ : ℕ} {α : Type u_1} {a₁ : array n₁ α} {a₂ : array n₂ α} (hn : n₁ = n₂) (ha : a₁ == a₂) :
a₁.to_list = a₂.to_list
source
theorem array.rev_list_reverse_aux {n : ℕ} {α : Type u} {a : array n α} (i : ℕ) (h : i ≤ n) (t : list α) :
(d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil).reverse_core t = d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h t
source
@[simp]
theorem array.rev_list_reverse {n : ℕ} {α : Type u} {a : array n α} :
a.rev_list.reverse = a.to_list
source
@[simp]
theorem array.to_list_reverse {n : ℕ} {α : Type u} {a : array n α} :
a.to_list.reverse = a.rev_list
source
theorem array.mem.def {n : ℕ} {α : Type u} {v : α} {a : array n α} :
v ∈ a ↔ ∃ (i : fin n), a.read i = v
source
theorem array.mem_rev_list_aux {n : ℕ} {α : Type u} {v : α} {a : array n α} {i : ℕ} (h : i ≤ n) :
(∃ (j : fin n), ↑j < i ∧ a.read j = v) ↔ v ∈ d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil
source
@[simp]
theorem array.mem_rev_list {n : ℕ} {α : Type u} {v : α} {a : array n α} :
v ∈ a.rev_list ↔ v ∈ a
source
@[simp]
theorem array.mem_to_list {n : ℕ} {α : Type u} {v : α} {a : array n α} :
v ∈ a.to_list ↔ v ∈ a
source
theorem array.rev_list_foldr_aux {n : ℕ} {α : Type u} {β : Type w} {b : β} {f : α → β → β} {a : array n α} {i : ℕ} (h : i ≤ n) :
list.foldr f b (d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil) = d_array.iterate_aux a (λ (_x : fin n), f) i h b
source
theorem array.rev_list_foldr {n : ℕ} {α : Type u} {β : Type w} {b : β} {f : α → β → β} {a : array n α} :
list.foldr f b a.rev_list = a.foldl b f
source
theorem array.to_list_foldl {n : ℕ} {α : Type u} {β : Type w} {b : β} {f : β → α → β} {a : array n α} :
list.foldl f b a.to_list = a.foldl b (function.swap f)
source
theorem array.rev_list_length_aux {n : ℕ} {α : Type u} (a : array n α) (i : ℕ) (h : i ≤ n) :
(d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h list.nil).length = i
source
@[simp]
theorem array.rev_list_length {n : ℕ} {α : Type u} (a : array n α) :
a.rev_list.length = n
source
@[simp]
theorem array.to_list_length {n : ℕ} {α : Type u} (a : array n α) :
a.to_list.length = n
source
theorem array.to_list_nth_le_aux {n : ℕ} {α : Type u} {a : array n α} (i : ℕ) (ih : i < n) (j : ℕ) {jh : j ≤ n} {t : list α} {h' : i < (d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) j jh t).length} :
(∀ (k : ℕ) (tl : k < t.length), j + k = i → t.nth_le k tl = a.read ⟨i, ih⟩) → (d_array.rev_iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) j jh t).nth_le i h' = a.read ⟨i, ih⟩
source
theorem array.to_list_nth_le {n : ℕ} {α : Type u} {a : array n α} (i : ℕ) (h : i < n) (h' : i < a.to_list.length) :
a.to_list.nth_le i h' = a.read ⟨i, h⟩
source
@[simp]
theorem array.to_list_nth_le' {n : ℕ} {α : Type u} (a : array n α) (i : fin n) (h' : ↑i < a.to_list.length) :
a.to_list.nth_le ↑i h' = a.read i
source
theorem array.to_list_nth {n : ℕ} {α : Type u} {a : array n α} {i : ℕ} {v : α} :
a.to_list.nth i = some v ↔ ∃ (h : i < n), a.read ⟨i, h⟩ = v
source
theorem array.write_to_list {n : ℕ} {α : Type u} {a : array n α} {i : fin n} {v : α} :
(a.write i v).to_list = a.to_list.update_nth ↑i v
source
theorem array.mem_to_list_enum {n : ℕ} {α : Type u} {a : array n α} {i : ℕ} {v : α} :
(i, v) ∈ a.to_list.enum ↔ ∃ (h : i < n), a.read ⟨i, h⟩ = v
source
@[simp]
theorem array.to_list_to_array {n : ℕ} {α : Type u} (a : array n α) :
a.to_list.to_array == a
source
@[simp]
theorem array.to_array_to_list {α : Type u} (l : list α) :
l.to_array.to_list = l
source
theorem array.push_back_rev_list_aux {n : ℕ} {α : Type u} {v : α} {a : array n α} (i : ℕ) (h : i ≤ n + 1) (h' : i ≤ n) :
d_array.iterate_aux (a.push_back v) (λ (_x : fin (n + 1)), λ (_x : α) (_y : list α), _x :: _y) i h list.nil = d_array.iterate_aux a (λ (_x : fin n), λ (_x : α) (_y : list α), _x :: _y) i h' list.nil
source
@[simp]
theorem array.push_back_rev_list {n : ℕ} {α : Type u} {v : α} {a : array n α} :
(a.push_back v).rev_list = v :: a.rev_list
source
@[simp]
theorem array.push_back_to_list {n : ℕ} {α : Type u} {v : α} {a : array n α} :
(a.push_back v).to_list = a.to_list ++ [v]
source
@[simp]
theorem array.read_push_back_left {n : ℕ} {α : Type u} {v : α} {a : array n α} (i : fin n) :
(a.push_back v).read (⇑fin.cast_succ i) = a.read i
source
@[simp]
theorem array.read_push_back_right {n : ℕ} {α : Type u} {v : α} {a : array n α} :
(a.push_back v).read (fin.last n) = v
source
@[simp]
theorem array.read_foreach {n : ℕ} {α : Type u} {β : Type v} {i : fin n} {f : fin n → α → β} {a : array n α} :
(a.foreach f).read i = f i (a.read i)
source
theorem array.read_map {n : ℕ} {α : Type u} {β : Type v} {i : fin n} {f : α → β} {a : array n α} :
(a.map f).read i = f (a.read i)
source
@[simp]
theorem array.read_map₂ {n : ℕ} {α : Type u} {i : fin n} {f : α → α → α} {a₁ a₂ : array n α} :
(array.map₂ f a₁ a₂).read i = f (a₁.read i) (a₂.read i)
source
def equiv.d_array_equiv_fin {n : ℕ} (α : fin n → Type u_1) :
d_array n α ≃ Π (i : fin n), α i

The natural equivalence between length-n heterogeneous arrays and dependent functions from fin n.

Equations
source
def equiv.array_equiv_fin (n : ℕ) (α : Type u_1) :
array n α ≃ (fin n → α)

The natural equivalence between length-n arrays and functions from fin n.

Equations
source
def equiv.vector_equiv_array (α : Type u_1) (n : ℕ) :
vector α n ≃ array n α

The natural equivalence between length-n vectors and length-n arrays.

Equations
source
@[protected, instance]
def array.traversable {n : ℕ} :
traversable (array n)
Equations
source
@[protected, instance]
def array.is_lawful_traversable {n : ℕ} :
is_lawful_traversable (array n)
Equations