(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "Cartesian.ma".
include "Nat.ma".
include "Util.ma".
include "List.ma".

include "logic/pts.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).

notation "hvbox(hd break :: tl)"
  right associative with precedence 52
  for @{ 'Cons $hd $tl }.
  
interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lookup.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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 (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 A B C n f tl ?)
        ]
    ])
    (refl ? n).
      ##
        [ #e;
          ndestruct(e);
          ##
        | ndestruct(e);
          napply tl'
          ##
        ]
nqed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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)
    ].
    
notation "v break @ q"
  right associative with precedence 47
  for @{ 'append $v $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)))
    ].
    //.
nqed.

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

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

nlet rec from_list (A: Type[0]) (l: List A) on l ≝
  match l return λl. Vector A (length A l) with
    [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
    | Cons hd tl ⇒ ? (hd :: (from_list A tl))
    ].
    //.
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))))
          ]
    ].
    //.
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)).
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* 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.

nlemma from_list_to_list_left_inverse:
  ∀A: Type[0].
  ∀l: List A.
    to_list A (length A l) (from_list A l) = l.