 Timestamp:
 Jun 27, 2012, 3:30:58 PM (8 years ago)
 Location:
 src/ASM
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2119 r2121 3 3 include "ASM/StatusProofs.ma". 4 4 include alias "arithmetics/nat.ma". 5 6 lemma mem_monotonic_wrt_append:7 ∀A: Type[0].8 ∀m, o: nat.9 ∀eq: A → A → bool.10 ∀reflex: ∀a. eq a a = true.11 ∀p: Vector A m.12 ∀a: A.13 ∀r: Vector A o.14 mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.15 #A #m #o #eq #reflex #p #a16 elim p try (#r #assm assumption)17 #m' #hd #tl #inductive_hypothesis #r #assm18 normalize19 cases (eq ??) try %20 @inductive_hypothesis assumption21 qed.22 23 lemma subvector_multiple_append:24 ∀A: Type[0].25 ∀o, n: nat.26 ∀eq: A → A → bool.27 ∀refl: ∀a. eq a a = true.28 ∀h: Vector A o.29 ∀v: Vector A n.30 ∀m: nat.31 ∀q: Vector A m.32 bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).33 #A #o #n #eq #reflex #h #v34 elim v try (normalize #m #irrelevant @I)35 #m' #hd #tl #inductive_hypothesis #m #q36 change with (bool_to_Prop (andb ??))37 cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)38 [1:39 @mem_monotonic_wrt_append try assumption40 @mem_monotonic_wrt_append try assumption41 normalize >reflex %42 2:43 #assm >assm44 >vector_cons_append45 change with (bool_to_Prop (subvector_with ??????))46 @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))47 try @associative_plus48 @inductive_hypothesis49 ]50 qed.51 52 lemma vector_cons_empty:53 ∀A: Type[0].54 ∀n: nat.55 ∀v: Vector A n.56 [[ ]] @@ v = v.57 #A #n #v58 cases v try %59 #n' #hd #tl %60 qed.61 5 62 6 lemma is_in_monotonic_wrt_append: … … 93 37 qed. 94 38 39 (*CSC: move elsewhere *) 95 40 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ 96 41 λa, b: addressing_mode. … … 161 106 ]. 162 107 163 lemma eq_bv_refl: 164 ∀n, b. 165 eq_bv n b b = true. 166 #n #b cases b // 167 qed. 168 169 lemma eq_b_refl: 170 ∀b. 171 eq_b b b = true. 172 #b cases b // 173 qed. 174 108 (*CSC: move elsewhere *) 175 109 lemma eq_addressing_mode_refl: 176 110 ∀a. eq_addressing_mode a a = true. … … 181 115 qed. 182 116 117 (*CSC: move elsewhere *) 183 118 definition eq_sum: 184 119 ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ … … 197 132 ]. 198 133 134 (*CSC: move elsewhere *) 199 135 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ 200 136 λlt, rt, leq, req, left, right. … … 203 139 leq l l' ∧ req r r'. 204 140 141 (*CSC: move elsewhere *) 205 142 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ 206 143 λi, j. … … 417 354 ]. 418 355 356 (*CSC: move elsewhere *) 419 357 lemma eq_sum_refl: 420 358 ∀A, B: Type[0]. … … 428 366 qed. 429 367 368 (*CSC: move elsewhere *) 430 369 lemma eq_prod_refl: 431 370 ∀A, B: Type[0]. … … 442 381 qed. 443 382 383 (*CSC: move elsewhere *) 444 384 lemma eq_preinstruction_refl: 445 385 ∀i. … … 546 486 qed. 547 487 488 (*CSC: move elsewhere *) 548 489 definition eq_instruction: instruction → instruction → bool ≝ 549 490 λi, j. … … 591 532 ]. 592 533 534 (*CSC: move elsewhere *) 593 535 lemma eq_instruction_refl: 594 536 ∀i. eq_instruction i i = true. … … 604 546 λA,n,eq,v,a. mem A eq (S n) v a. 605 547 606 definition tech_if_vect_member ≝ 607 λn,l,am,H. 608 bool_inv_rect_Type0 (vect_member … n … eq_a l am) ? H (λ_.True). 609 548 (*CSC: move elsewhere*) 610 549 definition is_in_cons_elim: 611 550 ∀len.∀hd,tl.∀m:addressing_mode … … 616 555 qed. 617 556 618 lemma vsplit_zero: 619 ∀A,m. 620 ∀v: Vector A m. 621 〈[[]], v〉 = vsplit A 0 m v. 622 #A #m #v 623 cases v try % 624 #n #hd #tl % 625 qed. 626 627 lemma Vector_O: 628 ∀A: Type[0]. 629 ∀v: Vector A 0. 630 v ≃ VEmpty A. 631 #A #v 632 generalize in match (refl … 0); 633 cases v in ⊢ (??%? → ?%%??); // 634 #n #hd #tl #absurd 635 destruct(absurd) 636 qed. 637 638 lemma Vector_Sn: 639 ∀A: Type[0]. 640 ∀n: nat. 641 ∀v: Vector A (S n). 642 ∃hd: A. ∃tl: Vector A n. 643 v ≃ VCons A n hd tl. 644 #A #n #v 645 generalize in match (refl … (S n)); 646 cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 647 [1: 648 #absurd destruct(absurd) 649 2: 650 #m #hd #tl #eq 651 <(injective_S … eq) 652 %{hd} %{tl} % 653 ] 654 qed. 655 656 lemma vector_append_zero: 657 ∀A,m. 658 ∀v: Vector A m. 659 ∀q: Vector A 0. 660 v = q@@v. 661 #A #m #v #q 662 >(Vector_O A q) % 663 qed. 664 557 (*CSC: move elsewhere*) 665 558 lemma prod_eq_left: 666 559 ∀A: Type[0]. … … 671 564 qed. 672 565 566 (*CSC: move elsewhere*) 673 567 lemma prod_eq_right: 674 568 ∀A: Type[0]. … … 677 571 #A #p #q #r #hyp 678 572 destruct % 679 qed.680 681 corollary prod_vector_zero_eq_left:682 ∀A, n.683 ∀q: Vector A O.684 ∀r: Vector A n.685 〈q, r〉 = 〈[[ ]], r〉.686 #A #n #q #r687 generalize in match (Vector_O A q …);688 #hyp destruct %689 qed.690 691 lemma tail_head:692 ∀a: Type[0].693 ∀m, n: nat.694 ∀hd: a.695 ∀l: Vector a m.696 ∀r: Vector a n.697 tail a ? (hd:::(l@@r)) = l@@r.698 #a #m #n #hd #l #r699 cases l try %700 #m' #hd' #tl' %701 qed.702 703 lemma head_head':704 ∀a: Type[0].705 ∀m: nat.706 ∀hd: a.707 ∀l: Vector a m.708 hd = head' … (hd:::l).709 #a #m #hd #l cases l try %710 #m' #hd' #tl %711 qed.712 713 lemma vsplit_succ:714 ∀A: Type[0].715 ∀m, n: nat.716 ∀l: Vector A m.717 ∀r: Vector A n.718 ∀v: Vector A (m + n).719 ∀hd: A.720 v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).721 #A #m722 elim m723 [1:724 #n #l #r #v #hd #eq #hyp725 destruct >(Vector_O … l) %726 2:727 #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp728 destruct729 cases (Vector_Sn … l) #hd' #tl'730 whd in ⊢ (???%);731 >tail_head732 <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))733 try (<hyp <head_head' %)734 elim l normalize //735 ]736 qed.737 738 lemma vsplit_prod:739 ∀A: Type[0].740 ∀m, n: nat.741 ∀p: Vector A (m + n).742 ∀v: Vector A m.743 ∀q: Vector A n.744 p = v@@q → 〈v, q〉 = vsplit A m n p.745 #A #m elim m746 [1:747 #n #p #v #q #hyp748 >hyp <(vector_append_zero A n q v)749 >(prod_vector_zero_eq_left A …)750 @vsplit_zero751 2:752 #r #ih #n #p #v #q #hyp753 >hyp754 cases (Vector_Sn A r v) #hd #exists755 cases exists #tl #jmeq756 >jmeq @vsplit_succ try %757 @ih %758 ]759 qed.760 761 definition vsplit_elim:762 ∀A: Type[0].763 ∀l, m: nat.764 ∀v: Vector A (l + m).765 ∀P: (Vector A l) × (Vector A m) → Prop.766 (∀vl: Vector A l.767 ∀vm: Vector A m.768 v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝769 λa: Type[0].770 λl, m: nat.771 λv: Vector a (l + m).772 λP. ?.773 cases daemon774 573 qed. 775 574 … … 785 584 ]. 786 585 586 (*CSC: move elsewhere *) 787 587 lemma add_bitvector_of_nat_Sm: 788 588 ∀n, m: nat. … … 824 624 qed. 825 625 626 (*CSC: move elsewhere*) 826 627 lemma destruct_bug_fix_1: 827 628 ∀n: nat. … … 830 631 qed. 831 632 633 (*CSC: move elsewhere*) 832 634 lemma destruct_bug_fix_2: 833 635 ∀m, n: nat. … … 836 638 qed. 837 639 640 (*CSC: move elsewhere*) 838 641 definition bitvector_3_cases: 839 642 ∀b: BitVector 3. … … 884 687 qed. 885 688 689 (*CSC: move elsewhere*) 886 690 lemma bitvector_3_elim_prop: 887 691 ∀P: BitVector 3 → Prop. … … 947 751 ]. 948 752 753 (*CSC: move elsewhere*) 949 754 lemma option_destruct_Some: 950 755 ∀A: Type[0]. … … 955 760 qed. 956 761 762 (*CSC: move elsewhere*) 957 763 lemma eq_instruction_to_eq: 958 764 ∀i1, i2: instruction. … … 1623 1429 ticks_of0 program sigma policy ppc fetched. 1624 1430 1431 (*CSC: move elsewhere*) 1625 1432 lemma eq_rect_Type1_r: 1626 1433 ∀A: Type[1]. … … 1633 1440 qed. 1634 1441 1635 axiom vsplit_append: 1636 ∀A: Type[0]. 1637 ∀m, n: nat. 1638 ∀v, v': Vector A m. 1639 ∀q, q': Vector A n. 1640 let 〈v', q'〉 ≝ vsplit A m n (v@@q) in 1641 v = v' ∧ q = q'. 1642 1643 lemma vsplit_vector_singleton: 1644 ∀A: Type[0]. 1645 ∀n: nat. 1646 ∀v: Vector A (S n). 1647 ∀rest: Vector A n. 1648 ∀s: Vector A 1. 1649 v = s @@ rest → 1650 ((get_index_v A ? v 0 ?) ::: rest) = v. 1651 [1: 1652 #A #n #v cases daemon (* XXX: !!! *) 1653 2: 1654 @le_S_S @le_O_n 1655 ] 1656 qed. 1657 1442 (*CSC: move elsewhere*) 1658 1443 example sub_minus_one_seven_eight: 1659 1444 ∀v: BitVector 7. … … 1792 1577 *) 1793 1578 1579 (*CSC: move elsewhere*) 1794 1580 lemma Some_Some_elim: 1795 1581 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P. … … 1797 1583 qed. 1798 1584 1585 (*CSC: move elsewhere*) 1799 1586 lemma pair_destruct_right: 1800 1587 ∀A: Type[0]. … … 1856 1643 qed. 1857 1644 1645 (*CSC: move elsewhere*) 1858 1646 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. 1859 1647 /2/ 
src/ASM/AssemblyProofSplit.ma
r2114 r2121 170 170 qed. 171 171 172 (*CSC: move elsewhere*) 172 173 lemma pair_replace: 173 174 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → … … 326 327 qed. 327 328 329 (*CSC: move elsewhere*) 328 330 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 329 331 #P #A #a #abs destruct … … 359 361 include alias "ASM/BitVectorTrie.ma". 360 362 363 (*CSC: move elsewhere*) 361 364 lemma jmpair_as_replace: 362 365 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c. … … 375 378 qed. 376 379 380 (*CSC: move elsewhere*) 377 381 lemma if_then_else_replace: 378 382 ∀T: Type[0]. … … 396 400 qed. 397 401 402 (*CSC: move elsewhere*) 398 403 lemma refl_to_jmrefl: 399 404 ∀a: Type[0]. 
src/ASM/BitVector.ma
r2006 r2121 129 129 else 130 130 notb c. 131 132 lemma eq_b_refl: 133 ∀b. 134 eq_b b b = true. 135 #b cases b // 136 qed. 131 137 132 138 lemma eq_b_eq: 
src/ASM/Vector.ma
r2032 r2121 21 21 VEmpty: Vector A O 22 22  VCons: ∀n: nat. A → Vector A n → Vector A (S n). 23 24 lemma Vector_O: 25 ∀A: Type[0]. 26 ∀v: Vector A 0. 27 v ≃ VEmpty A. 28 #A #v 29 generalize in match (refl … 0); 30 cases v in ⊢ (??%? → ?%%??); // 31 #n #hd #tl #absurd 32 destruct(absurd) 33 qed. 34 35 lemma Vector_Sn: 36 ∀A: Type[0]. 37 ∀n: nat. 38 ∀v: Vector A (S n). 39 ∃hd: A. ∃tl: Vector A n. 40 v ≃ VCons A n hd tl. 41 #A #n #v 42 generalize in match (refl … (S n)); 43 cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 44 [1: 45 #absurd destruct(absurd) 46 2: 47 #m #hd #tl #eq 48 <(injective_S … eq) 49 %{hd} %{tl} % 50 ] 51 qed. 23 52 24 53 (* ===================================== *) … … 194 223 vsplit' A m n v. 195 224 225 lemma vsplit_zero: 226 ∀A,m. 227 ∀v: Vector A m. 228 〈[[]], v〉 = vsplit A 0 m v. 229 #A #m #v 230 cases v try % 231 #n #hd #tl % 232 qed. 233 196 234 definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝ 197 235 λA: Type[0]. … … 326 364 327 365 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 366 367 lemma vector_append_zero: 368 ∀A,m. 369 ∀v: Vector A m. 370 ∀q: Vector A 0. 371 v = q@@v. 372 #A #m #v #q 373 >(Vector_O A q) % 374 qed. 375 376 lemma vector_cons_empty: 377 ∀A: Type[0]. 378 ∀n: nat. 379 ∀v: Vector A n. 380 [[ ]] @@ v = v. 381 #A #n #v 382 cases v try % 383 #n' #hd #tl % 384 qed. 328 385 329 386 lemma vector_cons_append: … … 367 424 qed. 368 425 426 lemma tail_head: 427 ∀a: Type[0]. 428 ∀m, n: nat. 429 ∀hd: a. 430 ∀l: Vector a m. 431 ∀r: Vector a n. 432 tail a ? (hd:::(l@@r)) = l@@r. 433 #a #m #n #hd #l #r 434 cases l try % 435 #m' #hd' #tl' % 436 qed. 437 438 lemma head_head': 439 ∀a: Type[0]. 440 ∀m: nat. 441 ∀hd: a. 442 ∀l: Vector a m. 443 hd = head' … (hd:::l). 444 #a #m #hd #l cases l try % 445 #m' #hd' #tl % 446 qed. 447 369 448 axiom vsplit_elim': 370 449 ∀A: Type[0]. … … 386 465 P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt) 387 466 (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt). 388 467 468 lemma vsplit_succ: 469 ∀A: Type[0]. 470 ∀m, n: nat. 471 ∀l: Vector A m. 472 ∀r: Vector A n. 473 ∀v: Vector A (m + n). 474 ∀hd: A. 475 v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)). 476 #A #m 477 elim m 478 [1: 479 #n #l #r #v #hd #eq #hyp 480 destruct >(Vector_O … l) % 481 2: 482 #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp 483 destruct 484 cases (Vector_Sn … l) #hd' #tl' 485 whd in ⊢ (???%); 486 >tail_head 487 <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r)) 488 try (<hyp <head_head' %) 489 elim l normalize // 490 ] 491 qed. 492 493 corollary prod_vector_zero_eq_left: 494 ∀A, n. 495 ∀q: Vector A O. 496 ∀r: Vector A n. 497 〈q, r〉 = 〈[[ ]], r〉. 498 #A #n #q #r 499 generalize in match (Vector_O A q …); 500 #hyp destruct % 501 qed. 502 503 lemma vsplit_prod: 504 ∀A: Type[0]. 505 ∀m, n: nat. 506 ∀p: Vector A (m + n). 507 ∀v: Vector A m. 508 ∀q: Vector A n. 509 p = v@@q → 〈v, q〉 = vsplit A m n p. 510 #A #m elim m 511 [1: 512 #n #p #v #q #hyp 513 >hyp <(vector_append_zero A n q v) 514 >(prod_vector_zero_eq_left A …) 515 @vsplit_zero 516 2: 517 #r #ih #n #p #v #q #hyp 518 >hyp 519 cases (Vector_Sn A r v) #hd #exists 520 cases exists #tl #jmeq 521 >jmeq @vsplit_succ try % 522 @ih % 523 ] 524 qed. 525 526 definition vsplit_elim: 527 ∀A: Type[0]. 528 ∀l, m: nat. 529 ∀v: Vector A (l + m). 530 ∀P: (Vector A l) × (Vector A m) → Prop. 531 (∀vl: Vector A l. 532 ∀vm: Vector A m. 533 v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝ 534 λa: Type[0]. 535 λl, m: nat. 536 λv: Vector a (l + m). 537 λP. ?. 538 cases daemon 539 qed. 540 541 axiom vsplit_append: 542 ∀A: Type[0]. 543 ∀m, n: nat. 544 ∀v, v': Vector A m. 545 ∀q, q': Vector A n. 546 let 〈v', q'〉 ≝ vsplit A m n (v@@q) in 547 v = v' ∧ q = q'. 548 549 lemma vsplit_vector_singleton: 550 ∀A: Type[0]. 551 ∀n: nat. 552 ∀v: Vector A (S n). 553 ∀rest: Vector A n. 554 ∀s: Vector A 1. 555 v = s @@ rest → 556 ((get_index_v A ? v 0 ?) ::: rest) = v. 557 [1: 558 #A #n #v cases daemon (* XXX: !!! *) 559 2: 560 @le_S_S @le_O_n 561 ] 562 qed. 563 389 564 let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat) 390 565 (f: A → B → A) (a: A) (v: Vector B n) on v ≝ … … 593 768 qed. 594 769 770 lemma mem_monotonic_wrt_append: 771 ∀A: Type[0]. 772 ∀m, o: nat. 773 ∀eq: A → A → bool. 774 ∀reflex: ∀a. eq a a = true. 775 ∀p: Vector A m. 776 ∀a: A. 777 ∀r: Vector A o. 778 mem A eq ? r a = true → mem A eq ? (p @@ r) a = true. 779 #A #m #o #eq #reflex #p #a 780 elim p try (#r #assm assumption) 781 #m' #hd #tl #inductive_hypothesis #r #assm 782 normalize 783 cases (eq ??) try % 784 @inductive_hypothesis assumption 785 qed. 786 787 595 788 let rec subvector_with 596 789 (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m) … … 622 815 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) // 623 816 qed. 817 818 lemma subvector_multiple_append: 819 ∀A: Type[0]. 820 ∀o, n: nat. 821 ∀eq: A → A → bool. 822 ∀refl: ∀a. eq a a = true. 823 ∀h: Vector A o. 824 ∀v: Vector A n. 825 ∀m: nat. 826 ∀q: Vector A m. 827 bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)). 828 #A #o #n #eq #reflex #h #v 829 elim v try (normalize #m #irrelevant @I) 830 #m' #hd #tl #inductive_hypothesis #m #q 831 change with (bool_to_Prop (andb ??)) 832 cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true) 833 [1: 834 @mem_monotonic_wrt_append try assumption 835 @mem_monotonic_wrt_append try assumption 836 normalize >reflex % 837 2: 838 #assm >assm 839 >vector_cons_append 840 change with (bool_to_Prop (subvector_with ??????)) 841 @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl)) 842 try @associative_plus 843 @inductive_hypothesis 844 ] 845 qed. 846 847 624 848 625 849 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.