Vectors #
Lemmas about Vector α n
@[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.toArray_injective
{α : Type u_1}
{n : Nat}
{v : Batteries.Vector α n}
{w : Batteries.Vector α n}
:
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_iff
{α : Type u_1}
{n : Nat}
{a : Batteries.Vector α n}
{b : Batteries.Vector α n}
:
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.
@[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 := ⋯ }
@[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) ⋯