Changeset 240 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 15, 2010, 10:22:41 AM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r238 r240 1 1 (* ===================================== *) 2 2 (* 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 8 include "Universes/Universes.ma". 9 10 include "Datatypes/Listlike/Vector/Vector.ma". 11 include "Datatypes/Listlike/List/List.ma". 12 13 include "Datatypes/Nat/Nat.ma". 14 include "Datatypes/Nat/Addition.ma". 15 include "Datatypes/Nat/Division_Modulus.ma". 16 include "Datatypes/Nat/Exponential.ma". 17 18 include "Datatypes/Bool.ma". 9 19 10 20 (* ===================================== *) … … 20 30 21 31 (* ===================================== *) 32 (* Lookup. *) 33 (* ===================================== *) 34 35 ndefinition get_index ≝ 36 λn: Nat. 37 λb: BitVector n. 38 λm: Nat. 39 get_index Bool n b m. 40 41 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 42 43 ndefinition set_index ≝ 44 λn: Nat. 45 λb: BitVector n. 46 λm: Nat. 47 set_index Bool n b m. 48 49 ndefinition drop ≝ 50 λn: Nat. 51 λb: BitVector n. 52 λm: Nat. 53 drop Bool n b m. 54 55 (* ===================================== *) 22 56 (* Creating bitvectors from scratch. *) 23 57 (* ===================================== *) … … 36 70 λc: BitVector n. 37 71 append Bool m n b c. 72 73 interpretation "BitVector append" 'append b c = (append b c). 38 74 39 75 ndefinition pad ≝ … … 42 78 let padding ≝ replicate Bool m False in 43 79 append Bool m n padding b. 80 81 (* ===================================== *) 82 (* Other manipulations. *) 83 (* ===================================== *) 84 85 ndefinition reverse ≝ 86 λn: Nat. 87 λb: BitVector n. 88 reverse Bool n b. 89 90 ndefinition length ≝ 91 λn: Nat. 92 λb: BitVector n. 93 length Bool n b. 44 94 45 95 (* ===================================== *) … … 51 101 λb: BitVector n. 52 102 λc: BitVector n. 53 zip Bool Bool Bool n conjunction b c. 103 zip_with Bool Bool Bool n conjunction b c. 104 105 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c). 54 106 55 107 ndefinition inclusive_disjunction ≝ … … 57 109 λb: BitVector n. 58 110 λ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 113 interpretation "BitVector inclusive disjunction" 114 'inclusive_disjunction b c = (inclusive_disjunction ? b c). 60 115 61 116 ndefinition exclusive_disjunction ≝ … … 63 118 λb: BitVector n. 64 119 λ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 122 interpretation "BitVector exclusive disjunction" 123 'exclusive_disjunction b c = (exclusive_disjunction ? b c). 124 125 ndefinition negation ≝ 68 126 λn: Nat. 69 127 λb: BitVector n. 70 128 map Bool Bool n (negation) b. 129 130 interpretation "BitVector negation" 'negation b c = (negation ? b c). 71 131 72 132 (* ===================================== *) … … 82 142 λm, n: Nat. 83 143 λb: BitVector n. 84 rotate_right Bool n m b. 144 rotate_right Bool n m b. 145 146 ndefinition shift_left ≝ 147 λm, n: Nat. 148 λb: BitVector n. 149 λc: Bool. 150 shift_left Bool n m b c. 151 152 ndefinition shift_right ≝ 153 λm, n: Nat. 154 λb: BitVector n. 155 λc: Bool. 156 shift_right Bool n m b c. 85 157 86 158 (* ===================================== *) … … 129 201  Cons o hd tl ⇒ 130 202 let hdval ≝ match hd with [ True ⇒ S Z  False ⇒ Z ] in 131 ((exponential (S (S Z)) o) *hdval) + nat_of_bitvector o tl203 ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl 132 204 ]. 
Deliverables/D4.1/Matita/Vector.ma
r237 r240 4 4 (* ===================================== *) 5 5 6 include "Cartesian.ma".7 include "Nat.ma".8 6 include "Util.ma". 9 include "List.ma". 10 11 include "logic/pts.ma". 7 8 include "Universes/Universes.ma". 9 10 include "Datatypes/Nat/Nat.ma". 11 include "Datatypes/Nat/Addition.ma". 12 include "Datatypes/Nat/Order.ma". 13 14 include "Datatypes/Listlike/List/List.ma". 15 16 include "Datatypes/Cartesian.ma". 17 12 18 include "Plogic/equality.ma". 13 19 … … 19 25 Empty: Vector A Z 20 26  Cons: ∀n: Nat. A → Vector A n → Vector A (S n). 27 28 (* ===================================== *) 29 (* Syntax. *) 30 (* ===================================== *) 21 31 22 32 notation "hvbox(hd break :: tl)" … … 26 36 interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl). 27 37 38 notation "hvbox (v break !! n)" 39 non associative with precedence 90 40 for @{ 'get_index $v $n }. 41 28 42 (* ===================================== *) 29 43 (* Lookup. *) 30 44 (* ===================================== *) 45 46 nlet 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 61 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n). 62 63 nlet 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 //. 83 nqed. 84 85 nlet 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 //. 96 nqed. 31 97 32 98 (* ===================================== *) … … 73 139 nqed. 74 140 75 nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)141 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) 76 142 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ 77 143 (match v return (λx.λr. x = n → Vector C x) with … … 82 148  Cons m hd' tl' ⇒ 83 149 λ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 ?) 85 151 ] 86 152 ]) … … 96 162 nqed. 97 163 164 ndefinition 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 98 171 (* ===================================== *) 99 172 (* Building vectors from scratch *) … … 162 235 (v: Vector A n) on v ≝ 163 236 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 //. 241 nqed. 167 242 168 243 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝ 169 244 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) 171 246  Cons hd tl ⇒ ? (hd :: (vector_of_list A tl)) 172 247 ]. … … 200 275 reverse A n (rotate_left A n m (reverse A n v)). 201 276 277 ndefinition 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 //. 287 nqed. 288 289 ndefinition 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 296 ndefinition 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 303 ndefinition 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 202 310 (* ===================================== *) 203 311 (* Lemmas. *)
Note: See TracChangeset
for help on using the changeset viewer.