From a24a7f7fa1603ee8b69a590d729f1cf6e8326677 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Jan 2015 16:52:30 -0800
Subject: [PATCH] test(tests/lean/run) define vector last and unzip functions
 using recursive equations

---
 tests/lean/run/eq18.lean | 12 ++++++++++++
 tests/lean/run/eq19.lean | 15 +++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 tests/lean/run/eq18.lean
 create mode 100644 tests/lean/run/eq19.lean

diff --git a/tests/lean/run/eq18.lean b/tests/lean/run/eq18.lean
new file mode 100644
index 000000000..cbc147156
--- /dev/null
+++ b/tests/lean/run/eq18.lean
@@ -0,0 +1,12 @@
+import data.vector
+open nat vector
+
+definition last {A : Type} : Π {n}, vector A (succ n) → A,
+last (a :: nil) := a,
+last (a :: v)   := last v
+
+theorem last_cons_nil {A : Type} {n : nat} (a : A) : last (a :: nil) = a :=
+rfl
+
+theorem last_cons {A : Type} {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
+rfl
diff --git a/tests/lean/run/eq19.lean b/tests/lean/run/eq19.lean
new file mode 100644
index 000000000..2e526ec21
--- /dev/null
+++ b/tests/lean/run/eq19.lean
@@ -0,0 +1,15 @@
+import data.vector data.prod
+open nat vector prod
+
+variables {A B : Type}
+
+definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n,
+unzip nil           := (nil, nil),
+unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
+
+theorem unzip_nil : unzip nil = (@nil A, @nil B) :=
+rfl
+
+theorem unzip_cons {n : nat} (a : A) (b : B) (t : vector (A × B) n) :
+  unzip ((a, b) :: t) = (a :: pr₁ (unzip t), b :: pr₂ (unzip t)) :=
+rfl