Ignore:
Timestamp:
Nov 20, 2012, 6:40:08 PM (7 years ago)
Author:
piccolo
Message:

corrected some inconsistencies
fixed some of lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2476 r2481  
    1818include "joint/semanticsUtils.ma".
    1919
    20 
    21 lemma ok_is_internal_function_of_program_noinit :
    22   ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.
    23   is_internal_function_of_program … prog i →
    24   is_internal_function ? (globalenv_noinit ? prog) i ≝
    25  λA,prog.ok_is_internal_function_of_program … prog.
    26 
    27 lemma is_internal_function_of_program_ok_noinit :
    28   ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i.
    29   is_internal_function ? (globalenv_noinit ? prog) i →
    30   is_internal_function_of_program … prog i ≝
    31   λA,prog.is_internal_function_of_program_ok … prog.
    32 
    33 definition if_in_global_env_to_if_in_prog_noinit :
    34   ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.
    35   (Σi.is_internal_function ? (globalenv_noinit ? prog) i) →
    36   Σi.is_internal_function_of_program ?? prog i ≝
    37   λA,prog,f.«f, is_internal_function_of_program_ok_noinit … (pi2 … f)».
    38 
    39 (*
    40 coercion if_in_prog_from_if_in_global_env nocomposites :
    41   ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.
    42   ∀f:Σi.is_internal_function ? (globalenv_noinit ? prog) i.
    43   Σi.is_internal_function_of_program ?? prog i ≝
    44   if_in_global_env_to_if_in_prog_noinit
    45   on _f : Sig ident (λi.is_internal_function ?? i)
    46   to Sig ident (λi.is_internal_function_of_program ??? i).
    47 *)
    48 
    4920definition graph_prog_params ≝
    5021λp,p',prog,stack_sizes.
     
    12798
    12899definition sigma_pc_opt:
    129  ∀p,p',graph_prog,stack_sizes.
     100 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
    130101  ((Σi.is_internal_function_of_program … graph_prog i) →
    131102    code_point (mk_graph_params p) → option ℕ) →
    132103   program_counter → option program_counter
    133104 ≝
    134   λp,p',prog,stack_sizes,sigma,pc.
    135   let pars ≝ graph_prog_params p p' prog stack_sizes in
    136   let ge ≝ ev_genv pars in
     105  λp,p',prog,sigma,pc.
     106  let pars ≝ make_sem_graph_params p p' in
     107  let ge ≝ globalenv_noinit … prog in
    137108  ! f ← int_funct_of_block ? ge (pc_block pc) ;
    138   ! lin_point ← sigma (pi1 … f) (point_of_pc ? pars pc) ;
     109  ! lin_point ← sigma f (point_of_pc ? pars pc) ;
    139110  return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
    140   @(is_internal_function_of_program_ok … prog … (pi2 … f))
    141 qed.
    142111
    143112definition well_formed_pc:
    144  ∀p,p',graph_prog,stack_sizes.
     113 ∀p,p',graph_prog.
    145114  ((Σi.is_internal_function_of_program … graph_prog i) →
    146115    label → option ℕ) →
    147116   program_counter → Prop
    148117 ≝
    149  λp,p',prog,stack_sizes,sigma,pc.
    150   sigma_pc_opt p p' prog stack_sizes sigma pc
     118 λp,p',prog,sigma,pc.
     119  sigma_pc_opt p p' prog sigma pc
    151120   ≠ None ….
    152121
    153122definition well_formed_status:
    154  ∀p,p',graph_prog,stack_sizes.
     123 ∀p,p',graph_prog.
    155124  ((Σi.is_internal_function_of_program … graph_prog i) →
    156125    label → option ℕ) →
    157126  state_pc (make_sem_graph_params p p') → Prop ≝
    158  λp,p',prog,stack_sizes,sigma,st.
    159  well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?.
     127 λp,p',prog,sigma,st.
     128 well_formed_pc p p' prog sigma (pc … st) ∧ ?.
    160129cases daemon (* TODO *)
    161130qed.
     
    188157 *)
    189158 definition sigma_pc :
    190 ∀p,p',graph_prog,stack_sizes.
     159∀p,p',graph_prog.
    191160∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
    192161    label → option ℕ).
    193162∀pc.
    194 ∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
     163∀prf : well_formed_pc p p' graph_prog sigma pc.
    195164program_counter ≝
    196 λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
     165λp,p',graph_prog,sigma,st.opt_safe ….
    197166 
    198167lemma sigma_pc_of_status_ok:
    199   ∀p,p',graph_prog,stack_sizes.
     168  ∀p,p',graph_prog.
    200169  ∀sigma.
    201170   ∀pc.
    202     ∀prf:well_formed_pc p p' graph_prog stack_sizes sigma pc.
    203     sigma_pc_opt p p' graph_prog stack_sizes sigma pc =
    204     Some … (sigma_pc p p' graph_prog stack_sizes sigma pc prf).
    205     #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed.
    206 
     171    ∀prf:well_formed_pc p p' graph_prog sigma pc.
     172    sigma_pc_opt p p' graph_prog sigma pc =
     173    Some … (sigma_pc p p' graph_prog sigma pc prf).
     174    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
    207175
    208176definition sigma_state :
    209177 ∀p.
    210178 ∀p':∀F.sem_unserialized_params p F.
    211  ∀graph_prog,stack_sizes.
     179 ∀graph_prog.
    212180  ∀sigma.
    213181(*   let lin_prog ≝ linearise ? graph_prog in *)
    214     ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)
    215      well_formed_status p p' graph_prog stack_sizes sigma s →
     182    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
     183     well_formed_status p p' graph_prog sigma s →
    216184      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
    217185
    218  λp,p',graph_prog,stack_sizes,sigma,s,prf.
     186 λp,p',graph_prog,sigma,s,prf.
    219187 let pc' ≝ sigma_pc … (proj1 … prf) in
    220188 mk_state_pc ? ? pc'.
     
    222190
    223191lemma sigma_pc_commute:
    224  ∀p,p',graph_prog,stack_sizes,sigma,st.
    225  ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st.
     192 ∀p,p',graph_prog,sigma,st.
     193 ∀prf : well_formed_status p p' graph_prog sigma st.
    226194 sigma_pc … (pc ? st) (proj1 … prf) =
    227195 pc ? (sigma_state … st prf).
    228 #p #p' #prog #stack_sizes #sigma #st #prf %
     196#p #p' #prog #sigma #st #prf %
    229197qed.
    230198
     
    234202
    235203definition sigma_function_name :
    236  ∀p,p',graph_prog.
     204 ∀p,graph_prog.
    237205 let lin_prog ≝ linearise p graph_prog in
    238  ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    239  let graph_stack_sizes ≝
    240   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    241     ? graph_prog lin_stack_sizes in
    242   (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) →
    243   (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
    244 λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
    245 @(ok_is_internal_function_of_program ??? (linearise … graph_prog) ??)
    246 @if_propagate
    247 @is_internal_function_of_program_ok [2: @(pi2 … f) |]
    248 qed.
     206  (Σf.is_internal_function_of_program … graph_prog f) →
     207  (Σf.is_internal_function_of_program … lin_prog f) ≝
     208λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    249209
    250210lemma if_of_function_commute:
    251  ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).∀stack_sizes.
    252  ∀graph_fun,prf.
    253  let graph_fd ≝ if_of_function ? (globalenv_noinit … graph_prog) graph_fun in
    254  let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes «graph_fun, prf» in
     211 ∀p.
     212 ∀graph_prog : joint_program (mk_graph_params p).
     213 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
     214 let graph_fd ≝ if_of_function … graph_fun in
     215 let lin_fun ≝ sigma_function_name … graph_fun in
    255216 let lin_fd ≝ if_of_function … lin_fun in
    256217 lin_fd = \fst (linearise_int_fun ?? graph_fd).
    257  #p #p' #graph_prog #stack_sizes #graph_fun #prf whd
    258 (* Old comment? usare match_opt_prf_elim ? *)
    259 cases daemon (* Job for Paolo *) qed.
     218 #p #graph_prog #graph_fun whd
     219 @prog_if_of_function_transform % qed.
    260220
    261221lemma bind_opt_inversion:
     
    271231∀p,p',graph_prog.
    272232let lin_prog ≝ linearise p graph_prog in
    273 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    274 let graph_stack_sizes ≝
    275  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    276     ? graph_prog lin_stack_sizes in
    277233∀sigma,pc.
    278 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
    279  pc_block (sigma_pc ? p' graph_prog graph_stack_sizes sigma pc prf) =
     234∀prf : well_formed_pc p p' graph_prog sigma pc.
     235 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
    280236 pc_block pc.
    281  #p #p' #graph_prog #stack_sizes #sigma #pc #prf
     237 #p #p' #graph_prog #sigma #pc #prf
    282238 whd in match sigma_pc; normalize nodelta
    283239 @opt_safe_elim #x #x_spec
     
    287243qed.
    288244
     245(*
    289246lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
    290247(! x ← m ; g x) ≠ None ? → m ≠ None ?.
     
    300257#A #B #C #m #x #b  #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption
    301258qed.
    302 
    303 axiom int_funct_of_block_transf_commute:
     259*)
     260
     261lemma funct_of_block_transf :
     262∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
     263∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
     264let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
     265funct_of_block … (globalenv_noinit … progr) bl = return f →
     266funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
     267#A #B #progr #transf #bl #f #prf whd
     268whd in match funct_of_block in ⊢ (%→?); normalize nodelta
     269cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
     270  ∀o.∀prf : Q o.
     271  ∀f1,f2.
     272  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
     273  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
     274  [ #A #B #Q #P * /2/ ] #aux
     275@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
     276#fd #EQfind whd in ⊢ (??%%→?);
     277generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
     278whd in match funct_of_block; normalize nodelta
     279@aux [ # fd' ]
     280[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
     281#prf' cases daemon qed.
     282
     283lemma description_of_function_transf :
     284∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
     285∀transf : ∀vars. A vars → B vars.
     286let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
     287∀f_out,prf.
     288description_of_function …
     289  (globalenv_noinit … progr') f_out =
     290transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
     291  «pi1 … f_out, prf»).
     292#A #B #progr #transf #f_out #prf
     293whd in match description_of_function in ⊢ (???%);
     294normalize nodelta
     295cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
     296  ∀o.∀prf : Q o.
     297  ∀f1,f2.
     298  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
     299  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
     300  [ #A #B #Q #P * /2/ ] #aux
     301@aux
     302[ #fd' ] * #fd #EQ destruct (EQ)
     303inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
     304#bl #EQfind >m_return_bind #EQfindf
     305whd in match description_of_function; normalize nodelta
     306@aux
     307[ #fdo' ] * #fdo #EQ destruct (EQ)
     308>find_symbol_transf >EQfind >m_return_bind
     309>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
     310qed.
     311
     312
     313lemma match_int_fun :
     314∀A,B : Type[0].∀P : B → Prop.
     315∀Q : fundef A → Prop.
     316∀m : fundef A.
     317∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
     318∀f2 : ∀fd.Q (External … fd) → B.
     319∀prf : Q m.
     320(∀fd,prf.P (f1 fd prf)) →
     321(∀fd,prf.P (f2 fd prf)) →
     322P (match m
     323return λx.Q x → ?
     324with
     325[ Internal fd ⇒ f1 fd
     326| External fd ⇒ f2 fd
     327] prf).
     328#A #B #P #Q * // qed.
     329(*)
     330 lemma match_int_fun :
     331∀A,B : Type[0].∀P : B → Prop.
     332∀m : fundef A.
     333∀f1 : ∀fd.m = Internal … fd → B.
     334∀f2 : ∀fd.m = External … fd → B.
     335(∀fd,prf.P (f1 fd prf)) →
     336(∀fd,prf.P (f2 fd prf)) →
     337P (match m
     338return λx.m = x → ?
     339with
     340[ Internal fd ⇒ f1 fd
     341| External fd ⇒ f2 fd
     342] (refl …)).
     343#A #B #P * // qed.
     344*)
     345(*
     346lemma prova :
     347∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
     348∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
     349∀ f,g,prf1.
     350match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
     351[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
     352External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
     353∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
     354#H1 #H2 #H3 #H4 #H5 #H6
     355@match_int_fun
     356#fd #EQ #EQ' whd in EQ' : (??%%); destruct
     357%[|%[| % ]] qed.
     358*)
     359
     360lemma int_funct_of_block_transf_commute:
    304361 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
    305362  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
     
    307364     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
    308365     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
     366#A #B #progr #transf #bl #f #prf
     367whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
     368#H
     369elim (bind_opt_inversion ??? ?? H) -H #x
     370* #x_spec
     371@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
     372#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
     373whd in match int_funct_of_block; normalize nodelta
     374>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
     375>m_return_bind
     376@match_int_fun #fd' #prf' [ % ]
     377@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
     378>(description_of_function_transf) [2: @x_prf ]
     379>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
     380
    309381
    310382lemma fetch_function_sigma_commute :
    311383 ∀p,p',graph_prog.
    312384 let lin_prog ≝ linearise p graph_prog in
    313  ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
    314  let graph_stack_sizes ≝
    315   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    316     ? graph_prog lin_stack_sizes in
    317385 ∀sigma,pc_st,f.
    318   ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc_st.
    319  fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st =
     386  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
     387 fetch_function … (globalenv_noinit … graph_prog) pc_st =
    320388  return f
    321 → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
    322  (sigma_pc … pc_st prf) =
     389→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
    323390  return sigma_function_name … f.
    324  #p #p' #graph_prog #stack_sizes #sigma #st #f #prf
     391 #p #p' #graph_prog #sigma #st #f #prf
    325392 whd in match fetch_function; normalize nodelta
    326393 >(sigma_pblock_eq_lemma … prf) #H
     
    391458
    392459lemma stmt_at_sigma_commute:
    393  ∀p,p',graph_prog,stack_sizes,graph_fun,prf2,lbl,pt.
     460 ∀p,graph_prog,graph_fun,lbl,pt.
    394461 let lin_prog ≝ linearise ? graph_prog in
    395  let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
     462 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
    396463 ∀sigma.good_sigma p graph_prog sigma →
    397  sigma «pi1 … graph_fun,prf2» lbl = return pt →
     464 sigma graph_fun lbl = return pt →
    398465 ∀stmt.
    399466   stmt_at …
     
    403470    (joint_if_code ?? (if_of_function ?? lin_fun))
    404471    pt = return (graph_to_lin_statement … stmt). 
    405  #p #p' #graph_prog #stack_sizes #graph_fun #prf2 #lbl #pt #sigma #good #prf
    406  #prf
     472 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf
    407473 (*
    408474 whd in match (stmt_at ????);
     
    424490
    425491lemma fetch_statement_sigma_commute:
    426   ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt.
     492  ∀p,p',graph_prog,pc,fn,stmt.
    427493  let lin_prog ≝ linearise ? graph_prog in
    428   let graph_stack_sizes ≝
    429    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    430     ? graph_prog lin_stack_sizes in
    431494  ∀sigma.good_sigma p graph_prog sigma →
    432   ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
    433   fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
    434     return 〈fn,stmt〉 →
    435   fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
    436    (sigma_pc … pc prf) =
     495  ∀prf : well_formed_pc p p' graph_prog sigma pc.
     496  fetch_statement ? (make_sem_graph_params p p') …
     497    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
     498  fetch_statement ? (make_sem_lin_params p p') …
     499    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
    437500    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
    438  #p #p' #graph_prog #stack_sizes #pc #fn #stmt #sigma #good #wfprf
     501 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
    439502 whd in match fetch_statement; normalize nodelta #H
    440  cases (bind_inversion ????? H) #id * -H #H
    441  >(fetch_function_sigma_commute … wfprf … H) -H >m_return_bind
     503 cases (bind_inversion ????? H) #id * -H #fetchfn
     504 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
    442505 #H cases (bind_inversion ????? H) #fstmt * -H #H
    443506 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
    444  >(stmt_at_sigma_commute … good … H)
    445  [3: @is_internal_function_of_program_ok [2: @(pi2 … fn)|]
    446  |2: cases daemon (* TO BE DONE, COMMUTATION LEMMA NEEDED *) ]
    447  %
     507 >(stmt_at_sigma_commute … good … H) [%]
     508 whd in match sigma_pc; normalize nodelta
     509 @opt_safe_elim #pc' #H
     510 cases (bind_opt_inversion ????? H)
     511 #i * #EQ1 -H #H
     512 cases (bind_opt_inversion ????? H)
     513 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
     514 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
     515 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
    448516qed.
    449517
     
    461529    (lin_abstract_status p p' lin_prog stack_sizes)
    462530 ≝ λp,p',graph_prog,stack_sizes,sigma,good.
    463    let stack_sizes' ≝
    464     stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
    465       ? graph_prog ? in
    466531   mk_status_rel …
    467532    (* sem_rel ≝ *) (λs1,s2.
    468      ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1.
     533     ∃prf: well_formed_status p p' graph_prog sigma s1.
    469534      s2 = sigma_state … s1 prf)
    470535    (* call_rel ≝ *) (λs1,s2.
    471       ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1.
     536      ∃prf:well_formed_status p p' graph_prog sigma s1.
    472537      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
    473538    (* sim_final ≝ *) ?.
     
    550615(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
    551616
     617lemma err_eq_from_io : ∀O,I,X,m,v.
     618  err_to_io O I X m = return v → m = return v.
     619#O #I #X * #x #v normalize #EQ destruct % qed.
    552620
    553621lemma linearise_ok:
     
    566634 #lin_stack_sizes
    567635 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
    568  whd
    569 #st1 #cl #st1' #st2 #move_st1_st1' * #wf_st1 #rel_st1_st2 #classified_st1_cl
    570 whd in move_st1_st1'; whd in match eval_state in move_st1_st1':(??%?);
    571 normalize nodelta in move_st1_st1';
    572 cases (IO_bind_inversion ??????? move_st1_st1') * #fn #stmt *
    573 #fetch_statement_spec -move_st1_st1' #move_st1_st1'
     636 whd whd in ⊢ (%→%→?);
     637 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
     638 #st1
     639 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?)
     640 #st1'
     641 change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?)
     642 #st2
     643 #ex * #wfprf #rel_st1_st2
     644 whd in ex;
     645 change with
     646  (eval_state
     647    (make_sem_graph_params p p')
     648    (prog_var_names ?? graph_prog)
     649     ?
     650    st1 = ?) in ex;
     651 whd in match eval_state in ex;
     652 normalize nodelta in ex;
     653 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt
     654 change with (Σi.is_internal_function_of_program … graph_prog i) in fn; *
     655 change with (globalenv_noinit ? graph_prog) in
     656  ⊢ (??(???%?)?→?);
     657    match (ge ?? (ev_genv ?)) in ⊢ (%→?);
     658 st1'
     659whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     660>fetch_statement_spec in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     661whd in fetch_statement_spec : (??()%);
    574662cases cl in classified_st1_cl; -cl #classified_st1_cl whd
    575663[4:
Note: See TracChangeset for help on using the changeset viewer.