 Timestamp:
 Jun 8, 2011, 6:07:20 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r904 r905 48 48 49 49 (* END RUSSELL **) 50 51 52 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ 53 λP. 54 P true ∧ P false. 55 56 let rec bitvector_elim_prop_internal 57 (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n  m) → Prop ≝ 58 match m return λm. m ≤ n → BitVector (n  m) → Prop with 59 [ O ⇒ λprf1. λprefix. P ? 60  S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?) 61 ]. 62 [ applyS prefix 63  letin res ≝ (bit ::: prefix) 64 < (minus_S_S ? ?) 65 > (minus_Sn_m ? ?) 66 [ @ res 67  @ prf2 68 ] 69  /2/ 70 ]. 71 qed. 72 73 definition bitvector_elim_prop ≝ 74 λn: nat. 75 λP: BitVector n → Prop. 76 bitvector_elim_prop_internal n P n ? ?. 77 [ @ (le_n ?) 78  < (minus_n_n ?) 79 @ [[ ]] 80 ] 81 qed. 82 83 lemma eq_b_eq: 84 ∀b, c. 85 eq_b b c = true → b = c. 86 #b #c 87 cases b 88 cases c 89 normalize // 90 qed. 91 92 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 93 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 94 #n #hd #tl #abs @⊥ // 95 qed. 96 97 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 98 ∃hd.∃tl.v ≃ VCons bool n hd tl. 99 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 100 [ #abs @⊥ // 101  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 102 qed. 103 104 lemma eq_bv_eq: 105 ∀n, v, q. 106 eq_bv n v q = true → v = q. 107 #n #v #q generalize in match v 108 elim q 109 [ #v #h @BitVector_O 110  #n #hd #tl #ih #v' #h 111 cases (BitVector_Sn ? v') 112 #hd' * #tl' #jmeq >jmeq in h; 113 #new_h 114 change in new_h with ((andb ? ?) = ?); 115 cases(conjunction_true … new_h) 116 #eq_heads #eq_tails 117 whd in eq_heads:(??(??(%))?); 118 cases(eq_b_eq … eq_heads) 119 whd in eq_tails:(??(?????(%))?); 120 change in eq_tails with (eq_bv ??? = ?); 121 <(ih tl') // 122 ] 123 qed. 124 125 lemma bool_eq_internal_eq: 126 ∀b, c. 127 (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c. 128 #b #c 129 cases b 130 [ normalize // 131  normalize 132 cases c 133 [ normalize // 134  normalize // 135 ] 136 ] 137 qed. 138 139 lemma eq_bv_refl: 140 ∀n,v. eq_bv n v v = true. 141 #n #v 142 elim v 143 [ // 144  #n #hd #tl #ih 145 normalize 146 cases hd 147 [ normalize 148 @ ih 149  normalize 150 @ ih 151 ] 152 ] 153 qed. 154 155 lemma eq_eq_bv: 156 ∀n, v, q. 157 v = q → eq_bv n v q = true. 158 #n #v 159 elim v 160 [ #q #h <h normalize % 161  #n #hd #tl #ih #q #h >h // 162 ] 163 qed. 50 164 51 165 let rec foldl_strong_internal … … 625 739 qed. 626 740 627 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.628 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //629 #n #hd #tl #abs @⊥ //630 qed.631 632 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).633 ∃hd.∃tl.v ≃ VCons bool n hd tl.634 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))635 [ #abs @⊥ //636  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]637 qed.638 639 741 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 640 742
Note: See TracChangeset
for help on using the changeset viewer.