Changeset 535 for Deliverables/D3.1/Csemantics/cerco/Vector.ma
 Timestamp:
 Feb 16, 2011, 4:25:02 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Vector.ma
r534 r535 12 12 include "arithmetics/nat.ma". 13 13 14 include "oldlib/eq.ma". 14 15 15 16 (* ===================================== *) … … 319 320 (* ===================================== *) 320 321 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. 322 (* At some points matita will attempt to reduce reverse with a known vector, 323 which reduces the equality proof for the cast. Normalising this proof needs 324 to be fast enough to keep matita usable. *) 325 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ 326 match n return λn'.∀m.S(n'+m) = n'+S m with 327 [ O ⇒ λm.refl ?? 328  S n' ⇒ λm. ? 329 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. 330 331 let rec revapp (A: Type[0]) (n: nat) (m:nat) 332 (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝ 333 match v return λn'.λ_. Vector A (n' + m) with 334 [ VEmpty ⇒ acc 335  VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ 336 ]. 337 > plus_n_Sm_fast @refl qed. 338 339 let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝ 340 (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. 341 < plus_n_O @refl qed. 329 342 330 343 (* ===================================== *) … … 436 449 qed. 437 450 451 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. 452 match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with 453 [ O ⇒ λP.λv.P [[ ]] → P v 454  S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 455 ] P v. 456 @(λA,n. λP:Vector A n → Prop. λv. match v return 457 ? 458 with [ VEmpty ⇒ ?  VCons m h t ⇒ ? ] P) 459 [ //  // ] qed. 460 (* XXX Proof below fails at qed. 461 #A #n #P * [ #H @H  #m #h #t #H @H ] qed. 462 *) 463 464 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 465 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 466 ∀n,x,y. 467 (x = y → P true) → 468 (x ≠ y → P false) → 469 P (eq_v A n f x y). 470 #P #A #f #f_elim #n #x elim x 471 [ #y @(vector_inv_n … y) 472 normalize /2/ 473  #m #h #t #IH #y @(vector_inv_n … y) 474 #h' #t' #Ht #Hf whd in ⊢ (?%) 475 @(f_elim ? h h') #Eh 476 [ @IH [ #Et @Ht >Eh >Et @refl  #NEt @Hf % #E' destruct (E') elim NEt /2/ ] 477  @Hf % #E' destruct (E') elim Eh /2/ 478 ] 479 ] qed. 480 438 481 (* ===================================== *) 439 482 (* Subvectors. *)
Note: See TracChangeset
for help on using the changeset viewer.