From 39e7e5cba8798e50b9e81bd49ff1254b2cce79ea Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 6 May 2017 02:36:03 -0400
Subject: [PATCH] feat(data/vector): more vector operations

---
 library/data/vector.lean         | 24 +++++++++++++++++++++++-
 library/init/data/fin/basic.lean |  2 +-
 library/init/data/fin/ops.lean   | 11 ++++++++---
 3 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/library/data/vector.lean b/library/data/vector.lean
index 151583bb4d..7a1eefc0e3 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -45,11 +45,21 @@ def tail : vector α n → vector α (n - 1)
 theorem tail_cons (a : α) : Π (v : vector α n), tail (a :: v) = v
 | ⟨ l, h ⟩ := rfl
 
-def to_list : vector α n → list α | ⟨ l, h ⟩ := l
+@[simp] theorem cons_head_tail : ∀ v : vector α (succ n), (head v :: tail v) = v
+| ⟨ [],     h ⟩ := by contradiction
+| ⟨ a :: v, h ⟩ := rfl
+
+def to_list (v : vector α n) : list α := v.1
+
+def nth : Π (v : vector α n), fin n → α | ⟨ l, h ⟩ i := l.nth_le i.1 (by rw h; exact i.2)
 
 def append {n m : nat} : vector α n → vector α m → vector α (n + m)
 | ⟨ l₁, h₁ ⟩ ⟨ l₂, h₂ ⟩ := ⟨ l₁ ++ l₂, by simp_using_hs ⟩
 
+@[elab_as_eliminator] def elim {α} {C : Π {n}, vector α n → Sort u} (H : ∀l : list α, C ⟨l, rfl⟩)
+  {n : nat} : Π (v : vector α n), C v
+| ⟨l, h⟩ := match n, h with ._, rfl := H l end
+
 /- map -/
 
 def map (f : α → β) : vector α n → vector β n
@@ -72,6 +82,13 @@ def dropn (i : ℕ) : vector α n → vector α (n - i)
 def taken (i : ℕ) : vector α n → vector α (min i n)
 | ⟨l, p⟩ := ⟨ list.taken i l, by simp_using_hs ⟩
 
+def remove_nth (i : fin n) : vector α n → vector α (n - 1)
+| ⟨l, p⟩ := ⟨ list.remove_nth l i.1, by rw[l.length_remove_nth i.1]; rw p; exact i.2 ⟩
+
+def of_fn : Π {n}, (fin n → α) → vector α n
+| 0 f := []
+| (n+1) f := f 0 :: of_fn (λi, f i.succ)
+
 section accum
   open prod
   variable {σ : Type}
@@ -92,12 +109,17 @@ end accum
 protected lemma eq {n : ℕ} : ∀ (a1 a2 : vector α n), to_list a1 = to_list a2 → a1 = a2
 | ⟨x, h1⟩ ⟨._, h2⟩ rfl := rfl
 
+protected theorem eq_nil (v : vector α 0) : v = [] :=
+v.eq [] (list.eq_nil_of_length_eq_zero v.2)
+
 @[simp] lemma to_list_mk (v : list α) (P : list.length v = n) : to_list (subtype.mk v P) = v :=
 rfl
 
 @[simp] lemma to_list_nil : to_list [] = @list.nil α :=
 rfl
 
+@[simp] lemma to_list_length (v : vector α n) : (to_list v).length = n := v.2
+
 @[simp] lemma to_list_cons (a : α) (v : vector α n) : to_list (a :: v) = a :: to_list v :=
 begin cases v, reflexivity end
 
diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index c1559a8453..d55ab57c7e 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -12,7 +12,7 @@ attribute [pp_using_anonymous_constructor] fin
 
 namespace fin
 
-def {u} elim0 {α : Type u} : fin 0 → α
+def {u} elim0 {α : Sort u} : fin 0 → α
 | ⟨_, h⟩ := absurd h (not_lt_zero _)
 
 variable {n : nat}
diff --git a/library/init/data/fin/ops.lean b/library/init/data/fin/ops.lean
index cedd522322..96f81a7f97 100644
--- a/library/init/data/fin/ops.lean
+++ b/library/init/data/fin/ops.lean
@@ -10,6 +10,9 @@ namespace fin
 open nat
 variable {n : nat}
 
+protected def succ : fin n → fin (succ n)
+| ⟨a, h⟩ := ⟨nat.succ a, succ_lt_succ h⟩
+
 def of_nat {n : nat} (a : nat) : fin (succ n) :=
 ⟨a % succ n, nat.mod_lt _ (nat.zero_lt_succ _)⟩
 
@@ -55,7 +58,7 @@ protected def lt : fin n → fin n → Prop
 protected def le : fin n → fin n → Prop
 | ⟨a, _⟩ ⟨b, _⟩ := a ≤ b
 
-instance : has_zero (fin (succ n)) := ⟨of_nat 0⟩
+instance : has_zero (fin (succ n)) := ⟨⟨0, succ_pos n⟩⟩
 instance : has_one (fin (succ n))  := ⟨of_nat 1⟩
 instance : has_add (fin n)         := ⟨fin.add⟩
 instance : has_sub (fin n)         := ⟨fin.sub⟩
@@ -71,6 +74,9 @@ instance decidable_lt : ∀ (a b : fin n), decidable (a < b)
 instance decidable_le : ∀ (a b : fin n), decidable (a ≤ b)
 | ⟨a, _⟩ ⟨b, _⟩ := by apply nat.decidable_le
 
+lemma of_nat_zero : @of_nat n 0 = 0 :=
+fin.eq_of_veq $ zero_mod n.succ
+
 lemma add_def (a b : fin n) : (a + b).val = (a.val + b.val) % n :=
 show (fin.add a b).val = (a.val + b.val) % n, from
 by cases a; cases b; simp [fin.add]
@@ -99,8 +105,7 @@ lemma le_def (a b : fin n) : (a ≤ b) = (a.val ≤ b.val) :=
 show (fin.le a b) = (a.val ≤ b.val), from
 by cases a; cases b; simp [fin.le]
 
-lemma val_zero : (0 : fin (succ n)).val = 0 :=
-begin unfold has_zero.zero of_nat, dsimp, rw zero_mod end
+lemma val_zero : (0 : fin (succ n)).val = 0 := rfl
 
 def pred {n : nat} : ∀ i : fin (succ n), i ≠ 0 → fin n
 | ⟨a, h₁⟩ h₂ := ⟨a.pred,