Changeset 2540 for src

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

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

File:
1 edited

Unmodified
Added
Removed
• src/common/StatusSimulation.ma

 r2539 ret_rel … sim_status_rel st1' st2_after_ret ∧ label_rel … st1' st2' | _ ⇒ | cl_other ⇒ (* st1 → st1' sim_status_rel st1' st2' ∧ label_rel … st1' st2' (*    | cl_jump ⇒ (* st1 → st1'           st1 → st1'--------\ |    /               |                  \ S  S,L       or      S                  S,L |  /                 |                    \ st2                 st2 →collapsable tal→ st2' *) (¬as_costed … st1 (* st1' will necessarily be costed *) ∧ sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨ (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'. tal_collapsable … tal ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2')*) | cl_jump ⇒ (* just like cl_other, but with a hypothesis more *) as_costed … st1' → ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' ]. lapply (sim_execute … H st1_R_st2) (* without try it fails... why? *) try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); * try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); [ #H lapply (H K) -H ] * #st2' ** -st2 -st2' [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *) | ft_advance_flat : ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 → (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) → ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) → flat_trace S start st2 stack | ft_advance_call : λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G) | taaf_step_jump s1 s2 s3 pre H G K ⇒ λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … G) λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K)) ] ft. #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: * [*]] #cl [#ncost_st1'] (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S [1,2: (* other/jump *) lapply (sim_execute … ex G') try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); * try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); [ #H lapply (H ncost_st1') -H ] * #st2' *#taaf ** #ncost #G'' #H'' %{st2'} %{st2'}
Note: See TracChangeset for help on using the changeset viewer.