Changeset 1927 for src/ASM/CostsProof.ma
- Timestamp:
- May 9, 2012, 1:05:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1923 r1927 287 287 let pc ≝ program_counter ? cm initial in 288 288 let label ≝ 289 match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False | Some _ ⇒ True]→ costlabel with289 match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with 290 290 [ None ⇒ λabs. ⊥ 291 291 | Some l ⇒ λ_. l ] labelled_proof in … … 326 326 labelled_cost @ return_cost 327 327 ]. 328 [ %{pc} whd in match label; generalize in match labelled_proof; whd in ⊢ (% → ?); 329 cases (lookup_opt costlabel … pc cost_labels) normalize 330 [ #abs cases abs | // ] 331 | // ] 328 [1: 329 %{pc} whd in match label; generalize in match labelled_proof; whd in ⊢ (% → ?); 330 whd in match (as_costed ??); whd in match (as_label ??); normalize nodelta 331 cases (lookup_opt costlabel … (program_counter … initial) cost_labels) 332 normalize 333 [ #abs cases abs #absurd @⊥ @absurd % | // ] 334 | cases abs #absurd @absurd % ] 332 335 qed. 333 336 … … 687 690 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 688 691 normalize in match (nth_safe ? ? ? ?); 689 whd in costed_assm; lapply costed_assm 692 whd in costed_assm; lapply costed_assm whd in match (as_label ??); 690 693 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 691 694 [1: 692 #_ #absurd cases absurd695 #_ #absurd @⊥ cases absurd #absurd @absurd % 693 696 |2: 694 697 normalize nodelta #cost_label #Some_assm #_ #p
Note: See TracChangeset
for help on using the changeset viewer.