Changeset 3492

Timestamp:

Sep 24, 2014, 6:44:14 PM (5 years ago)

Author:

sacerdot

Message:

...

File:

• LTS/Vm.ma (modified) (1 diff)

LTS/Vm.ma

@@ -891 +891 @@
   | @eqb_elim normalize nodelta
     [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels
+    >(rewrite_in_dependent_map ??? [])
+    [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral
+      lapply (instr_map_ok … good … prf …)
     
-      >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |]|
-      >rewrite_in_dependent_map [2: 
-      @chop_append_singleton
-      whd in ⊢ (??%% → ?); whd in match (dependent_map ????);
-      
-       >(act_neutral … a1) in H;
-      
-      
-       #H #H1
-      cases st2 in prf; -st2 [3: #st2] #prf
-      lapply(instr_map_ok … good … prf … rel_fin)
-      
-       lapply prf * 
-      #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
-      >act_neutral >act_neutral @(instr_map_ok … good … rel_fin) 
-      
-      
-       @opt_safe_elim #k_init
-      #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
-      >act_neutral whd in match (big_op ??); >act_op >act_neutral
-      
-     
-       #H >act_neutral whd in prf;
-        
-        cases l in prf H1 H2;
-        [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf
-        ** [normalize in ⊢ (% → ?);
-         ⊢ (??%% → ?);
-
- #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] 
-  cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %]
-   #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1
-   #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption
-| -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); *
-  [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?);
-   (*
-    #EQlabels
-  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
-  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
-    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
-    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 
-  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
-    #H cases(bind_inversion ????? H) -H *
-    [ #seq * [|#lbl1]
-    | #newpc
-    | #cond #newpc #ltrue #lfalse
-    | #lin #io #lout
-    | #f
-    |
-    ] 
-    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
-    normalize nodelta >EQfetch >m_return_bind normalize nodelta
-    cases(asm_is_io ??) normalize nodelta 
-    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
-    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
-      [3: cases x normalize nodelta
-      |6: #H cases(bind_inversion ????? H) -H #y * #_
-      ]
-    ]
-    whd in ⊢ (??%% → ?); #EQ destruct 
-    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
-    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
-    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
-    >act_neutral
-    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
-  ]*)
-| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
+      >(act_neutral ?? (act_abs ? abs_t) a1))
+      change
+      with (get_costlabels_of_trace ??? (?@?))
+      in match (get_costlabels_of_trace ????);
+      cases l
+    
+      >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |skip]|3:skip]
+      cases daemon
+    | cases daemon ]]
+| -st1 #st1 #st3 #st4 #l whd in ⊢ (% → ?);
+
+ * #H3 #H4
+
+  -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
   #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
   whd #costs >dependent_map_append