feature(data/vector2, data/list): add insert_nth for vectors and lists

data/equiv/fin.lean

@@ -70,3 +70,9 @@ def fin_prod_fin_equiv : (fin m × fin n) ≃ fin (m * n) :=
             = y.1 % n : nat.add_mul_mod_self_left _ _ _
         ... = y.1 : nat.mod_eq_of_lt y.2),
   right_inv := λ x, fin.eq_of_veq $ nat.mod_add_div _ _ }
+
+instance subsingleton_fin_zero : subsingleton (fin 0) :=
+fin_zero_equiv.subsingleton
+
+instance subsingleton_fin_one : subsingleton (fin 1) :=
+fin_one_equiv.subsingleton

data/fin.lean

@@ -22,6 +22,9 @@ by cases a; refl
 protected lemma ext_iff (a b : fin n) : a = b ↔ a.val = b.val :=
 iff.intro (congr_arg _) fin.eq_of_veq
 
+lemma eq_iff_veq (a b : fin n) : a = b ↔ a.1 = b.1 :=
+⟨veq_of_eq, eq_of_veq⟩
+
 instance fin_to_nat (n : ℕ) : has_coe (fin n) nat := ⟨fin.val⟩
 
 instance {n : ℕ} : decidable_linear_order (fin n) :=
@@ -56,6 +59,12 @@ by cases j; simp [fin.pred]
 @[simp] lemma pred_succ (i : fin n) {h : i.succ ≠ 0} : i.succ.pred h = i :=
 by cases i; refl
 
+@[simp] lemma pred_inj :
+  ∀ {a b : fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
+| ⟨0,   _⟩  b         ha hb := by contradiction
+| ⟨i+1, _⟩  ⟨0,   _⟩  ha hb := by contradiction
+| ⟨i+1, hi⟩ ⟨j+1, hj⟩ ha hb := by simp [fin.eq_iff_veq]
+
 /-- The greatest value of `fin (n+1)` -/
 def last (n : ℕ) : fin (n+1) := ⟨_, n.lt_succ_self⟩
 
@@ -108,6 +117,9 @@ rfl
 @[simp] lemma add_nat_val (i : fin (n + m)) (h : i.val ≥ m) : (i.add_nat m).val = i.val + m :=
 rfl
 
+@[simp] lemma cast_succ_inj {a b : fin n} : a.cast_succ = b.cast_succ ↔ a = b :=
+by simp [eq_iff_veq]
+
 theorem succ_above_ne (p : fin (n+1)) (i : fin n) : p.succ_above i ≠ p :=
 begin
   assume eq,

data/list/basic.lean

@@ -882,6 +882,32 @@ def to_array (l : list α) : array l.length α :=
 def modify_nth (f : α → α) : ℕ → list α → list α :=
 modify_nth_tail (modify_head f)
 
+lemma modify_nth_tail_modify_nth_tail {f g : list α → list α} (m : ℕ) :
+  ∀n (l:list α), (l.modify_nth_tail f n).modify_nth_tail g (m + n) =
+    l.modify_nth_tail (λl, (f l).modify_nth_tail g m) n
+| 0     l      := rfl
+| (n+1) []     := rfl
+| (n+1) (a::l) := congr_arg (list.cons a) (modify_nth_tail_modify_nth_tail n l)
+
+lemma modify_nth_tail_modify_nth_tail_le
+  {f g : list α → list α} (m n : ℕ) (l : list α) (h : n ≤ m) :
+  (l.modify_nth_tail f n).modify_nth_tail g m =
+    l.modify_nth_tail (λl, (f l).modify_nth_tail g (m - n)) n :=
+begin
+  rcases le_iff_exists_add.1 h with ⟨m, rfl⟩,
+  rw [nat.add_sub_cancel_left, add_comm, modify_nth_tail_modify_nth_tail]
+end
+
+lemma modify_nth_tail_modify_nth_tail_same {f g : list α → list α} (n : ℕ) (l:list α) :
+  (l.modify_nth_tail f n).modify_nth_tail g n = l.modify_nth_tail (g ∘ f) n :=
+by rw [modify_nth_tail_modify_nth_tail_le n n l (le_refl n), nat.sub_self]; refl
+
+lemma modify_nth_tail_id :
+  ∀n (l:list α), l.modify_nth_tail id n = l
+| 0     l      := rfl
+| (n+1) []     := rfl
+| (n+1) (a::l) := congr_arg (list.cons a) (modify_nth_tail_id n l)
+
 theorem remove_nth_eq_nth_tail : ∀ n (l : list α), remove_nth l n = modify_nth_tail tail n l
 | 0     l      := by cases l; refl
 | (n+1) []     := rfl
@@ -943,6 +969,50 @@ theorem nth_update_nth_ne (a : α) {m n} (l : list α) (h : m ≠ n) :
   nth (update_nth l m a) n = nth l n :=
 by simp only [update_nth_eq_modify_nth, nth_modify_nth_ne _ _ h]
 
+section insert_nth
+variable {a : α}
+
+def insert_nth (n : ℕ) (a : α) : list α → list α := modify_nth_tail (list.cons a) n
+
+@[simp] lemma insert_nth_nil (a : α) : insert_nth 0 a [] = [a] := rfl
+
+lemma length_insert_nth : ∀n as, n ≤ length as → length (insert_nth n a as) = length as + 1
+| 0     as       h := rfl
+| (n+1) []       h := (nat.not_succ_le_zero _ h).elim
+| (n+1) (a'::as) h := congr_arg nat.succ $ length_insert_nth n as (nat.le_of_succ_le_succ h)
+
+lemma remove_nth_insert_nth (n:ℕ) (l : list α) : (l.insert_nth n a).remove_nth n = l :=
+by rw [remove_nth_eq_nth_tail, insert_nth, modify_nth_tail_modify_nth_tail_same];
+from modify_nth_tail_id _ _
+
+lemma insert_nth_remove_nth_of_ge : ∀n m as, n < length as → m ≥ n →
+  insert_nth m a (as.remove_nth n) = (as.insert_nth (m + 1) a).remove_nth n
+| 0     0     []      has _   := (lt_irrefl _ has).elim
+| 0     0     (a::as) has hmn := by simp [remove_nth, insert_nth]
+| 0     (m+1) (a::as) has hmn := rfl
+| (n+1) (m+1) (a::as) has hmn :=
+  congr_arg (cons a) $
+    insert_nth_remove_nth_of_ge n m as (nat.lt_of_succ_lt_succ has) (nat.le_of_succ_le_succ hmn)
+
+lemma insert_nth_remove_nth_of_le : ∀n m as, n < length as → m ≤ n →
+  insert_nth m a (as.remove_nth n) = (as.insert_nth m a).remove_nth (n + 1)
+| n       0       (a :: as) has hmn := rfl
+| (n + 1) (m + 1) (a :: as) has hmn :=
+  congr_arg (cons a) $
+    insert_nth_remove_nth_of_le n m as (nat.lt_of_succ_lt_succ has) (nat.le_of_succ_le_succ hmn)
+
+lemma insert_nth_comm (a b : α) :
+  ∀(i j : ℕ) (l : list α) (h : i ≤ j) (hj : j ≤ length l),
+    (l.insert_nth i a).insert_nth (j + 1) b = (l.insert_nth j b).insert_nth i a
+| 0       j     l      := by simp [insert_nth]
+| (i + 1) 0     l      := assume h, (nat.not_lt_zero _ h).elim
+| (i + 1) (j+1) []     := by simp
+| (i + 1) (j+1) (c::l) :=
+  assume h₀ h₁,
+  by simp [insert_nth]; exact insert_nth_comm i j l (nat.le_of_succ_le_succ h₀) (nat.le_of_succ_le_succ h₁)
+
+end insert_nth
+
 /- take, drop -/
 @[simp] theorem take_zero (l : list α) : take 0 l = [] := rfl
 

data/vector2.lean

@@ -8,8 +8,11 @@ Additional theorems about the `vector` type.
 import data.vector data.list.basic data.sigma data.equiv.basic
        category.traversable
 
+universes u
+variables {n : ℕ}
+
 namespace vector
-variables {α : Type*} {n : ℕ}
+variables {α : Type*}
 
 attribute [simp] head_cons tail_cons
 
@@ -73,7 +76,7 @@ by simp [nth_zero]
   (a : α) (v : vector α n) (i : fin n) : nth (a :: v) i.succ = nth v i :=
 by rw [← nth_tail, tail_cons]
 
-def {u} m_of_fn {m} [monad m] {α : Type u} : ∀ {n}, (fin n → m α) → m (vector α n)
+def m_of_fn {m} [monad m] {α : Type u} : ∀ {n}, (fin n → m α) → m (vector α n)
 | 0     f := pure nil
 | (n+1) f := do a ← f 0, v ← m_of_fn (λi, f i.succ), pure (a :: v)
 
@@ -82,7 +85,7 @@ theorem m_of_fn_pure {m} [monad m] [is_lawful_monad m] {α} :
 | 0     f := rfl
 | (n+1) f := by simp [m_of_fn, @m_of_fn_pure n, of_fn]
 
-def {u} mmap {m} [monad m] {α} {β : Type u} (f : α → m β) :
+def mmap {m} [monad m] {α} {β : Type u} (f : α → m β) :
   ∀ {n}, vector α n → m (vector β n)
 | _ ⟨[], rfl⟩   := pure nil
 | _ ⟨a::l, rfl⟩ := do h' ← f a, t' ← mmap ⟨l, rfl⟩, pure (h' :: t')
@@ -103,13 +106,71 @@ def {u} mmap {m} [monad m] {α} {β : Type u} (f : α → m β) :
 def to_array : vector α n → array n α
 | ⟨xs, h⟩ := cast (by rw h) xs.to_array
 
+section insert_nth
+variable {a : α}
+
+def insert_nth (a : α) (i : fin (n+1)) (v : vector α n) : vector α (n+1) :=
+⟨v.1.insert_nth i.1 a,
+  begin
+    rw [list.length_insert_nth, v.2],
+    rw [v.2, ← nat.succ_le_succ_iff],
+    exact i.2
+  end⟩
+
+lemma insert_nth_val {i : fin (n+1)} {v : vector α n} :
+  (v.insert_nth a i).val = v.val.insert_nth i.1 a :=
+rfl
+
+@[simp] lemma remove_nth_val {i : fin n} :
+  ∀{v : vector α n}, (remove_nth i v).val = v.val.remove_nth i.1
+| ⟨l, hl⟩ := rfl
+
+lemma remove_nth_insert_nth {v : vector α n} {i : fin (n+1)} : remove_nth i (insert_nth a i v) = v :=
+subtype.eq $ list.remove_nth_insert_nth i.1 v.1
+
+lemma remove_nth_insert_nth_ne {v : vector α (n+1)} :
+  ∀{i j : fin (n+2)} (h : i ≠ j),
+    remove_nth i (insert_nth a j v) = insert_nth a (i.pred_above j h.symm) (remove_nth (j.pred_above i h) v)
+| ⟨i, hi⟩ ⟨j, hj⟩ ne :=
+  begin
+    have : i ≠ j := fin.vne_of_ne ne,
+    refine subtype.eq _,
+    dsimp [insert_nth, remove_nth, fin.pred_above, fin.cast_lt],
+    rcases lt_trichotomy i j with h | h | h,
+    { have h_nji : ¬ j < i := lt_asymm h,
+      have j_pos : 0 < j := lt_of_le_of_lt (zero_le i) h,
+      simp [h, h_nji, fin.lt_iff_val_lt_val],
+      rw [show j.pred = j - 1, from rfl, list.insert_nth_remove_nth_of_ge, nat.sub_add_cancel j_pos],
+      { rw [v.2], exact lt_of_lt_of_le h (nat.le_of_succ_le_succ hj) },
+      { exact nat.le_sub_right_of_add_le h } },
+    { exact (this h).elim },
+    { have h_nij : ¬ i < j := lt_asymm h,
+      have i_pos : 0 < i := lt_of_le_of_lt (zero_le j) h,
+      simp [h, h_nij, fin.lt_iff_val_lt_val],
+      rw [show i.pred = i - 1, from rfl, list.insert_nth_remove_nth_of_le, nat.sub_add_cancel i_pos],
+      { show i - 1 + 1 ≤ v.val.length,
+        rw [v.2, nat.sub_add_cancel i_pos],
+        exact nat.le_of_lt_succ hi },
+      { exact nat.le_sub_right_of_add_le h } }
+  end
+
+lemma insert_nth_comm (a b : α) (i j : fin (n+1)) (h : i ≤ j) :
+  ∀(v : vector α n), (v.insert_nth a i).insert_nth b j.succ = (v.insert_nth b j).insert_nth a i.cast_succ
+| ⟨l, hl⟩ :=
+  begin
+    refine subtype.eq _,
+    simp [insert_nth_val, fin.succ_val, fin.cast_succ],
+    apply list.insert_nth_comm,
+    { assumption },
+    { rw hl, exact nat.le_of_succ_le_succ j.2 }
+  end
+
+end insert_nth
+
 end vector
 
 namespace vector
 
-universes u
-variables {n : ℕ}
-
 section traverse
 
 variables {F G : Type u → Type u}