Vectors #
Lemmas about Vector α n
theorem
Batteries.Vector.length_toList
{α : Type u_1}
{n : Nat}
(xs : Batteries.Vector α n)
:
xs.toList.length = n
@[simp]
theorem
Batteries.Vector.getElem_toArray
{α : Type u_1}
{n : Nat}
(xs : Batteries.Vector α n)
(i : Nat)
(h : i < xs.size)
:
xs.toArray[i] = xs[i]
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]
@[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⟩
@[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.
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.
theorem
Batteries.Vector.ext
{α : Type u_1}
{n : Nat}
{a 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.
@[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_toArray := size } = { toArray := data.push x, size_toArray := ⋯ }
@[simp]
theorem
Batteries.Vector.getElem_push_last
{α : Type u_1}
{n : Nat}
{v : Batteries.Vector α n}
{x : α}
:
(Batteries.Vector.push x v)[n] = x
@[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]
@[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]
@[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.
@[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. #
theorem
Batteries.Vector.forall_zero_iff
{α : Type u_1}
{P : Batteries.Vector α 0 → Prop}
:
(∀ (v : Batteries.Vector α 0), P v) ↔ P Batteries.Vector.empty
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)
instance
Batteries.Vector.instDecidableForallVectorZero
{α : Type u_1}
(P : Batteries.Vector α 0 → Prop)
[Decidable (P Batteries.Vector.empty)]
:
Decidable (∀ (v : Batteries.Vector α 0), P v)
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
- Batteries.Vector.instDecidableForallVectorSucc P = decidable_of_iff' (∀ (x : α) (v : Batteries.Vector α n), P (Batteries.Vector.push x v)) ⋯
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
- Batteries.Vector.instDecidableExistsVectorZero P = decidable_of_iff (¬∀ (v : Batteries.Vector α 0), ¬P v) ⋯
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
- Batteries.Vector.instDecidableExistsVectorSucc P = decidable_of_iff (¬∀ (v : Batteries.Vector α (n + 1)), ¬P v) ⋯