 Timestamp:
 Mar 30, 2011, 6:47:35 PM (10 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r724 r726 102 102 false) b c. 103 103 104 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.104 lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. 105 105 (x = y → P true) → 106 106 (x ≠ y → P false) → 
src/ASM/BitVectorTrie.ma
r698 r726 7 7  Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 8 8  Stub: ∀n: nat. BitVectorTrie A n. 9 10 let rec lookup_opt (A: Type[0]) (n: nat) 11 (b: BitVector n) (t: BitVectorTrie A n) on t 12 : option A ≝ 13 (match t return λx.λ_. BitVector x → option A with 14 [ Leaf l ⇒ λ_.Some ? l 15  Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l) 16  Stub _ ⇒ λ_.None ? 17 ]) b. 9 18 10 19 let rec lookup (A: Type[0]) (n: nat) 
src/ASM/Vector.ma
r700 r726 429 429 (* ===================================== *) 430 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 ] with 433 [ 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 ] with 437 [ VEmpty ⇒ I  VCons m hd tl ⇒ tl ]. 438 431 439 let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝ 432 (match b return λx.λ_. n = x → bool with 433 [ VEmpty ⇒ 434 match c return λx.λ_. x = O → bool with 435 [ VEmpty ⇒ λ_. true 436  VCons p hd tl ⇒ λabsd.⊥ 437 ] 438  VCons o hd tl ⇒ 439 match c return λx.λ_. x = S o → bool with 440 [ VEmpty ⇒ λabsd.⊥ 441  VCons p hd' tl' ⇒ 442 λprf. 443 if (f hd hd') then 444 (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉)) 445 else 446 false 447 ] 448 ]) (refl ? n). 449 [1,2: 450 destruct 451  lapply (injective_S … prf); 452 # X 453 < X 454 % 455 ] 456 qed. 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 440 (match b return λx.λ_. Vector A x → bool with 441 [ VEmpty ⇒ λc. 442 match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool  _ ⇒ True ] with 443 [ VEmpty ⇒ true 444  VCons p hd tl ⇒ I 445 ] 446  VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c)) 447 ] 448 ) c. 449 450 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n. 451 match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with 460 452 [ O ⇒ λP.λv.P [[ ]] → P v 461 453  S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 462 454 ] P v. 463 @(λA,n. λP:Vector A n → Prop. λv. match v return455 @(λA,n. λP:Vector A n → Type[0]. λv. match v return 464 456 ? 465 457 with [ VEmpty ⇒ ?  VCons m h t ⇒ ? ] P) … … 469 461 *) 470 462 471 (* dpm: commented out to get out stuff to typecheck *) 472 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 473 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 463 lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f. 464 (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 474 465 ∀n,x,y. 475 466 (x = y → P true) →
Note: See TracChangeset
for help on using the changeset viewer.