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
mk lemmas #
@[simp]
theorem
Batteries.Vector.indexOf?_mk
{α : Type u_1}
{n : Nat}
[BEq α]
(a : Array α)
(h : a.size = n)
(x : α)
:
{ toArray := a, size_toArray := h }.indexOf? x = Option.map (Fin.cast h) (a.indexOf? x)
@[simp]
theorem
Batteries.Vector.map_mk
{α : Type u_1}
{n : Nat}
{β : Type u_2}
(a : Array α)
(h : a.size = n)
(f : α → β)
:
Batteries.Vector.map f { toArray := a, size_toArray := h } = { toArray := Array.map f a, size_toArray := ⋯ }
@[simp]
theorem
Batteries.Vector.push_mk
{α : Type u_1}
{n : Nat}
(a : Array α)
(h : a.size = n)
(x : α)
:
Batteries.Vector.push x { toArray := a, size_toArray := h } = { toArray := a.push x, size_toArray := ⋯ }
@[simp]
theorem
Batteries.Vector.mk_zipWith_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{n : Nat}
(f : α → β → γ)
(a : Array α)
(b : Array β)
(ha : a.size = n)
(hb : b.size = n)
:
{ toArray := a, size_toArray := ha }.zipWith { toArray := b, size_toArray := hb } f = { toArray := a.zipWith b f, size_toArray := ⋯ }
@[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]
toArray lemmas #
@[simp]
theorem
Batteries.Vector.toArray_append
{α : Type u_1}
{m n : Nat}
(a : Batteries.Vector α m)
(b : Batteries.Vector α n)
:
@[simp]
theorem
Batteries.Vector.toArray_drop
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(m : Nat)
:
(a.drop m).toArray = a.extract m a.size
@[simp]
@[simp]
theorem
Batteries.Vector.toArray_mkEmpty
{α : Type u_1}
(cap : Nat)
:
(Batteries.Vector.mkEmpty cap).toArray = Array.mkEmpty cap
@[simp]
theorem
Batteries.Vector.toArray_eraseIdx!
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(hi : i < n)
:
(a.eraseIdx! i).toArray = a.eraseIdx! i
@[simp]
theorem
Batteries.Vector.toArray_eraseIdxN
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(hi : i < n)
:
(a.eraseIdxN i hi).toArray = a.eraseIdxN i ⋯
@[simp]
theorem
Batteries.Vector.toArray_feraseIdx
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Fin n)
:
@[simp]
theorem
Batteries.Vector.toArray_extract
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(start stop : Nat)
:
(a.extract start stop).toArray = a.extract start stop
@[simp]
theorem
Batteries.Vector.toArray_map
{α : Type u_1}
{β : Type u_2}
{n : Nat}
(f : α → β)
(a : Batteries.Vector α n)
:
(Batteries.Vector.map f a).toArray = Array.map f a.toArray
@[simp]
theorem
Batteries.Vector.toArray_ofFn
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
:
(Batteries.Vector.ofFn f).toArray = Array.ofFn f
@[simp]
theorem
Batteries.Vector.toArray_pop
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
:
a.pop.toArray = a.pop
@[simp]
theorem
Batteries.Vector.toArray_push
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(x : α)
:
(Batteries.Vector.push x a).toArray = a.push x
@[simp]
theorem
Batteries.Vector.toArray_range
{n : Nat}
:
(Batteries.Vector.range n).toArray = Array.range n
@[simp]
theorem
Batteries.Vector.toArray_reverse
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
:
a.reverse.toArray = a.reverse
@[simp]
theorem
Batteries.Vector.toArray_set
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Fin n)
(x : α)
:
@[simp]
theorem
Batteries.Vector.toArray_set!
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(x : α)
:
(a.set! i x).toArray = a.set! i x
@[simp]
theorem
Batteries.Vector.toArray_setD
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(x : α)
:
(a.setD i x).toArray = a.setD i x
@[simp]
theorem
Batteries.Vector.toArray_setN
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(x : α)
(hi : i < n)
:
(a.setN i x hi).toArray = a.setN i x ⋯
@[simp]
theorem
Batteries.Vector.toArray_singleton
{α : Type u_1}
(x : α)
:
(Batteries.Vector.singleton x).toArray = #[x]
@[simp]
theorem
Batteries.Vector.toArray_swap
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i j : Fin n)
:
@[simp]
theorem
Batteries.Vector.toArray_swap!
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i j : Nat)
:
(a.swap! i j).toArray = a.swap! i j
@[simp]
theorem
Batteries.Vector.toArray_swapN
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i j : Nat)
(hi : i < n)
(hj : j < n)
:
(a.swapN i j hi hj).toArray = a.swapN i j ⋯ ⋯
@[simp]
theorem
Batteries.Vector.toArray_swapAt
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Fin n)
(x : α)
:
@[simp]
theorem
Batteries.Vector.toArray_swapAt!
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(x : α)
:
((a.swapAt! i x).fst, (a.swapAt! i x).snd.toArray) = ((a.swapAt! i x).fst, (a.swapAt! i x).snd)
@[simp]
theorem
Batteries.Vector.toArray_swapAtN
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(i : Nat)
(x : α)
(hi : i < n)
:
((a.swapAtN i x hi).fst, (a.swapAtN i x hi).snd.toArray) = ((a.swapAtN i x ⋯).fst, (a.swapAtN i x ⋯).snd)
@[simp]
theorem
Batteries.Vector.toArray_take
{α : Type u_1}
{n : Nat}
(a : Batteries.Vector α n)
(m : Nat)
:
(a.take m).toArray = a.take m
@[simp]
theorem
Batteries.Vector.toArray_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{n : Nat}
(f : α → β → γ)
(a : Batteries.Vector α n)
(b : Batteries.Vector β n)
:
(a.zipWith b f).toArray = a.zipWith b.toArray f
toList lemmas #
theorem
Batteries.Vector.length_toList
{α : Type u_1}
{n : Nat}
(xs : Batteries.Vector α n)
:
xs.toList.length = n
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]
getElem lemmas #
@[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.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
empty lemmas #
@[simp]
theorem
Batteries.Vector.map_empty
{α : Type u_1}
{β : Type u_2}
(f : α → β)
:
Batteries.Vector.map f Batteries.Vector.empty = Batteries.Vector.empty
theorem
Batteries.Vector.eq_empty
{α : Type u_1}
(v : Batteries.Vector α 0)
:
v = Batteries.Vector.empty
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) ⋯