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)

namespace vector
  -- print definition no_confusion
  infixr `::` := vcons

  local abbreviation no_confusion := @vector.no_confusion
  local abbreviation below := @vector.below

  theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
  begin
     intro h, apply (no_confusion h), intros, assumption
  end

  theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
  begin
     intro h, apply heq.to_eq, apply (no_confusion h), intros, eassumption,
  end

  set_option pp.universes true
  check @below

  namespace manual
  section
    universe variables l₁ l₂
    variable {A : Type.{l₁}}
    variable {C : Π (n : nat), vector A n → Type.{l₂}}
    definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v :=
    have general : C n v × @vector.below A C n v, from
      vector.rec_on v
       (pair (H zero vnil poly_unit.star) poly_unit.star)
       (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁),
          have b : @vector.below A C _ (vcons a₁ v₁), from
            r₁,
          have c : C (succ n₁) (vcons a₁ v₁), from
            H (succ n₁) (vcons a₁ v₁) b,
          pair c b),
    pr₁ general
  end
  end manual

  -- check vector.brec_on

  definition bw := @below

  definition sum {n : nat} (v : vector nat n) : nat :=
  vector.brec_on v (λ (n : nat) (v : vector nat n),
    vector.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 :=
  vector.brec_on v (λ (n : nat) (v : vector nat n),
    vector.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.{l} {A : Type.{l+1}} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
  vector.brec_on w (λ (n : nat) (w : vector A n),
    vector.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 :=
  vector.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 :=
  @vector.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 :=
  @vector.brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w
  (λ (n : nat) (w : vector nat n),
    vector.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

  definition map {A B C : Type} {n : nat} (f : A → B → C) (w : vector A n) (v : vector B n) : vector C n :=
  let P := λ (n : nat) (v : vector A n), vector B n → vector C n in
  @vector.brec_on A P n w
  (λ (n : nat) (w : vector A n),
     begin
       cases w with [n', h₁, t₁],
       show @below A P zero vnil → vector B zero → vector C zero, from
         λ b v, vnil,
       show @below A P (succ n') (h₁ :: t₁) → vector B (succ n') → vector C (succ n'), from
         λ b v,
         begin
           cases v with [n', h₂, t₂],
           have r : vector B n' → vector C n', from pr₁ b,
           exact ((f h₁ h₂) :: r t₂),
         end
     end) v

  theorem map_nil_nil {A B C : Type} (f : A → B → C) : map f vnil vnil = vnil :=
  rfl

  theorem map_cons_cons {A B C : Type} (f : A → B → C) (a : A) (b : B) {n : nat} (va : vector A n) (vb : vector B n) :
          map f (a :: va) (b :: vb) = f a b :: map f va vb :=
  rfl

  example : map nat.add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil :=
  rfl

  print definition map

end vector