From 0a29581b0ea625d7e459fb3a9e923f2b3c2f283a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jul 2015 18:08:35 -0700
Subject: [PATCH] feat(library/data/vec): add more theorems to vec (vectors as
 subtypes)

---
 library/data/list/basic.lean |  8 +++
 library/data/vec.lean        | 96 +++++++++++++++++++++++++++++++++++-
 2 files changed, 102 insertions(+), 2 deletions(-)

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 0cbcb2c66..d2f2b5423 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -107,6 +107,10 @@ theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a]
 theorem concat_ne_nil [simp] (a : T) : ∀ (l : list T), concat a l ≠ [] :=
 by intro l; induction l; repeat contradiction
 
+theorem length_concat [simp] (a : T) : ∀ (l : list T), length (concat a l) = length l + 1
+| []      := rfl
+| (x::xs) := by rewrite [concat_cons, *length_cons, length_concat]
+
 /- last -/
 
 definition last : Π l : list T, l ≠ [] → T
@@ -175,6 +179,10 @@ calc
   concat x l = concat x (reverse (reverse l)) : reverse_reverse
          ... = reverse (x :: reverse l)       : rfl
 
+theorem length_reverse : ∀ (l : list T), length (reverse l) = length l
+| []      := rfl
+| (x::xs) := begin unfold reverse, rewrite [length_concat, length_cons, length_reverse] end
+
 /- head and tail -/
 
 definition head [h : inhabited T] : list T → T
diff --git a/library/data/vec.lean b/library/data/vec.lean
index 9f5313d85..682ba6a82 100644
--- a/library/data/vec.lean
+++ b/library/data/vec.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 vectors as list subtype
 -/
-import logic data.list data.subtype
+import logic data.list data.subtype data.fin
 open nat list subtype function
 
 definition vec [reducible] (A : Type) (n : nat) := {l : list A | length l = n}
@@ -13,6 +13,9 @@ definition vec [reducible] (A : Type) (n : nat) := {l : list A | length l = n}
 namespace vec
   variables {A B C : Type}
 
+  theorem induction_on [recursor 4] {P : ∀ {n}, vec A n → Prop} : ∀ {n} (v : vec A n), (∀ (l : list A) {n : nat} (h : length l = n), P (tag l h)) → P v
+  | n (tag l h) H := @H l n h
+
   definition nil : vec A 0 :=
   tag [] rfl
 
@@ -28,6 +31,78 @@ namespace vec
   | 0        := inhabited.mk nil
   | (succ n) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
 
+  protected definition has_decidable_eq [instance] [h : decidable_eq A] : ∀ (n : nat), decidable_eq (vec A n) :=
+  _
+
+  definition of_list (l : list A) : vec A (list.length l) :=
+  tag l rfl
+
+  definition to_list {n : nat} : vec A n → list A
+  | (tag l h) := l
+
+  theorem to_list_of_list (l : list A) : to_list (of_list l) = l :=
+  rfl
+
+  theorem to_list_nil : to_list nil = ([] : list A) :=
+  rfl
+
+  theorem length_to_list {n : nat} : ∀ (v : vec A n), list.length (to_list v) = n
+  | (tag l h) := h
+
+  theorem heq_of_list_eq {n m} : ∀ {v₁ : vec A n} {v₂ : vec A m}, to_list v₁ = to_list v₂ → n = m → v₁ == v₂
+  | (tag l₁ h₁) (tag l₂ h₂) e₁ e₂ := begin
+      clear heq_of_list_eq,
+      subst e₂, subst h₁,
+      unfold to_list at e₁,
+      subst l₁
+    end
+
+  theorem list_eq_of_heq {n m} {v₁ : vec A n} {v₂ : vec A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ :=
+  begin
+    intro h₁ h₂, revert v₁ v₂ h₁,
+    subst n, intro v₁ v₂ h₁, rewrite [heq.to_eq h₁]
+  end
+
+  theorem of_list_to_list {n : nat} (v : vec A n) : of_list (to_list v) == v :=
+  begin
+    apply heq_of_list_eq, rewrite to_list_of_list, rewrite length_to_list
+  end
+
+  definition append {n m : nat} : vec A n → vec A m → vec A (n + m)
+  | (tag l₁ h₁) (tag l₂ h₂) := tag (list.append l₁ l₂) (by rewrite [length_append, h₁, h₂])
+
+  infix ++ := append
+
+  open eq.ops
+
+  lemma push_eq_rec : ∀ {n m : nat} {l : list A} (h₁ : n = m) (h₂ : length l = n), h₁ ▹ (tag l h₂) = tag l (h₁ ▹ h₂)
+  | n n l (eq.refl n) h₂ := rfl
+
+  theorem append_nil_right {n : nat} (v : vec A n) : v ++ nil = v :=
+  induction_on v (λ l n h, by unfold [vec.append, vec.nil]; congruence; apply list.append_nil_right)
+
+  theorem append_nil_left {n : nat} (v : vec A n) : !zero_add ▹ (nil ++ v) = v :=
+  induction_on v (λ l n h, begin unfold [vec.append, vec.nil], rewrite [push_eq_rec] end)
+
+  theorem append_nil_left_heq {n : nat} (v : vec A n) : nil ++ v == v :=
+  heq_of_eq_rec_left !zero_add (append_nil_left v)
+
+  theorem append.assoc {n₁ n₂ n₃} : ∀ (v₁ : vec A n₁) (v₂ : vec A n₂) (v₃ : vec A n₃), !add.assoc ▹ ((v₁ ++ v₂) ++ v₃) = v₁ ++ (v₂ ++ v₃)
+  | (tag l₁ h₁) (tag l₂ h₂) (tag l₃ h₃) := begin
+    unfold vec.append, rewrite push_eq_rec,
+    congruence,
+    apply list.append.assoc
+  end
+
+  theorem append.assoc_heq {n₁ n₂ n₃} (v₁ : vec A n₁) (v₂ : vec A n₂) (v₃ : vec A n₃) : (v₁ ++ v₂) ++ v₃ == v₁ ++ (v₂ ++ v₃) :=
+  heq_of_eq_rec_left !add.assoc (append.assoc v₁ v₂ v₃)
+
+  definition reverse {n : nat} : vec A n → vec A n
+  | (tag l h) := tag (list.reverse l) (by rewrite [length_reverse, h])
+
+  theorem reverse_reverse {n : nat} (v : vec A n) : reverse (reverse v) = v :=
+  induction_on v (λ l n h, begin unfold reverse, congruence, apply list.reverse_reverse end)
+
   theorem vec0_eq_nil : ∀ (v : vec A 0), v = nil
   | (tag []     h) := rfl
   | (tag (a::l) h) := by contradiction
@@ -61,6 +136,24 @@ namespace vec
   definition mem {n : nat} (a : A) (v : vec A n) : Prop :=
   a ∈ elt_of v
 
+  notation e ∈ s := mem e s
+  notation e ∉ s := ¬ e ∈ s
+
+  theorem not_mem_nil (a : A) : a ∉ nil :=
+  list.not_mem_nil a
+
+  theorem mem_cons [simp] {n : nat} (a : A) (v : vec A n) : a ∈ a :: v :=
+  induction_on v (λ l n h, !list.mem_cons)
+
+  theorem mem_cons_of_mem {n : nat} (y : A) {x : A} {v : vec A n} : x ∈ v → x ∈ y :: v :=
+  induction_on v (λ l n h₁ h₂, list.mem_cons_of_mem y h₂)
+
+  theorem eq_or_mem_of_mem_cons {n : nat} {x y : A} {v : vec A n} : x ∈ y::v → x = y ∨ x ∈ v :=
+  induction_on v (λ l n h₁ h₂, eq_or_mem_of_mem_cons h₂)
+
+  theorem mem_singleton {n : nat} {x a : A} : x ∈ (a::nil : vec A 1) → x = a :=
+  assume h, list.mem_singleton h
+
   definition last {n : nat} : vec A (succ n) → A
   | (tag l h) := list.last l (ne_nil_of_length_eq_succ h)
 
@@ -79,5 +172,4 @@ namespace vec
 
   theorem map_map {n : nat} (g : B → C) (f : A → B) (v : vec A n) : map g (map f v) = map (g ∘ f) v :=
   begin cases v, rewrite *map_tag, apply subtype.eq, apply list.map_map end
-
 end vec