Changeset 1927 for src/ASM/CostsProof.ma

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:

• src/ASM/CostsProof.ma (modified) (3 diffs)

src/ASM/CostsProof.ma

@@ -287 +287 @@
      let pc ≝ program_counter ? cm initial in
      let label ≝
-      match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
+      match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with
       [ None ⇒ λabs. ⊥
       | Some l ⇒ λ_. l ] labelled_proof in
@@ -326 +326 @@
         labelled_cost @ return_cost
   ].
- [ %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
-  cases (lookup_opt costlabel … pc cost_labels) normalize
-  [ #abs cases abs | // ]
- | // ]
+ [1:
+  %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
+   whd in match (as_costed ??); whd in match (as_label ??); normalize nodelta
+   cases (lookup_opt costlabel … (program_counter … initial) cost_labels)
+   normalize
+  [ #abs cases abs #absurd @⊥ @absurd % | // ]
+ | cases abs #absurd @absurd % ]
 qed.
 
@@ -687 +690 @@
         generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
         normalize in match (nth_safe ? ? ? ?);
-        whd in costed_assm; lapply costed_assm  
+        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
         inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
         [1:
-          #_ #absurd cases absurd
+          #_ #absurd @⊥ cases absurd #absurd @absurd %
         |2:
           normalize nodelta #cost_label #Some_assm #_ #p