Documentation

Batteries.Data.Vector.Lemmas

theorem Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Vector α n} :
v.toArray = w.toArrayv = w
theorem Vector.ext {α : Type u_1} {n : Nat} {a b : Vector α n} (h : ∀ (i : Nat) (x : i < n), a[i] = b[i]) :
a = b

mk lemmas #

theorem Vector.toArray_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.toArray = a
@[simp]
theorem Vector.allDiff_mk {α : Type u_1} {n : Nat} [BEq α] (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.allDiff = a.allDiff
@[simp]
theorem Vector.mk_append_mk {α : Type u_1} {n m : Nat} (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
{ toArray := a, size_toArray := ha } ++ { toArray := b, size_toArray := hb } = { toArray := a ++ b, size_toArray := }
@[simp]
theorem Vector.back!_mk {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.back! = a.back!
@[simp]
theorem Vector.back?_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.back? = a.back?
@[simp]
theorem Vector.drop_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) :
{ toArray := a, size_toArray := h }.drop m = { toArray := a.extract m a.size, size_toArray := }
@[simp]
theorem Vector.eraseIdx_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (h' : i < n) :
{ toArray := a, size_toArray := h }.eraseIdx i h' = { toArray := a.eraseIdx i , size_toArray := }
@[simp]
theorem Vector.eraseIdx!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (hi : i < n) :
{ toArray := a, size_toArray := h }.eraseIdx! i = { toArray := a.eraseIdx i , size_toArray := }
@[simp]
theorem Vector.extract_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (start stop : Nat) :
{ toArray := a, size_toArray := h }.extract start stop = { toArray := a.extract start stop, size_toArray := }
@[simp]
theorem Vector.getElem_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (hi : i < n) :
{ toArray := a, size_toArray := h }[i] = a[i]
@[simp]
theorem Vector.get_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) :
{ toArray := a, size_toArray := h }.get i = a[i]
@[simp]
theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) :
{ toArray := a, size_toArray := h }.getD i x = a.getD i x
@[simp]
theorem Vector.uget_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n) :
{ toArray := a, size_toArray := h }.uget i hi = a.uget i
@[simp]
theorem 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 Vector.mk_isEqv_mk {α : Type u_1} {n : Nat} (r : ααBool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
{ toArray := a, size_toArray := ha }.isEqv { toArray := b, size_toArray := hb } r = a.isEqv b r
@[simp]
theorem Vector.mk_isPrefixOf_mk {α : Type u_1} {n m : Nat} [BEq α] (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
{ toArray := a, size_toArray := ha }.isPrefixOf { toArray := b, size_toArray := hb } = a.isPrefixOf b
@[simp]
theorem Vector.map_mk {α : Type u_1} {n : Nat} {β : Type u_2} (a : Array α) (h : a.size = n) (f : αβ) :
Vector.map f { toArray := a, size_toArray := h } = { toArray := Array.map f a, size_toArray := }
@[simp]
theorem Vector.pop_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.pop = { toArray := a.pop, size_toArray := }
@[simp]
theorem Vector.push_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (x : α) :
Vector.push x { toArray := a, size_toArray := h } = { toArray := a.push x, size_toArray := }
@[simp]
theorem Vector.reverse_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.reverse = { toArray := a.reverse, size_toArray := }
@[simp]
theorem Vector.set_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (w : i < n) :
{ toArray := a, size_toArray := h }.set i x w = { toArray := a.set i x , size_toArray := }
@[simp]
theorem Vector.set!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) :
{ toArray := a, size_toArray := h }.set! i x = { toArray := a.set! i x, size_toArray := }
@[simp]
theorem Vector.setIfInBounds_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) :
{ toArray := a, size_toArray := h }.setIfInBounds i x = { toArray := a.setIfInBounds i x, size_toArray := }
@[deprecated Vector.set_mk]
theorem Vector.setN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (w : i < n) :
{ toArray := a, size_toArray := h }.set i x w = { toArray := a.set i x , size_toArray := }

Alias of Vector.set_mk.

@[simp]
theorem Vector.swap_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : j < n) (hj : i < n) :
{ toArray := a, size_toArray := h }.swap i j hj hi = { toArray := a.swap i j , size_toArray := }
@[simp]
theorem Vector.swapIfInBounds_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) :
{ toArray := a, size_toArray := h }.swapIfInBounds i j = { toArray := a.swapIfInBounds i j, size_toArray := }
@[deprecated Vector.swap_mk]
theorem Vector.swapN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : j < n) (hj : i < n) :
{ toArray := a, size_toArray := h }.swap i j hj hi = { toArray := a.swap i j , size_toArray := }

Alias of Vector.swap_mk.

@[simp]
theorem Vector.swapAt_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) :
{ toArray := a, size_toArray := h }.swapAt i x hi = ((a.swapAt i x ).fst, { toArray := (a.swapAt i x ).snd, size_toArray := })
@[simp]
theorem Vector.swapAt!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) :
{ toArray := a, size_toArray := h }.swapAt! i x = ((a.swapAt! i x).fst, { toArray := (a.swapAt! i x).snd, size_toArray := })
@[deprecated Vector.swapAt_mk]
theorem Vector.swapAtN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) :
{ toArray := a, size_toArray := h }.swapAt i x hi = ((a.swapAt i x ).fst, { toArray := (a.swapAt i x ).snd, size_toArray := })

Alias of Vector.swapAt_mk.

@[simp]
theorem Vector.take_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (m : Nat) :
{ toArray := a, size_toArray := h }.take m = { toArray := a.take m, size_toArray := }
@[simp]
theorem 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 Vector.getElem_toArray {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < xs.size) :
xs.toArray[i] = xs[i]

toArray lemmas #

@[simp]
theorem Vector.toArray_append {α : Type u_1} {m n : Nat} (a : Vector α m) (b : Vector α n) :
(a ++ b).toArray = a.toArray ++ b.toArray
@[simp]
theorem Vector.toArray_drop {α : Type u_1} {n : Nat} (a : Vector α n) (m : Nat) :
(a.drop m).toArray = a.extract m a.size
@[simp]
theorem Vector.toArray_empty {α : Type u_1} :
{ toArray := #[], size_toArray := }.toArray = #[]
@[simp]
theorem Vector.toArray_mkEmpty {α : Type u_1} (cap : Nat) :
(Vector.mkEmpty cap).toArray = Array.mkEmpty cap
@[simp]
theorem Vector.toArray_eraseIdx {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (h : i < n) :
(a.eraseIdx i h).toArray = a.eraseIdx i
@[simp]
theorem Vector.toArray_eraseIdx! {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (hi : i < n) :
(a.eraseIdx! i).toArray = a.eraseIdx! i
@[simp]
theorem Vector.toArray_extract {α : Type u_1} {n : Nat} (a : Vector α n) (start stop : Nat) :
(a.extract start stop).toArray = a.extract start stop
@[simp]
theorem Vector.toArray_map {α : Type u_1} {β : Type u_2} {n : Nat} (f : αβ) (a : Vector α n) :
(Vector.map f a).toArray = Array.map f a.toArray
@[simp]
theorem Vector.toArray_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) :
(Vector.ofFn f).toArray = Array.ofFn f
@[simp]
theorem Vector.toArray_pop {α : Type u_1} {n : Nat} (a : Vector α n) :
a.pop.toArray = a.pop
@[simp]
theorem Vector.toArray_push {α : Type u_1} {n : Nat} (a : Vector α n) (x : α) :
(Vector.push x a).toArray = a.push x
@[simp]
theorem Vector.toArray_range {n : Nat} :
(Vector.range n).toArray = Array.range n
@[simp]
theorem Vector.toArray_reverse {α : Type u_1} {n : Nat} (a : Vector α n) :
a.reverse.toArray = a.reverse
@[simp]
theorem Vector.toArray_set {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) :
(a.set i x h).toArray = a.set i x
@[simp]
theorem Vector.toArray_set! {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) :
(a.set! i x).toArray = a.set! i x
@[simp]
theorem Vector.toArray_setIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) :
(a.setIfInBounds i x).toArray = a.setIfInBounds i x
@[deprecated Vector.toArray_setIfInBounds]
theorem Vector.toArray_setD {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) :
(a.setIfInBounds i x).toArray = a.setIfInBounds i x

Alias of Vector.toArray_setIfInBounds.

@[deprecated Vector.toArray_set]
theorem Vector.toArray_setN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) :
(a.set i x h).toArray = a.set i x

Alias of Vector.toArray_set.

@[simp]
theorem Vector.toArray_singleton {α : Type u_1} (x : α) :
(Vector.singleton x).toArray = #[x]
@[simp]
theorem Vector.toArray_swap {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) :
(a.swap i j hj hi).toArray = a.swap i j
@[simp]
theorem Vector.toArray_swapIfInBounds {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) :
(a.swapIfInBounds i j).toArray = a.swapIfInBounds i j
@[deprecated Vector.toArray_swapIfInBounds]
theorem Vector.toArray_swap! {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) :
(a.swapIfInBounds i j).toArray = a.swapIfInBounds i j

Alias of Vector.toArray_swapIfInBounds.

@[deprecated Vector.toArray_swap]
theorem Vector.toArray_swapN {α : Type u_1} {n : Nat} (a : Vector α n) (i j : Nat) (hi : j < n) (hj : i < n) :
(a.swap i j hj hi).toArray = a.swap i j

Alias of Vector.toArray_swap.

@[simp]
theorem Vector.toArray_swapAt {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) :
((a.swapAt i x h).fst, (a.swapAt i x h).snd.toArray) = ((a.swapAt i x ).fst, (a.swapAt i x ).snd)
@[simp]
theorem Vector.toArray_swapAt! {α : Type u_1} {n : Nat} (a : 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)
@[deprecated Vector.toArray_swapAt]
theorem Vector.toArray_swapAtN {α : Type u_1} {n : Nat} (a : Vector α n) (i : Nat) (x : α) (h : i < n) :
((a.swapAt i x h).fst, (a.swapAt i x h).snd.toArray) = ((a.swapAt i x ).fst, (a.swapAt i x ).snd)

Alias of Vector.toArray_swapAt.

@[simp]
theorem Vector.toArray_take {α : Type u_1} {n : Nat} (a : Vector α n) (m : Nat) :
(a.take m).toArray = a.take m
@[simp]
theorem Vector.toArray_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} (f : αβγ) (a : Vector α n) (b : Vector β n) :
(a.zipWith b f).toArray = a.zipWith b.toArray f

toList lemmas #

theorem Vector.length_toList {α : Type u_1} {n : Nat} (xs : Vector α n) :
xs.toList.length = n
theorem Vector.getElem_toList {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
xs.toList[i] = xs[i]

getElem lemmas #

@[simp]
theorem Vector.getElem_ofFn {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) (h : i < n) :
(Vector.ofFn f)[i] = f i, h
@[simp]
theorem Vector.getElem_push_last {α : Type u_1} {n : Nat} {v : Vector α n} {x : α} :
(Vector.push x v)[n] = x
@[simp]
theorem Vector.getElem_push_lt {α : Type u_1} {n : Nat} {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
(Vector.push x v)[i] = v[i]
@[simp]
theorem Vector.getElem_pop {α : Type u_1} {n : Nat} {v : Vector α n} {i : Nat} (h : i < n - 1) :
v.pop[i] = v[i]
@[simp]
theorem Vector.getElem_pop' {α : Type u_1} {n : Nat} (v : 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 Vector.push_pop_back {α : Type u_1} {n : Nat} (v : Vector α (n + 1)) :
Vector.push v.back v.pop = v

empty lemmas #

theorem Vector.map_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
Vector.map f { toArray := #[], size_toArray := } = { toArray := #[], size_toArray := }
theorem Vector.eq_empty {α : Type u_1} (v : Vector α 0) :
v = { toArray := #[], size_toArray := }

Decidable quantifiers. #

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