- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVector.ma
r990 r1516 29 29 30 30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??)//31 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); // 32 32 #n #hd #tl #abs @⊥ destruct (abs) 33 33 qed. … … 35 35 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 36 36 ∃hd.∃tl.v ≃ VCons bool n hd tl. 37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))37 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 38 38 [ #abs @⊥ destruct (abs) 39 39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] … … 132 132 (x ≠ y → P false) → 133 133 P (eq_bv n x y). 134 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)134 #P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf) 135 135 #Q * *; normalize /3/ 136 136 qed. … … 177 177 ∀n, v, q. 178 178 eq_bv n v q = true → v = q. 179 #n #v #q generalize in match v 179 #n #v #q generalize in match v; 180 180 elim q 181 181 [ #v #h @BitVector_O … … 184 184 #hd' * #tl' #jmeq >jmeq in h; 185 185 #new_h 186 change in new_h with ((andb ? ?) = ?);186 change in new_h; with ((andb ? ?) = ?); 187 187 cases(conjunction_true … new_h) 188 188 #eq_heads #eq_tails … … 190 190 cases(eq_b_eq … eq_heads) 191 191 whd in eq_tails:(??(?????(%))?); 192 change in eq_tails with (eq_bv ??? = ?);192 change in eq_tails; with (eq_bv ??? = ?); 193 193 <(ih tl') // 194 194 ] -
src/ASM/BitVectorTrie.ma
r1479 r1516 61 61 (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q. 62 62 #A #n #f #t #P #Q #H 63 generalize in match (refl ? n) generalize in match H -H; generalize in match Q -Q; generalize in match P-P;64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?) 63 generalize in match (refl ? n); generalize in match H; -H; generalize in match Q; -Q; generalize in match P; -P; 64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?); 65 65 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP) 66 66 | #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?) … … 79 79 ∀P: Prop. 80 80 (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P. 81 #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H -H; generalize in match P-P;82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) -t81 #A #n #f #t #P #H generalize in match (refl ? n); generalize in match H; -H; generalize in match P; -P; 82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?); -t 83 83 [ #a #f #P #Hf #_ normalize @(Hf [[]]) 84 84 | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x))) … … 107 107 | #n #t' #X #Y #HXY #HX %1 108 108 [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ] 109 | whd in Hl @Hl ]109 | whd in Hl; @Hl ] 110 110 qed. 111 111 … … 170 170 ∀P:BitVector n → A → Prop. 171 171 forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a. 172 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)172 #A #n #t #P generalize in match (refl ? n); elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?); 173 173 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf) 174 174 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b) … … 306 306 lemma BitVectorTrie_O: 307 307 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 308 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))308 #A #v generalize in match (refl … O); cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)); 309 309 [ #w #_ %1 %[@w] % 310 310 | #n #l #r #abs @⊥ destruct(abs) … … 314 314 lemma BitVectorTrie_Sn: 315 315 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 316 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)316 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%); 317 317 [ #m #abs @⊥ destruct(abs) 318 318 | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // … … 350 350 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 351 351 #A #a #v #n #c elim c -c -n 352 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //352 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; // 353 353 | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 354 354 #t cases(BitVectorTrie_Sn … t) 355 355 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 356 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //356 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 357 357 | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 358 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize358 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize 359 359 [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]] 360 360 qed. … … 363 363 ∀A.∀n.∀b.∀a. 364 364 lookup A n b (Stub A ?) a = a. 365 #A #n #b #a cases n in b ⊢ (??(??%%%?)?) 365 #A #n #b #a cases n in b ⊢ (??(??%%%?)?); 366 366 [ #b >(BitVector_O b) normalize @refl 367 367 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd … … 375 375 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 376 376 lookup_opt A n b t = None A → ∀x.lookup A n b t x = x. 377 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)377 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?); 378 378 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct 379 379 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb … … 389 389 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 390 390 lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a. 391 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)391 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?); 392 392 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl 393 393 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb … … 403 403 ∀A.∀n.∀b.∀t.∀x,a. 404 404 lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a. 405 #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)405 #A #n #b #t #x #a generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ?); 406 406 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl 407 407 | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB … … 436 436 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 437 437 lookup_opt … b (insert … b v t) = Some A v. 438 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?) 438 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?); 439 439 [ #x #b >(BitVector_O b) normalize @refl 440 440 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd … … 442 442 | normalize @Hl 443 443 ] 444 | #n' #b cases n' in b ⊢ ? 444 | #n' #b cases n' in b ⊢ ?; 445 445 [ #b >(BitVector_O b) normalize @refl 446 446 | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd … … 454 454 (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t. 455 455 #A #v #n #c elim c -c -n 456 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //456 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; // 457 457 | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 458 458 #t cases(BitVectorTrie_Sn … t) 459 459 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 460 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //460 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 461 461 | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 462 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize462 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize 463 463 [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]] 464 464 qed. … … 476 476 ] 477 477 | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize 478 [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %) #Heq3478 [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3 479 479 [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 // 480 |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H 480 |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H; 481 481 [1,3: #X %1 // 482 482 |2,4: >Heq3 // … … 499 499 ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P. 500 500 lookup_opt A n b t = (None A) → forall A n (insert A n b a t) P → forall A n t P. 501 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)501 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%); 502 502 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct 503 503 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H … … 527 527 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop). 528 528 (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P. 529 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)529 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ? → ??%%% → ?); 530 530 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ] 531 531 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf … … 565 565 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P. 566 566 forall A n t P → P b a → forall A n (insert A n b a t) P. 567 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%)567 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%); 568 568 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/ 569 569 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP … … 587 587 ] 588 588 ] 589 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%) 589 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%); 590 590 [ #b #P #Hf #HP normalize %1 [ @HP | // ] 591 591 | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP) … … 603 603 ] 604 604 | #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t) 605 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?) 605 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?); 606 606 #X lapply (option_map_none … X) @IH 607 607 | #E >E normalize // … … 622 622 cases (BitVectorTrie_Sn … t) 623 623 [ * #t1 * #t2 #E' >E' 624 whd in ⊢ (??%? → ??%?) cases bhd #U624 whd in ⊢ (??%? → ??%?); cases bhd #U 625 625 cases (option_map_some ????? U) 626 626 #tn' * #U' #E'' <E'' 627 whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)627 whd in ⊢ (??%?); whd in ⊢ (??(???%%)?); 628 628 @(IH … U') 629 629 | #E >E normalize #E' destruct … … 642 642 @(vector_inv_n … b) #bhd #btl 643 643 cases (BitVectorTrie_Sn … t) 644 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd644 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?); cases bhd 645 645 #U cases (option_map_some ????? U) #tn' * #U' #E' <E' 646 646 #b' @(vector_inv_n … b') #bhd' #btl' 647 647 cases bhd' 648 648 [ 2,3: #_ @refl 649 | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))650 @(IH … U') % #E'' >E'' in NE * #H @H @refl649 | *: #NE whd in ⊢ (??%%); whd in ⊢ (??(???%%)(???%%)); 650 @(IH … U') % #E'' >E'' in NE; * #H @H @refl 651 651 ] 652 | #E >E whd in ⊢ (??%? → ?) #NE destruct652 | #E >E whd in ⊢ (??%? → ?); #NE destruct 653 653 ] 654 654 ] qed. -
src/ASM/BitVectorZ.ma
r891 r1516 58 58 #n #bv elim bv 59 59 [ // 60 | #m * #t #IH whd in ⊢ (??%) //60 | #m * #t #IH whd in ⊢ (??%); // 61 61 ] qed. 62 62 … … 109 109 | #tl #_ normalize @le_S_S 110 110 change with (? ≤ pos_length one + m) 111 generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl111 generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl 112 112 [ // | #o * #t normalize #IH #p <plus_n_Sm 113 113 change with (? ≤ pos_length (p1 p) + o) … … 145 145 theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n. 146 146 #n #bv @(vector_inv_n ? (S n) ? bv) * 147 [ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))147 [ #t whd in ⊢ (?%%); lapply (bv_Z_unsigned_min … (negation_bv n t)) 148 148 cases (Z_of_unsigned_bitvector n (negation_bv n t)) // 149 149 #p * 150 | #t whd in ⊢ (?%?) //150 | #t whd in ⊢ (?%?); // 151 151 ] qed. -
src/ASM/Status.ma
r1515 r1516 916 916 @ le_S_S 917 917 lapply (le_n n) 918 generalize in ⊢ (?%? → ?(??%?)?) 919 elim n in ⊢ (∀_:?. ??% → ?(?%??)?) 918 generalize in ⊢ (?%? → ?(??%?)?); 919 elim n in ⊢ (∀_:?. ??% → ?(?%??)?); 920 920 [ normalize 921 921 #n … … 924 924 [ // 925 925 | #H #K 926 inversion K926 @(le_inv_ind ?? K …) 927 927 [ # H1 928 928 < H1 … … 946 946 # x # K1 947 947 lapply (le_S_S_to_le … K1) 948 generalize in match m 948 generalize in match m; 949 949 elim x 950 950 normalize … … 955 955 // 956 956 # q # K2 957 applyH957 @H 958 958 /3/ 959 959 ] -
src/ASM/Util.ma
r1323 r1516 219 219 #ABSURD 220 220 elim (ABSURD nil_absurd) 221 | normalize in cons_proof 221 | normalize in cons_proof; 222 222 @le_S_S_to_le 223 223 assumption … … 275 275 | 3: normalize 276 276 generalize in match (sig2 … (reduce_strong A B tl tl1)); 277 >p2 >p3 >p4 normalize in ⊢ (% → ?) 277 >p2 >p3 >p4 normalize in ⊢ (% → ?); 278 278 #HYP // 279 279 ] … … 377 377 ∀a:A. 378 378 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 379 #A #a #P #H #x #p 380 generalize in match H 381 generalize in match P 382 cases p 383 // 379 #A #a #P #H #x #p lapply H lapply P cases p // 384 380 qed. 385 381 … … 400 396 @ p 401 397 | 4: 402 normalize in prf2 398 normalize in prf2; 403 399 normalize 404 400 @ le_S_S_to_le … … 562 558 #A #B #H #acc #suff elim suff 563 559 [ #pre >append_nil % 564 | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]560 | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ] 565 561 qed. 566 562 -
src/ASM/Vector.ma
r1330 r1516 60 60 ]) lt. 61 61 [ cases (not_le_Sn_O O) 62 normalize in absd1 62 normalize in absd1; 63 63 # H 64 64 cases (H absd1) 65 65 | cases (not_le_Sn_O (S o)) 66 normalize in prf 66 normalize in prf; 67 67 # H 68 68 cases (H prf) 69 69 | normalize 70 normalize in prf 70 normalize in prf; 71 71 @ le_S_S_to_le 72 72 assumption … … 474 474 | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 475 475 ] P v. 476 #A #n #P #v generalize in matchP cases v normalize //476 #A #n #P #v lapply P cases v normalize // 477 477 qed. 478 478 … … 487 487 normalize /2/ 488 488 | #m #h #t #IH #y @(vector_inv_n … y) 489 #h' #t' #Ht #Hf whd in ⊢ (?%) 489 #h' #t' #Ht #Hf whd in ⊢ (?%); 490 490 @(f_elim ? h h') #Eh 491 491 [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ] … … 497 497 #A #f #f_true #n #v elim v 498 498 [ // 499 | #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl499 | #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl 500 500 ] qed. 501 501 … … 508 508 [ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl 509 509 | #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t' 510 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/510 #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/ 511 511 ] qed. 512 512
Note: See TracChangeset
for help on using the changeset viewer.