From a628836f28aeb05decc89e762484eea73e142287 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Mar 2015 22:51:11 -0700
Subject: [PATCH] feat(library/data/vector): add theorems

---
 library/data/vector.lean | 94 +++++++++++++++++++++++++++++++++++++---
 1 file changed, 89 insertions(+), 5 deletions(-)

diff --git a/library/data/vector.lean b/library/data/vector.lean
index 5c4e06ecb..66cb351c0 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.vector
 Author: Floris van Doorn, Leonardo de Moura
 -/
-import data.nat.basic
+import data.nat data.list
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
@@ -82,18 +82,38 @@ namespace vector
                     map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
   rfl
 
-  -- Remark: why do we need to provide indices?
   definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
   | 0        m nil    w := w
   | (succ n) m (a::v) w := a :: (append v w)
 
-  theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
+  theorem nil_append {n : nat} (v : vector A n) : append nil v = v :=
   rfl
 
   theorem append_cons {n m : nat} (h : A) (t : vector A n) (v : vector A m) :
     append (h::t) v = h :: (append t v) :=
   rfl
 
+  theorem append_nil : Π {n : nat} (v : vector A n), append v nil == v
+  | zero      nil    := !heq.refl
+  | (succ n)  (h::t) :=
+    begin
+      change (h :: append t nil == h :: t),
+      have H₁ : append t nil == t, from append_nil t,
+      revert H₁, generalize (append t nil),
+      rewrite [-add_eq_addl, add_zero],
+      intros (w, H₁),
+      rewrite [heq.to_eq H₁],
+      apply heq.refl
+    end
+
+  theorem map_append (f : A → B) : ∀ {n m : nat} (v : vector A n) (w : vector A m), map f (append v w) = append (map f v) (map f w)
+  | zero     m   nil       w   :=  rfl
+  | (succ n) m   (h :: t)  w   :=
+     begin
+       change (f h :: map f (append t w) = f h :: append (map f t) (map f w)),
+       rewrite map_append
+     end
+
   definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
   | unzip nil           := (nil, nil)
   | unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
@@ -121,7 +141,7 @@ namespace vector
   | (succ n) (a::va) (b::vb) := calc
        unzip (zip (a :: va) (b :: vb))
              = (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl
-        ...  = (a :: pr₁ (va, vb), b :: pr₂ (va, vb))                       : {unzip_zip va vb}
+        ...  = (a :: pr₁ (va, vb), b :: pr₂ (va, vb))                       : by rewrite unzip_zip
         ...  = (a :: va, b :: vb)                                           : rfl
 
   theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
@@ -129,7 +149,7 @@ namespace vector
   | (succ n) ((a, b) :: v)  := calc
     zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
          = (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
-     ... = (a, b) :: v                                   : {zip_unzip v}
+     ... = (a, b) :: v                                   : by rewrite zip_unzip
 
   /- Concat -/
 
@@ -148,4 +168,68 @@ namespace vector
   | (succ n) (b::v) a := calc
     last (concat (b::v) a) = last (concat v a) : rfl
                     ...    = a                 : last_concat v a
+
+  /- Reverse -/
+
+  definition reverse : Π {n : nat}, vector A n → vector A n
+  | zero     nil       := nil
+  | (succ n) (x :: xs) := concat (reverse xs) x
+
+  theorem reverse_concat : Π {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs
+  | zero     nil        a := rfl
+  | (succ n) (x :: xs)  a :=
+    begin
+      change (concat (reverse (concat xs a)) x = a :: reverse (x :: xs)),
+      rewrite reverse_concat
+    end
+
+  theorem reverse_reverse : Π {n : nat} (xs : vector A n), reverse (reverse xs) = xs
+  | zero     nil       := rfl
+  | (succ n) (x :: xs) :=
+    begin
+      change (reverse (concat (reverse xs) x) = x :: xs),
+      rewrite [reverse_concat, reverse_reverse]
+    end
+
+  /- list <-> vector -/
+
+  definition of_list {A : Type} : Π (l : list A), vector A (list.length l)
+  | list.nil        := nil
+  | (list.cons a l) := a :: (of_list l)
+
+  definition to_list {A : Type} : Π {n : nat}, vector A n → list A
+  | zero     nil       := list.nil
+  | (succ n) (a :: vs) := list.cons a (to_list vs)
+
+  theorem to_list_of_list {A : Type} : ∀ (l : list A), to_list (of_list l) = l
+  | list.nil         := rfl
+  | (list.cons a l)  :=
+    begin
+      change (list.cons a (to_list (of_list l)) = list.cons a l),
+      rewrite to_list_of_list
+    end
+
+  theorem length_to_list {A : Type} : ∀ {n : nat} (v : vector A n), list.length (to_list v) = n
+  | zero     nil       := rfl
+  | (succ n) (a :: vs) :=
+    begin
+      change (succ (list.length (to_list vs)) = succ n),
+      rewrite length_to_list
+    end
+
+  theorem of_list_to_list {A : Type} : ∀ {n : nat} (v : vector A n), of_list (to_list v) == v
+  | zero     nil       := !heq.refl
+  | (succ n) (a :: vs) :=
+    begin
+      change (a :: of_list (to_list vs) == a :: vs),
+      have H₁ : of_list (to_list vs) == vs, from of_list_to_list vs,
+      revert H₁,
+      generalize (of_list (to_list vs)),
+      rewrite length_to_list at *,
+      intro vs', intro H,
+      have H₂ : vs' = vs, from heq.to_eq H,
+      rewrite H₂,
+      apply heq.refl
+   end
+
 end vector