Changeset 744 for src/ASM/Vector.ma
- Timestamp:
- Apr 7, 2011, 6:53:59 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Vector.ma
r726 r744 12 12 include "arithmetics/nat.ma". 13 13 14 include "utilities/extranat.ma". 14 15 include "utilities/oldlib/eq.ma". 15 16 … … 152 153 qed. 153 154 154 let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝ 155 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝ 156 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with 157 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ]. 158 159 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝ 160 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with 161 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ]. 162 163 let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝ 155 164 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with 156 165 [ O ⇒ λv. 〈[[ ]], v〉 157 | S m' ⇒ λv. 158 match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with 159 [ VEmpty ⇒ λK. ⊥ 160 | VCons o he tl ⇒ λK. 161 match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with 162 [ pair v1 v2 ⇒ 〈he:::v1, v2〉 163 ] 164 ] (?: (S (m' + n)) = S (m' + n))]. 165 // 166 [ destruct 167 | lapply (injective_S … K) 168 // 169 ] 170 qed. 166 | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉 167 ]. 168 (* Prevent undesirable unfolding. *) 169 let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝ 170 split' A m n v. 171 171 172 172 173 definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝ … … 329 330 (* At some points matita will attempt to reduce reverse with a known vector, 330 331 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. 332 to be fast enough to keep matita usable, so use plus_n_Sm_fast. *) 337 333 338 334 let rec revapp (A: Type[0]) (n: nat) (m:nat) … … 347 343 (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. 348 344 < plus_n_O @refl qed. 345 346 let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝ 347 match n return λn.Vector A (n+m) with 348 [ O ⇒ v 349 | S n' ⇒ a:::(pad_vector A a n' m v) 350 ]. 349 351 350 352 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 404 406 qed. 405 407 408 409 (* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *) 410 definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝ 411 λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ]. 412 406 413 definition shift_right_1 ≝ 407 414 λA: Type[0]. … … 409 416 λv: Vector A (S n). 410 417 λa: A. 411 reverse … (shift_left_1 … (reverse … v) a). 412 413 definition shift_left ≝ 418 let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'. 419 (* reverse … (shift_left_1 … (reverse … v) a).*) 420 421 definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝ 414 422 λA: Type[0]. 415 423 λn, m: nat. 416 λv: Vector A (S n). 417 λa: A. 418 iterate … (λx. shift_left_1 … x a) v m. 424 match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with 425 [ nat_lt _ _ ⇒ λv,a. replicate … a 426 | nat_eq _ ⇒ λv,a. replicate … a 427 | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a)) 428 ]. 429 430 (* iterate … (λx. shift_left_1 … x a) v m.*) 419 431 420 432 definition shift_right ≝ … … 428 440 (* Decidable equality. *) 429 441 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 430 431 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝432 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with433 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].434 435 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝436 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with437 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].438 442 439 443 let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
Note: See TracChangeset
for help on using the changeset viewer.