Changeset 2121 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 27, 2012, 3:30:58 PM (8 years ago)
 File:

 1 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/
Note: See TracChangeset
for help on using the changeset viewer.