Documentation

Batteries.Data.Vector.Lemmas

Vectors #

Lemmas about Vector α n

source
@[simp]
theorem Batteries.Vector.length_toList {α : Type u_1} {n : Nat} (xs : Batteries.Vector α n) :
xs.toList.length = n
source
@[simp]
theorem Batteries.Vector.getElem_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
{ toArray := data, size_eq := size }[i] = data[i]
source
@[simp]
theorem Batteries.Vector.getElem_toArray {α : Type u_1} {n : Nat} (xs : Batteries.Vector α n) (i : Nat) (h : i < xs.toArray.size) :
xs.toArray[i] = xs[i]
source
@[simp]
theorem Batteries.Vector.getElem_toList {α : Type u_1} {n : Nat} (xs : Batteries.Vector α n) (i : Nat) (h : i < xs.toList.length) :
xs.toList[i] = xs[i]
source
@[simp]
theorem Batteries.Vector.getElem_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (h : i < n) :
(Batteries.Vector.ofFn f)[i] = f ⟨i, h⟩
source
@[simp]
theorem Batteries.Vector.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) :
Batteries.Vector.map f Batteries.Vector.empty = Batteries.Vector.empty

An empty vector maps to a empty vector.

source
theorem Batteries.Vector.toArray_injective {α : Type u_1} {n : Nat} {v : Batteries.Vector α n} {w : Batteries.Vector α n} :
v.toArray = w.toArray → v = w
source
theorem Batteries.Vector.eq_empty {α : Type u_1} (v : Batteries.Vector α 0) :
v = Batteries.Vector.empty

A vector of length 0 is an empty vector.

source
theorem Batteries.Vector.ext {α : Type u_1} {n : Nat} {a : Batteries.Vector α n} {b : Batteries.Vector α n} (h : ∀ (i : Nat) (x : i < n), a[i] = b[i]) :
a = b

Vector.ext is an extensionality theorem. Vectors a and b are equal to each other if their elements are equal for each valid index.

source
@[simp]
theorem Batteries.Vector.push_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} {x : α} :
Batteries.Vector.push x { toArray := data, size_eq := size } = { toArray := data.push x, size_eq := ⋯ }
source
@[simp]
theorem Batteries.Vector.pop_mk {α : Type u_1} {n : Nat} {data : Array α} {size : data.size = n} :
{ toArray := data, size_eq := size }.pop = { toArray := data.pop, size_eq := ⋯ }
source
@[simp]
theorem Batteries.Vector.getElem_push_last {α : Type u_1} {n : Nat} {v : Batteries.Vector α n} {x : α} :
(Batteries.Vector.push x v)[n] = x
source
@[simp]
theorem Batteries.Vector.getElem_push_lt {α : Type u_1} {n : Nat} {v : Batteries.Vector α n} {x : α} {i : Nat} (h : i < n) :
(Batteries.Vector.push x v)[i] = v[i]
source
@[simp]
theorem Batteries.Vector.getElem_pop {α : Type u_1} {n : Nat} {v : Batteries.Vector α n} {i : Nat} (h : i < n - 1) :
v.pop[i] = v[i]
source
@[simp]
theorem Batteries.Vector.getElem_pop' {α : Type u_1} {n : Nat} (v : Batteries.Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
v.pop[i] = v[i]

Variant of getElem_pop that will sometimes fire when getElem_pop gets stuck because of defeq issues in the implicit size argument.

source
@[simp]
theorem Batteries.Vector.push_pop_back {α : Type u_1} {n : Nat} (v : Batteries.Vector α (n + 1)) :
Batteries.Vector.push v.back v.pop = v

Decidable quantifiers. #

source
theorem Batteries.Vector.forall_zero_iff {α : Type u_1} {P : Batteries.Vector α 0 → Prop} :
(∀ (v : Batteries.Vector α 0), P v) ↔ P Batteries.Vector.empty
source
theorem Batteries.Vector.forall_cons_iff {α : Type u_1} {n : Nat} {P : Batteries.Vector α (n + 1) → Prop} :
(∀ (v : Batteries.Vector α (n + 1)), P v) ↔ ∀ (x : α) (v : Batteries.Vector α n), P (Batteries.Vector.push x v)
source
instance Batteries.Vector.instDecidableForallVectorZero {α : Type u_1} (P : Batteries.Vector α 0 → Prop) [Decidable (P Batteries.Vector.empty)] :
Decidable (∀ (v : Batteries.Vector α 0), P v)
Equations
source
instance Batteries.Vector.instDecidableForallVectorSucc {α : Type u_1} {n : Nat} (P : Batteries.Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (v : Batteries.Vector α n), P (Batteries.Vector.push x v))] :
Decidable (∀ (v : Batteries.Vector α (n + 1)), P v)
Equations
source
instance Batteries.Vector.instDecidableExistsVectorZero {α : Type u_1} (P : Batteries.Vector α 0 → Prop) [Decidable (P Batteries.Vector.empty)] :
Decidable (∃ (v : Batteries.Vector α 0), P v)
Equations
source
instance Batteries.Vector.instDecidableExistsVectorSucc {α : Type u_1} {n : Nat} (P : Batteries.Vector α (n + 1) → Prop) [Decidable (∀ (x : α) (v : Batteries.Vector α n), ¬P (Batteries.Vector.push x v))] :
Decidable (∃ (v : Batteries.Vector α (n + 1)), P v)
Equations