Changeset 3535 for LTS/Vm.ma


Ignore:
Timestamp:
Mar 16, 2015, 4:30:28 PM (5 years ago)
Author:
piccolo
Message:

final statement of cerco with the first pass integrated in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3524 r3535  
    685685definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
    686686λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
    687 ∧ is_costlabelled_act l.
     687∧ is_costlabelled_act l ∧ pre_measurable_trace … t1.
    688688
    689689definition big_op: ∀M: monoid. list M → M ≝
     
    821821      normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
    822822      inversion(emits_labels … i)
    823       [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
     823      [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
     824        normalize nodelta >EQ1 *
    824825        [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
    825       | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
     826      | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta
     827        >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
    826828        *
    827829      ]
     
    882884qed.
    883885
     886(*
    884887definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
    885888λa.match a with
     
    888891| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
    889892].
     893*)
    890894
    891895lemma get_cost_label_of_trace_tind : ∀S : abstract_status.
     
    922926(* For every pre_measurable, terminated trace *)
    923927∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
    924  terminated_trace … t → pre_measurable_trace … t →
     928 terminated_trace … t →
    925929
    926930(* Let labels be the costlabels observed in the trace (last one excluded) *)
     
    951955]
    952956#p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
    953 #l1 * #prf1 * #EQ destruct #Hlabelled
     957#l1 * #prf1 ** #EQ destruct #Hlabelled
    954958>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
    955959[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
     
    12001204]
    12011205#p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
    1202 cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2
    1203 ***** #EQ destruct #Hl1 #Hl2 #_ #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1)
     1206cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2
     1207******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
     1208#acts cases(actionlabel_ok … Hl1)
    12041209#c1 #EQc1 >rewrite_in_dependent_map
    1205 [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?);
     1210[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?);
    12061211     >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
    12071212      >get_cost_label_of_trace_tind in ⊢ (??%?);
    1208      >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
     1213     >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?);
    12091214     >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
    12101215     whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?);
     
    12151220 >(big_op_associative ? [?]) #a1 >act_op #HR
    12161221letin actsl ≝ (dependent_map ????);
    1217 @(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
    1218   [ /6 width=6 by conj, ex_intro/
    1219   | lapply(sub_trace_premeasurable_l2 … premeas)
     1222@(static_dynamic_inv … EQmap … (t13 @ (t_ind … prf2 (t_base …))) … HR)
     1223  [ /7 width=6 by conj, ex_intro/
     1224  (*| lapply(sub_trace_premeasurable_l2 … pre_t13)
    12201225    change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?);
    12211226    change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?);
     
    12241229    change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?);
    12251230    change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?);
    1226     <append_associative #H @(sub_trace_premeasurable_l1 … H)
    1227   | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
     1231    <append_associative #H @(sub_trace_premeasurable_l1 … H) *)
     1232  | cases s1 in prf1 t13; [3: #st1] cases s0 [3,6,9: #st0] *
    12281233    [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
    12291234        #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr
Note: See TracChangeset for help on using the changeset viewer.