Changeset 2540 for src/common


Ignore:
Timestamp:
Dec 6, 2012, 3:17:12 PM (7 years ago)
Author:
tranquil
Message:

cl_jump case now provides a proof of costedness of the following state

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2539 r2540  
    124124      ret_rel … sim_status_rel st1' st2_after_ret ∧
    125125      label_rel … st1' st2'
    126     | _
     126    | cl_other
    127127        (*         
    128128        st1 → st1'
     
    141141      sim_status_rel st1' st2' ∧
    142142      label_rel … st1' st2'
    143 (*    | cl_jump ⇒
    144       (*
    145           st1 → st1'           st1 → st1'--------\
    146           |    /               |                  \
    147           S  S,L       or      S                  S,L
    148           |  /                 |                    \
    149           st2                 st2 →collapsable tal→ st2'
    150       *)
    151       (¬as_costed … st1 (* st1' will necessarily be costed *) ∧
    152        sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨
    153       (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'.
    154         tal_collapsable … tal ∧
    155         sim_status_rel st1' st2' ∧ label_rel … st1' st2')*)
     143    | cl_jump ⇒
     144      (* just like cl_other, but with a hypothesis more *)
     145      as_costed … st1' →
     146      ∃st2'.
     147      ∃taa2 : trace_any_any_free … st2 st2'.
     148      (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     149      sim_status_rel st1' st2' ∧
     150      label_rel … st1' st2'
    156151    ].
    157152
     
    490485  lapply (sim_execute … H st1_R_st2)
    491486  (* without try it fails... why? *)
    492   try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     487  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     488  [ #H lapply (H K) -H ] *
    493489  #st2' ** -st2 -st2'
    494490  [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *)
     
    620616| ft_advance_flat :
    621617  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
    622   (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) →
     618  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
    623619  flat_trace S start st2 stack
    624620| ft_advance_call :
     
    654650    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
    655651  | taaf_step_jump s1 s2 s3 pre H G K ⇒
    656     λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … G)
     652    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K))
    657653  ] ft.
    658654
     
    809805#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
    810806[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
    811 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
     807|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: * [*]] #cl [#ncost_st1']
    812808  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    813809  [1,2: (* other/jump *)
    814810    lapply (sim_execute … ex G')
    815     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     811    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
     812    [ #H lapply (H ncost_st1') -H ] *
    816813    #st2' *#taaf ** #ncost #G'' #H''
    817814    %{st2'} %{st2'}
Note: See TracChangeset for help on using the changeset viewer.