Helper Lemmas about Vector

These are used in Soundness.lean.

theorem List.nonempty_drop_sub_succ {α✝ : Type u_1} {δ : List α✝} (δ_not_empty : δ ≠ []) (k : Fin δ.length) : (drop (↑k + 1) δ).length + 1 = δ.length.succ - (↑k + 1)

theorem Vector.my_cast_head {α : Type u_1} (n m : ℕ) (v : List.Vector α n.succ) (h : n = m) : (h ▸ v).head = v.head

theorem Vector.my_cast_eq_val_head {α : Type u_1} (n m : ℕ) (v : List.Vector α n.succ) (h : n = m) (h2 : ↑v ≠ []) : (h ▸ v).head = (↑v).head h2

theorem Vector.my_cast_toList {α : Type u_1} (n m : ℕ) (t : List α) (ht : t.length = n) (h : n = m) : t = List.Vector.toList (h ▸ ⟨t, ht⟩)

theorem aux_simplify_vector_type {α : Type u_1} {q p : ℕ} (t : List α) (h : t.length = q + 1 + 1 - (p + 1 + 1)) : let help := ⋯; ⟨t, h⟩ = ⋯ ▸ ⟨t, ⋯⟩

theorem Vector.my_drop_succ_cons {α : Type u_1} {m n : ℕ} (x : α) (t : List α) (h : (x :: t).length = n.succ) (hyp : m < n) : let help := ⋯; List.Vector.drop (m + 1) ⟨x :: t, h⟩ = ⋯ ▸ List.Vector.drop m ⟨t, ⋯⟩

theorem Vector.get_succ_eq_head_drop {α : Type u_1} {n : ℕ} {v : List.Vector α n.succ} (k : Fin n) (j : ℕ) (h : n + 1 - (↑k + 1) = j + 1) : v.get k.succ = (h ▸ List.Vector.drop (↑k + 1) v).head

theorem Vector.drop_get_eq_get_add' {α : Type u_1} {n i : ℕ} (v : List.Vector α n) (l r : ℕ) {h : i = l + r} {hi : i < n} {hr : r < n - l} : v.get ⟨i, hi⟩ = (List.Vector.drop l v).get ⟨r, hr⟩

Generalized vesrion of Vector.drop_get_eq_get_add.

theorem Vector.drop_get_eq_get_add {α : Type u_1} {n : ℕ} (v : List.Vector α n) (k : ℕ) (i : Fin (n - k)) (still_lt : k + ↑i < n) : (List.Vector.drop k v).get i = v.get ⟨k + ↑i, still_lt⟩

A Vector analogue of List.getElem_drop.

theorem Fin.my_cast_val {j : ℕ} (n m : ℕ) (h : n = m) (j_lt : j < n) : ↑(h ▸ ⟨j, j_lt⟩) = j

theorem Vector.drop_last_eq_last {α : Type u_1} {n : ℕ} {v : List.Vector α n.succ} (k : Fin n) (j : ℕ) (h : n.succ - (↑k + 1) = j.succ) : (h ▸ List.Vector.drop (↑k + 1) v).last = v.last

theorem Vector.my_cast_heq {α : Type u_1} (n m : ℕ) (h : n = m) (v : List.Vector α n) : HEq (h ▸ v) v