Documentation

Batteries.Data.Vector.Lemmas

theorem Batteries.Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Batteries.Vector α n} :
v.toArray = w.toArrayv = w
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 #

theorem Batteries.Vector.toArray_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.toArray = a
@[simp]
theorem Batteries.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 Batteries.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 Batteries.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 Batteries.Vector.back?_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) :
{ toArray := a, size_toArray := h }.back? = a.back?
@[simp]
theorem Batteries.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 Batteries.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 Batteries.Vector.feraseIdx_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) :
{ toArray := a, size_toArray := h }.feraseIdx i = { toArray := a.feraseIdx (Fin.cast i), size_toArray := }
@[simp]
theorem Batteries.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 Batteries.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 Batteries.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.get (Fin.cast i)
@[simp]
theorem Batteries.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 Batteries.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 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.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 Batteries.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 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.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 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.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 Batteries.Vector.set_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) (x : α) :
{ toArray := a, size_toArray := h }.set i x = { toArray := a.set (Fin.cast i) x, size_toArray := }
@[simp]
theorem Batteries.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 Batteries.Vector.setD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) :
{ toArray := a, size_toArray := h }.setD i x = { toArray := a.setD i x, size_toArray := }
@[simp]
theorem Batteries.Vector.setN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) (hi : i < n) :
{ toArray := a, size_toArray := h }.setN i x hi = { toArray := a.setN i x , size_toArray := }
@[simp]
theorem Batteries.Vector.swap_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Fin n) :
{ toArray := a, size_toArray := h }.swap i j = { toArray := a.swap (Fin.cast i) (Fin.cast j), size_toArray := }
@[simp]
theorem Batteries.Vector.swap!_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) :
{ toArray := a, size_toArray := h }.swap! i j = { toArray := a.swap! i j, size_toArray := }
@[simp]
theorem Batteries.Vector.swapN_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i j : Nat) (hi : i < n) (hj : j < n) :
{ toArray := a, size_toArray := h }.swapN i j hi hj = { toArray := a.swapN i j , size_toArray := }
@[simp]
theorem Batteries.Vector.swapAt_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) (x : α) :
{ toArray := a, size_toArray := h }.swapAt i x = ((a.swapAt (Fin.cast i) x).fst, { toArray := (a.swapAt (Fin.cast i) x).snd, size_toArray := })
@[simp]
theorem Batteries.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 := })
@[simp]
theorem Batteries.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 }.swapAtN i x hi = ((a.swapAtN i x ).fst, { toArray := (a.swapAtN i x ).snd, size_toArray := })
@[simp]
theorem Batteries.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 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) :
(a ++ b).toArray = a.toArray ++ b.toArray
@[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]
theorem Batteries.Vector.toArray_empty {α : Type u_1} :
Batteries.Vector.empty.toArray = #[]
@[simp]
@[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) :
(a.feraseIdx i).toArray = a.feraseIdx (Fin.cast i)
@[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α) :
@[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_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 : α) :
(a.set i x).toArray = a.set (Fin.cast i) 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) :
(a.swap i j).toArray = a.swap (Fin.cast i) (Fin.cast j)
@[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 : α) :
((a.swapAt i x).fst, (a.swapAt i x).snd.toArray) = ((a.swapAt (Fin.cast i) x).fst, (a.swapAt (Fin.cast i) x).snd)
@[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 : α} :
@[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 α 0Prop} :
(∀ (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.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
instance Batteries.Vector.instDecidableExistsVectorZero {α : Type u_1} (P : Batteries.Vector α 0Prop) [Decidable (P Batteries.Vector.empty)] :
Decidable (∃ (v : Batteries.Vector α 0), P v)
Equations
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