Documentation

Lilac.Vec.Lemma

Vec Lemmas #

TODO: Header

Fun.Vec.to #

source
@[simp]
theorem Lilac.Fun.Vec.to_nil {α : Sort u_1} :
↑nil = #()
source
@[simp]
theorem Lilac.Vec.to_nil {α : Sort u_1} :
#().to = Fun.Vec.nil
source
@[simp]
theorem Lilac.Fun.Vec.to_cons {α : Sort u_1} {n : Nat} {hd : α} {tl : Vec α n} :
↑(cons hd tl) = hd :: ↑tl
source
@[simp]
theorem Lilac.Fun.Vec.to_iso {α : Sort u_1} {n : Nat} {v : Vec α n} :
(↑v).to = v

to #

source
@[simp]
theorem Lilac.Vec.to_iso {α : Sort u_1} {n : Nat} {v : Vec α n} :
↑v.to = v

append #

source
@[simp]
theorem Lilac.Vec.append_nil_left {α : Type u_1} {n : Nat} {v : Vec α n} :
#() ++ v = v
source
@[simp]
theorem Lilac.Vec.append_cons {α : Type u_1} {n1 n2 : Nat} {x : α} {v1 : Vec α n1} {v2 : Vec α n2} :
x :: v1 ++ v2 = x :: (v1 ++ v2)
source
@[simp]
theorem Lilac.Vec.append_nil_right {α : Type u_1} {n : Nat} {v : Vec α n} :
v ++ #() ≍ v
source
@[simp]
theorem Lilac.Vec.append_assoc {α : Type u_1} {n1 n2 n3 : Nat} {v1 : Vec α n1} {v2 : Vec α n2} {v3 : Vec α n3} :
v1 ++ v2 ++ v3 ≍ v1 ++ (v2 ++ v3)

list #

source
@[simp]
theorem Lilac.Vec.list_tail {n : Nat} {α : Type u_1} [NeZero n] {v : Vec α n} :
v.tail.list = v.list.tail
source
@[simp]
theorem Lilac.Vec.list_set {α : Type u_1} {a : α} {n : Nat} {i : Fin n} {v : Vec α n} :
(v.set i a).list = v.list.set (↑i) a
source
@[simp]
theorem Lilac.Vec.list_concat {α : Type u_1} {n : Nat} {x : α} {v : Vec α n} :
(v.concat x).list = v.list.concat x
source
@[simp]
theorem Lilac.Vec.list_append {α : Type u_1} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} :
(v1 ++ v2).list = v1.list ++ v2.list
source
@[simp]
theorem Lilac.Vec.list_flatten {α : Type u_1} {n m : Nat} {v : Vec (Vec α n) m} :
v.flatten.list = (list <$> v.list).flatten
source
@[simp]
theorem Lilac.Vec.list_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {v : Vec α n} :
(map f v).list = List.map f v.list
source
@[simp]
theorem Lilac.Vec.list_replicate {x n : Nat} :
(replicate n x).list = List.replicate n x
source
@[simp]
theorem Lilac.Vec.list_reverse {α : Type u_1} {n : Nat} {v : Vec α n} :
v.reverse.list = v.list.reverse
source
@[simp]
theorem Lilac.Vec.list_take {α : Type u_1} {n k : Nat} {h : k ≤ n} {v : Vec α n} :
(take k h v).list = List.take k v.list
source
@[simp]
theorem Lilac.Vec.list_cast {α : Type u} {m n : Nat} {h : m = n} {v : Vec α m} :
(cast ⋯ v).list = v.list
source
@[simp]
theorem Lilac.Vec.list_drop {α : Type u} {m n : Nat} {v : Vec α m} {h : n ≤ m} :
(drop n h v).list = List.drop n v.list
source
@[simp]
theorem Lilac.Vec.list_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {v1 : Vec α n} {v2 : Vec β n} :
(zipWith f v1 v2).list = List.zipWith f v1.list v2.list
source
@[simp]
theorem Lilac.Vec.list_zip {α : Type u_1} {β : Type u_2} {n : Nat} {v1 : Vec α n} {v2 : Vec β n} :
(v1.zip v2).list = v1.list.zip v2.list
source
@[simp]
theorem Lilac.Vec.list_zipIdx {α : Type u_1} {n k : Nat} {v : Vec α n} :
(v.zipIdx k).list = v.list.zipIdx k
source
@[simp]
theorem Lilac.Vec.list_range {k : Nat} (n : Nat) :
(range n k).list = List.range' k n
source
theorem Lilac.Vec.list_of_at_least_one_nonempty {α : Type u_1} {n : Nat} {v : Vec α (n + 1)} :
v.list ≠ []

length #

Vec carries its own length, hence why length is marked reducible. This also means that most operations on length are trivial and the simplifier will reject them.

source
theorem Lilac.Vec.length_to {α : Sort u_1} {n : Nat} {v : Fun.Vec α n} :
(↑v).length = n
source
@[simp]
theorem Lilac.Vec.length_tail {α : Sort u_1} {n : Nat} [NeZero n] {v : Vec α n} :
v.tail.length = n - 1
source
theorem Lilac.Vec.length_set {α : Sort u_1} {n : Nat} {i : Fin n} {x : α} {v : Vec α n} :
(v.set i x).length = n
source
@[simp]
theorem Lilac.Vec.length_concat {α : Sort u_1} {n : Nat} {x : α} {v : Vec α n} :
(v.concat x).length = n + 1
source
@[simp]
theorem Lilac.Vec.length_append {α : Type u_1} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} :
(v1 ++ v2).length = n + m
source
@[simp]
theorem Lilac.Vec.length_flatten {α : Type u_1} {n m : Nat} {v : Vec (Vec α n) m} :
v.flatten.length = n * m
source
theorem Lilac.Vec.length_map {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {v : Vec α n} :
(map f v).length = n
source
theorem Lilac.Vec.length_reverse {α : Sort u_1} {n : Nat} {v : Vec α n} :
v.reverse.length = n
source
theorem Lilac.Vec.length_take {α : Sort u_1} {m n : Nat} {h : n ≤ m} {v : Vec α m} :
(take n h v).length = n
source
@[simp]
theorem Lilac.Vec.length_drop {α : Sort u_1} {m n : Nat} {h : n ≤ m} {v : Vec α m} :
(drop n h v).length = m - n
source
theorem Lilac.Vec.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {v1 : Vec α n} {v2 : Vec β n} :
(zipWith f v1 v2).length = n
source
theorem Lilac.Vec.length_zip {α : Type u_1} {β : Type u_2} {n : Nat} {v1 : Vec α n} {v2 : Vec β n} :
(v1.zip v2).length = n
source
theorem Lilac.Vec.length_range {n k : Nat} :
(range n k).length = n
source
theorem Lilac.Vec.length_zipIdx {α : Type u_1} {n k : Nat} {v : Vec α n} :
(v.zipIdx k).length = n

get #

source
@[simp]
theorem Lilac.Vec.get_cons_zero {α : Type u_1} {n : Nat} {x : α} {xs : Vec α n} :
(x :: xs)[0] = x
source
@[simp]
theorem Lilac.Vec.get_cons_succ {α : Type u_1} {n : Nat} {x : α} {xs : Vec α n} {i : Fin n} :
(x :: xs)[i.succ] = xs[i]
source
theorem Lilac.Vec.get_set_neq {α : Type u_1} {n : Nat} {i j : Fin n} (h : i ≠ j) {a : α} {v : Vec α n} :
(v.set i a)[j] = v[j]
source
@[simp]
theorem Lilac.Vec.get_set_eq {α : Type u_1} {a : α} {n : Nat} {i : Fin n} {v : Vec α n} :
(v.set i a)[i] = a
source
theorem Lilac.Vec.get_concat_castLT {α : Type u_1} {a : α} {n : Nat} {i : Fin (n + 1)} (h : ↑i ≠ n) {v : Vec α n} :
(v.concat a)[i] = v[i.castLT ⋯]
source
theorem Lilac.Vec.get_concat_castSucc {α : Type u_1} {a : α} {n : Nat} {i : Fin n} {v : Vec α n} :
(v.concat a)[i.castSucc] = v[i]
source
theorem Lilac.Vec.get_append_lt {α : Type u_1} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} {i : Fin (m + n)} (h : ↑i < n) :
(v1 ++ v2)[i] = v1[i.castLT h]
source
theorem Lilac.Vec.get_append_ge {α : Type u_1} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} {i : Fin (m + n)} (h : ↑i ≥ n) :
(v1 ++ v2)[i] = v2[Fin.subNat n (Fin.cast ⋯ i) h]
source
@[simp]
theorem Lilac.Vec.get_map {α : Type u_1} {β : Type u_2} {f : α → β} {n : Nat} {v : Vec α n} {i : Fin n} :
(map f v)[i] = f v[i]
source
@[simp]
theorem Lilac.Vec.get_replicate {α : Type u_1} {x : α} {n : Nat} {i : Fin n} :
(replicate n x)[i] = x
source
@[simp]
theorem Lilac.Vec.get_cons_last {α : Type u_1} {n : Nat} {x : α} {xs : Vec α (n + 1)} :
(x :: xs)[Fin.last (n + 1)] = xs[Fin.last n]
source
@[simp]
theorem Lilac.Vec.get_concat_last {α : Type u_1} {n : Nat} {a : α} {xs : Vec α n} :
(xs.concat a)[Fin.last n] = a
source
@[simp]
theorem Lilac.Vec.get_rev_cons {α : Type u_1} {x : α} {n : Nat} {xs : Vec α n} {i : Fin n} :
(x :: xs)[i.castSucc.rev] = xs[i.rev]
source
@[simp]
theorem Lilac.Vec.get_reverse {α : Type u_1} {n : Nat} {v : Vec α n} {i : Fin n} :
v.reverse[i] = v[i.rev]
source
@[simp]
theorem Lilac.Vec.get_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β → γ} {v1 : Vec α n} {v2 : Vec β n} {i : Fin n} :
(zipWith f v1 v2)[i] = f v1[i] v2[i]
source
@[simp]
theorem Lilac.Vec.get_zip {α : Type u_1} {β : Type u_2} {n : Nat} {v1 : Vec α n} {v2 : Vec β n} {i : Fin n} :
(v1.zip v2)[i] = (v1[i], v2[i])
source
@[simp]
theorem Lilac.Vec.get_range {k n : Nat} {i : Fin n} :
(range n k)[i] = ↑i + k
source
@[simp]
theorem Lilac.Vec.get_zipIdx {α : Type u_1} {k n : Nat} {v : Vec α n} {i : Fin n} :
(v.zipIdx k)[i] = (v[i], ↑i + k)
source
theorem Lilac.Vec.head_zeroth_index_agree {α : Type u_1} {n : Nat} [NeZero n] {v : Vec α n} :
v.head = v[Fin.ofNat n 0]
source
@[simp]
theorem Lilac.Vec.head_set_zero {α : Sort u_1} {x : α} {n : Nat} [NeZero n] {v : Vec α n} :
(v.set 0 x).head = x
source
@[simp]
theorem Lilac.Vec.head_set_succ {α : Sort u_1} {a : α} {n : Nat} {i : Fin n} [NeZero n] [NeZero i] {v : Vec α n} :
(v.set i a).head = v.head
source
@[simp]
theorem Lilac.Vec.head_concat {α : Sort u_1} {a : α} {n : Nat} [NeZero n] {v : Vec α n} :
(v.concat a).head = v.head
source
@[simp]
theorem Lilac.Vec.head_append {α : Type u_1} {n m : Nat} [NeZero n] {v1 : Vec α n} (v2 : Vec α m) :
(v1 ++ v2).head = v1.head
source
@[simp]
theorem Lilac.Vec.head_flatten {α : Type u_1} {n m : Nat} [NeZero n] [NeZero m] {v : Vec (Vec α n) m} :
v.flatten.head = v.head.head
source
@[simp]
theorem Lilac.Vec.head_map {α : Type u_1} {β : Type u_2} {f : α → β} {n : Nat} [NeZero n] {v : Vec α n} :
(map f v).head = f v.head
source
@[simp]
theorem Lilac.Vec.head_replicate {α : Sort u_1} {x : α} {n : Nat} [NeZero n] :
(replicate n x).head = x
source
@[simp]
theorem Lilac.Vec.head_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {n : Nat} [NeZero n] {v1 : Vec α n} {v2 : Vec β n} :
(zipWith f v1 v2).head = f v1.head v2.head
source
@[simp]
theorem Lilac.Vec.head_zip {α : Type u_1} {β : Type u_2} {n : Nat} [NeZero n] {v1 : Vec α n} {v2 : Vec β n} :
(v1.zip v2).head = (v1.head, v2.head)
source
@[simp]
theorem Lilac.Vec.head_range {n k : Nat} [NeZero n] :
(range n k).head = k
source
@[simp]
theorem Lilac.Vec.head_zipIdx {α : Type u_1} {n k : Nat} [NeZero n] {v : Vec α n} :
(v.zipIdx k).head = (v.head, k)

tail #

source
@[simp]
theorem Lilac.Vec.tail_append {α : Type u_1} {n m : Nat} [NeZero n] {v1 : Vec α n} {v2 : Vec α m} :
(v1 ++ v2).tail ≍ v1.tail ++ v2

set #

foldl #

foldr #

concat #

flatten #

map #

Why don't we use Functor / LawfulFunctor? Because Lean's type inference is not capable of figuring out the right functor f when using Functor.map. Try it yourself: implement Functor (Vec · n) and notice how (· + 2) <$> #(1, 2) fails. Solutions:

  1. Try to fix Lean's type inference algorithm, unclear if Lean developers will be receptive
  2. Use Vec.map directly (not horrible, v.map f is good ergonomics)
  3. Define our own IndexedFunctor type that will resolve the index correctly:
class IndexedFunctor (I : Type u) (F : Type v -> I -> Type w) where
  imap {α β i} (f : α -> β) : F α i -> F β i

instance : IndexedFunctor Nat Vec where
  imap := Vec.map

#eval IndexedFunctor.imap (· + 2) #(1, 2)

For now we choose 2

source
@[simp]
theorem Lilac.Vec.map_id {α : Type u_1} {n : Nat} {v : Vec α n} :
map id v = v
source
@[simp]
theorem Lilac.Vec.map_id_lambda {α : Type u_1} {n : Nat} {v : Vec α n} :
map (fun (x : α) => x) v = v
source
@[simp]
theorem Lilac.Vec.map_tail {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} [NeZero n] {v : Vec α n} :
map f v.tail = (map f v).tail
source
@[simp]
theorem Lilac.Vec.map_set {α : Type u_1} {β : Type u_2} {x : α} {f : α → β} {n : Nat} {i : Fin n} {v : Vec α n} :
map f (v.set i x) = (map f v).set i (f x)
source
@[simp]
theorem Lilac.Vec.map_concat {α : Type u_1} {β : Type u_2} {n : Nat} {x : α} {f : α → β} {v : Vec α n} :
map f (v.concat x) = (map f v).concat (f x)
source
@[simp]
theorem Lilac.Vec.map_append {α : Type u_1} {β : Type u_2} {n m : Nat} {f : α → β} {v1 : Vec α n} {v2 : Vec α m} :
map f (v1 ++ v2) = map f v1 ++ map f v2
source
@[simp]
theorem Lilac.Vec.map_flatten {α : Type u_1} {β : Type u_2} {n m : Nat} {f : α → β} {v : Vec (Vec α n) m} :
map f v.flatten = (map (map f) v).flatten
source
@[simp]
theorem Lilac.Vec.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → β} {h : β → γ} {v : Vec α n} :
map h (map f v) = map (h ∘ f) v
source
@[simp]
theorem Lilac.Vec.map_replicate {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} {n : Nat} :
map f (replicate n a) = replicate n (f a)
source
@[simp]
theorem Lilac.Vec.map_reverse {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → β} {v : Vec α n} :
map f v.reverse = (map f v).reverse
source
@[simp]
theorem Lilac.Vec.map_take {α : Type u_1} {β : Type u_2} {f : α → β} {m : Nat} {n : Fin m} {h : ↑n ≤ m} {v : Vec α m} :
map f (take (↑n) h v) = take (↑n) h (map f v)
source
@[simp]
theorem Lilac.Vec.map_cast {α : Type u_1} {β : Type u_2} {f : α → β} {m n : Nat} {h : m = n} {v : Vec α m} :
map f (cast ⋯ v) = cast ⋯ (map f v)
source
@[simp]
theorem Lilac.Vec.map_drop {α : Type u_1} {β : Type u_2} {f : α → β} {m : Nat} {n : Fin m} {h : ↑n ≤ m} {v : Vec α m} :
map f (drop (↑n) h v) = drop (↑n) h (map f v)

beq #

source
theorem Lilac.Vec.beq_refl {α : Type u_1} {n : Nat} [BEq α] [ReflBEq α] {a : Vec α n} :
(a == a) = true
source
instance Lilac.instReflBEqVec {α : Type u_1} {n : Nat} [BEq α] [ReflBEq α] :
ReflBEq (Vec α n)
source
theorem Lilac.Vec.beq_lawful {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {v1 v2 : Vec α n} :
v1.beq v2 = true → v1 = v2
source
instance Lilac.instLawfulBEqVec {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] :
LawfulBEq (Vec α n)
source
theorem Lilac.Vec.beq_head_tail {α : Type u_1} [BEq α] {n : Nat} [NeZero n] {v1 v2 : Vec α n} :
(v1.head == v2.head) = true ∧ (v1.tail == v2.tail) = true ↔ (v1 == v2) = true
source
theorem Lilac.Vec.beq_get {α : Type u_1} [BEq α] {n : Nat} {v1 v2 : Vec α n} (h : ∀ (i : Fin n), (v1[i] == v2[i]) = true) :
(v1 == v2) = true

replicate #

reverse #

contains #

take #

drop #

any #

source
theorem Lilac.Vec.any_append_left {α : Type u_1} {p : α → Bool} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} :
v1.any p = true → (v1 ++ v2).any p = true
source
theorem Lilac.Vec.any_append_right {α : Type u_1} {p : α → Bool} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} :
v2.any p = true → (v1 ++ v2).any p = true
source
theorem Lilac.Vec.any_append_iff {α : Type u_1} {p : α → Bool} {n m : Nat} {v1 : Vec α n} {v2 : Vec α m} :
v1.any p = true ∨ v2.any p = true ↔ (v1 ++ v2).any p = true
source
theorem Lilac.Vec.any_list {α : Type u_1} {p : α → Bool} {n : Nat} {v : Vec α n} :
v.any p = true ↔ v.list.any p = true
source
theorem Lilac.Vec.any_get {α : Type u_1} {p : α → Bool} {n : Nat} {v : Vec α n} {h : v.any p = true} :
∃ (i : Fin n), p v[i] = true
source
theorem Lilac.Vec.any_tail {α : Sort u_1} {p : α → Bool} {n : Nat} [NeZero n] {v : Vec α n} {h : v.any p = true} {not_head : ¬p v.head = true} :
v.tail.any p = true
source
theorem Lilac.Vec.any_set {α : Sort u_1} {p : α → Bool} {a : α} {n : Nat} {v : Vec α n} {i : Fin n} {h : p a = true} :
(v.set i a).any p = true

all #

zipWith #

zip #

unzip #

range #

zipIdx #

find? #

findIdx? #

erase #

count #

traverse #

sequence #

sum #

Mem #