Changeset 374 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 5, 2010, 11:54:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r373 r374 12 12 13 13 ninductive Vector (A: Type[0]): Nat → Type[0] ≝ 14 Empty: Vector A Z15  Cons: ∀n: Nat. A → Vector A n → Vector A (S n).14 VEmpty: Vector A Z 15  VCons: ∀n: Nat. A → Vector A n → Vector A (S n). 16 16 17 17 (* ===================================== *) … … 27 27 for ${fold right @'vnil rec acc @{'vcons $x $acc}}. 28 28 29 interpretation "Vector vnil" 'vnil = ( Empty ?).30 interpretation "Vector vcons" 'vcons hd tl = ( Cons ? ? hd tl).29 interpretation "Vector vnil" 'vnil = (VEmpty ?). 30 interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl). 31 31 32 32 notation "hvbox(l break !!! break n)" … … 43 43 [ Z ⇒ 44 44 match v return λx.λ_. Z < x → A with 45 [ Empty ⇒ λabsd1: Z < Z. ?46  Cons p hd tl ⇒ λprf1: Z < S p. hd45 [ VEmpty ⇒ λabsd1: Z < Z. ? 46  VCons p hd tl ⇒ λprf1: Z < S p. hd 47 47 ] 48 48  S o ⇒ 49 49 (match v return λx.λ_. S o < x → A with 50 [ Empty ⇒ λprf: S o < Z. ?51  Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?50 [ VEmpty ⇒ λprf: S o < Z. ? 51  VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ? 52 52 ]) 53 53 ]) lt. … … 73 73 [ Z ⇒ 74 74 match v with 75 [ Empty ⇒ Nothing A76  Cons p hd tl ⇒ Just A hd75 [ VEmpty ⇒ Nothing A 76  VCons p hd tl ⇒ Just A hd 77 77 ] 78 78  S o ⇒ 79 79 match v with 80 [ Empty ⇒ Nothing A81  Cons p hd tl ⇒ get_index_weak_v A p tl o80 [ VEmpty ⇒ Nothing A 81  VCons p hd tl ⇒ get_index_weak_v A p tl o 82 82 ] 83 83 ]. … … 89 89 [ Z ⇒ 90 90 match v return λx.λ_. Z < x → Vector A x with 91 [ Empty ⇒ λabsd1: Z < Z. Empty A92  Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)91 [ VEmpty ⇒ λabsd1: Z < Z. [[ ]] 92  VCons p hd tl ⇒ λprf1: Z < S p. (a ::: tl) 93 93 ] 94 94  S o ⇒ 95 95 (match v return λx.λ_. S o < x → Vector A x with 96 [ Empty ⇒ λprf: S o < Z. Empty A97  Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)96 [ VEmpty ⇒ λprf: S o < Z. [[ ]] 97  VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?) 98 98 ]) 99 99 ]) lt. … … 107 107 [ Z ⇒ 108 108 match v with 109 [ Empty ⇒ Nothing (Vector A n)110  Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))109 [ VEmpty ⇒ Nothing (Vector A n) 110  VCons o hd tl ⇒ Just (Vector A n) (? (VCons A o a tl)) 111 111 ] 112 112  S o ⇒ 113 113 match v with 114 [ Empty ⇒ Nothing (Vector A n)115  Cons p hd tl ⇒114 [ VEmpty ⇒ Nothing (Vector A n) 115  VCons p hd tl ⇒ 116 116 let settail ≝ set_index_weak A p tl o a in 117 117 match settail with 118 118 [ Nothing ⇒ Nothing (Vector A n) 119  Just j ⇒ Just (Vector A n) (? ( Cons A p hd j))119  Just j ⇒ Just (Vector A n) (? (VCons A p hd j)) 120 120 ] 121 121 ] … … 130 130  S o ⇒ 131 131 match v with 132 [ Empty ⇒ Nothing (Vector A n)133  Cons p hd tl ⇒ ? (drop A p tl o)132 [ VEmpty ⇒ Nothing (Vector A n) 133  VCons p hd tl ⇒ ? (drop A p tl o) 134 134 ] 135 135 ]. … … 144 144  S m' ⇒ λv. 145 145 match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with 146 [ Empty ⇒ λK.⊥147  Cons o he tl ⇒ λK.148 match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with146 [ VEmpty ⇒ λK.⊥ 147  VCons o he tl ⇒ λK. 148 match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with 149 149 [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 150 150 // [ ndestruct  nlapply (S_inj … K); //] … … 154 154 ≝ λA,n,v. 155 155 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with 156 [ Empty ⇒ λK.⊥157  Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉156 [ VEmpty ⇒ λK.⊥ 157  VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉 158 158 ] (? : S ? = S ?). 159 159 // [ ndestruct  nlapply (S_inj … K); //] … … 170 170 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 171 171 match v with 172 [ Empty ⇒ x173  Cons n hd tl ⇒ f hd (fold_right A B n f x tl)172 [ VEmpty ⇒ x 173  VCons n hd tl ⇒ f hd (fold_right A B n f x tl) 174 174 ]. 175 175 … … 178 178 (v: Vector A n) (q: Vector B n) on v : C n ≝ 179 179 (match v return λx.λ_. x = n → C n with 180 [ Empty ⇒180 [ VEmpty ⇒ 181 181 match q return λx.λ_. Z = x → C x with 182 [ Empty ⇒ λprf: Z = Z. c183  Cons o hd tl ⇒ λabsd. ⊥184 ] 185  Cons o hd tl ⇒182 [ VEmpty ⇒ λprf: Z = Z. c 183  VCons o hd tl ⇒ λabsd. ⊥ 184 ] 185  VCons o hd tl ⇒ 186 186 match q return λx.λ_. S o = x → C x with 187 [ Empty ⇒ λabsd: S o = Z. ⊥188  Cons p hd' tl' ⇒ λprf: S o = S p.189 (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉187 [ VEmpty ⇒ λabsd: S o = Z. ⊥ 188  VCons p hd' tl' ⇒ λprf: S o = S p. 189 (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉ 190 190 ] 191 191 ]) (refl ? n). … … 196 196 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 197 197 match v with 198 [ Empty ⇒ x199  Cons n hd tl ⇒ f (fold_left A B n f x tl) hd198 [ VEmpty ⇒ x 199  VCons n hd tl ⇒ f (fold_left A B n f x tl) hd 200 200 ]. 201 201 … … 207 207 (f: A → B) (v: Vector A n) on v ≝ 208 208 match v with 209 [ Empty ⇒ Empty B210  Cons n hd tl ⇒ (f hd) ::: (map A B n f tl)209 [ VEmpty ⇒ [[ ]] 210  VCons n hd tl ⇒ (f hd) ::: (map A B n f tl) 211 211 ]. 212 212 … … 214 214 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ 215 215 (match v return (λx.λr. x = n → Vector C x) with 216 [ Empty ⇒ λ_. Empty C217  Cons n hd tl ⇒216 [ VEmpty ⇒ λ_. [[ ]] 217  VCons n hd tl ⇒ 218 218 match q return (λy.λr. S n = y → Vector C (S n)) with 219 [ Empty ⇒ ?220  Cons m hd' tl' ⇒219 [ VEmpty ⇒ ? 220  VCons m hd' tl' ⇒ 221 221 λe: S n = S m. 222 222 (f hd hd') ::: (zip_with A B C n f tl ?) … … 247 247 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝ 248 248 match n return λn. Vector A n with 249 [ Z ⇒ Empty A249 [ Z ⇒ [[ ]] 250 250  S m ⇒ h ::: (replicate A m h) 251 251 ]. … … 254 254 (v: Vector A n) (q: Vector A m) on v ≝ 255 255 match v return (λn.λv. Vector A (n + m)) with 256 [ Empty ⇒ q257  Cons o hd tl ⇒ hd ::: (append A o m tl q)256 [ VEmpty ⇒ q 257  VCons o hd tl ⇒ hd ::: (append A o m tl q) 258 258 ]. 259 259 … … 268 268 a ::: 269 269 (match v with 270 [ Empty ⇒Empty A271  Cons o hd tl ⇒ scan_left A B o f (f a hd) tl270 [ VEmpty ⇒ VEmpty A 271  VCons o hd tl ⇒ scan_left A B o f (f a hd) tl 272 272 ]). 273 273 … … 275 275 (f: A → B → A) (b: B) (v: Vector A n) on v ≝ 276 276 match v with 277 [ Empty ⇒ ?278  Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)277 [ VEmpty ⇒ ? 278  VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl) 279 279 ]. 280 280 //. … … 284 284 (* Other manipulations. *) 285 285 (* ===================================== *) 286 287 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝288 match v with289 [ Empty ⇒ Z290  Cons n hd tl ⇒ S $ length A n tl291 ].292 286 293 287 nlet rec reverse (A: Type[0]) (n: Nat) 294 288 (v: Vector A n) on v ≝ 295 289 match v return (λm.λv. Vector A m) with 296 [ Empty ⇒ Empty A297  Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))290 [ VEmpty ⇒ [[ ]] 291  VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) 298 292 ]. 299 293 nrewrite < (succ_plus ? ?). … … 309 303 (v: Vector A n) on v ≝ 310 304 match v return λn.λv. List A with 311 [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A) 312  Cons o hd tl ⇒ hd :: (list_of_vector A o tl) 313 ]. 314 //. 315 nqed. 305 [ VEmpty ⇒ [] 306  VCons o hd tl ⇒ hd :: (list_of_vector A o tl) 307 ]. 316 308 317 309 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝ 318 310 match l return λl. Vector A (length A l) with 319 [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A) 320  Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl)) 321 ]. 322 nnormalize. 323 //. 324 //. 325 nqed. 311 [ Empty ⇒ [[ ]] 312  Cons hd tl ⇒ hd ::: (vector_of_list A tl) 313 ]. 326 314 327 315 (* ===================================== *) … … 335 323  S o ⇒ 336 324 match v with 337 [ Empty ⇒ Empty A338  Cons p hd tl ⇒339 rotate_left A (S p) o ( ? (append A p ? tl (Cons A ? hd (Empty A))))325 [ VEmpty ⇒ [[ ]] 326  VCons p hd tl ⇒ 327 rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S Z) ↦ Vector A (S p)⌉) 340 328 ] 341 329 ]. 342 nrewrite < (succ_plus ? ?). 343 nrewrite > (plus_zero ?). 344 //. 330 //. 345 331 nqed. 346 332 … … 350 336 λv: Vector A n. 351 337 reverse A n (rotate_left A n m (reverse A n v)). 352 338 353 339 ndefinition shift_left_1 ≝ 354 340 λA: Type[0]. 355 341 λn: Nat. 356 λv: Vector A n.342 λv: Vector A (S n). 357 343 λa: A. 358 match vwith359 [ Empty ⇒ ?360  Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))361 ].362 //.344 match v return λy.λ_. y = S n → Vector A y with 345 [ VEmpty ⇒ λH.⊥ 346  VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl) 347 ] (refl ? (S n)). 348 ndestruct. 363 349 nqed. 364 350 … … 366 352 λA: Type[0]. 367 353 λn: Nat. 368 λv: Vector A n.354 λv: Vector A (S n). 369 355 λa: A. 370 reverse A n (shift_left_1 A n (reverse A nv) a).356 reverse … (shift_left_1 … (reverse … v) a). 371 357 372 358 ndefinition shift_left ≝ 373 359 λA: Type[0]. 374 360 λn, m: Nat. 375 λv: Vector A n.361 λv: Vector A (S n). 376 362 λa: A. 377 iterate (Vector A n) (λx. shift_left_1 A nx a) v m.363 iterate … (λx. shift_left_1 … x a) v m. 378 364 379 365 ndefinition shift_right ≝ 380 366 λA: Type[0]. 381 367 λn, m: Nat. 382 λv: Vector A n.368 λv: Vector A (S n). 383 369 λa: A. 384 iterate (Vector A n) (λx. shift_right_1 A nx a) v m.370 iterate … (λx. shift_right_1 … x a) v m. 385 371 386 372 (* ===================================== *) … … 388 374 (* ===================================== *) 389 375 390 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b ≝376 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool ≝ 391 377 (match b return λx.λ_. n = x → Bool with 392 [ Empty ⇒378 [ VEmpty ⇒ 393 379 match c return λx.λ_. x = Z → Bool with 394 [ Empty ⇒ λ_. true395  Cons p hd tl ⇒ λabsd.?396 ] 397  Cons o hd tl ⇒380 [ VEmpty ⇒ λ_. true 381  VCons p hd tl ⇒ λabsd.⊥ 382 ] 383  VCons o hd tl ⇒ 398 384 match c return λx.λ_. x = S o → Bool with 399 [ Empty ⇒ λabsd. ?400  Cons p hd' tl' ⇒385 [ VEmpty ⇒ λabsd.⊥ 386  VCons p hd' tl' ⇒ 401 387 λprf. 402 388 if (f hd hd') then 403 (eq_v A o f tl ?)389 (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉)) 404 390 else 405 391 false … … 407 393 ]) (refl ? n). 408 394 ##[##1,2: ndestruct 409  nlapply (S_inj … prf); #X; nrewrite < X; 410 napply tl' ] 395  nlapply (S_inj … prf); #X; nrewrite < X; @] 411 396 nqed. 412 397 … … 452 437 @. 453 438 nqed. 454 455 nlemma length_correct:456 ∀A: Type[0].457 ∀n: Nat.458 ∀v: Vector A n.459 length A n v = n.460 #A n v.461 nelim v.462 nnormalize.463 @.464 #N H V H2.465 nnormalize.466 nrewrite > H2.467 @.468 nqed.469 470 nlemma map_length:471 ∀A, B: Type[0].472 ∀n: Nat.473 ∀v: Vector A n.474 ∀f: A → B.475 length A n v = length B n (map A B n f v).476 #A B n v f.477 nelim v.478 nnormalize.479 @.480 #N H V H2.481 nnormalize.482 nrewrite > H2.483 @.484 nqed.
Note: See TracChangeset
for help on using the changeset viewer.