 Timestamp:
 May 30, 2011, 6:38:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r856 r859 59 59 qed. 60 60 61 include "basics/jmeq.ma". 62 63 notation > "hvbox(a break ≃ b)" 64 non associative with precedence 45 65 for @{ 'jmeq ? $a ? $b }. 66 67 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" 68 non associative with precedence 45 69 for @{ 'jmeq $t $a $u $b }. 70 71 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). 72 73 lemma eq_to_jmeq: 74 ∀A: Type[0]. 75 ∀x, y: A. 76 x = y → x ≃ y. 77 // 78 qed. 79 80 axiom vector_associativity_of_append: 81 ∀A: Type[0]. 82 ∀n, m, o: nat. 83 ∀v: Vector A n. 84 ∀q: Vector A m. 85 ∀r: Vector A o. 86 ((v @@ q) @@ r) 87 ≃ 88 (v @@ (q @@ r)). 89 90 axiom vector_cons_append: 91 ∀A: Type[0]. 92 ∀n: nat. 93 ∀a: A. 94 ∀v: Vector A n. 95 a ::: v = [[ a ]] @@ v. 96 97 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. 98 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % 99 qed. 100 101 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?. 102 103 lemma super_rewrite2: 104 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 105 ∀P: ∀m. Vector A m → Prop. 106 n=m → v1 ≃ v2 → P n v1 → P m v2. 107 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 108 qed. 109 110 lemma mem_middle_vector: 111 ∀A: Type[0]. 112 ∀m, o: nat. 113 ∀eq: A → A → bool. 114 ∀reflex: ∀a. eq a a = true. 115 ∀p: Vector A m. 116 ∀a: A. 117 ∀r: Vector A o. 118 mem A eq ? (p@@(a:::r)) a = true. 119 # A # M # O # EQ # REFLEX # P # A 120 elim P 121 [ normalize 122 > (REFLEX A) 123 normalize 124 # H 125 % 126  # NN # AA # PP # IH 127 normalize 128 cases (EQ A AA) // 129 @ IH 130 ] 131 qed. 132 133 lemma mem_monotonic_wrt_append: 134 ∀A: Type[0]. 135 ∀m, o: nat. 136 ∀eq: A → A → bool. 137 ∀reflex: ∀a. eq a a = true. 138 ∀p: Vector A m. 139 ∀a: A. 140 ∀r: Vector A o. 141 mem A eq ? r a = true → mem A eq ? (p @@ r) a = true. 142 # A # M # O # EQ # REFLEX # P # A 143 elim P 144 [ #R #H @H 145  #NN #AA # PP # IH #R #H 146 normalize 147 cases (EQ A AA) 148 [ normalize % 149  @ IH @ H 150 ] 151 ] 152 qed. 153 154 lemma subvector_hd_tl: 155 ∀A: Type[0]. 156 ∀o, n: nat. 157 ∀eq: A → A → bool. 158 ∀refl: ∀a. eq a a = true. 159 ∀h: Vector A o. 160 ∀v: Vector A n. 161 ∀m: nat. 162 ∀q: Vector A m. 163 bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)). 164 # A # O # N # EQ # REFLEX # H # V 165 elim V 166 [ normalize 167 # M # V % 168  # NN # AA # VV # IH # MM # QQ 169 change with (bool_to_Prop (andb ??)) 170 cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true) 171 [ 172  # HH > HH 173 > (vector_cons_append ? ? AA VV) 174 change with (bool_to_Prop (subvector_with ??????)) 175 @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ?? 176 (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS))) 177 ? 178 (vector_associativity_of_append A ? ? ? QQ [[AA]] VV)) 179 [ >associative_plus // 180  @IH ] 181 ] 182 @(mem_monotonic_wrt_append) 183 [ @ REFLEX 184  @(mem_monotonic_wrt_append) 185 [ @ REFLEX 186  normalize 187 > REFLEX 188 normalize 189 % 190 ] 191 ] 192 qed. 61 193 (* 62 194 lemma subvector_hd_tl: … … 100 232 whd in ⊢ (% → ?) 101 233 ] 234 *) 102 235 103 236 let rec list_addressing_mode_tags_elim … … 140 273 ] 141 274 ]. 275 (* 142 276 143 277 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ 144 278 λP. 145 279 P (ADD … ACC_A 146 P (DA … ACC_A). 280 P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. 281 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % 282 qed. 147 283 % 148 284 qed. … … 173 309 174 310 (* RUSSEL **) 175 176 include "basics/jmeq.ma".177 178 notation > "hvbox(a break ≃ b)"179 non associative with precedence 45180 for @{ 'jmeq ? $a ? $b }.181 182 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"183 non associative with precedence 45184 for @{ 'jmeq $t $a $u $b }.185 186 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).187 311 188 312 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
Note: See TracChangeset
for help on using the changeset viewer.