Ignore:
Timestamp:
Dec 10, 2012, 2:33:40 PM (7 years ago)
Author:
tranquil
Message:

in BackEndOps?, cleaner def of be_op2
new statement of fetch_statement_sigma_commute and first part of further lemmas

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2547 r2548  
    12211221normalize //
    12221222qed.
    1223 
     1223check pc_of_label
    12241224lemma fetch_statement_sigma_commute:
    12251225  ∀p,p',graph_prog,pc,f,fn,stmt.
     
    12291229  fetch_statement (make_sem_graph_params p p') …
    12301230    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
    1231   All ? (λlbl.well_formed_pc p p' graph_prog sigma
    1232       (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
    1233     (stmt_labels … stmt) ∧
     1231  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
     1232      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
     1233      pc_of_label (make_sem_lin_params p p') …
     1234          (globalenv_noinit … lin_prog)
     1235          (pc_block pc)
     1236          lbl = return sigma_pc … prf)
     1237    (stmt_explicit_labels … stmt) ∧
    12341238  match stmt with
    12351239  [  sequential s nxt ⇒
     
    12411245                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
    12421246          ∃prf'.
     1247            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
    12431248            let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
     1249            (nxt_pc = sigma_nxt ∨
     1250              (fetch_statement (make_sem_lin_params p p') …
     1251                (globalenv_noinit … lin_prog) nxt_pc =
     1252                return 〈f, \fst (linearise_int_fun … fn),
     1253                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
     1254              (pc_of_label (make_sem_lin_params p p') …
     1255                (globalenv_noinit … lin_prog)
     1256                (pc_block pc)
     1257                nxt = return sigma_nxt)))
     1258        | COND a ltrue ⇒
     1259            ∃prf'.
    12441260            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
    1245             (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
    1246              (globalenv_noinit … lin_prog) nxt_pc =
    1247              return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
    1248         | COND a ltrue ⇒
    1249             (∃ prf'.
    1250             let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
    1251             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
     1261            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
    12521262            (fetch_statement (make_sem_lin_params p p') …
    12531263            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    12541264              return 〈f, \fst (linearise_int_fun … fn),
    12551265                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
    1256              nxt_pc = sigma_nxt)) ∨ 
    1257              fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
     1266             nxt_pc = sigma_nxt)) ∨
     1267            (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
    12581268             =
    1259              return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉
     1269             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
     1270            pc_of_label (make_sem_lin_params p p') …
     1271                (globalenv_noinit … lin_prog)
     1272                (pc_block pc)
     1273                nxt = return sigma_nxt)
    12601274         ]
    12611275    | final z ⇒   fetch_statement (make_sem_lin_params p p') …
     
    12771291lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt)
    12781292[@lin_pt_spec|] * #H1 #H2 %
    1279 [ -H2 @(All_mp … H1) #lab #lab_spec
     1293[ -H2 @(All_mp … (All_append_r H1) #lab #lab_spec
    12801294  whd in match well_formed_pc; normalize nodelta
    12811295  whd in match sigma_pc_opt; normalize nodelta >fetchfn
     
    14091423@opt_safe_elim -H
    14101424#res #_
    1411 #H
     1425#H cases daemon (*
    14121426#H  @('bind_inversion H) -H
    14131427* #f #stmt
     
    14611475
    14621476xxxxxxxxxxxxxx
    1463 
     1477*)
    14641478qed.
    14651479
     
    18991913 qed.
    19001914
     1915lemma eval_seq_no_call_no_goto :
     1916 ∀p,p',graph_prog.
     1917 let lin_prog ≝ linearise p graph_prog in
     1918 ∀stack_sizes.
     1919 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1920 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
     1921 ∀prf : well_formed_state_pc … gss st.
     1922   fetch_statement (make_sem_lin_params p p') …
     1923    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
     1924      return 〈f, \fst (linearise_int_fun … fn),
     1925        sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
     1926   eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1927      f fn stmt st = return st' →
     1928 let st_pc' ≝ mk_state_pc ? st'
     1929  (succ_pc (make_sem_graph_params p p') …
     1930    (pc … st) nxt) in
     1931 ∀prf'.
     1932 succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it =
     1933   sigma_pc p p' graph_prog sigma
     1934    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
     1935 ∃prf''.
     1936 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     1937  (sigma_state_pc … gss st prf)
     1938  (sigma_state_pc … gss st_pc' prf'').
     1939 bool_to_Prop (taaf_non_empty … taf).
     1940#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
     1941#prf #EQfetch' #EQeval #prf' #EQsucc_pc
     1942cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
     1943#prf'' #EQeval'
     1944% [ @hide_prf % assumption ]
     1945%{(taaf_step … (taa_base …) …)} [3: % ]
     1946[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
     1947  whd in match joint_classify_step; normalize nodelta
     1948  @no_call_other assumption
     1949| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
     1950  whd in match eval_statement_no_pc; normalize nodelta
     1951  >EQeval' >m_return_bind
     1952  whd in match eval_statement_advance; normalize nodelta
     1953  >no_call_advance [2: assumption ]
     1954  whd in match (next ???);
     1955  >EQsucc_pc %
     1956]
     1957qed.
     1958
     1959lemma eval_seq_no_call_goto :
     1960 ∀p,p',graph_prog.
     1961 let lin_prog ≝ linearise p graph_prog in
     1962 ∀stack_sizes.
     1963 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
     1964 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
     1965 ∀prf : well_formed_state_pc … gss st.
     1966  fetch_statement (make_sem_lin_params p p') …
     1967    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
     1968      return 〈f, \fst (linearise_int_fun … fn),
     1969        sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
     1970   eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1971      f fn stmt st = return st' →
     1972 let st_pc' ≝ mk_state_pc ? st'
     1973  (succ_pc (make_sem_graph_params p p') …
     1974    (pc … st) nxt) in
     1975 (? : Prop) →
     1976 fetch_statement (make_sem_lin_params p p') …
     1977   (globalenv_noinit … lin_prog)
     1978     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
     1979   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
     1980 ∃prf''.
     1981 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
     1982  (sigma_state_pc … gss st prf)
     1983  (sigma_state_pc … gss st_pc' prf'').
     1984 bool_to_Prop (taaf_non_empty … taf).
     1985#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
     1986#prf #EQfetch' #EQeval #prf' #EQsucc_pc
     1987cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
     1988#prf'' #EQeval'
     1989% [ @hide_prf % assumption ]
     1990%{(taaf_step … (taa_base …) …)} [3: % ]
     1991[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
     1992  whd in match joint_classify_step; normalize nodelta
     1993  @no_call_other assumption
     1994| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
     1995  whd in match eval_statement_no_pc; normalize nodelta
     1996  >EQeval' >m_return_bind
     1997  whd in match eval_statement_advance; normalize nodelta
     1998  >no_call_advance [2: assumption ]
     1999  whd in match (next ???);
     2000  >EQsucc_pc %
     2001]
     2002qed.
     2003
     2004
     2005 
     2006
     2007  [ assumption
     2008  | assu
     2009 
     2010  fetch_statement (make_sem_lin_params p p') …
     2011          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
     2012              return 〈f, \fst (linearise_int_fun … fn),
     2013                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
     2014          ∃prf'.
     2015            let nxt_pc ≝  in
     2016            let sigma_nxt ≝  in
     2017            (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
     2018             (globalenv_noinit … lin_prog) nxt_pc =
     2019             return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
     2020
    19012021inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    19022022    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
Note: See TracChangeset for help on using the changeset viewer.