From faf90c4b87a8c4ee00fee9272cb98234931e40ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Nov 2014 17:23:59 -0800
Subject: [PATCH] test(tests/lean/run): test brec_on on vectors

---
 tests/lean/run/vector.lean | 63 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 60 insertions(+), 3 deletions(-)

diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 3c6919844..8a14f4ead 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -2,11 +2,12 @@ import logic data.nat.basic data.prod data.unit
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
-vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+vnil {} : vector A zero,
+vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   print definition no_confusion
+  infixr `::` := vcons
 
   theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
   begin
@@ -24,6 +25,8 @@ namespace vector
     variable C : Π (n : nat), vector A n → Type.{l₂}
     definition below {n : nat} (v : vector A n) :=
     rec_on v unit.{max 1 l₂} (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : Type.{max 1 l₂}), C n₁ v₁ × r₁)
+
+   definition bw {n : nat} {A : Type} {C : Π (n : nat), vector A n → Type} (v : vector A n) := @below A C n v
   end
 
   section
@@ -33,7 +36,7 @@ namespace vector
     definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), below C v → C n v) : C n v :=
     have general : C n v × below C v, from
       rec_on v
-       (pair (H zero (vnil A) unit.star) unit.star)
+       (pair (H zero vnil unit.star) unit.star)
        (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × below C v₁),
           have b : below C (vcons a₁ v₁), from
             r₁,
@@ -45,4 +48,58 @@ namespace vector
 
   check brec_on
 
+  definition sum {n : nat} (v : vector nat n) : nat :=
+  brec_on v (λ (n : nat) (v : vector nat n),
+    cases_on v
+      (λ (B : bw vnil), zero)
+      (λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)),
+         a + pr₁ B))
+
+  example :  sum (10 :: 20 :: vnil) = 30 :=
+  rfl
+
+  definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n :=
+  brec_on v (λ (n : nat) (v : vector nat n),
+    cases_on v
+      (λ (B : bw vnil), vnil)
+      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)),
+         vcons (a₁+k) (pr₁ B)))
+
+  example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
+  rfl
+
+  definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
+  brec_on w (λ (n : nat) (w : vector A n),
+    cases_on w
+      (λ (B : bw vnil), v)
+      (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : bw (vcons a₁ v₁)),
+         vcons a₁ (pr₁ B)))
+
+  example : append (1 :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
+  rfl
+
+  definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
+  cases_on v
+    (λ H : succ n = 0, nat.no_confusion H)
+    (λn' h t (H : succ n = succ n'), h)
+    rfl
+
+  definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n :=
+  @cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v
+    (λ H : succ n = 0, nat.no_confusion H)
+    (λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'),
+       t)
+    rfl
+
+  definition add {n : nat} (w v : vector nat n) : vector nat n :=
+  @brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w
+  (λ (n : nat) (w : vector nat n),
+    cases_on w
+      (λ (B : bw vnil) (w : vector nat zero), vnil)
+      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)),
+         vcons (a₁ + head v) (pr₁ B (tail v)))) v
+
+  example : add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil :=
+  rfl
+
 end vector