Changeset 697 for src/ASM/Vector.ma
Legend:
- Unmodified
- Added
- Removed
-
src/ASM
-
Property
svn:mergeinfo
set to
(toggle deleted branches)
/src/Clight/cerco merged eligible /Deliverables/D3.1/C-semantics/cerco 531-693 /Deliverables/D4.1/Matita/new-matita-development 476-530
-
Property
svn:mergeinfo
set to
(toggle deleted branches)
-
src/ASM/Vector.ma
r690 r697 6 6 include "basics/list.ma". 7 7 include "basics/bool.ma". 8 include "basics/ sums.ma".8 include "basics/types.ma". 9 9 10 10 include "cerco/Util.ma". … … 12 12 include "arithmetics/nat.ma". 13 13 14 include "oldlib/eq.ma". 14 15 15 16 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 159 160 | VCons o he tl ⇒ λK. 160 161 match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with 161 [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉162 [ pair v1 v2 ⇒ 〈he:::v1, v2〉 162 163 ] 163 164 ] (?: (S (m' + n)) = S (m' + n))]. … … 200 201 ]. 201 202 203 let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat) 204 (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝ 205 match v with 206 [ VEmpty ⇒ x 207 | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl) 208 ]. 209 202 210 let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0]) 203 211 (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat) … … 228 236 match v with 229 237 [ VEmpty ⇒ x 230 | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd238 | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl 231 239 ]. 232 240 … … 269 277 λv: Vector A n. 270 278 λq: Vector B n. 271 zip_with A B (A × B) n ( mk_pair A B) v q.279 zip_with A B (A × B) n (pair A B) v q. 272 280 273 281 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 319 327 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 320 328 321 let rec reverse (A: Type[0]) (n: nat) 322 (v: Vector A n) on v ≝ 323 match v return (λm.λv. Vector A m) with 324 [ VEmpty ⇒ [[ ]] 325 | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) 326 ]. 327 // 328 qed. 329 (* At some points matita will attempt to reduce reverse with a known vector, 330 which reduces the equality proof for the cast. Normalising this proof needs 331 to be fast enough to keep matita usable. *) 332 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ 333 match n return λn'.∀m.S(n'+m) = n'+S m with 334 [ O ⇒ λm.refl ?? 335 | S n' ⇒ λm. ? 336 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. 337 338 let rec revapp (A: Type[0]) (n: nat) (m:nat) 339 (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝ 340 match v return λn'.λ_. Vector A (n' + m) with 341 [ VEmpty ⇒ acc 342 | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ 343 ]. 344 > plus_n_Sm_fast @refl qed. 345 346 let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝ 347 (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. 348 < plus_n_O @refl qed. 329 349 330 350 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 436 456 qed. 437 457 458 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. 459 match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with 460 [ O ⇒ λP.λv.P [[ ]] → P v 461 | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 462 ] P v. 463 @(λA,n. λP:Vector A n → Prop. λv. match v return 464 ? 465 with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P) 466 [ // | // ] qed. 467 (* XXX Proof below fails at qed. 468 #A #n #P * [ #H @H | #m #h #t #H @H ] qed. 469 *) 470 471 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 472 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 473 ∀n,x,y. 474 (x = y → P true) → 475 (x ≠ y → P false) → 476 P (eq_v A n f x y). 477 #P #A #f #f_elim #n #x elim x 478 [ #y @(vector_inv_n … y) 479 normalize /2/ 480 | #m #h #t #IH #y @(vector_inv_n … y) 481 #h' #t' #Ht #Hf whd in ⊢ (?%) 482 @(f_elim ? h h') #Eh 483 [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ] 484 | @Hf % #E' destruct (E') elim Eh /2/ 485 ] 486 ] qed. 487 438 488 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 439 489 (* Subvectors. *)
Note: See TracChangeset
for help on using the changeset viewer.