Changeset 240


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

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

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r238 r240  
    11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    22(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
    3 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    4 
    5 include "Vector.ma".
    6 include "List.ma".
    7 include "Nat.ma".
    8 include "Bool.ma".
     3(*               Most functions are specialised versions of those found in    *)
     4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
     5(*               BitVector variants.                                          *)
     6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     7
     8include "Universes/Universes.ma".
     9
     10include "Datatypes/Listlike/Vector/Vector.ma".
     11include "Datatypes/Listlike/List/List.ma".
     12
     13include "Datatypes/Nat/Nat.ma".
     14include "Datatypes/Nat/Addition.ma".
     15include "Datatypes/Nat/Division_Modulus.ma".
     16include "Datatypes/Nat/Exponential.ma".
     17
     18include "Datatypes/Bool.ma".
    919
    1020(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    2030
    2131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     32(* Lookup.                                                                    *)
     33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     34
     35ndefinition get_index ≝
     36  λn: Nat.
     37  λb: BitVector n.
     38  λm: Nat.
     39    get_index Bool n b m.
     40   
     41interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
     42   
     43ndefinition set_index ≝
     44  λn: Nat.
     45  λb: BitVector n.
     46  λm: Nat.
     47    set_index Bool n b m.
     48   
     49ndefinition drop ≝
     50  λn: Nat.
     51  λb: BitVector n.
     52  λm: Nat.
     53    drop Bool n b m.
     54
     55(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2256(* Creating bitvectors from scratch.                                          *)
    2357(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    3670  λc: BitVector n.
    3771    append Bool m n b c.
     72   
     73interpretation "BitVector append" 'append b c = (append b c).
    3874
    3975ndefinition pad ≝
     
    4278    let padding ≝ replicate Bool m False in
    4379      append Bool m n padding b.
     80     
     81(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     82(* Other manipulations.                                                       *)
     83(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     84
     85ndefinition reverse ≝
     86  λn: Nat.
     87  λb: BitVector n.
     88    reverse Bool n b.
     89
     90ndefinition length ≝
     91  λn: Nat.
     92  λb: BitVector n.
     93    length Bool n b.
    4494
    4595(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    51101  λb: BitVector n.
    52102  λc: BitVector n.
    53     zip Bool Bool Bool n conjunction b c.
     103    zip_with Bool Bool Bool n conjunction b c.
     104   
     105interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
    54106   
    55107ndefinition inclusive_disjunction ≝
     
    57109  λb: BitVector n.
    58110  λc: BitVector n.
    59     zip Bool Bool Bool n inclusive_disjunction b c.
     111    zip_with Bool Bool Bool n inclusive_disjunction b c.
     112   
     113interpretation "BitVector inclusive disjunction"
     114  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
    60115         
    61116ndefinition exclusive_disjunction ≝
     
    63118  λb: BitVector n.
    64119  λc: BitVector n.
    65     zip Bool Bool Bool n exclusive_disjunction b c.
    66    
    67 ndefinition complement ≝
     120    zip_with Bool Bool Bool n exclusive_disjunction b c.
     121   
     122interpretation "BitVector exclusive disjunction"
     123  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
     124   
     125ndefinition negation ≝
    68126  λn: Nat.
    69127  λb: BitVector n.
    70128    map Bool Bool n (negation) b.
     129   
     130interpretation "BitVector negation" 'negation b c = (negation ? b c).
    71131
    72132(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    82142  λm, n: Nat.
    83143  λb: BitVector n.
    84     rotate_right Bool n m b.   
     144    rotate_right Bool n m b.
     145   
     146ndefinition shift_left ≝
     147  λm, n: Nat.
     148  λb: BitVector n.
     149  λc: Bool.
     150    shift_left Bool n m b c.
     151   
     152ndefinition shift_right ≝
     153  λm, n: Nat.
     154  λb: BitVector n.
     155  λc: Bool.
     156    shift_right Bool n m b c.
    85157   
    86158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    129201    | Cons o hd tl ⇒
    130202      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
    131         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     203        ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl
    132204    ].
  • 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.