Changeset 240 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 15, 2010, 10:22:41 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.