- Timestamp:
- May 31, 2011, 11:27:13 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r863 r864 174 174 qed. 175 175 176 lemma subvector_ hd_tl:176 lemma subvector_multiple_append: 177 177 ∀A: Type[0]. 178 178 ∀o, n: nat. … … 213 213 ] 214 214 qed. 215 (* 215 216 216 lemma subvector_hd_tl: 217 217 ∀A: Type[0]. 218 ∀n: nat. 218 ∀o: nat. 219 ∀eq: A → A → bool. 220 ∀refl: ∀a. eq a a = true. 219 221 ∀h: A. 220 ∀eq: A → A → bool. 221 ∀v: Vector A n. 222 ∀m: nat. 223 ∀q: Vector A m. 224 bool_to_Prop (subvector_with A ? ? eq v (h ::: q @@ v)). 225 # A 226 # N 227 # H 228 # EQ 229 # V 230 elim V 231 [ normalize 232 # M 233 # Q 234 % 235 | # NN 236 # AA 237 # VV 238 # IH 239 # MM 240 # QQ 241 whd 242 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 243 change in ⊢ (match (match ? with [_ ⇒ % | _ ⇒ ?]) with [_ ⇒ ? | _ ⇒ ?]) 244 with (subvector_with ??????) 245 change in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]) with (andb ??) 246 change with (bool_to_Prop ?); 247 cut ((mem A EQ (S MM+S NN) (H:::QQ@@AA:::VV) AA) = true) 248 [ 249 | # H 250 > H 251 applyS (IH ? (QQ@@[[AA]])) 252 ] 253 generalize in match (IH ? (QQ@@[[AA]])) 254 whd in ⊢ (% → ?) 255 ] 256 *) 257 222 ∀v: Vector A o. 223 bool_to_Prop (subvector_with A ? ? eq v (h ::: v)). 224 225 axiom eq_a_reflexive: 226 ∀a. eq_a a a = true. 227 258 228 (* 259 229 let rec list_addressing_mode_tags_elim … … 293 263 [1: @ (execute_1_technical ? ? tl) 294 264 [ // 295 | 265 | @ (subvector_hd_tl addressing_mode_tag (S y) (S len) eq_a eq_a_reflexive) 296 266 ] 297 267 ].
Note: See TracChangeset
for help on using the changeset viewer.