Ignore:
Timestamp:
Nov 15, 2010, 10:22:41 AM (9 years ago)
Author:
mulligan
Message:

Updated Vector / BitVector? files taken from my Matita library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vector.ma

    r237 r240  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "Cartesian.ma".
    7 include "Nat.ma".
    86include "Util.ma".
    9 include "List.ma".
    10 
    11 include "logic/pts.ma".
     7
     8include "Universes/Universes.ma".
     9
     10include "Datatypes/Nat/Nat.ma".
     11include "Datatypes/Nat/Addition.ma".
     12include "Datatypes/Nat/Order.ma".
     13
     14include "Datatypes/Listlike/List/List.ma".
     15
     16include "Datatypes/Cartesian.ma".
     17
    1218include "Plogic/equality.ma".
    1319
     
    1925  Empty: Vector A Z
    2026| Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
     27
     28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     29(* Syntax.                                                                    *)
     30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2131
    2232notation "hvbox(hd break :: tl)"
     
    2636interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
    2737
     38notation "hvbox (v break !! n)"
     39  non associative with precedence 90
     40  for @{ 'get_index $v $n }.
     41
    2842(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2943(* Lookup.                                                                    *)
    3044(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     45
     46nlet rec get_index (A: Type[0]) (n: Nat)
     47                   (v: Vector A n) (m: Nat) on m ≝
     48  match m with
     49    [ Z ⇒
     50      match v with
     51        [ Empty ⇒ Nothing A
     52        | Cons p hd tl ⇒ Just A hd
     53        ]
     54    | S o ⇒
     55      match v with
     56        [ Empty ⇒ Nothing A
     57        | Cons p hd tl ⇒ get_index A p tl o
     58        ]
     59    ].
     60   
     61interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
     62   
     63nlet rec set_index (A: Type[0]) (n: Nat)
     64                   (v: Vector A n) (m: Nat) (a: A) on m ≝
     65  match m with
     66    [ Z ⇒
     67      match v with
     68        [ Empty ⇒ Nothing (Vector A n)
     69        | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
     70        ]
     71    | S o ⇒
     72      match v with
     73        [ Empty ⇒ Nothing (Vector A n)
     74        | Cons p hd tl ⇒
     75            let settail ≝ set_index A p tl o a in
     76              match settail with
     77                [ Nothing ⇒ Nothing (Vector A n)
     78                | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
     79                ]
     80        ]
     81    ].
     82    //.
     83nqed.
     84
     85nlet rec drop (A: Type[0]) (n: Nat)
     86              (v: Vector A n) (m: Nat) on m ≝
     87  match m with
     88    [ Z ⇒ Just (Vector A n) v
     89    | S o ⇒
     90      match v with
     91        [ Empty ⇒ Nothing (Vector A n)
     92        | Cons p hd tl ⇒ ? (drop A p tl o)
     93        ]
     94    ].
     95    //.
     96nqed.
    3197   
    3298(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    73139nqed.
    74140
    75 nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
     141nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
    76142             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
    77143  (match v return (λx.λr. x = n → Vector C x) with
     
    82148        | Cons m hd' tl' ⇒
    83149            λe: S n = S m.
    84               (f hd hd') :: (zip A B C n f tl ?)
     150              (f hd hd') :: (zip_with A B C n f tl ?)
    85151        ]
    86152    ])
     
    96162nqed.
    97163
     164ndefinition zip ≝
     165  λA, B: Type[0].
     166  λn: Nat.
     167  λv: Vector A n.
     168  λq: Vector B n.
     169    zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
     170
    98171(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    99172(* Building vectors from scratch                                              *)
     
    162235                        (v: Vector A n) on v ≝
    163236  match v return λn.λv. List A with
    164     [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A
    165     | Cons o hd tl ⇒ cic:/matita/Cerco/List/List.con(0,2,1) A hd (list_of_vector A o tl)
    166     ].
     237    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/List/List/List.con(0,1,1) A)
     238    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
     239    ].
     240    //.
     241nqed.
    167242
    168243nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    169244  match l return λl. Vector A (length A l) with
    170     [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     245    [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)
    171246    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
    172247    ].
     
    200275    reverse A n (rotate_left A n m (reverse A n v)).
    201276   
     277ndefinition shift_left_1 ≝
     278  λA: Type[0].
     279  λn: Nat.
     280  λv: Vector A n.
     281  λa: A.
     282    match v with
     283      [ Empty ⇒ ?
     284      | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
     285      ].
     286      //.
     287nqed.
     288
     289ndefinition shift_right_1 ≝
     290  λA: Type[0].
     291  λn: Nat.
     292  λv: Vector A n.
     293  λa: A.
     294    reverse A n (shift_left_1 A n (reverse A n v) a).
     295   
     296ndefinition shift_left ≝
     297  λA: Type[0].
     298  λn, m: Nat.
     299  λv: Vector A n.
     300  λa: A.
     301    iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
     302   
     303ndefinition shift_right ≝
     304  λA: Type[0].
     305  λn, m: Nat.
     306  λv: Vector A n.
     307  λa: A.
     308    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
     309   
    202310(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    203311(* Lemmas.                                                                    *)
Note: See TracChangeset for help on using the changeset viewer.