Changeset 1976 for src/ASM/CostsProof.ma

Timestamp:

May 21, 2012, 7:04:21 PM (8 years ago)

Author:

tranquil

Message:

• monads: just changed some defs, which had to be propagated in some files
• ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
• added a library for permutations of lists (useful with fold AC ops on lists)
• first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)

File:

• src/ASM/CostsProof.ma (modified) (1 diff)

src/ASM/CostsProof.ma

@@ -722 +722 @@
   @nat_of_bitvector_lt_bound
 qed.
+
+definition ASM_cost_map :
+  ∀code_memory: BitVectorTrie Byte 16.
+  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_map: identifier_map CostTag nat.
+  (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
+  as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
+  λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
+  (lookup_present … cost_map (pi1 … l_sig) ?).
+  cases l_sig #l * #pc @(codom_dom pc)
+  qed.
+  
+include "utilities/permutations.ma".
+
+lemma tech_cost_sum_eq_as_cost :
+  ∀code_memory: BitVectorTrie Byte 16.
+  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_map: identifier_map CostTag nat.
+  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
+  ∀trace.
+  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
+  (Σ_{l ∈ trace}(ASM_cost_map code_memory … codom_dom l)).
+#cmem #clab #cmap #codom_dom #trace
+@(list_elim_left … trace)
+[ %
+| #tl #hd #IH >append_length >commutative_plus
+  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
+  whd in ⊢ (??%%); <IH
+  <tech_cost_of_label_shift [2: %]
+  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
+  [ %
+  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
+  ]
+]
+qed.