Changeset 3050


Ignore:
Timestamp:
Apr 1, 2013, 5:18:05 PM (4 years ago)
Author:
piccolo
Message:

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_traces.ma

    r2895 r3050  
    11251125| Finalstate _ ⇒ None ?
    11261126].
    1127 
    1128 lemma nth_opt_Exists : ∀A,n,l,a.
    1129   nth_opt A n l = Some A a →
    1130   Exists A (λa'. a' = a) l.
    1131 #A #n elim n
    1132 [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
    1133 | #m #IH *
    1134   [ #a #E normalize in E; destruct
    1135   | #a #l #a' #E %2 @IH @E
    1136   ]
    1137 ] qed.
    11381127
    11391128lemma eval_successor : ∀ge,f,fs,m,tr,s'.
  • src/common/ExtraMonads.ma

    r2801 r3050  
    7474}.
    7575
     76record MonadGenRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     77{ m_gen_rel :5> ∀X,Y.(X → Y → Prop) → (M1 X → M2 Y → Prop)
     78; m_gen_return : ∀X,Y,R,x,y.R x y → m_gen_rel X Y R (return x) (return y)
     79; m_gen_bind : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
     80           ∀f,g.(∀x,y.R1 x y → m_gen_rel Z W R2 (f x) (g y)) → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
     81; m_gen_bind_inversion  : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
     82         ∀f,g.(∀x,y.m = return x → n = return y → R1 x y → m_gen_rel Z W R2 (f x) (g y))
     83         → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
     84; m_gen_rel_ext : ∀X,Y,R1,R2.(∀x,y.R1 x y → R2 x y) → ∀u,v.m_gen_rel X Y R1 u v → m_gen_rel X Y R2 u v
     85}.
    7686
    7787definition res_preserve : MonadFunctRel Res Res ≝
     
    107117qed.
    108118
     119definition gen_res_preserve : MonadGenRel Res Res ≝
     120mk_MonadGenRel ??
     121(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     122????.
     123[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     124| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     125  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     126  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     127  %{(refl …)} assumption
     128| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     129  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     130  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     131  normalize %{EQw} assumption
     132| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     133  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     134  #Rxy %{y} %{(refl …)} @H assumption
     135]
     136qed.
     137
    109138definition opt_preserve : MonadFunctRel Option Option ≝
    110139  mk_MonadFunctRel ??
     
    139168qed.
    140169
     170definition gen_opt_preserve : MonadGenRel Option Option ≝
     171mk_MonadGenRel ??
     172(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     173????.
     174[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     175| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     176  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     177  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     178  %{(refl …)} assumption
     179| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     180  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     181  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     182  normalize %{EQw} assumption
     183| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     184  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     185  #Rxy %{y} %{(refl …)} @H assumption
     186]
     187qed.
     188
     189
    141190definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    142191  λO,I.mk_MonadFunctRel ??
     
    168217| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    169218  % //
     219]
     220qed.
     221
     222definition gen_io_preserve : ∀O,I.MonadGenRel (IOMonad O I)(IOMonad O I) ≝
     223λO,I.mk_MonadGenRel ??
     224(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
     225????.
     226[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
     227| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     228  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     229  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
     230  %{(refl …)} assumption
     231| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
     232  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
     233  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
     234  normalize %{EQw} assumption
     235| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
     236  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
     237  #Rxy %{y} %{(refl …)} @H assumption
    170238]
    171239qed.
     
    193261  ∀ y.
    194262  FR ?? G (f (F y)) (g y).
     263 
     264definition gen_preserving ≝
     265λM1,M2.λFR : MonadGenRel M1 M2.
     266 λX,Y,A,B : Type[0].
     267 λR1 : X → Y → Prop.
     268 λR2 : A → B → Prop.
     269 λf : X → M1 A.
     270 λg : Y → M2 B.
     271 ∀x,y. R1 x y →
     272 FR ?? R2 (f x) (g y).
    195273
    196274definition preserving2 ≝
     
    219297   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
    220298   
     299definition gen_preserving2 ≝
     300λM1,M2.λFR : MonadGenRel M1 M2.
     301  λX,Y,Z,W,A,B : Type[0].
     302  λR1 : X → Y → Prop.
     303  λR2 : Z → W → Prop.
     304  λR3 : A → B → Prop.
     305  λf : X → Z → M1 A.
     306  λg : Y → W → M2 B.
     307  ∀x,y,z,w. R1 x y → R2 z w →
     308  FR ?? R3 (f x z) (g y w). 
     309
    221310lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    222311#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
    223312
    224313lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
    225 #X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     314#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     315
     316lemma res_preserve_error_gen : ∀X,Y,R,e,n.gen_res_preserve X Y R (Error … e) n.
     317#X #Y #R #e #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
    226318
    227319lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
     
    238330qed.
    239331
     332lemma gen_mfr_return_eq : ∀M1,M2.∀FR : MonadGenRel M1 M2.
     333∀X,Y,R,x,y,n.R x y →
     334n = return x → FR X Y R n (return y).
     335#M1 #M2 #FR #X #Y #R #x #y #n #H #EQ destruct @m_gen_return assumption
     336qed.
     337
    240338lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    241339#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     
    246344lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
    247345#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
     346
     347lemma opt_preserve_none_gen : ∀X,Y,R,n.gen_opt_preserve X Y R (None ?) n.
     348#X #Y #R #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
    248349
    249350lemma m_list_map_All_ok :
     
    283384qed.
    284385
     386lemma res_to_opt_gen_preserve : ∀X,Y,R,m,n.
     387gen_res_preserve X Y R m n → gen_opt_preserve X Y R (res_to_opt … m) (res_to_opt … n).
     388#X #Y #R #m #n #H #x #EQ whd in H; cases(H x ?)
     389[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
     390| cases m in EQ; normalize #x #EQ destruct %
     391]
     392qed.
     393
    285394lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    286395       opt_preserve X Y P F m n →
     
    301410qed.
    302411
     412lemma opt_to_res_gen_preserve :  ∀X,Y,R,m,n,e1,e2.
     413gen_opt_preserve X Y R m n →
     414gen_res_preserve X Y R (opt_to_res … e1 m) (opt_to_res … e2 n).
     415#X #Y #R #m #n #e1 #e2 #H #x #EQ whd in H; cases(H x ?)
     416[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
     417| cases m in EQ; normalize [2: #x] #EQ destruct %
     418]
     419qed.
     420
    303421lemma err_eq_from_io : ∀O,I,X,m,v.
    304422  err_to_io O I X m = return v → m = return v.
  • src/joint/StatusSimulationHelper.ma

    r2991 r3050  
    1717include "common/StatusSimulation.ma".
    1818include "joint/semantics_blocks.ma".
     19include "utilities/listb_extra.ma".
     20include "utilities/lists.ma".
    1921
    2022lemma set_no_pc_eta:
     
    4648qed.
    4749
    48 let rec bind_instantiates B X (b : bind_new B X) (l : list B) on b : (option X) ≝
     50let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝
    4951  match b with
    5052  [ bret B ⇒
     
    5759    [ nil ⇒ None ?
    5860    | cons r l' ⇒
    59       bind_instantiates B X (f r) l'
     61      bind_instantiate B X (f r) l'
    6062    ]
    6163  ].
    6264 
    63 lemma bind_instantiates_bind_new_instantiates : ∀B,X.∀b : bind_new B X.
     65lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X.
    6466∀l : list B.∀x : X.
    65 bind_instantiates B X b l = Some ? x →
     67bind_instantiate B X b l = Some ? x →
    6668bind_new_instantiates B X x b l.
    6769#B #X #b elim b
     
    7274qed.
    7375
    74 lemma bind_new_instantiates_bind_instantiates : ∀B,X.∀b : bind_new B X.
     76lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
    7577∀l : list B.∀x : X.
    7678bind_new_instantiates B X x b l →
    77 bind_instantiates B X b l = Some ? x.
     79bind_instantiate B X b l = Some ? x.
    7880#B #X #b elim b
    7981[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
     
    8284qed.
    8385
    84 
    85 definition joint_state_relation ≝
    86 λP_in,P_out.program_counter → state P_in → state P_out → Prop.
    87 
    88 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
     86coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
     87∀l : list B.∀x : X.
     88∀prf : bind_new_instantiates B X x b l.
     89bind_instantiate B X b l = Some ? x ≝
     90bind_instantiate_instantiates
     91on _prf : bind_new_instantiates ?????
     92to eq (option ?) (bind_instantiate ????) (Some ??).
    8993
    9094definition lbl_funct_type ≝  block → label → (list label).
    9195definition regs_funct_type ≝ block → label → (list register).
     96
    9297
    9398definition preamble_length ≝
     
    99104λf_regs : regs_funct_type.λbl : block.λlbl : label.
    100105! bl ← code_block_of_block bl ;
    101 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
     106! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
    102107                           (joint_globalenv P_in prog stack_size) bl);
    103 ! stmt ← stmt_at P_in (prog_var_names … prog) (joint_if_code … fn) lbl;
    104 ! data ← bind_instantiates ?? (init … fn) (init_regs bl);
     108! stmt ← stmt_at P_in (joint_if_code … fn) lbl;
     109! data ← bind_instantiate ?? (init … fn) (init_regs bl);
    105110match stmt with
    106111[ sequential step nxt ⇒
    107     ! step_block ← bind_instantiates ?? (f_step … data lbl step) (f_regs bl lbl);
     112    ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl);
    108113    return |\fst (\fst step_block)|
    109114| final fin ⇒
    110     ! fin_block ← bind_instantiates ?? (f_fin … data lbl fin) (f_regs bl lbl);
     115    ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl);
    111116    return |\fst fin_block|
    112117| FCOND abs _ _ _ ⇒ Ⓧabs
     
    122127λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
    123128! bl ← code_block_of_block bl ;
    124 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
     129! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
    125130                           (joint_globalenv p_in prog stack_size) bl);
    126131! 〈res,s〉 ←
     
    200205qed.
    201206
     207lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
     208∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
     209(∀ prf : r = Code.P (g prf)) →
     210P ((match r return λx.(r = x → ?) with
     211    [XData ⇒ f | Code ⇒ g])(refl ? r)).
     212#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
     213qed.
     214
    202215definition sigma_stored_pc ≝
    203216λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
    204217match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
    205218      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
     219     
     220lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
     221code_block_of_block bl = return bl.
     222* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
     223[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
     224qed.
     225
     226(*TO BE MOVED*)
     227lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
     228#A #l1 elim l1 [#l2 #P *] #hd #tl #IH *
     229[#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
     230qed.
     231
     232lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
     233#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
     234[#a normalize // ] #hd1 #tl1 #a normalize *
     235[ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
     236| #H %2 >append_cons @IH assumption]
     237qed.
     238
     239lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
     240∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
     241seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
     242#p #globals #code #src #l1 lapply src -src elim l1
     243[ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
     244#hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
     245#hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
     246#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
     247qed.
     248
     249lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
     250∀f_lbls : lbl_funct_type.∀f_regs.
     251b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs →
     252∀id,fn.
     253∀bl:Σb.block_region b = Code. ∀pt,stmt.
     254block_id … bl ≠ -1 →
     255fetch_internal_function …
     256   (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
     257stmt_at p_in … (joint_if_code … fn) pt = return stmt → 
     258∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
     259match n with
     260[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
     261| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
     262    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt
     263].
     264#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
     265#bl #pt #stmt * #Hbl #EQfn #EQstmt   
     266lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
     267@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
     268#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
     269lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
     270[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
     271[ * #pre_instr #instr #post_instr | #pre_instr #instr] *
     272[ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
     273 [ @eq_identifier_elim #EQentry normalize nodelta
     274   [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
     275     whd in ⊢ (???% → ?); #EQ destruct(EQ)
     276   |*: #Hregs
     277   ]
     278 | #Hregs
     279 ]
     280| #Hregs
     281]
     282#syntax_spec
     283[4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
     284[1,2,4,5: %{(|pre_instr|)} | %{O}]
     285cut(? : Prop)
     286[3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
     287 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
     288           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
     289 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
     290   >m_return_bind >EQfn >m_return_bind inversion(find ????)
     291   [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
     292     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
     293   >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
     294   normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
     295   whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
     296   >m_return_bind cases stmt1 in EQfind; -stmt1
     297   [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
     298   cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
     299   [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
     300   >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
     301   whd in match (length ??); normalize nodelta
     302   [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %]
     303   whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
     304   #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
     305   #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
     306   cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) **
     307   #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     308   whd in match code_has_point; normalize nodelta >EQstmt @I
     309 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
     310     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
     311     #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?);
     312     [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
     313     |*:   #EQt_stmt
     314     ]
     315     %{mid1} cut(? : Prop)
     316     [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta
     317       >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
     318       [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
     319         whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
     320         [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
     321       lapply(find_predicate ?????? EQfind) whd in match preamble_length;
     322       normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
     323       whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
     324       >m_return_bind cases stmt1 in EQfind; -stmt1
     325       [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
     326       cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *]
     327       [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
     328       >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
     329       whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
     330       [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
     331         #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
     332         #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
     333         @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
     334         >e0 @Exists_append2 % %
     335       |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
     336         lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
     337         @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     338         whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
     339         >(find_lookup ?????? EQfind) @I
     340       ]   
     341     |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
     342                whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
     343                #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
     344                [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
     345                try % try( #n %) #n <minus_n_n %
     346     |*:
     347     ]
     348  ]
     349 |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
     350   >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
     351   normalize nodelta
     352   [1,2,3,4: >Hregs %
     353   | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
     354     #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
     355     whd in match (bind_instantiate ????); %
     356   ]
     357 |*:
     358 ]
     359qed.
     360
     361lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
     362f_regs,pc.
     363sigma_pc_opt p_in p_out prog stack_sizes init
     364   init_regs f_lbls f_regs pc ≠ None ? →
     365 pc_block … pc =
     366 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init
     367                                           init_regs f_lbls f_regs pc).
     368#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
     369whd in match sigma_stored_pc; normalize nodelta
     370inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1
     371whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta
     372[ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) -H
     373#lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
     374qed.
     375
     376lemma fetch_statement_sigma_stored_pc :
     377∀p_in,p_out,prog,stack_sizes,
     378init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
     379b_graph_transform_program_props p_in p_out stack_sizes
     380  init prog init_regs f_lbls f_regs →
     381block_id … (pc_block pc) ≠ -1 →
     382let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
     383fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
     384return 〈f,fn,stmt〉 →
     385∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
     386match stmt with
     387[ sequential step nxt ⇒
     388    ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
     389                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
     390    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
     391                                           init_regs f_lbls f_regs pc' = pc ∧
     392    ∃fn',nxt'.
     393    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
     394    if not_emptyb … (added_prologue … data) ∧
     395       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
     396    then return 〈f,fn',sequential ?? (NOOP …) nxt'〉
     397    else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉
     398| final fin ⇒
     399    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
     400                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
     401    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
     402                                           init_regs f_lbls f_regs pc' = pc ∧
     403    ∃fn'.fetch_statement p_out …
     404       (joint_globalenv p_out trans_prog stack_sizes) pc'
     405       = return 〈f,fn',final ?? (\snd fin_block)〉           
     406| FCOND abs _ _ _ ⇒ Ⓧabs
     407].
     408#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
     409#good #Hbl #EQfetch
     410lapply(b_graph_transform_program_fetch_statement … good pc f fn ?)
     411[2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
     412      #H cases(H EQfetch) -H |*:]
     413#data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H;
     414[ #step #nxt | #fin | *] normalize nodelta #EQfetch -stmt
     415[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
     416  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
     417* #block *
     418[ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
     419  #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
     420  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
     421  * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     422  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
     423|*: #Hregs #syntax_spec
     424]
     425cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
     426[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
     427  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
     428  % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
     429  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
     430  @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_
     431|*: %{block} >Hregs %{(refl …)}
     432]
     433cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
     434normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
     435[   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
     436    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     437|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
     438    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt}
     439    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
     440    >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H %
     441|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
     442|6,7,8: %{pc}
     443]
     444whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
     445@eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
     446[1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
     447%{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
     448[1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
     449[1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
     450|*: #l1 * #mid **
     451]
     452#EQmid #EQpre whd in ⊢ (% → ?);
     453[1,2,3,4: * #nxt1 *] #EQt_stmt
     454[1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}]
     455whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
     456@('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
     457#EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
     458normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
     459[1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
     460   #EQ destruct(EQ)]
     461[1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
     462[1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
     463   * #mid * #rest ** #EQ destruct(EQ)]
     464[1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     465[4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %]
     466        #EQ <EQ in EQentry; * #H @⊥ @H %]
     467* #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
     468whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
     469lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
     470>nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
     471#EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
     472[1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %]
     473      @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_
     474      >point_of_pc_of_point %]
     475destruct(EQ3) >point_of_pc_of_point >EQt_stmt %
     476qed.
     477
     478definition make_is_relation_from_beval : (beval → beval → Prop) →
     479internal_stack → internal_stack → Prop≝
     480λR,is1,is2.
     481match is1 with
     482[ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
     483| one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
     484| both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
     485].
     486
     487lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
     488∀Ristack1 : internal_stack → internal_stack → Prop.
     489∀Ristack2 : internal_stack → internal_stack → Prop.
     490(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
     491(∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 →
     492                                   Ristack2 (one_is bv1) (one_is bv2)) →
     493(∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 →
     494                         Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) →
     495                         gen_preserving2 ?? gen_res_preserve …
     496                              Ristack1 Rbeval Ristack2 is_push is_push.
     497#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4
     498whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta
     499[2:#x|3: #x #y #_ @res_preserve_error_gen]
     500cases is2 normalize nodelta
     501 [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
     502 [@H2 [assumption | @(H … H5) ] | @H1 assumption]
     503qed.
     504(*
     505lemma is_push_ok : ∀R : beval → beval → Prop.
     506               gen_preserving2 ?? gen_res_preserve …
     507                       (make_is_relation_from_beval R) R
     508                       (make_is_relation_from_beval R)
     509                       is_push is_push.
     510#R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
     511qed.
     512*)
     513lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
     514∀Ristack1 : internal_stack → internal_stack → Prop.
     515∀Ristack2 : internal_stack → internal_stack → Prop.
     516(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
     517Ristack2 empty_is empty_is →
     518(∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) →
     519          gen_preserving ?? gen_res_preserve …
     520                              Ristack1
     521                              (λx,y.Rbeval (\fst x) (\fst y) ∧
     522                                Ristack2 (\snd x) (\snd y)) is_pop is_pop.
     523#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
     524cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
     525[1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
     526@m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
     527qed.
     528
     529(*
     530lemma is_pop_ok1 : ∀R : beval → beval → Prop.
     531           gen_preserving ?? gen_res_preserve …
     532                         (make_is_relation_from_beval R)
     533                         (λx,y.R (\fst x) (\fst y) ∧
     534                               (make_is_relation_from_beval R) (\snd x) (\snd y))
     535                         is_pop is_pop.
     536#R @is_pop_ok //
     537qed.
     538
     539
     540definition make_weak_state_relation ≝
     541λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
     542(make_is_relation_from_beval R) (istack … st1) (istack … st2).
     543*)
     544
     545
     546lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
     547(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
     548                  make_is_relation_from_beval Rbeval is1 is2) →
     549(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
     550 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
     551(∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 →
     552 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) →
     553                    gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
     554                                   (push p_in) (push p_out).
     555#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
     556whd in match push; normalize nodelta
     557@(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
     558[ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
     559  [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
     560  | @(H … H3) %
     561  ]
     562| * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?);
     563  [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return
     564  [ @(H2 … H3) assumption
     565  | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
     566    #EQ destruct(EQ)
     567  | @(H1 … H3) assumption
     568  ]
     569]
     570qed.
     571
     572
     573lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
     574(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
     575                  make_is_relation_from_beval Rbeval is1 is2) →
     576(∀st1,st2.Rstate1 st1 st2 →
     577 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) →
     578(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
     579 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
     580               gen_preserving ?? gen_res_preserve …
     581                 Rstate1
     582                (λx,y.Rbeval (\fst x) (\fst y) ∧
     583                 Rstate2(\snd x) (\snd y))
     584                (pop p_in) (pop p_out).
     585#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3
     586whd in match pop; normalize nodelta
     587@(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧
     588           (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 
     589[ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
     590| * #bv1 * [|#x|#x1 #x2] * #bv2 *
     591[1,4,7:|2,5,8: #y
     592|*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
     593#_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
     594% // [ @(H1 … H3) | @(H2 … H3) assumption]
     595qed.
     596
     597
     598definition joint_state_relation ≝
     599λP_in,P_out.program_counter → state P_in → state P_out → Prop.
     600
     601definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
    206602
    207603
     
    219615; fetch_ok_sigma_state_ok :
    220616   ∀st1,st2,f,fn. st_rel st1 st2 →
    221     fetch_internal_function … (prog_var_names … prog)
     617    fetch_internal_function …
    222618     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    223619     = return 〈f,fn〉 →
     
    225621; fetch_ok_pc_ok :
    226622  ∀st1,st2,f,fn.st_rel st1 st2 →
    227    fetch_internal_function … (prog_var_names … prog)
     623   fetch_internal_function …
    228624     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    229625     = return 〈f,fn〉 →
     
    231627; fetch_ok_sigma_last_pop_ok :
    232628  ∀st1,st2,f,fn.st_rel st1 st2 →
    233    fetch_internal_function … (prog_var_names … prog)
     629   fetch_internal_function …
    234630     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    235631     = return 〈f,fn〉 →
     
    238634; st_rel_def :
    239635  ∀st1,st2,pc,lp1,lp2,f,fn.
    240   fetch_internal_function … (prog_var_names … prog)
     636  fetch_internal_function …
    241637     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
    242638   st_no_pc_rel pc st1 st2 →
     
    247643  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    248644  ∀st1,st2,f,fn,stmt.
    249   fetch_statement … (prog_var_names … prog)
     645  fetch_statement …
    250646  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
    251647  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
     
    262658    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
    263659    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
    264     (eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
     660    (eval_state P_in (joint_globalenv P_in prog stack_sizes)
    265661      st1 = return st1' →
    266662    ∃st2'. st_rel st1' st2' ∧
    267     eval_state P_out (prog_var_names … trans_prog)
     663    eval_state P_out
    268664     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
    269665; cond_commutation :
    270666    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    271     ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     667    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    272668    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    273     ∀f,fn,a,ltrue,lfalse.
     669    ∀f,fn,a,ltrue,lfalse,bv,b.
    274670    block_id … (pc_block (pc … st1)) ≠ -1 →
    275671    let cond ≝ (COND P_in ? a ltrue) in
    276672    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    277673    return 〈f, fn,  sequential … cond lfalse〉 → 
    278     eval_state P_in (prog_var_names … prog)
    279     (joint_globalenv P_in prog stack_sizes) st1 = return st1'
     674    acca_retrieve … P_in (st_no_pc … st1) a = return bv →
     675    bool_of_beval … bv = return b
    280676    st_rel st1 st2 →
    281677    ∀t_fn.
    282     fetch_internal_function … (prog_var_names … trans_prog)
     678    fetch_internal_function …
    283679     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    284680     return 〈f,t_fn〉 →
     
    287683     (λregs2.λblp.(\snd blp) = [ ] ∧
    288684        ∀mid.
    289           stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
     685          stmt_at P_out … (joint_if_code ?? t_fn) mid
    290686          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
    291687         ∃st2_pre_mid_no_pc.
    292             repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
     688            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    293689             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
    294690            = return st2_pre_mid_no_pc ∧
    295             st_no_pc_rel (pc … st1') (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
    296             joint_classify_step … ((\snd (\fst blp)) mid)  = cl_jump ∧
    297             cost_label_of_stmt P_out (prog_var_names … trans_prog)
    298                                (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
    299             let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
     691            let new_pc ≝ if b then
     692                           (pc_of_point P_in (pc_block (pc … st1)) ltrue)
     693                         else
     694                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
     695            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
     696            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
     697            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
     698                  bool_of_beval … bv' = return b
     699            (*let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
    300700                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
    301701            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
    302702            eval_statement_advance P_out (prog_var_names … trans_prog)
    303703             (joint_globalenv P_out trans_prog stack_sizes) f t_fn
    304              (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'
     704             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*)
    305705   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    306706  ) (init ? fn)
     
    314714  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    315715  return 〈f, fn,  sequential … seq nxt〉 → 
    316   eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
     716  eval_state P_in (joint_globalenv P_in prog stack_sizes)
    317717  st1 = return st1' →
    318718  st_rel st1 st2 →
    319719  ∀t_fn.
    320   fetch_internal_function … (prog_var_names … trans_prog)
     720  fetch_internal_function …
    321721     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    322722  return 〈f,t_fn〉 →
     
    324724     (λregs1.λdata.bind_new_P' ??
    325725      (λregs2.λblp.
    326        ∃l : list (joint_seq P_out (prog_var_names … trans_prog)).
     726       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
    327727                            blp = (ensure_step_block ?? l) ∧
    328728       ∃st2_fin_no_pc.
    329            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
     729           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    330730              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    331731           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
     
    341741  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
    342742}.
    343 
    344 (*TO BE MOVED*)
    345 lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
    346 decidable (In A l a).
    347 #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
    348 [ #H % %2 assumption | * #H cases (DEC hd)
    349 [ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
    350 qed.
    351 
    352 lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
    353 #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
    354 % #H1 @H % >H1 %
    355 qed.
    356 
    357 lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
    358 #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
    359 [ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
    360 qed.
    361743
    362744lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
     
    415797∀f,fn,stmt,st1,st2.
    416798good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
    417                     st_no_pc_rel st_rel 
     799                    st_no_pc_rel st_rel
    418800st_rel st1 st2 →
    419801fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     
    477859qed.*)
    478860
    479 (*TO BE MOVED*)
    480 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
    481 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
    482 #A #P #l1 elim l1
    483 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]
    484 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
    485 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
    486 qed.
    487861
    488862lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    495869let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
    496870good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
    497                     st_no_pc_rel st_rel
     871                    st_no_pc_rel st_rel 
    498872∀st1,st1' : joint_abstract_status prog_pars_in.
    499873∀st2 : joint_abstract_status prog_pars_out.
    500 ∀f.
    501 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     874∀f : ident.
     875∀fn : joint_closed_internal_function P_in ?.
    502876∀a,ltrue,lfalse.
    503877block_id … (pc_block (pc … st1)) ≠ -1 →
    504878st_rel st1 st2 →
    505879 let cond ≝ (COND P_in ? a ltrue) in
    506   fetch_statement P_in
     880  fetch_statement P_in ?
    507881   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    508      return 〈f, fn,  sequential … cond lfalse〉 →
    509  eval_state P_in (prog_var_names … prog)
     882     return 〈f, fn, sequential … cond lfalse〉 →
     883 eval_state P_in
    510884  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
    511885as_costed (joint_abstract_status prog_pars_in) st1' →
     
    514888bool_to_Prop (taaf_non_empty … taf).
    515889#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
    516 #st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 #EQfetch
    517 #EQeval
     890#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
     891#EQfetch #EQeval
    518892@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    519893whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     
    543917* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    544918cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    545                (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
     919               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
    546920[2,4: % assumption]
    547921#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    548 cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
    549 #EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid
     922cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
     923normalize nodelta
     924#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
    550925[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    551926     (last_pop … st2))}
     
    572947      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
    573948      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
    574       >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
     949      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
    575950      #H @H %
    576951]
     
    594969|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
    595970      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
    596       assumption
     971      >EQt_cond %
    597972|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
    598     >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
    599     cases(blm mid1) in CL_JUMP COST Hst2_mid;
    600     [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    601     |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    602     ]
    603     #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta
    604     >m_return_bind assumption
     973    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
     974    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     975    whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
     976    >rel_v_v' >m_return_bind normalize nodelta
     977    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
     978      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
    605979]
    606980qed.
     
    619993∀st1,st1' : joint_abstract_status prog_pars_in.
    620994∀st2 : joint_abstract_status prog_pars_out.
    621 ∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
     995∀f.∀fn : joint_closed_internal_function P_in ?.
    622996∀stmt,nxt.
    623997block_id … (pc_block (pc … st1)) ≠ -1 →
     
    6271001   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    6281002     return 〈f, fn,  sequential ?? seq nxt〉 →
    629  eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
     1003 eval_state P_in (joint_globalenv P_in prog stack_sizes)
    6301004  st1 = return st1' →
    6311005∃st2'. st_rel st1' st2' ∧           
     
    6881062∀st2 : joint_abstract_status prog_pars_out.
    6891063∀f.
    690 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
     1064∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
    6911065block_id … (pc_block (pc … st1)) ≠ -1 →
    6921066st_rel st1 st2 →
     
    6951069  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    6961070    return 〈f, fn,  sequential ?? cost nxt〉 →
    697  eval_state P_in (prog_var_names … prog) (ev_genv … prog_pars_in)
     1071 eval_state P_in (ev_genv … prog_pars_in)
    6981072            st1 = return st1' →
    6991073∃ st2'. st_rel st1' st2' ∧
  • src/utilities/listb_extra.ma

    r2728 r3050  
    11include "basics/lists/listb.ma".
    22include "ASM/Util.ma".
     3include "utilities/lists.ma".
    34
    45lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
     
    1718] qed.
    1819
     20
     21lemma nth_opt_Exists : ∀A,n,l,a.
     22  nth_opt A n l = Some A a →
     23  Exists A (λa'. a' = a) l.
     24#A #n elim n
     25[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
     26| #m #IH *
     27  [ #a #E normalize in E; destruct
     28  | #a #l #a' #E %2 @IH @E
     29  ]
     30] qed.
     31
     32
     33lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
     34decidable (In A l a).
     35#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
     36[ #H % %2 assumption | * #H cases (DEC hd)
     37[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
     38qed.
     39
     40lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
     41#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
     42% #H1 @H % >H1 %
     43qed.
     44
     45lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
     46#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
     47[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
     48qed.
     49
     50lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
     51All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
     52#A #P #l1 elim l1
     53[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
     54#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
     55* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
     56qed.
Note: See TracChangeset for help on using the changeset viewer.