Changeset 856 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 30, 2011, 1:44:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r855 r856 1 1 include "ASM/Assembly.ma". 2 2 include "ASM/Interpret.ma". 3 4 (*5 axiom append_cons_commute:6 ∀A: Type[0].7 ∀l, r: list A.8 ∀h: A.9 l @ h::r = l @ [h] @ r.10 *)11 (*12 axiom append_associative:13 ∀A: Type[0].14 ∀l, c, r: list A.15 (l @ c) @ r = l16 *)17 3 18 4 let rec foldl_strong_internal … … 42 28 foldl_strong_internal A P l H [ ] l acc (refl …). 43 29 44 (* RUSSEL **)45 46 30 definition bit_elim: ∀P: bool → bool. bool ≝ 47 31 λP. … … 75 59 qed. 76 60 61 (* 77 62 lemma subvector_hd_tl: 78 63 ∀A: Type[0]. … … 185 170  @ (instruction_elim INSTR) 186 171 ]. 172 *) 187 173 188 (* > append_cons_commute 189 @ 174 (* RUSSEL **) 190 175 191 176 include "basics/jmeq.ma". … … 218 203 #A #P #p cases p #w #q @q 219 204 qed. 205 206 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. 207 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % 208 qed. 209 210 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?. 220 211 221 212 (* END RUSSELL **) … … 270 261  Some r ⇒ λ_.r] (policy_ok p). 271 262 cases abs // 263 qed. 264 265 lemma length_append: 266 ∀A.∀l1,l2:list A. 267 l1 @ l2 = l1 + l2. 268 #A #l1 elim l1 269 [ // 270  #hd #tl #IH #l2 normalize <IH //] 272 271 qed. 273 272 … … 308 307 let 〈pc, costs〉 ≝ pc_costs in 309 308 〈labels, costs〉. 310 [ 311  309 [ whd cases construct in p3 #PC #CODE #JMEQ whd #pc #Hpc 310 generalize in match (sig2 … t) whd in ⊢ (% → ?) 311 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1 312 >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc 313 whd in ⊢ (??(????%?)?) labels1; 314 cases label 315 [ whd in ⊢ (??(????%?)?) 316 cases (le_to_or_lt_eq … Hpc) 317 [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)] 318 (* lemmas needed here *) 319  #H1 generalize in match (injective_S … H1) H1 #H1 320 (* ??? *) 321 ] 322  label #label whd in ⊢ (??(????%?)?) 323 324 ] 325  (* dummy case *) 312 326  whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ] 313 327 qed. … … 343 357 #A #P 344 358 qed.*) 345 346 lemma length_append:347 ∀A.∀l1,l2:list A.348 l1 @ l2 = l1 + l2.349 #A #l1 elim l1350 [ //351  #hd #tl #IH #l2 normalize <IH //]352 qed.353 359 354 360 lemma rev_preserves_length:
Note: See TracChangeset
for help on using the changeset viewer.