feat(tests/lean/run/blast_vector_test): test ematch + cc at vectors

tests/lean/run/blast_vector_test.lean

@@ -0,0 +1,77 @@
+import data.nat
+open nat
+
+lemma addl_eq_add [simp] (n m : nat) : (:n ⊕ m:) = n + m :=
+!add_eq_addl
+
+-- Casting notation
+notation `⟨`:max a `⟩`:0 := cast (by inst_simp) a
+
+inductive vector (A : Type) : nat → Type :=
+| nil {} : vector A zero
+| cons   : Π {n}, A → vector A n → vector A (succ n)
+
+namespace vector
+
+notation a :: b := cons a b
+notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
+
+variable {A : Type}
+
+private definition append_aux : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
+| 0        m []     w := w
+| (succ n) m (a::v) w := a :: (append_aux v w)
+
+theorem append_aux_nil_left [simp] {n : nat} (v : vector A n) : append_aux [] v == v :=
+!heq.refl
+
+theorem append_aux_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : append_aux (h::t) v ==  h :: (append_aux t v) :=
+!heq.refl
+
+definition append {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) :=
+⟨append_aux v w⟩
+
+section
+local attribute append [reducible]
+theorem append_nil_left [simp] {n : nat} (v : vector A n) : append [] v == v :=
+by inst_simp
+
+theorem append_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : (: append (h::t) v :) == (: h::(append t v) :) :=
+by inst_simp
+end
+
+theorem append_nil_right [simp] {n : nat} (v : vector A n) : append v [] == v :=
+by rec_inst_simp
+
+attribute succ_add [simp]
+
+theorem append_assoc [simp] {n₁ n₂ n₃ : nat} (v₁ : vector A n₁) (v₂ : vector A n₂) (v₃ : vector A n₃) : append v₁ (append v₂ v₃) == append (append v₁ v₂) v₃ :=
+by rec_inst_simp
+
+definition concat : Π {n : nat}, vector A n → A → vector A (succ n)
+| concat []     a := [a]
+| concat (b::v) a := b :: concat v a
+
+theorem concat_nil [simp] (a : A) : concat [] a = [a] :=
+rfl
+
+theorem concat_cons [simp] {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
+rfl
+
+definition reverse : Π {n : nat}, vector A n → vector A n
+| 0     []        := []
+| (n+1) (x :: xs) := concat (reverse xs) x
+
+theorem reverse_nil [simp] : reverse [] = @nil A :=
+rfl
+
+theorem reverse_cons [simp] {n : nat} (a : A) (v : vector A n) : reverse (a::v) = concat (reverse v) a :=
+rfl
+
+theorem reverse_concat [simp] : ∀ {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs :=
+by rec_inst_simp
+
+theorem reverse_reverse [simp] : ∀ {n : nat} (xs : vector A n), reverse (reverse xs) = xs :=
+by rec_inst_simp
+
+end vector