From 5dc42762dede41e3d3154aa3cfd1aafa38fd7fd6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Nov 2014 21:58:42 -0800
Subject: [PATCH] feat(library/data): define 'nat.addl' addition using
 recursion on the first argument, prove it to be equivalent to 'add', and use
 it to define vector.append

---
 library/data/nat/basic.lean | 30 ++++++++++++++++++++++++++++++
 library/data/vector.lean    | 16 +++++++---------
 2 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 0a061c75f..13abdb61c 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -40,6 +40,36 @@ definition add (x y : ℕ) : ℕ :=
 nat.rec x (λ n r, succ r) y
 notation a + b := add a b
 
+definition addl (x y : ℕ) : ℕ :=
+nat.rec y (λ n r, succ r) x
+infix `⊕`:65 := addl
+
+theorem addl.succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
+nat.induction_on n
+  rfl
+  (λ n₁ ih, calc
+    succ n₁ ⊕ succ m = succ (n₁ ⊕ succ m)   : rfl
+             ...     = succ (succ (n₁ ⊕ m)) : ih
+             ...     = succ (succ n₁ ⊕ m)   : rfl)
+
+theorem add_eq_addl (x : ℕ) : ∀y, x + y = x ⊕ y :=
+nat.induction_on x
+  (λ y, nat.induction_on y
+    rfl
+    (λ y₁ ih, calc
+      zero + succ y₁ = succ (zero + y₁)  : rfl
+              ...    = succ (zero ⊕ y₁) : {ih}
+              ...    = zero ⊕ (succ y₁) : rfl))
+  (λ x₁ ih₁ y, nat.induction_on y
+    (calc
+      succ x₁ + zero  = succ (x₁ + zero)  : rfl
+                  ... = succ (x₁ ⊕ zero) : {ih₁ zero}
+                  ... = succ x₁ ⊕ zero   : rfl)
+    (λ y₁ ih₂, calc
+      succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
+                   ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
+                   ...  = succ x₁ ⊕ succ y₁   : addl.succ_right))
+
 definition of_num [coercion] [reducible] (n : num) : ℕ :=
 num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
diff --git a/library/data/vector.lean b/library/data/vector.lean
index 0200aa6a0..bdce5a2df 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -116,21 +116,18 @@ namespace vector
                      map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
   rfl
 
-  definition append_core (w : vector A m) (v : vector A n) : vector A (n + m) :=
+  definition append (w : vector A n) (v : vector A m) : vector A (n ⊕ m) :=
   rec_on w
     v
-    (λ (a₁ : A) (m₁ : nat) (v₁ : vector A m₁) (r₁ : vector A (n + m₁)), a₁ :: r₁)
+    (λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : vector A (n₁ ⊕ m)), a₁ :: r₁)
 
-  theorem append_vnil (v : vector A n) : append_core nil v = v :=
+  theorem append_nil (v : vector A n) : append nil v = v :=
   rfl
 
-  theorem append_vcons (h : A) (t : vector A n) (v : vector A m) :
-    append_core (h :: t) v = h :: (append_core t v) :=
+  theorem append_cons (h : A) (t : vector A n) (v : vector A m) :
+    append (h :: t) v = h :: (append t v) :=
   rfl
 
-  definition append (w : vector A n) (v : vector A m) : vector A (n + m) :=
-  eq.rec_on !add.comm (append_core w v)
-
   definition unzip : vector (A × B) n → vector A n × vector B n :=
   nat.rec_on n
     (λ v, (nil, nil))
@@ -183,7 +180,8 @@ namespace vector
   rfl
 
   theorem length_append (v₁ : vector A n) (v₂ : vector A m) : length (append v₁ v₂) = length v₁ + length v₂ :=
-  rfl
+  calc length (append v₁ v₂) = length v₁ ⊕ length v₂ : rfl
+                         ... = length v₁ + length v₂ : add_eq_addl
 
   -- Concat
   -- ------