data.array.lemmas - mathlib3 docs

source

@[protected, instance]

def d_array.inhabited {n : ℕ} {α : fin n → Type u} [Π (i : fin n), inhabited (α i)] :

inhabited (d_array n α)

Equations

d_array.inhabited = {default := {data := inhabited.default (pi.inhabited (fin n))}}

source

@[protected, instance]

def array.inhabited {n : ℕ} {α : Type u_1} [inhabited α] :

inhabited (array n α)

Equations

array.inhabited = d_array.inhabited

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 = option.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)