(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
(*            them.                                                           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "Util.ma".

include "Universes.ma".

include "Nat.ma".
include "List.ma".
include "Cartesian.ma".
include "Maybe.ma".
include "Plogic/equality.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* The datatype.                                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ninductive Vector (A: Type[0]): Nat → Type[0] ≝
  Empty: Vector A Z
| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Syntax.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

notation "[[ list0 x sep ; ]]"
  non associative with precedence 90
  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.

interpretation "Vector vnil" 'vnil = (Empty ?).
interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lookup.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

naxiom succ_less_than_injective:
  ∀m, n: Nat.
    less_than_p (S m) (S n) → m < n.
    
naxiom nothing_less_than_Z:
  ∀m: Nat.
    ¬(m < Z).

nlet rec get_index (A: Type[0]) (n: Nat)
                   (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
  (match m with
    [ Z ⇒
      match v return λx.λ_. Z < x → A with
        [ Empty ⇒ λabsd1: Z < Z. ?
        | Cons p hd tl ⇒ λprf1: Z < S p. hd
        ]
    | S o ⇒
      (match v return λx.λ_. S o < x → A with
        [ Empty ⇒ λprf: S o < Z. ?
        | Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?
        ])
    ]) lt.
    ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1)
    ##| ncases (nothing_less_than_Z (S o)); #K; ncases (K prf)
    ##| napply succ_less_than_injective; nassumption
    ##]
nqed.

nlet rec get_index_weak (A: Type[0]) (n: Nat)
                   (v: Vector A n) (m: Nat) on m ≝
  match m with
    [ Z ⇒
      match v with
        [ Empty ⇒ Nothing A
        | Cons p hd tl ⇒ Just A hd
        ]
    | S o ⇒
      match v with
        [ Empty ⇒ Nothing A
        | Cons p hd tl ⇒ get_index_weak A p tl o
        ]
    ].
    
interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).

(*
nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
  (match m with
    [ Z ⇒
      match v return λx.λ_. Z < x → Vector A x with
        [ Empty ⇒ λabsd1: Z < Z. Empty A
        | Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl)
        ]
    | S o ⇒
      (match v return λx.λ_. S o < x → Vector A x with
        [ Empty ⇒ λprf: S o < Z. Empty A
        | Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?)
        ])
    ]) lt.
    napply succ_less_than_injective.
    nassumption.
nqed.
*)
    
nlet rec set_index_weak (A: Type[0]) (n: Nat)
                        (v: Vector A n) (m: Nat) (a: A) on m ≝
  match m with
    [ Z ⇒
      match v with
        [ Empty ⇒ Nothing (Vector A n)
        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
        ]
    | S o ⇒
      match v with
        [ Empty ⇒ Nothing (Vector A n)
        | Cons p hd tl ⇒
            let settail ≝ set_index_weak A p tl o a in
              match settail with
                [ Nothing ⇒ Nothing (Vector A n)
                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
                ]
        ]
    ].
    //.
nqed.

nlet rec drop (A: Type[0]) (n: Nat)
              (v: Vector A n) (m: Nat) on m ≝
  match m with
    [ Z ⇒ Just (Vector A n) v
    | S o ⇒
      match v with
        [ Empty ⇒ Nothing (Vector A n)
        | Cons p hd tl ⇒ ? (drop A p tl o)
        ]
    ].
    //.
nqed.
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Folds and builds.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
  match v with
    [ Empty ⇒ x
    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
    ].
    
nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
  match v with
    [ Empty ⇒ x
    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
    ].
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Maps and zips.                                                             *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
             (f: A → B) (v: Vector A n) on v ≝
  match v with
    [ Empty ⇒ Empty B
    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
    ].

(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
   currently in there.
*)
nlemma eq_rect_Type0_r :
  ∀A: Type[0].
  ∀a:A.
  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
  #A a P H x p.
  ngeneralize in match H.
  ngeneralize in match P.
  ncases p.
  //.
nqed.

nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
  (match v return (λx.λr. x = n → Vector C x) with
    [ Empty ⇒ λ_. Empty C
    | Cons n hd tl ⇒
      match q return (λy.λr. S n = y → Vector C (S n)) with
        [ Empty ⇒ ?
        | Cons m hd' tl' ⇒
            λe: S n = S m.
              (f hd hd') :: (zip_with A B C n f tl ?)
        ]
    ])
    (refl ? n).
      ##
        [ #e;
          ndestruct(e);
          ##
        | ndestruct(e);
          napply tl'
          ##
        ]
nqed.

ndefinition zip ≝
  λA, B: Type[0].
  λn: Nat.
  λv: Vector A n.
  λq: Vector B n.
    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Building vectors from scratch                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
  match n return λn. Vector A n with
    [ Z ⇒ Empty A
    | S m ⇒ h :: (replicate A m h)
    ].

nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
                (v: Vector A n) (q: Vector A m) on v ≝
  match v return (λn.λv. Vector A (n + m)) with
    [ Empty ⇒ q
    | Cons o hd tl ⇒ hd :: (append A o m tl q)
    ].
    
interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
    
nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
  a ::
    (match v with
       [ Empty ⇒ Empty A
       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
       ]).

nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
  match v with
    [ Empty ⇒ ?
    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
    ].
    //.
nqed.
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Other manipulations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
  match v with
    [ Empty ⇒ Z
    | Cons n hd tl ⇒ S $ length A n tl
    ].

nlet rec reverse (A: Type[0]) (n: Nat)
                 (v: Vector A n) on v ≝
  match v return (λm.λv. Vector A m) with
    [ Empty ⇒ Empty A
    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
    ].
    nrewrite < (succ_plus ? ?).
    nrewrite > (plus_zero ?).
    //.
nqed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Conversions to and from lists.                                             *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec list_of_vector (A: Type[0]) (n: Nat)
                        (v: Vector A n) on v ≝
  match v return λn.λv. List A with
    [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    ].
    //.
nqed.

nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
  match l return λl. Vector A (length A l) with
    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
    ].
    nnormalize.
    //.
    //.
nqed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
(* Rotates and shifts.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlet rec rotate_left (A: Type[0]) (n: Nat)
                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
  match m with
    [ Z ⇒ v
    | S o ⇒
        match v with
          [ Empty ⇒ Empty A
          | Cons p hd tl ⇒
             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
          ]
    ].
    nrewrite < (succ_plus ? ?).
    nrewrite > (plus_zero ?).
    //.
nqed.

ndefinition rotate_right ≝
  λA: Type[0].
  λn, m: Nat.
  λv: Vector A n.
    reverse A n (rotate_left A n m (reverse A n v)).
    
ndefinition shift_left_1 ≝
  λA: Type[0].
  λn: Nat.
  λv: Vector A n.
  λa: A.
    match v with
      [ Empty ⇒ ?
      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
      ].
      //.
nqed.

ndefinition shift_right_1 ≝
  λA: Type[0].
  λn: Nat.
  λv: Vector A n.
  λa: A.
    reverse A n (shift_left_1 A n (reverse A n v) a).
    
ndefinition shift_left ≝
  λA: Type[0].
  λn, m: Nat.
  λv: Vector A n.
  λa: A.
    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
    
ndefinition shift_right ≝
  λA: Type[0].
  λn, m: Nat.
  λv: Vector A n.
  λa: A.
    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    
    
nlemma map_fusion:
  ∀A, B, C: Type[0].
  ∀n: Nat.
  ∀v: Vector A n.
  ∀f: A → B.
  ∀g: B → C.
    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
  #A B C n v f g.
  nelim v.
  nnormalize.
  @.
  #N H V H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

nlemma length_correct:
  ∀A: Type[0].
  ∀n: Nat.
  ∀v: Vector A n.
    length A n v = n.
  #A n v.
  nelim v.
  nnormalize.
  @.
  #N H V H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.

nlemma map_length:
  ∀A, B: Type[0].
  ∀n: Nat.
  ∀v: Vector A n.
  ∀f: A → B.
    length A n v = length B n (map A B n f v).
  #A B n v f.
  nelim v.
  nnormalize.
  @.
  #N H V H2.
  nnormalize.
  nrewrite > H2.
  @.
nqed.