Changeset 465 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r374 r465 4 4 (* ===================================== *) 5 5 6 include "Nat.ma". 7 include "List.ma". 6 include "datatypes/list.ma". 7 include "basics/bool.ma". 8 include "datatypes/sums.ma". 9 10 include "Util.ma". 11 12 include "arithmetics/nat.ma". 13 8 14 9 15 (* ===================================== *) … … 11 17 (* ===================================== *) 12 18 13 ninductive Vector (A: Type[0]): Nat → Type[0] ≝14 VEmpty: Vector A Z15  VCons: ∀n: Nat. A → Vector A n → Vector A (S n).19 ninductive Vector (A: Type[0]): nat → Type[0] ≝ 20 VEmpty: Vector A O 21  VCons: ∀n: nat. A → Vector A n → Vector A (S n). 16 22 17 23 (* ===================================== *) … … 38 44 (* ===================================== *) 39 45 40 nlet rec get_index_v (A: Type[0]) (n: Nat)41 (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝46 nlet rec get_index_v (A: Type[0]) (n: nat) 47 (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝ 42 48 (match m with 43 [ Z⇒44 match v return λx.λ_. Z< x → A with45 [ VEmpty ⇒ λabsd1: Z < Z. ?46  VCons p hd tl ⇒ λprf1: Z< S p. hd49 [ O ⇒ 50 match v return λx.λ_. O < x → A with 51 [ VEmpty ⇒ λabsd1: O < O. ? 52  VCons p hd tl ⇒ λprf1: O < S p. hd 47 53 ] 48 54  S o ⇒ 49 55 (match v return λx.λ_. S o < x → A with 50 [ VEmpty ⇒ λprf: S o < Z. ?56 [ VEmpty ⇒ λprf: S o < O. ? 51 57  VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ? 52 58 ]) 53 59 ]) lt. 54 ##[ ncases (not hing_less_than_Z Z); #K; ncases (K absd1)55 ## ncases (not hing_less_than_Z (S o)); #K; ncases (K prf)56 ## n apply succ_less_than_injective; nassumption60 ##[ ncases (not_le_Sn_O O); nnormalize in absd1; #H; ncases (H absd1); 61 ## ncases (not_le_Sn_O (S o)); nnormalize in prf; #H; ncases (H prf); 62 ## nnormalize; nnormalize in prf; napply le_S_S_to_le; nassumption; 57 63 ##] 58 64 nqed. … … 60 66 ndefinition get_index' ≝ 61 67 λA: Type[0]. 62 λn, m: Nat.68 λn, m: nat. 63 69 λb: Vector A (S (n + m)). 64 70 get_index_v A (S (n + m)) b n ?. 65 71 nnormalize; 66 napply less_than_or_equal_monotone; 67 napply less_than_or_equal_plus; 68 nqed. 69 70 nlet rec get_index_weak_v (A: Type[0]) (n: Nat) 71 (v: Vector A n) (m: Nat) on m ≝ 72 //; 73 nqed. 74 75 nlet rec get_index_weak_v (A: Type[0]) (n: nat) 76 (v: Vector A n) (m: nat) on m ≝ 72 77 match m with 73 [ Z⇒78 [ O ⇒ 74 79 match v with 75 [ VEmpty ⇒ No thingA76  VCons p hd tl ⇒ JustA hd80 [ VEmpty ⇒ None A 81  VCons p hd tl ⇒ Some A hd 77 82 ] 78 83  S o ⇒ 79 84 match v with 80 [ VEmpty ⇒ No thingA85 [ VEmpty ⇒ None A 81 86  VCons p hd tl ⇒ get_index_weak_v A p tl o 82 87 ] … … 85 90 interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n). 86 91 87 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝92 nlet rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝ 88 93 (match m with 89 [ Z⇒90 match v return λx.λ_. Z< x → Vector A x with91 [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]92  VCons p hd tl ⇒ λprf1: Z< S p. (a ::: tl)94 [ O ⇒ 95 match v return λx.λ_. O < x → Vector A x with 96 [ VEmpty ⇒ λabsd1: O < O. [[ ]] 97  VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl) 93 98 ] 94 99  S o ⇒ 95 100 (match v return λx.λ_. S o < x → Vector A x with 96 [ VEmpty ⇒ λprf: S o < Z. [[ ]]101 [ VEmpty ⇒ λprf: S o < O. [[ ]] 97 102  VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?) 98 103 ]) 99 104 ]) lt. 100 n apply succ_less_than_injective.101 nassumption.102 nqed. 103 104 nlet rec set_index_weak (A: Type[0]) (n: Nat)105 (v: Vector A n) (m: Nat) (a: A) on m ≝105 nnormalize in prf ⊢ %; 106 /2/; 107 nqed. 108 109 nlet rec set_index_weak (A: Type[0]) (n: nat) 110 (v: Vector A n) (m: nat) (a: A) on m ≝ 106 111 match m with 107 [ Z⇒112 [ O ⇒ 108 113 match v with 109 [ VEmpty ⇒ No thing(Vector A n)110  VCons o hd tl ⇒ Just(Vector A n) (? (VCons A o a tl))114 [ VEmpty ⇒ None (Vector A n) 115  VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl)) 111 116 ] 112 117  S o ⇒ 113 118 match v with 114 [ VEmpty ⇒ No thing(Vector A n)119 [ VEmpty ⇒ None (Vector A n) 115 120  VCons p hd tl ⇒ 116 121 let settail ≝ set_index_weak A p tl o a in 117 122 match settail with 118 [ No thing ⇒ Nothing(Vector A n)119  Just j ⇒ Just(Vector A n) (? (VCons A p hd j))123 [ None ⇒ None (Vector A n) 124  Some j ⇒ Some (Vector A n) (? (VCons A p hd j)) 120 125 ] 121 126 ] … … 124 129 nqed. 125 130 126 nlet rec drop (A: Type[0]) (n: Nat)127 (v: Vector A n) (m: Nat) on m ≝131 nlet rec drop (A: Type[0]) (n: nat) 132 (v: Vector A n) (m: nat) on m ≝ 128 133 match m with 129 [ Z ⇒ Just(Vector A n) v134 [ O ⇒ Some (Vector A n) v 130 135  S o ⇒ 131 136 match v with 132 [ VEmpty ⇒ No thing(Vector A n)137 [ VEmpty ⇒ None (Vector A n) 133 138  VCons p hd tl ⇒ ? (drop A p tl o) 134 139 ] … … 137 142 nqed. 138 143 139 nlet rec split (A: Type[0]) (m,n: Nat) on m140 : Vector A ( m+n) → (Vector A m) × (Vector A n)144 nlet rec split (A: Type[0]) (m,n: nat) on m 145 : Vector A (plus m n) → (Vector A m) × (Vector A n) 141 146 ≝ 142 match m return λm. Vector A ( m+n) → (Vector A m) × (Vector A n) with143 [ Z⇒ λv.〈[[ ]], v〉147 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with 148 [ O ⇒ λv.〈[[ ]], v〉 144 149  S m' ⇒ λv. 145 match v return λl.λ_:Vector A l.l = S ( m' +n) → (Vector A (S m')) × (Vector A n) with150 match v return λl.λ_:Vector A l.l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with 146 151 [ VEmpty ⇒ λK.⊥ 147 152  VCons o he tl ⇒ λK. 148 153 match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with 149 [ mk_ Cartesianv1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].150 // [ ndestruct  nlapply ( S_inj… K); //]154 [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 155 // [ ndestruct  nlapply (injective_S … K); //] 151 156 nqed. 152 157 … … 157 162  VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉 158 163 ] (? : S ? = S ?). 159 // [ ndestruct  nlapply ( S_inj… K); //]160 nqed. 161 162 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝163 λA,v. f irst … (head … v).164 // [ ndestruct  nlapply (injective_S … K); //] 165 nqed. 166 167 ndefinition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝ 168 λA,v. fst … (head … v). 164 169 165 170 (* ===================================== *) … … 167 172 (* ===================================== *) 168 173 169 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)174 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat) 170 175 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 171 176 match v with … … 174 179 ]. 175 180 176 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])177 (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)181 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0]) 182 (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat) 178 183 (v: Vector A n) (q: Vector B n) on v : C n ≝ 179 184 (match v return λx.λ_. x = n → C n with 180 185 [ VEmpty ⇒ 181 match q return λx.λ_. Z= x → C x with182 [ VEmpty ⇒ λprf: Z = Z. c186 match q return λx.λ_. O = x → C x with 187 [ VEmpty ⇒ λprf: O = O. c 183 188  VCons o hd tl ⇒ λabsd. ⊥ 184 189 ] 185 190  VCons o hd tl ⇒ 186 191 match q return λx.λ_. S o = x → C x with 187 [ VEmpty ⇒ λabsd: S o = Z. ⊥192 [ VEmpty ⇒ λabsd: S o = O. ⊥ 188 193  VCons p hd' tl' ⇒ λprf: S o = S p. 189 194 (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 195 ] 191 196 ]) (refl ? n). 192 ##[##1,2: ndestruct  ##3,4: nlapply ( S_inj… prf); // ]197 ##[##1,2: ndestruct  ##3,4: nlapply (injective_S … prf); // ] 193 198 nqed. 194 199 195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)200 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat) 196 201 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 197 202 match v with … … 204 209 (* ===================================== *) 205 210 206 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)211 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) 207 212 (f: A → B) (v: Vector A n) on v ≝ 208 213 match v with … … 211 216 ]. 212 217 213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)218 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat) 214 219 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ 215 220 (match v return (λx.λr. x = n → Vector C x) with … … 228 233 ndestruct(e); 229 234 ## 230  nlapply ( S_inj… e); #H; nrewrite > H;235  nlapply (injective_S … e); #H; nrewrite > H; 231 236 napply tl' 232 237 ## … … 236 241 ndefinition zip ≝ 237 242 λA, B: Type[0]. 238 λn: Nat.243 λn: nat. 239 244 λv: Vector A n. 240 245 λq: Vector B n. 241 zip_with A B ( Cartesian A B) n (mk_CartesianA B) v q.246 zip_with A B (A × B) n (mk_pair A B) v q. 242 247 243 248 (* ===================================== *) … … 245 250 (* ===================================== *) 246 251 247 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝252 nlet rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝ 248 253 match n return λn. Vector A n with 249 [ Z⇒ [[ ]]254 [ O ⇒ [[ ]] 250 255  S m ⇒ h ::: (replicate A m h) 251 256 ]. 252 257 253 nlet rec append (A: Type[0]) (n: Nat) (m: Nat) 258 (* DPM: fixme. Weird matita bug in base case. *) 259 nlet rec append (A: Type[0]) (n: nat) (m: nat) 254 260 (v: Vector A n) (q: Vector A m) on v ≝ 255 261 match v return (λn.λv. Vector A (n + m)) with 256 [ VEmpty ⇒ q262 [ VEmpty ⇒ (? q) 257 263  VCons o hd tl ⇒ hd ::: (append A o m tl q) 258 264 ]. 265 #H; nassumption; 266 nqed. 259 267 260 268 notation "hvbox(l break @@ r)" … … 264 272 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 265 273 266 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)274 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: nat) 267 275 (f: A → B → A) (a: A) (v: Vector B n) on v ≝ 268 276 a ::: … … 272 280 ]). 273 281 274 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)282 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: nat) 275 283 (f: A → B → A) (b: B) (v: Vector A n) on v ≝ 276 284 match v with … … 285 293 (* ===================================== *) 286 294 287 nlet rec reverse (A: Type[0]) (n: Nat)295 nlet rec reverse (A: Type[0]) (n: nat) 288 296 (v: Vector A n) on v ≝ 289 297 match v return (λm.λv. Vector A m) with … … 291 299  VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) 292 300 ]. 293 nrewrite < (succ_plus ? ?). 294 nrewrite > (plus_zero ?). 295 //. 301 //; 296 302 nqed. 297 303 … … 300 306 (* ===================================== *) 301 307 302 nlet rec list_of_vector (A: Type[0]) (n: Nat)308 nlet rec list_of_vector (A: Type[0]) (n: nat) 303 309 (v: Vector A n) on v ≝ 304 match v return λn.λv. List A with310 match v return λn.λv. list A with 305 311 [ VEmpty ⇒ [] 306 312  VCons o hd tl ⇒ hd :: (list_of_vector A o tl) 307 313 ]. 308 314 309 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝315 nlet rec vector_of_list (A: Type[0]) (l: list A) on l ≝ 310 316 match l return λl. Vector A (length A l) with 311 [ Empty⇒ [[ ]]312  Cons hd tl ⇒ hd ::: (vector_of_list A tl)317 [ nil ⇒ [[ ]] 318  cons hd tl ⇒ hd ::: (vector_of_list A tl) 313 319 ]. 314 320 … … 317 323 (* ===================================== *) 318 324 319 nlet rec rotate_left (A: Type[0]) (n: Nat)320 (m: Nat) (v: Vector A n) on m: Vector A n ≝325 nlet rec rotate_left (A: Type[0]) (n: nat) 326 (m: nat) (v: Vector A n) on m: Vector A n ≝ 321 327 match m with 322 [ Z⇒ v328 [ O ⇒ v 323 329  S o ⇒ 324 330 match v with 325 331 [ VEmpty ⇒ [[ ]] 326 332  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)⌉)333 rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉) 328 334 ] 329 335 ]. … … 333 339 ndefinition rotate_right ≝ 334 340 λA: Type[0]. 335 λn, m: Nat.341 λn, m: nat. 336 342 λv: Vector A n. 337 343 reverse A n (rotate_left A n m (reverse A n v)). … … 339 345 ndefinition shift_left_1 ≝ 340 346 λA: Type[0]. 341 λn: Nat.347 λn: nat. 342 348 λv: Vector A (S n). 343 349 λa: A. … … 351 357 ndefinition shift_right_1 ≝ 352 358 λA: Type[0]. 353 λn: Nat.359 λn: nat. 354 360 λv: Vector A (S n). 355 361 λa: A. … … 358 364 ndefinition shift_left ≝ 359 365 λA: Type[0]. 360 λn, m: Nat.366 λn, m: nat. 361 367 λv: Vector A (S n). 362 368 λa: A. … … 365 371 ndefinition shift_right ≝ 366 372 λA: Type[0]. 367 λn, m: Nat.373 λn, m: nat. 368 374 λv: Vector A (S n). 369 375 λa: A. … … 374 380 (* ===================================== *) 375 381 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 ≝377 (match b return λx.λ_. n = x → Bool with382 nlet rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝ 383 (match b return λx.λ_. n = x → bool with 378 384 [ VEmpty ⇒ 379 match c return λx.λ_. x = Z → Bool with385 match c return λx.λ_. x = O → bool with 380 386 [ VEmpty ⇒ λ_. true 381 387  VCons p hd tl ⇒ λabsd.⊥ 382 388 ] 383 389  VCons o hd tl ⇒ 384 match c return λx.λ_. x = S o → Bool with390 match c return λx.λ_. x = S o → bool with 385 391 [ VEmpty ⇒ λabsd.⊥ 386 392  VCons p hd' tl' ⇒ … … 393 399 ]) (refl ? n). 394 400 ##[##1,2: ndestruct 395  nlapply ( S_inj… prf); #X; nrewrite < X; @]401  nlapply (injective_S … prf); #X; nrewrite < X; @] 396 402 nqed. 397 403 … … 402 408 ndefinition mem ≝ 403 409 λA: Type[0]. 404 λeq_a : A → A → Bool.405 λn: Nat.410 λeq_a : A → A → bool. 411 λn: nat. 406 412 λl: Vector A n. 407 413 λx: A. 408 fold_right … (λy,v. inclusive_disjunction (eq_a x y)v) false l.414 fold_right … (λy,v. (eq_a x y) ∨ v) false l. 409 415 410 416 ndefinition subvector_with ≝ 411 417 λA: Type[0]. 412 λn: Nat.413 λm: Nat.414 λf: A → A → Bool.418 λn: nat. 419 λm: nat. 420 λf: A → A → bool. 415 421 λv: Vector A n. 416 422 λq: Vector A m. 417 fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x)v) true v.423 fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v. 418 424 419 425 (* ===================================== *) … … 423 429 nlemma map_fusion: 424 430 ∀A, B, C: Type[0]. 425 ∀n: Nat.431 ∀n: nat. 426 432 ∀v: Vector A n. 427 433 ∀f: A → B.
Note: See TracChangeset
for help on using the changeset viewer.