feat(data/vector/mem): Lemmas about membership in a vector (#15154)

Add a number of lemmas about membership in different `vector`s. Some just wrap the `list` versions but some of the `n+1` cases are more general.

src/data/vector/basic.lean

@@ -48,6 +48,19 @@ instance zero_subsingleton : subsingleton (vector α 0) :=
 @[simp] theorem cons_tail (a : α) : ∀ (v : vector α n), (a ::ᵥ v).tail = v
 | ⟨_, _⟩ := rfl
 
+lemma eq_cons_iff (a : α) (v : vector α n.succ) (v' : vector α n) :
+  v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v' :=
+⟨λ h, h.symm ▸ ⟨head_cons a v', tail_cons a v'⟩,
+ λ h, trans (cons_head_tail v).symm (by rw [h.1, h.2])⟩
+
+lemma ne_cons_iff (a : α) (v : vector α n.succ) (v' : vector α n) :
+  v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v' :=
+by rw [ne.def, eq_cons_iff a v v', not_and_distrib]
+
+lemma exists_eq_cons (v : vector α n.succ) :
+  ∃ (a : α) (as : vector α n), v = a ::ᵥ as :=
+⟨v.head, v.tail, (eq_cons_iff v.head v v.tail).2 ⟨rfl, rfl⟩⟩
+
 @[simp] theorem to_list_of_fn : ∀ {n} (f : fin n → α), to_list (of_fn f) = list.of_fn f
 | 0     f := rfl
 | (n+1) f := by rw [of_fn, list.of_fn_succ, to_list_cons, to_list_of_fn]
@@ -64,6 +77,20 @@ v.2
 @[simp] lemma to_list_map {β : Type*} (v : vector α n) (f : α → β) : (v.map f).to_list =
   v.to_list.map f := by cases v; refl
 
+@[simp] lemma head_map {β : Type*} (v : vector α (n + 1)) (f : α → β) :
+  (v.map f).head = f v.head :=
+begin
+  obtain ⟨a, v', h⟩ := vector.exists_eq_cons v,
+  rw [h, map_cons, head_cons, head_cons],
+end
+
+@[simp] lemma tail_map {β : Type*} (v : vector α (n + 1)) (f : α → β) :
+  (v.map f).tail = v.tail.map f :=
+begin
+  obtain ⟨a, v', h⟩ := vector.exists_eq_cons v,
+  rw [h, map_cons, tail_cons, tail_cons],
+end
+
 theorem nth_eq_nth_le : ∀ (v : vector α n) (i),
   nth v i = v.to_list.nth_le i.1 (by rw to_list_length; exact i.2)
 | ⟨l, h⟩ i := rfl
@@ -129,11 +156,6 @@ end
 @[simp] lemma map_id {n : ℕ} (v : vector α n) : vector.map id v = v :=
   vector.eq _ _ (by simp only [list.map_id, vector.to_list_map])
 
-lemma mem_iff_nth {a : α} {v : vector α n} : a ∈ v.to_list ↔ ∃ i, v.nth i = a :=
-by simp only [list.mem_iff_nth_le, fin.exists_iff, vector.nth_eq_nth_le];
-  exact ⟨λ ⟨i, hi, h⟩, ⟨i, by rwa to_list_length at hi, h⟩,
-    λ ⟨i, hi, h⟩, ⟨i, by rwa to_list_length, h⟩⟩
-
 lemma nodup_iff_nth_inj {v : vector α n} : v.to_list.nodup ↔ function.injective v.nth :=
 begin
   cases v with l hl,
@@ -146,9 +168,6 @@ begin
     have := @h ⟨i, hi⟩ ⟨j, hj⟩, simp [nth_eq_nth_le] at *, tauto }
 end
 
-@[simp] lemma nth_mem (i : fin n) (v : vector α n) : v.nth i ∈ v.to_list :=
-by rw [nth_eq_nth_le]; exact list.nth_le_mem _ _ _
-
 theorem head'_to_list : ∀ (v : vector α n.succ),
   (to_list v).head' = some (head v)
 | ⟨a::l, e⟩ := rfl

src/data/vector/mem.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2022 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+import data.vector.basic
+/-!
+# Theorems about membership of elements in vectors
+
+This file contains theorems for membership in a `v.to_list` for a vector `v`.
+Having the length available in the type allows some of the lemmas to be
+  simpler and more general than the original version for lists.
+In particular we can avoid some assumptions about types being `inhabited`,
+  and make more general statements about `head` and `tail`.
+-/
+
+namespace vector
+variables {α β : Type*} {n : ℕ} (a a' : α)
+
+@[simp] lemma nth_mem (i : fin n) (v : vector α n) : v.nth i ∈ v.to_list :=
+by { rw nth_eq_nth_le,  exact list.nth_le_mem _ _ _ }
+
+lemma mem_iff_nth (v : vector α n) : a ∈ v.to_list ↔ ∃ i, v.nth i = a :=
+by simp only [list.mem_iff_nth_le, fin.exists_iff, vector.nth_eq_nth_le];
+  exact ⟨λ ⟨i, hi, h⟩, ⟨i, by rwa to_list_length at hi, h⟩,
+    λ ⟨i, hi, h⟩, ⟨i, by rwa to_list_length, h⟩⟩
+
+lemma not_mem_nil : a ∉ (vector.nil : vector α 0).to_list := id
+
+@[simp] lemma not_mem_zero (v : vector α 0) : a ∉ v.to_list :=
+(vector.eq_nil v).symm ▸ (not_mem_nil a)
+
+lemma mem_cons_iff (v : vector α n) :
+  a' ∈ (a ::ᵥ v).to_list ↔ a' = a ∨ a' ∈ v.to_list :=
+by rw [vector.to_list_cons, list.mem_cons_iff]
+
+lemma mem_succ_iff (v : vector α (n + 1)) :
+  a ∈ v.to_list ↔ a = v.head ∨ a ∈ v.tail.to_list :=
+begin
+  obtain ⟨a', v', h⟩ := exists_eq_cons v,
+  simp_rw [h, vector.mem_cons_iff, vector.head_cons, vector.tail_cons],
+end
+
+lemma mem_cons_self (v : vector α n) : a ∈ (a ::ᵥ v).to_list :=
+(vector.mem_iff_nth a (a ::ᵥ v)).2 ⟨0, vector.nth_cons_zero a v⟩
+
+@[simp] lemma head_mem (v : vector α (n + 1)) : v.head ∈ v.to_list :=
+(vector.mem_iff_nth v.head v).2 ⟨0, vector.nth_zero v⟩
+
+lemma mem_cons_of_mem (v : vector α n) (ha' : a' ∈ v.to_list) : a' ∈ (a ::ᵥ v).to_list :=
+(vector.mem_cons_iff a a' v).2 (or.inr ha')
+
+lemma mem_of_mem_tail (v : vector α n) (ha : a ∈ v.tail.to_list) : a ∈ v.to_list :=
+begin
+  induction n with n hn,
+  { exact false.elim (vector.not_mem_zero a v.tail ha) },
+  { exact (mem_succ_iff a v).2 (or.inr ha) }
+end
+
+lemma mem_map_iff (b : β) (v : vector α n) (f : α → β) :
+  b ∈ (v.map f).to_list ↔ ∃ (a : α), a ∈ v.to_list ∧ f a = b :=
+by rw [vector.to_list_map, list.mem_map]
+
+lemma not_mem_map_zero (b : β) (v : vector α 0) (f : α → β) : b ∉ (v.map f).to_list :=
+by simpa only [vector.eq_nil v, vector.map_nil, vector.to_list_nil] using list.not_mem_nil b
+
+lemma mem_map_succ_iff (b : β) (v : vector α (n + 1)) (f : α → β) :
+  b ∈ (v.map f).to_list ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.to_list ∧ f a = b :=
+by rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]
+
+end vector