Changeset 1927 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 9, 2012, 1:05:21 PM (8 years ago)
Author:
mulligan
Message:

Reduced complexity of good_program predicate, ported to new notion of as_label, reintroduced some deleted code from common/StructuredTraces.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1923 r1927  
    287287     let pc ≝ program_counter ? cm initial in
    288288     let label ≝
    289       match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
     289      match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with
    290290      [ None ⇒ λabs. ⊥
    291291      | Some l ⇒ λ_. l ] labelled_proof in
     
    326326        labelled_cost @ return_cost
    327327  ].
    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 % ]
    332335qed.
    333336
     
    687690        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    688691        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 ??);
    690693        inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
    691694        [1:
    692           #_ #absurd cases absurd
     695          #_ #absurd @⊥ cases absurd #absurd @absurd %
    693696        |2:
    694697          normalize nodelta #cost_label #Some_assm #_ #p
Note: See TracChangeset for help on using the changeset viewer.