feat(library/data): add type equivalence lemmas for subtype and vector

library/data/equiv.lean

@@ -9,17 +9,22 @@ We say two types are equivalent if they are isomorphic.
 import data.sum data.nat
 open function
 
-structure equiv (A B : Type) :=
+structure equiv [class] (A B : Type) :=
   (to_fun    : A → B)
   (inv       : B → A)
   (left_inv  : left_inverse inv to_fun)
   (right_inv : right_inverse inv to_fun)
 
 namespace equiv
-attribute equiv.to_fun [coercion]
-
 infix `≃`:50 := equiv
 
+namespace ops
+  attribute equiv.to_fun [coercion]
+  definition inverse [reducible] {A B : Type} [h : A ≃ B] : B → A :=
+  λ b, @equiv.inv A B h b
+  postfix `⁻¹` := inverse
+end ops
+
 protected theorem refl [refl] (A : Type) : A ≃ A :=
 mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)
 
@@ -236,4 +241,15 @@ end
 
 definition inhabited_of_equiv {A B : Type} [h : inhabited A] : A ≃ B → inhabited B
 | (mk f g l r) := inhabited.mk (f (inhabited.value h))
+
+section
+open subtype
+override equiv.ops
+definition subtype_equiv_of_subtype {A B : Type} {p : A → Prop} : A ≃ B → {a : A | p a} ≃ {b : B | p (b⁻¹)}
+| (mk f g l r) :=
+  mk (λ s, match s with tag v h := tag (f v) (eq.rec_on (eq.symm (l v)) h) end)
+     (λ s, match s with tag v h := tag (g v) (eq.rec_on (eq.symm (r v)) h) end)
+     (λ s, begin cases s, esimp, congruence, rewrite l, reflexivity end)
+     (λ s, begin cases s, esimp, congruence, rewrite r, reflexivity end)
+end
 end equiv

library/data/vector.lean

@@ -100,6 +100,19 @@ namespace vector
   | (succ n) (a :: t) (mk 0 h)        := by reflexivity
   | (succ n) (a :: t) (mk (succ i) h) := by rewrite [map_cons, *nth_succ, nth_map]
 
+  section
+  open function
+  theorem map_id : ∀ {n : nat} (v : vector A n), map id v = v
+  | 0        []      := rfl
+  | (succ n) (x::xs) := by rewrite [map_cons, map_id]
+
+  theorem map_map (g : B → C) (f : A → B) : ∀ {n :nat} (v : vector A n), map g (map f v) = map (g ∘ f) v
+  | 0        []       := rfl
+  | (succ n) (a :: l) :=
+    show (g ∘ f) a :: map g (map f l) = map (g ∘ f) (a :: l),
+    by rewrite (map_map l)
+  end
+
   definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
   | map2 []      []      := []
   | map2 (a::va) (b::vb) := f a b :: map2 va vb
@@ -273,4 +286,13 @@ namespace vector
       end
     | inr Hnab := by right; intro h; injection h; contradiction
   end
+
+  section
+  open equiv function
+  definition vector_equiv_of_equiv {A B : Type} : A ≃ B → ∀ n, vector A n ≃ vector B n
+  | (mk f g l r) n :=
+    mk (map f) (map g)
+     begin intros, rewrite [map_map, id_of_left_inverse l, map_id], reflexivity end
+     begin intros, rewrite [map_map, id_of_righ_inverse r, map_id], reflexivity end
+  end
 end vector