Ignore:
Timestamp:
Nov 11, 2010, 12:27:04 PM (9 years ago)
Author:
mulligan
Message:

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File:
1 edited

Legend:

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

    r230 r231  
    1010include "logic/pts.ma".
    1111include "Plogic/equality.ma".
     12
     13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     14(* The datatype.                                                              *)
     15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1216
    1317ninductive Vector (A: Type[0]): Nat → Type[0] ≝
     
    2125interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
    2226
     27(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     28(* Lookup.                                                                    *)
     29(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     30   
     31(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     32(* Folds and builds.                                                          *)
     33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     34   
     35nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
     36                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
     37  match v with
     38    [ Empty ⇒ x
     39    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
     40    ].
     41   
     42nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
     43                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
     44  match v with
     45    [ Empty ⇒ x
     46    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
     47    ].
     48   
     49(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     50(* Maps and zips.                                                             *)
     51(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     52
    2353nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
    2454             (f: A → B) (v: Vector A n) on v ≝
     
    2757    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
    2858    ].
    29    
    30 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
    31                     (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    32   match v with
    33     [ Empty ⇒ x
    34     | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
    35     ].
    36    
    37 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
    38                     (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    39   match v with
    40     [ Empty ⇒ x
    41     | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
    42     ].
    43    
    44 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
    45   match v with
    46     [ Empty ⇒ Z
    47     | Cons n hd tl ⇒ S $ length A n tl
    48     ].
    49 
    50 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
    51   match n return λn. Vector A n with
    52     [ Z ⇒ Empty A
    53     | S m ⇒ h :: (replicate A m h)
    54     ].
    55    
     59
     60(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
     61   currently in there.
     62*)
    5663nlemma eq_rect_Type0_r :
    5764  ∀A: Type[0].
     
    8895nqed.
    8996
     97(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     98(* Building vectors from scratch                                              *)
     99(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     100
     101nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
     102  match n return λn. Vector A n with
     103    [ Z ⇒ Empty A
     104    | S m ⇒ h :: (replicate A m h)
     105    ].
     106
    90107nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
    91108                (v: Vector A n) (q: Vector A m) on v ≝
     
    94111    | Cons o hd tl ⇒ hd :: (append A o m tl q)
    95112    ].
     113   
     114notation "v break @ q"
     115  right associative with precedence 47
     116  for @{ 'append $v $q }.
     117 
     118interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
     119   
     120nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
     121                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
     122  a ::
     123    (match v with
     124       [ Empty ⇒ Empty A
     125       | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
     126       ]).
     127
     128nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
     129                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
     130  match v with
     131    [ Empty ⇒ ?
     132    | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
     133    ].
     134    //.
     135nqed.
     136   
     137(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     138(* Other manipulations.                                                       *)
     139(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     140   
     141nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
     142  match v with
     143    [ Empty ⇒ Z
     144    | Cons n hd tl ⇒ S $ length A n tl
     145    ].
    96146
    97147nlet rec reverse (A: Type[0]) (n: Nat)
     
    104154nqed.
    105155
     156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     157(* Conversions to and from lists.                                             *)
     158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     159
    106160nlet rec to_list (A: Type[0]) (n: Nat)
    107161                 (v: Vector A n) on v ≝
     
    110164    | Cons o hd tl ⇒ hd :: (to_list A o tl)
    111165    ].
    112    
    113 nlet rec rotate_left (A: Type[0]) (n: Nat) (v: Vector A n)
    114                      (m: Nat) on m: Vector A n ≝
     166
     167nlet rec from_list (A: Type[0]) (l: List A) on l ≝
     168  match l return λl. Vector A (length A l) with
     169    [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
     170    | Cons hd tl ⇒ ? (hd :: (from_list A tl))
     171    ].
     172    //.
     173nqed.
     174
     175(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     176(* Rotates and shifts.                                                        *)
     177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     178   
     179nlet rec rotate_left (A: Type[0]) (n: Nat)
     180                     (m: Nat) (v: Vector A n) on m: Vector A n ≝
    115181  match m with
    116182    [ Z ⇒ v
     
    119185          [ Empty ⇒ Empty A
    120186          | Cons p hd tl ⇒
    121              rotate_left A (S p) (? (append A p ? tl (Cons A ? hd (Empty A)))) o
     187             rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
    122188          ]
    123189    ].
    124190    //.
    125191nqed.
     192
     193ndefinition rotate_right ≝
     194  λA: Type[0].
     195  λn, m: Nat.
     196  λv: Vector A n.
     197    reverse A n (rotate_left A n m (reverse A n v)).
     198   
     199(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     200(* Lemmas.                                                                    *)
     201(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
    126202   
    127203nlemma map_fusion:
     
    172248  @.
    173249nqed.
     250
     251nlemma from_list_to_list_left_inverse:
     252  ∀A: Type[0].
     253  ∀l: List A.
     254    to_list A (length A l) (from_list A l) = l.
Note: See TracChangeset for help on using the changeset viewer.