Ignore:
Timestamp:
Dec 7, 2012, 8:37:51 PM (7 years ago)
Author:
tranquil
Message:

going on in proof of linearise
simplified by use of monadic functional relations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2543 r2547  
    1717include "joint/Traces.ma".
    1818include "joint/semanticsUtils.ma".
     19
     20lemma bind_option_inversion_star:
     21  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     22  (∀x.f = Some … x → g x = Some … y → P) →
     23  (! x ← f ; g x = Some … y) → P.
     24#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
     25
     26interpretation "option bind inversion" 'bind_inversion =
     27  (bind_option_inversion_star ???????).
     28
     29lemma bind_inversion_star : ∀X,Y.∀P : Prop.
     30∀m : res X.∀f : X → res Y.∀v : Y.
     31(∀x. m = return x → f x = return v → P) →
     32! x ← m ; f x = return v → P.
     33#X #Y #P #m #f #v #H #G
     34elim (bind_inversion ????? G) #x * @H qed.
     35
     36interpretation "res bind inversion" 'bind_inversion =
     37  (bind_inversion_star ???????).
     38
     39lemma IO_bind_inversion:
     40  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     41  (∀x.f = return x → g x = return y → P) →
     42  (! x ← f ; g x = return y) → P.
     43#O #I #A #B #P #f #g #y cases f normalize
     44[ #o #f #_ #H destruct
     45| #a #G #H @(G ? (refl …) H)
     46| #e #_ #H destruct
     47] qed.
     48
     49interpretation "IO bind inversion" 'bind_inversion =
     50  (IO_bind_inversion ?????????).
     51
     52record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     53  { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
     54  ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
     55  ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
     56      m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
     57                  m_frel ?? Q G (m_bind … m f) (m_bind … n g)
     58  ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
     59  }.
     60
     61(*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
     62  λO,I.mk_MonadFunctRel ??
     63  (λX,Y,F,m,n.∀x.m = return x → n = return F x)
     64  ???.
     65[ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     66| #X #Y #Z #W #F #G *
     67  [ #o #f | #u | #e ] #n #H #f #g #K #x
     68  whd in ⊢ (??%%→?); #EQ destruct(EQ)
     69  >(H ? (refl …)) @K @EQ
     70| #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H %
     71]
     72qed.*)
     73
     74definition res_preserve : MonadFunctRel Res Res ≝
     75  mk_MonadFunctRel ??
     76  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
     77  ???.
     78[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     79| #X #Y #Z #W #P #Q #F #G *
     80  [ #u | #e ] #n #H #f #g #K #x
     81  whd in ⊢ (??%%→?); #EQ destruct(EQ)
     82  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
     83| #X #Y #P #F #G #H #u #v #K #x #EQ
     84  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
     85]
     86qed.
     87
     88definition opt_preserve : MonadFunctRel Option Option ≝
     89  mk_MonadFunctRel ??
     90  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
     91  ???.
     92[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     93| #X #Y #Z #W #P #Q #F #G *
     94  [ | #u ] #n #H #f #g #K #x
     95  whd in ⊢ (??%%→?); #EQ destruct(EQ)
     96  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
     97| #X #Y #P #F #G #H #u #v #K #x #EQ
     98  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
     99]
     100qed.
     101
     102definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
     103  λO,I.mk_MonadFunctRel ??
     104  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
     105  ???.
     106[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
     107| #X #Y #Z #W #P #Q #F #G *
     108  [ #o #f | #u | #e ] #n #H #f #g #K #x
     109  whd in ⊢ (??%%→?); #EQ destruct(EQ)
     110  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
     111| #X #Y #P #F #G #H #u #v #K #x #EQ
     112  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
     113]
     114qed.
     115
     116definition preserving ≝
     117  λM1,M2.λFR : MonadFunctRel M1 M2.
     118  λX,Y,A,B : Type[0].
     119  λP : X → Prop.
     120  λQ : A → Prop.
     121  λF : ∀x : X.P x → Y.
     122  λG : ∀a : A.Q a → B.
     123  λf : X → M1 A.
     124  λg : Y → M2 B.
     125  ∀x,prf.
     126  FR … G
     127    (f x) (g (F x prf)).
     128
     129definition preserving2 ≝
     130  λM1,M2.λFR : MonadFunctRel M1 M2.
     131  λX,Y,Z,W,A,B : Type[0].
     132  λP : X → Prop.
     133  λQ : Y → Prop.
     134  λR : A → Prop.
     135  λF : ∀x : X.P x → Z.
     136  λG : ∀y : Y.Q y → W.
     137  λH : ∀a : A.R a → B.
     138  λf : X → Y → M1 A.
     139  λg : Z → W → M2 B.
     140  ∀x,y,prf1,prf2.
     141  FR … H
     142    (f x y) (g (F x prf1) (G y prf2)).
    19143
    20144definition graph_prog_params ≝
     
    156280 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
    157281 λp,p',graph_prog,sigma,is.opt_safe ….
     282 
     283lemma sigma_is_empty : ∀p,p',graph_prog,sigma.
     284  ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is.
     285#p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta
     286@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
     287
     288lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
     289#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     290
     291lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
     292∀X,Y,P,F,v,n.
     293∀prf.n = return F v prf →
     294FR X Y P F (return v) n.
     295#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
     296
     297lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
     298#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
    158299
    159300lemma sigma_is_pop_commute :
    160  ∀p,p',graph_prog,sigma,is,bv,is'.
     301 ∀p,p',graph_prog,sigma,is.
    161302 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
    162  is_pop is = return 〈bv, is'〉 →
    163  ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
    164  ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
    165  is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
    166 cases daemon qed.
     303 res_preserve …
     304  (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧
     305       sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?)
     306  (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)
     307  (is_pop is) (is_pop (sigma_is … prf)).
     308#p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf
     309[ @res_preserve_error
     310|*:
     311 whd in match sigma_is in ⊢ (?????????%); normalize nodelta
     312 @opt_safe_elim #is'
     313  #H @('bind_inversion H) -H #bv1' #EQ1
     314  [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
     315 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     316 @mfr_return_eq
     317 [1,3: @hide_prf %%
     318 |*: whd in match sigma_beval; whd in match sigma_is;
     319  normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''
     320 ]
     321 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]
     322  whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
     323 [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') %
     324]
     325qed.
     326
     327(* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
     328  opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v).
     329#X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ
     330lapply (H … EQ) cases v [ * ] #y #K @K qed.
     331
     332lemma err_eq_from_io : ∀O,I,X,m,v.
     333  err_to_io O I X m = return v → m = return v.
     334#O #I #X * #x #v normalize #EQ destruct % qed.
     335
     336lemma res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
     337  res_preserve P u v → IO_preserve O I P u v.
     338#X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ
     339lapply (H … EQ) cases v [2: #e * ] #y #K @K qed.
     340
     341lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
     342  res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v.
     343#X #Y #P #e #u #v #H #x #EQ
     344lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ]
     345#y #K @K qed.
     346
     347lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
     348  IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v.
     349#X #Y #P #O #I #u #v #H #x #EQ
     350lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ]
     351#y #K @K qed. *)
    167352
    168353definition well_formed_mem :
     
    211396  nextblock m1 = nextblock m2 → m1 = m2.
    212397
     398lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
     399#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     400
    213401lemma beloadv_sigma_commute:
    214 ∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
    215 beloadv m ptr = return bv →
    216 ∃ prf2.
    217 beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr =
    218                return sigma_beval p p' graph_prog sigma bv prf2.
    219 #p #p' #graph_prog #sigma #m #ptr #bv #prf1
     402∀p,p',graph_prog,sigma,ptr.
     403preserving … opt_preserve …
     404 (sigma_mem p p' graph_prog sigma)
     405 (sigma_beval p p' graph_prog sigma)
     406 (λm.beloadv m ptr)
     407 (λm.beloadv m ptr).
     408#p #p' #graph_prog  #sigma #ptr #m #prf #bv
    220409whd in match beloadv;
    221410whd in match do_if_in_bounds;
     
    238427
    239428lemma bestorev_sigma_commute :
    240 ∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
    241 bestorev m ptr bv = return m' →
    242 ∃prf3.
    243 bestorev (sigma_mem p p' graph_prog sigma m prf1)
    244           ptr
    245           (sigma_beval p p' graph_prog sigma bv prf2)
    246 =
    247 return (sigma_mem p p' graph_prog sigma m' prf3).
    248 #p #p' #graph_prog #sigma #m #ptr #bv #m' #prf1 #prf2
     429∀p,p',graph_prog,sigma,ptr.
     430preserving2 ?? opt_preserve …
     431  (sigma_mem p p' graph_prog sigma)
     432  (sigma_beval p p' graph_prog sigma)
     433  (sigma_mem p p' graph_prog sigma)
     434  (λm.bestorev m ptr)
     435  (λm.bestorev m ptr).
     436#p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m'
    249437whd in match bestorev;
    250438whd in match do_if_in_bounds;
     
    326514  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
    327515; sigma_load_sp_commute :
    328   ∀reg,ptr.
    329   load_sp (make_sem_graph_params p p') reg = return ptr →
    330   ∃prf.
    331   load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
     516  preserving … res_preserve …
     517    (λ_.True)
     518    …
     519    sigma_regs
     520    (λx.λ_.x)
     521    (load_sp (make_sem_graph_params p p'))
     522    (load_sp (make_sem_lin_params p p'))
    332523; sigma_save_sp_commute :
    333524  ∀reg,ptr,prf1. ∃prf2.
     
    361552  (sigma_regs … gsss (regs … st) ?)
    362553  (sigma_mem p p' graph_prog sigma (m … st) ?).
    363 @hide_prf
    364 [ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))
    365 | @(proj2 … (proj1 … prf)) | @(proj2 … prf)]
     554@hide_prf cases prf ** //
    366555qed.
    367556
     
    455644  cases daemon qed.
    456645
    457 (*
    458 inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
    459  | isMemberHead : ∀ tl.isMember A x (x :: tl)
    460  | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
    461 (*
    462 definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →
    463       (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
    464       #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
    465     @(isMemberTail ? x y l tl l_spec tl_member)
    466     qed.
    467   *)             
    468 
    469 let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝
    470 match l with [ nil ⇒ λprf : l = nil ?.nil ?
    471              | cons x tl ⇒ λprf : l = cons ? x tl.
    472               f x ? :: ext_map ?? tl (λy,prf'.f y ?)
    473              ] (refl …).
    474 @hide_prf
    475 >prf
    476 [ %1
    477 | %2 assumption
    478 ] qed.
    479               (f x (isMemberHead A x l tl prf)) ::   
    480               ext_map A B tl (lift_f_tail A B l tl x prf f) ]
    481               (refl ? l).
    482 *)
    483 
    484646definition helper_def_store__commute :
    485647  ∀p,p',graph_prog,sigma.
     
    491653  Prop ≝
    492654  λp,p',graph_prog,sigma,X,gsss,store.
    493   ∀a : X ?.∀bv,r,r',prf1,prf1'.
    494   store … a bv r = return r' →
    495   ∃prf2.
    496   store ??? a
    497     (sigma_beval p p' graph_prog sigma bv prf1')
    498     (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
    499 
     655  ∀a : X p.preserving2 … res_preserve …
     656    (sigma_beval p p' graph_prog sigma)
     657    (sigma_regs … gsss)
     658    (sigma_regs … gsss)
     659    (store … a)
     660    (store … a).
     661 
    500662definition helper_def_retrieve__commute :
    501663  ∀p,p',graph_prog,sigma.
     
    506668  Prop ≝
    507669  λp,p',graph_prog,sigma,X,gsss,retrieve.
    508   ∀a : X p.∀r,bv,prf1.
    509   retrieve … r a = return bv →
    510   ∃prf2.
    511   retrieve … (sigma_regs … gsss r prf1) a
    512      = return sigma_beval p p' graph_prog sigma bv prf2.
    513 
     670  ∀a : X p.
     671  preserving … res_preserve …
     672    (sigma_regs … gsss)
     673    (sigma_beval p p' graph_prog sigma)
     674    (λr.retrieve … r a)
     675    (λr.retrieve … r a).
    514676
    515677record good_state_sigma
     
    533695; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
    534696; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
    535 ; pair_reg_move_commute : ∀mv,r1,r2,prf1.
    536   pair_reg_move_ ? ? (p' ?) r1 mv = return r2 →
    537   ∃prf2 .
    538   pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv =
    539     return sigma_regs p p' graph_prog sigma gsss r2 prf2
    540 ; save_frame_commute :
    541   ∀b,dest,st1,st2,prf1.
    542   save_frame ?? (p' ?) b dest st1 = return st2 →
    543   let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1))
    544     (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
    545   ∃prf2.
    546   save_frame ?? (p' ?) b dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
     697; pair_reg_move_commute : ∀mv.
     698  preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss)
     699    (λr.pair_reg_move_ ? ? (p' ?) r mv)
     700    (λr.pair_reg_move_ ? ? (p' ?) r mv)
    547701; allocate_locals_commute :
    548   ∀ loc, r1, prf1. ∃ prf2.
     702  ∀loc, r1, prf1. ∃ prf2.
    549703  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
    550704  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
     705; save_frame_commute :
     706  ∀dest,fl.
     707  preserving … res_preserve …
     708    (λst : state_pc ?.λprf.
     709      mk_state_pc …
     710        (sigma_state … gsss st (proj2 ?? prf))
     711        (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf)))
     712    (sigma_state … gsss)
     713    (save_frame ?? (p' ?) fl dest)
     714    (save_frame ?? (p' ?) fl dest)
    551715; eval_ext_seq_commute :
    552716  let lin_prog ≝ linearise p graph_prog in
    553717  ∀ stack_sizes.
    554   ∀ext,i,fn,st1,st2,prf1.
    555   eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
    556     ext i fn st1 = return st2 →
    557   ∃prf2.
    558   eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
    559     ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
    560    return sigma_state p p' graph_prog sigma gsss st2 prf2
     718  ∀ext,i,fn.
     719  preserving … res_preserve …
     720    (sigma_state … gsss)
     721    (sigma_state … gsss)
     722    (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
     723      ext i fn)
     724    (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
     725      ext i (\fst (linearise_int_fun … fn)))
     726}.
     727(* TO BE ADAPTED AS ABOVE
    561728; setup_call_commute :
    562729  ∀ n , parsT, call_args , st1 , st2 , prf1.
     
    597764            return mk_state_pc ? st2' pc'
    598765}.
     766*)
    599767
    600768
     
    606774  ∀X : ? → Type[0].
    607775  ∀store.
    608   ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
     776  ∀gsss : good_state_sigma p p' graph_prog sigma.
    609777  ∀H : helper_def_store__commute … gsss store.
    610   ∀a : X p.∀bv,st,st',prf1,prf1'.
    611   helper_def_store ? store … a bv st = return st' →
    612   ∃prf2.
    613   helper_def_store ? store … a
    614     (sigma_beval p p' graph_prog sigma bv prf1')
    615     (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
    616 #p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2
    617 whd in match helper_def_store; normalize nodelta
    618 #H1 elim(bind_inversion ????? H1) -H1 #graph_reg * #store_spec
    619 #EQ whd in EQ : (??%%); destruct(EQ)
    620 elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec)
    621 #wf_graph_reg #store_spec1 %
    622 [ % [ % ] [%] ]
    623 [ @(proj1 … (proj1 … (proj1 … prf1)))
    624 | @(proj2 … (proj1 … (proj1 … prf1)))
    625 | @wf_graph_reg
    626 | @(proj2 … prf1)
    627 ] >store_spec1 >m_return_bind %
    628 qed.
    629 
    630 
     778  ∀a : X p.
     779  preserving2 … res_preserve …
     780    (sigma_beval p p' graph_prog sigma)
     781    (sigma_state … gsss)
     782    (sigma_state … gsss)
     783    (helper_def_store ? store … a)
     784    (helper_def_store ? store … a).
     785#p #p' #graph_prog #sigma #X #store #gsss #H #a
     786#bv #st #prf1 #prf2
     787@(mfr_bind … (sigma_regs … gsss)) [@H]
     788#r #prf3 @mfr_return cases st in prf2;
     789#frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption
     790qed.
    631791
    632792lemma retrieve_commute :
     
    636796 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
    637797 ∀H : helper_def_retrieve__commute … gsss retrieve.
    638  ∀a : X p .∀st,bv,prf1.
    639  helper_def_retrieve ? retrieve … st a = return bv →
    640  ∃prf2.
    641      helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
    642      return sigma_beval p p' graph_prog sigma bv prf2.
    643 #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1
    644 whd in match helper_def_retrieve; normalize nodelta
    645 #retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec)
    646 #wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 %
    647 qed.
     798 ∀a : X p .
     799 preserving … res_preserve …
     800    (sigma_state … gsss)
     801    (sigma_beval p p' graph_prog sigma)
     802    (λst.helper_def_retrieve ? retrieve … st a)
     803    (λst.helper_def_retrieve ? retrieve … st a).
     804#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed.
    648805
    649806(*
     
    686843*)
    687844
    688 lemma res_eq_from_opt :
    689   ∀A,m,v.res_to_opt A m = return v → m = return v.
    690 #A * #x #v normalize #EQ destruct % qed.
    691 
    692845(*
    693846lemma if_of_function_commute:
     
    702855 @prog_if_of_function_transform % qed.
    703856*)
    704 lemma bind_option_inversion_star:
    705   ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
    706   (∀x.f = Some … x → g x = Some … y → P) →
    707   (! x ← f ; g x = Some … y) → P.
    708 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
    709 
    710 interpretation "option bind inversion" 'bind_inversion =
    711   (bind_option_inversion_star ???????).
    712 
    713857lemma sigma_pblock_eq_lemma :
    714858∀p,p',graph_prog.
     
    720864 #p #p' #graph_prog #sigma #pc #prf
    721865 whd in match sigma_pc; normalize nodelta
    722  @opt_safe_elim #x @'bind_inversion * #i #fn #_
    723  @'bind_inversion #n #_ whd in ⊢ (??%?→?);
     866 @opt_safe_elim #x #H @('bind_inversion H) -H * #i #fn #_
     867 #H @('bind_inversion H) -H #n #_ whd in ⊢ (??%?→?);
    724868 #EQ destruct %
    725869qed.
     
    8811025 whd in match fetch_function; normalize nodelta
    8821026 #H lapply (opt_eq_from_res ???? H) -H
    883  @'bind_inversion #id #eq_symbol_for_block
    884  @'bind_inversion #fd #eq_find_funct
     1027 #H @('bind_inversion H) -H #id #eq_symbol_for_block
     1028 #H @('bind_inversion H) -H #fd #eq_find_funct
    8851029 whd in ⊢ (??%?→?); #EQ destruct(EQ)
    8861030 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
    887  >(find_funct_ptr_transf A B …  eq_find_funct) >m_return_bind %
    888 qed.
    889 
    890 lemma bind_inversion_star : ∀X,Y.∀P : Prop.
    891 ∀m : res X.∀f : X → res Y.∀v : Y.
    892 (∀x. m = return x → f x = return v → P) →
    893 ! x ← m ; f x = return v → P.
    894 #X #Y #P #m #f #v #H #G
    895 elim (bind_inversion ????? G) #x * @H qed.
    896 
    897 interpretation "res bind inversion" 'bind_inversion =
    898   (bind_inversion_star ???????).
     1031 >(find_funct_ptr_transf A B …  eq_find_funct) %
     1032qed.
    8991033
    9001034lemma fetch_internal_function_transf :
     
    9091043#A #B #prog #trans #bl #i #f
    9101044 whd in match fetch_internal_function; normalize nodelta
    911  @'bind_inversion * #id * #fd normalize nodelta #EQfetch
     1045 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
    9121046 whd in ⊢ (??%%→?); #EQ destruct(EQ)
    9131047 >(fetch_function_transf … EQfetch) %
     
    10051139//
    10061140qed.
    1007   
     1141 
    10081142(*
    10091143
     
    10381172
    10391173lemma pc_of_label_sigma_commute :
    1040   ∀p,p',graph_prog,pc,lbl,i,fn.
     1174  ∀p,p',graph_prog,bl,lbl,i,fn.
    10411175  let lin_prog ≝ linearise ? graph_prog in
    10421176  ∀sigma.good_sigma p graph_prog sigma →
    1043   ∀prf : well_formed_pc p p' graph_prog sigma pc.
    10441177  fetch_internal_function …
    1045     (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 →
    1046   let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in
     1178    (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 →
     1179  let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in
    10471180  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
    10481181  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
    1049     (pc_block (sigma_pc … pc prf)) lbl =
     1182    bl lbl =
    10501183        return sigma_pc p p' graph_prog sigma pc' prf'.
    1051 #p #p' #graph_prog #pc #lbl #i #fn
     1184#p #p' #graph_prog #bl #lbl #i #fn
    10521185#sigma #good cases (good fn) -good * #_ #all_labels_in
    1053 #good #prf #fetchfn >lin_code_has_label #lbl_in
     1186#good #fetchfn >lin_code_has_label #lbl_in
    10541187whd in match pc_of_label; normalize nodelta
    1055 >sigma_pblock_eq_lemma
    10561188> (fetch_internal_function_transf … fetchfn) >m_return_bind
    10571189inversion (point_of_label ????)
     
    10991231  All ? (λlbl.well_formed_pc p p' graph_prog sigma
    11001232      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
    1101     (stmt_explicit_labels … stmt) ∧
     1233    (stmt_labels … stmt) ∧
    11021234  match stmt with
    11031235  [  sequential s nxt ⇒
     
    11451277lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt)
    11461278[@lin_pt_spec|] * #H1 #H2 %
    1147 [ -H2 @(All_mp … (All_append_r … H1)) #lab #lab_spec
     1279[ -H2 @(All_mp … H1) #lab #lab_spec
    11481280  whd in match well_formed_pc; normalize nodelta
    11491281  whd in match sigma_pc_opt; normalize nodelta >fetchfn
     
    11731305        whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
    11741306        cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
    1175         lapply all_labels_spec #Z
    1176         lapply(All_nth ? ? 0 ? Z nxt) whd in match stmt_labels; normalize nodelta
    1177         #Z1 normalize in Z1; lapply(Z1 ?) [%] inversion(sigma ??)
    1178         [#_ #ABS @⊥ elim ABS #ABS @ABS %] #sn #sigma_graph_f_spec >sigma_graph_f_spec
    1179         #_ #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
     1307        cases all_labels_spec #Z #_ #sn
     1308        whd in match (point_of_succ ???);
     1309        >(opt_to_opt_safe … Z) % #ABS whd in ABS : (??%?); destruct(ABS)
    11801310      | cases(proj2 … H3)
    11811311        [ #Z %1 whd in match sigma_pc; normalize nodelta
    11821312          @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta
    11831313          >lin_pc_spec #EQ destruct(EQ)
    1184           @opt_safe_elim #pc2 >fetchfn >m_return_bind
    1185           whd in match point_of_pc; whd in match succ_pc; normalize nodelta
    1186           whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
     1314          @opt_safe_elim #pc2 >fetchfn >m_return_bind >graph_succ_pc
     1315          >point_of_pc_of_point
    11871316          >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ)
     1317          whd in match succ_pc;
    11881318          whd in match point_of_pc; whd in match point_of_succ; normalize nodelta
    11891319          >point_of_offset_of_point %
     
    12061336   ]
    12071337   | cases H3
    1208       [ * #Z1 #Z2 %1 % [ @hide_prf  whd in match well_formed_pc; normalize nodelta
     1338      [ * #Z1 #Z2 %1 % [ @hide_prf  whd in match well_formed_pc;
    12091339        whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
    1210         whd in match point_of_pc; whd in match succ_pc; normalize nodelta
    1211         whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
    1212         >Z2 >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
     1340        >graph_succ_pc >point_of_pc_of_point
     1341        >Z2 % #ABS whd in ABS : (??%?); destruct(ABS)
    12131342      ] %
    12141343      [ whd in match sigma_pc; normalize nodelta
     
    12801409@opt_safe_elim -H
    12811410#res #_
    1282 #H lapply (res_eq_from_opt ??? H) -H
     1411#H
    12831412#H  @('bind_inversion H) -H
    12841413* #f #stmt
     
    13351464qed.
    13361465
    1337 lemma IO_bind_inversion:
    1338   ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    1339   (∀x.f = return x → g x = return y → P) →
    1340   (! x ← f ; g x = return y) → P.
    1341 #O #I #A #B #P #f #g #y cases f normalize
    1342 [ #o #f #_ #H destruct
    1343 | #a #G #H @(G ? (refl …) H)
    1344 | #e #_ #H destruct
    1345 ] qed.
    1346 
    1347 interpretation "IO bind inversion" 'bind_inversion =
    1348   (IO_bind_inversion ?????????).
    1349 
    1350 lemma err_eq_from_io : ∀O,I,X,m,v.
    1351   err_to_io O I X m = return v → m = return v.
    1352 #O #I #X * #x #v normalize #EQ destruct % qed.
    1353 
    1354 lemma err_eq_to_io : ∀O,I,X,m,v.
    1355    m = return v → err_to_io O I X m = return v.
    1356 #O #I #X #m #v #H >H //
    1357 qed.
    1358 
    13591466lemma set_istack_sigma_commute :
    1360 ∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2.
    1361 sigma_is_opt p p' graph_prog sigma is = return sigma_is →
    1362 set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) =
    1363 sigma_state ???? gss (set_istack ? is st) prf2.
    1364 #p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H
     1467∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3.
     1468set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) =
     1469sigma_state ???? gss (set_istack ? is st) prf3.
     1470#p #p' #graph_prog #sigma #gss *
     1471#frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed.
     1472(* #st #is #sigmais #prf1 #prf2 #H
    13651473whd in match set_istack; normalize nodelta
    13661474whd in match sigma_state; normalize nodelta
     
    13691477cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
    13701478#EQ >EQ //
    1371 qed.
     1479qed.*)
    13721480
    13731481(* this should make things easier for ops using memory (where pc cant happen) *)
     
    13911499qed.
    13921500
     1501lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
     1502bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
     1503#p #p' #graph_prog #sigma *
     1504[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
     1505% whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
     1506
    13931507lemma is_push_sigma_commute :
    1394 ∀ p, p', graph_prog,sigma,is,val,is',prf1,prf2.
    1395 (is_push is val=return is') →
    1396 ∃prf3.
    1397 is_push (sigma_is p p' graph_prog sigma is prf1)
    1398   (sigma_beval p p' graph_prog sigma val prf2) =
    1399 return sigma_is p p' graph_prog sigma is' prf3.
     1508∀ p, p', graph_prog,sigma.
     1509preserving2 … res_preserve …
     1510  (sigma_is p p' graph_prog sigma)
     1511  (sigma_beval p p' graph_prog sigma) 
     1512  (sigma_is p p' graph_prog sigma)
     1513  is_push is_push.
    14001514#p #p' #graph_prog #sigma *
    1401 [ | #bv1 | #bv1 #bv2 ] #val #is' #prf1 #prf2
     1515[ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is'
    14021516whd in ⊢ (??%%→?); #EQ destruct(EQ)
    14031517whd in match sigma_beval; normalize nodelta
     
    14231537qed.
    14241538
     1539lemma byte_of_val_inv :
     1540  ∀e,bv,v.Byte_of_val e bv = return v → bv = BVByte v.
     1541#e *
     1542[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] #v
     1543whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
     1544
     1545lemma bit_of_val_inv :
     1546  ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v.
     1547#e *
     1548[ #b || #b #ptr #p #o ] #v
     1549whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
     1550
    14251551lemma beopaccs_sigma_commute :
    1426 ∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2.
    1427 ∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?.
    1428 ∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?.
    1429 be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 →
    1430 ∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?.
    1431 ∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?.
    1432 be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) =
    1433 return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉.
     1552∀p,p',graph_prog,sigma,op.
     1553preserving2 … res_preserve …
     1554  (sigma_beval p p' graph_prog sigma)
     1555  (sigma_beval p p' graph_prog sigma)
     1556  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
     1557            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
     1558  (be_opaccs op) (be_opaccs op).
    14341559#p #p' #graph_prog #sigma #op
     1560#bv1 #bv2 #prf1 #prf2
     1561@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
     1562[2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
     1563  [2: #by2 * cases (opaccs ????) #by1' #by2'
     1564    @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1565  ]
     1566]
     1567#v #EQ %{I}
     1568>sigma_bv_no_pc try assumption
     1569>(byte_of_val_inv … EQ) %
     1570qed.
     1571
     1572lemma beop1_sigma_commute :
     1573∀p,p',graph_prog,sigma,op.
     1574preserving … res_preserve …
     1575  (sigma_beval p p' graph_prog sigma)
     1576  (sigma_beval p p' graph_prog sigma)
     1577  (be_op1 op) (be_op1 op).
     1578#p #p' #graph_prog #sigma #op
     1579#bv #prf
     1580@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
     1581[2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
     1582#v #EQ %{I} >sigma_bv_no_pc try assumption
     1583>(byte_of_val_inv … EQ) %
     1584qed.
     1585
     1586
     1587lemma sigma_ptr_commute :
     1588∀ p, p', graph_prog , sigma.
     1589preserving … res_preserve …
     1590  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
     1591            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
     1592  (λx.λ_ : True.x)
     1593  pointer_of_address pointer_of_address.
     1594#p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2
     1595#ptr whd in ⊢ (??%?→?);
     1596cases val1 in prf1;
     1597[|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ]
     1598#prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
     1599cases val2 in prf2 EQ;
     1600[|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ]
     1601#prf2 normalize nodelta #EQ destruct(EQ)
     1602%{I}
     1603>sigma_bv_no_pc [2: %]
     1604>sigma_bv_no_pc [2: %] @EQ
     1605qed.
     1606
     1607lemma beop2_sigma_commute :
     1608∀p,p',graph_prog,sigma,carry,op.
     1609preserving2 … res_preserve …
     1610  (sigma_beval p p' graph_prog sigma)
     1611  (sigma_beval p p' graph_prog sigma)
     1612  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉)
     1613  (be_op2 carry op) (be_op2 carry op).
     1614#p #p' #graph_prog #sigma #carry #op
    14351615@bv_pc_other
    1436 [ #pc1 #p1 #val2
    1437 | #val1 #val1_no_pc @bv_pc_other
    1438   [ #pc #p | #val2 #val2_no_pc ]
    1439 
    1440 #opaccs1 #opaccs2
    1441 #prf1 #prf2
    1442 [1,2: [2: #H @('bind_inversion H) #by1 #_ ]
    1443   whd in ⊢ (??%%→?); #EQ destruct]
     1616[ #pc1 #p1 #bv2
     1617| #bv1 #bv1_no_pc
     1618  @bv_pc_other
     1619  [ #pc2 #p2
     1620  | #bv2 #bv2_no_pc
     1621  ]
     1622] #prf1 #prf2
     1623* #res #carry'
     1624[1,2:
     1625  [2: cases bv1 in prf1;
     1626    [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ]
     1627   whd in ⊢ (??%%→?);
     1628  #EQ destruct(EQ) ]
    14441629#EQ
    1445 >(sigma_bv_no_pc … val1_no_pc)
    1446 >(sigma_bv_no_pc … val2_no_pc)
    1447 cut (bv_no_pc opaccs1 ∧ bv_no_pc opaccs2)
    1448 [ cases val1 in EQ; cases daemon ] *
    1449 #H1 #H2 @('bind_inversion EQ) #bt #bt_spec
    1450 #H3 @('bind_inversion H3) #bt'
    1451 #bt_spec' cases (opaccs eval op bt bt')
    1452 #ev_bt #ev_bt' normalize nodelta
    1453 #EQ1 whd in EQ1 : (??%%); destruct(EQ1)
    1454 % [ whd in match sigma_beval_opt ; normalize nodelta %
    1455 #ABS whd in ABS : (??%?); destruct(ABS) ]
    1456 % [ whd in match sigma_beval_opt ; normalize nodelta %
    1457 #ABS whd in ABS : (??%?); destruct(ABS) ]
    1458 >(sigma_bv_no_pc … H1)
    1459 >(sigma_bv_no_pc … H2) assumption
    1460 qed.
    1461 
    1462 lemma sigma_ptr_commute :
    1463 ∀ p, p', graph_prog , sigma , val1, val2, ptr, prf1, prf2.
    1464 pointer_of_address 〈val1,val2〉= return ptr →
    1465 pointer_of_address 〈sigma_beval p p' graph_prog sigma val1 prf1,
    1466                     sigma_beval p p' graph_prog sigma val2 prf2〉 = return ptr.
    1467 #p #p' #graph_prog #sigma #val1 #val2 #ptr #prf1 #prf2
    1468 whd in match sigma_beval; normalize nodelta
    1469 @opt_safe_elim #sigma_val1 #sigma_val1_spec
    1470 @opt_safe_elim #sigma_Val2 #sigma_val2_spec
    1471 whd in match pointer_of_address; whd in match pointer_of_bevals;
    1472 normalize nodelta cases val1 in sigma_val1_spec; normalize nodelta
    1473   [1,2,3,4,5: [|| #ptr1 #ptr2 #p | #by | #p] #_ #ABS whd in ABS : (??%%); destruct(ABS)
    1474   |   #ptr2 #p2 whd in match sigma_beval_opt; normalize nodelta
    1475       #EQ whd in EQ : (??%%); destruct(EQ) cases val2 in sigma_val2_spec; normalize nodelta
    1476       [1,2,3,4,5: [|| #ptr1 #ptr2 #p | #by | #p] #_ #ABS whd in ABS : (??%%); destruct(ABS)
    1477       |  #ptr1 #p1 whd in match sigma_beval_opt; normalize nodelta
    1478          #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta //
    1479       | #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)
     1630cut (bv_no_pc res)
     1631[ -prf1 -prf2
     1632  cases bv1 in bv1_no_pc EQ;
     1633  [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] *
     1634  cases bv2 in bv2_no_pc;
     1635  [3,10,17,24,31,38: #ptr21 #ptr22 #p2
     1636  |4,11,18,25,32,39: #by2
     1637  |5,12,19,26,33,40: #p2
     1638  |6,13,20,27,34,41: #ptr2 #p2
     1639  |7,14,21,28,35,42: #pc2 #p2
     1640  ] *
     1641  cases op
     1642  whd in match be_op2; whd in ⊢ (???%→?);
     1643  normalize nodelta
     1644  #EQ destruct(EQ) try %
     1645  try (whd in EQ : (??%?); destruct(EQ) %)
     1646  lapply EQ -EQ
     1647  [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1648  |2,12,13,16,18: @if_elim #_  whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1649  |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ
     1650    cases (op2 eval bit ???) #res' #bit'
     1651    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1652  |17: cases (ptype ptr1) normalize nodelta
     1653    [ @if_elim #_
     1654      [ #H @('bind_inversion H) #bit #EQbit
     1655      cases (op2 eval bit ???) #res' #bit'
    14801656      ]
    1481   |   #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)
     1657    ]
     1658    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
     1659  |*: whd in ⊢ (??%?→?);
     1660    cases (ptype ?) normalize nodelta
     1661    try (#EQ destruct(EQ) @I)
     1662    cases (part_no ?) normalize nodelta
     1663    try (#n lapply (refl ℕ n) #_)
     1664    try (#EQ destruct(EQ) @I)
     1665    try (#H @('bind_inversion H) -H * #EQbit
     1666         whd in ⊢ (??%%→?);)
     1667    try (#EQ destruct(EQ) @I)
     1668    [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?);
     1669         #EQ destruct(EQ) @I
     1670    |*: cases carry normalize nodelta
     1671      try (#b lapply (refl bool b) #_)
     1672      try (#ptr lapply (refl pointer ptr) #_ #p #o)
     1673      try (#EQ destruct(EQ) @I)
     1674      @if_elim #_
     1675      try (#EQ destruct(EQ) @I)
     1676      @If_elim #prf
     1677      try (#EQ destruct(EQ) @I)
     1678      cases (op2_bytes ?????)
     1679      #res' #bit' whd in ⊢ (??%%→?);
     1680      #EQ destruct(EQ) @I
     1681    ]
    14821682  ]
    1483 skip
    1484 qed.
    1485  
     1683] #res_no_pc
     1684%{(bv_no_pc_wf … res_no_pc)}
     1685>(sigma_bv_no_pc … bv1_no_pc)
     1686>(sigma_bv_no_pc … bv2_no_pc)
     1687>(sigma_bv_no_pc … res_no_pc)
     1688assumption
     1689qed.
     1690
     1691definition combine_strong :
     1692  ∀A,B,C,D : Type[0].
     1693  ∀P : A → Prop.∀Q : C → Prop.
     1694  (∀x.P x → B) → (∀x.Q x → D) →
     1695  (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝
     1696λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉.
     1697
     1698lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.
     1699well_formed_state p p' graph_prog sigma gss st →
     1700well_formed_regs … gss r →
     1701well_formed_state … gss (set_regs … r st).
     1702#p #p' #graph_prog #sigma #gss #st #r
     1703*** #H1 #H2 #_ #H4 #H3
     1704%{H4} %{H3} %{H2} @H1
     1705qed.
     1706
     1707lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is.
     1708well_formed_state p p' graph_prog sigma gss st →
     1709sigma_is_opt p p' graph_prog sigma is ≠ None ? →
     1710well_formed_state … gss (set_istack … is st).
     1711#p #p' #graph_prog #sigma #gss #st #is
     1712*** #H1 #H2 #H3 #H4 #H5
     1713%{H4} %{H3} %{H5} @H1
     1714qed.
     1715
     1716lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m.
     1717well_formed_state p p' graph_prog sigma gss st →
     1718well_formed_mem p p' graph_prog sigma m →
     1719well_formed_state … gss (set_m … m st).
     1720#p #p' #graph_prog #sigma #gss #st #m
     1721*** #H1 #H2 #H3 #H4 #H5
     1722%{H5} %{H3} %{H2} @H1
     1723qed.
     1724
     1725lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
     1726       opt_preserve X Y P F m n →
     1727       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
     1728#X #Y #P #F #m #n #e1 #e2 #H #v #prf
     1729cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
     1730>EQ %
     1731qed.
     1732
     1733lemma err_eq_from_io : ∀O,I,X,m,v.
     1734  err_to_io O I X m = return v → m = return v.
     1735#O #I #X * #x #v normalize #EQ destruct % qed.
     1736
     1737lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
     1738       res_preserve X Y P F m n →
     1739       io_preserve O I X Y P F m n.
     1740#O #I #X #Y #P #F #m #n #H #v #prf
     1741cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
     1742>EQ %
     1743qed.
    14861744
    14871745lemma eval_seq_no_pc_sigma_commute :
     
    14901748 ∀stack_sizes.
    14911749 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
    1492  ∀f,fn,st,stmt,st'.
    1493  ∀prf : well_formed_state … gss st.
    1494   eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    1495    f fn stmt st = return st' →
    1496   ∃prf'.
    1497   eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    1498     f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
    1499   return sigma_state … gss st' prf'.
     1750 ∀f,fn,stmt.
     1751 preserving … res_preserve …
     1752   (sigma_state … gss)
     1753   (sigma_state … gss)
     1754   (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
     1755      f fn stmt)
     1756   (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
     1757      f (\fst (linearise_int_fun … fn)) stmt).
    15001758  #p #p' #graph_prog #stack_sizes #sigma #gss #f
    1501   #fn #st #stmt
    1502   #st' #prf
     1759  #fn #stmt
    15031760  whd in match eval_seq_no_pc;
    15041761  cases stmt normalize nodelta
    1505   [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
    1506   | (* MOVE *) #mv_sig #H
    1507     whd in match pair_reg_move; normalize nodelta
    1508     @('bind_inversion H) -H #reg #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1509     elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec)
    1510     #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %]
    1511     % [ 2: @(proj2 … prf)
    1512       |    % [2: assumption] %
    1513              [ @(proj1 … (proj1 … (proj1 … prf)))
    1514              | @(proj2 … (proj1 … (proj1 … prf)))
    1515              ]
    1516       ]
     1762  [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return
     1763  | (* MOVE *) #mv_sig #st #prf'
     1764    @(mfr_bind … (sigma_regs … gss))
     1765    [ @pair_reg_move_commute
     1766    | #r #prf @mfr_return @wf_set_regs assumption
     1767    ]
    15171768  | (* POP *)
    1518     #a #H @('bind_inversion H) -H
    1519     * #val #st1 #vals_spec #H
    1520     lapply vals_spec -vals_spec
    1521     whd in match pop; normalize nodelta
    1522     whd in match is_pop; normalize nodelta
    1523     lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is
    1524     inversion (istack (make_sem_graph_params p p') st) normalize nodelta
    1525     [#_ #ABS normalize in ABS; destruct(ABS)]
    1526     [ #Bv | #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind
    1527     #EQ whd in EQ : (??%%); destruct(EQ)
    1528     elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H)
    1529     [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is
    1530            whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is;
    1531            inversion(sigma_beval_opt ?????)
    1532            [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS //
    1533                   inversion(sigma_beval_opt ?????) normalize nodelta
    1534                   [ #bev %
    1535                   | #bev #bev_s >bev_s in ABS; normalize nodelta
    1536                     #ABS @⊥ @ABS normalize %
    1537                   ]
    1538            ]
    1539            [#H1 #H2 % #ABS destruct(ABS) | #H1 #H2 % #ABS destruct(ABS)]
     1769    #a #st #prf
     1770    @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss)))
     1771    [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2'
     1772      @mfr_return %{prf1'} @wf_set_is assumption
     1773    | * #bv #st' * #prf1' #prf2'
     1774      @mfr_bind [3: @acca_store__commute |*:]
     1775      #r #prf3' @mfr_return @wf_set_regs assumption
    15401776    ]
    1541     [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))]
    1542              % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))]
    1543              whd in match sigma_is_opt; normalize nodelta
    1544              [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)]
    1545              >is_stack_st_spec in wf_is;
    1546              whd in match sigma_is_opt; normalize nodelta
    1547              cases(sigma_beval_opt ?????)
    1548              [ normalize * #ABS @⊥ @ABS %
    1549              | #bev #_ normalize % #ABS destruct(ABS)
    1550              ]
    1551      ] 
    1552      #prf' #acca_store_commute %{prf'}     
    1553     whd in match sigma_state in ⊢ (??(?????(?????%?)?)?);
    1554     whd in match sigma_is; normalize nodelta
    1555     @opt_safe_elim #int_stack #int_stack_sigma_spec
    1556     >is_stack_st_spec in int_stack_sigma_spec;
    1557     whd in match sigma_is_opt; normalize nodelta
    1558     #IS_SPEC @('bind_inversion IS_SPEC) -IS_SPEC
    1559     [ #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1560     | #sigma_bv_not_used #sigma_bv_not_used_spec #IS_SPEC
    1561       @('bind_inversion IS_SPEC) -IS_SPEC
    1562       #sigma_bv  #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
    1563       normalize nodelta >m_return_bind
    1564       <acca_store_commute
    1565       whd in match helper_def_store;  whd in match acca_store;
    1566       whd in match sigma_beval; normalize nodelta
    1567      @opt_safe_elim #xx #xx_spec
    1568      [  >xx_spec in sigma_bv_spec; #EQ destruct(EQ) //
    1569      | cut(xx =sigma_bv) [>xx_spec in sigma_bv_spec; #EQ destruct(EQ) %]
    1570        #EQ >EQ @m_bind_ext_eq #reg
    1571        change with (return set_regs (make_sem_lin_params p p') ?
    1572                                    (set_istack (make_sem_lin_params p p') ? ?) = ?);
    1573        >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)
    1574        [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec
    1575            >m_return_bind whd in ⊢ (??%%); % | % |]
    1576      ]
    15771777  | (* PUSH *)
    1578      #a #H @('bind_inversion H) -H
    1579      #val  #graph_ret_spec
    1580      change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?)
    1581      #graph_push_spec
    1582      elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf graph_ret_spec)
    1583      #val_wf #acca_arg_retrieve_commute
    1584      whd in match push in graph_push_spec; normalize nodelta  in graph_push_spec;
    1585      @('bind_inversion graph_push_spec) -graph_push_spec
    1586      #int_stack #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1587      %
    1588      [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]]
    1589        [2: @(proj2 … (proj1 … prf))] [2: @(proj2 … prf)]
    1590        lapply int_stack_spec -int_stack_spec
    1591        cases int_stack
    1592        [  whd in match is_push; normalize nodelta 
    1593           cases(istack ? ?) normalize nodelta
    1594           [2: #x ] [3: #x #y] #EQ whd in EQ : (??%%); destruct(EQ)
    1595        |2,3: [#x | #y #x ] whd in match is_push; normalize nodelta
    1596         inversion(istack ? ?) normalize nodelta
    1597         [ #_ #EQ whd in EQ : (??%%); destruct(EQ)
    1598            whd in match sigma_is_opt; normalize nodelta
    1599            inversion(sigma_beval_opt ?????)
    1600            [  #EQ @⊥ elim val_wf #H @H //
    1601            |  #z #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
    1602            ]
    1603         | #x #_ #ABS whd in ABS : (??%%); destruct(ABS)
    1604         | #x #y #_ #ABS whd in ABS : (???%); destruct(ABS)
    1605         | #_ #ABS whd in ABS : (??%%); destruct(ABS)
    1606         | #z #H #EQ whd in EQ : (??%%); destruct(EQ)
    1607           whd in match sigma_is_opt; normalize nodelta
    1608           inversion(sigma_beval_opt ???? y)
    1609           [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))     
    1610            whd in match sigma_is_opt; >H normalize nodelta >ABS
    1611            whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
    1612           | #sigma_y #H >m_return_bind
    1613             cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %]
    1614             #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H)
    1615           ]
    1616         | #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ)
    1617           ]
    1618         ]
    1619      | change with (acca_arg_retrieve ????? = ?) in acca_arg_retrieve_commute;
    1620        >acca_arg_retrieve_commute in ⊢ (??%?); >m_return_bind
    1621        elim(is_push_sigma_commute … (proj2 … (proj1 …(proj1 … prf))) val_wf int_stack_spec)
    1622           #wf_is #EQ whd in match push; normalize nodelta >EQ %
     1778     #a #st #prf
     1779     @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1780     [ @acca_arg_retrieve_commute
     1781     | #bv #prf_bv
     1782       @(mfr_bind … (sigma_is p p' graph_prog sigma))
     1783       [ @is_push_sigma_commute
     1784       | #is #prf_is @mfr_return @wf_set_is assumption
     1785       ]
    16231786     ]
    16241787  | (*C_ADDRESS*)
     
    16281791    change with ((dpl_reg p) → ?) #dpl 
    16291792    change with ((dph_reg p) → ?) #dph
    1630     change with ((( ! st1 ← dpl_store p
    1631                                      (joint_closed_internal_function (make_sem_graph_params p p'))
    1632                                      ?
    1633                                      ?
    1634                                      ?
    1635                                      ? ; ? ) = ?) → ?)
    1636     change with ((( ! st1 ← dpl_store ????
    1637     (BVptr
    1638       (mk_pointer
    1639          (opt_safe block
    1640            (find_symbol
    1641               (fundef
    1642                  (joint_closed_internal_function
    1643                     (make_sem_graph_params p p')
    1644                     ?
    1645                   )
    1646                )
    1647                (globalenv_noinit ? graph_prog)
    1648                ?
    1649            )
    1650            ?
    1651          )
    1652          ?
    1653       )
    1654       ?
    1655     ) ? ; ?) = ?) → ?)
    1656     change with ((( ! st1 ← ? ;
    1657         dph_store p (joint_closed_internal_function (make_sem_graph_params p p'))
    1658                   ? ?
    1659                   (BVptr
    1660       (mk_pointer
    1661          (opt_safe block
    1662            (find_symbol
    1663               (fundef
    1664                  (joint_closed_internal_function
    1665                     (make_sem_graph_params p p')
    1666                     ?
    1667                   )
    1668                )
    1669                (globalenv_noinit ? graph_prog)
    1670                ?
    1671            )
    1672            ?
    1673          )
    1674          ?
    1675       )
    1676       ?
    1677     ) ?) = ?) → ?)
    1678     #H @('bind_inversion H) -H
    1679     #st1 #dpl_st1
    1680     elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1)
    1681     [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); %
    1682         #ABS destruct(ABS)]
    1683     #wf_st1 whd in match helper_def_store; normalize nodelta
    1684     #H @('bind_inversion H) -H #reg1 #reg1_spec #EQ whd in EQ : (??%%);
    1685     destruct(EQ) -EQ
    1686     #dph_st'
    1687     elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st')
    1688     [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?));
    1689         % #ABS destruct(ABS)]
    1690     #wf_st' whd in match helper_def_store; normalize nodelta
    1691     #H @('bind_inversion H) -H #reg2 #reg2_spec #EQ whd in EQ : (??%%);
    1692     destruct(EQ) -EQ %{wf_st'} <e1
    1693     whd in match dpl_store; normalize nodelta
    1694     whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec;
    1695     whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec;
    1696     lapply reg1_spec -reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?);
    1697     destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec
    1698     #reg1_spec @opt_safe_elim #block_lin #block_lin_spec
    1699     cut(find_symbol
    1700          (fundef
    1701             (joint_closed_internal_function
    1702                 (make_sem_lin_params p p')
    1703                 (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog))
    1704             )
    1705           )
    1706           (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog))
    1707           sy
    1708           =
    1709           find_symbol
    1710             (fundef
    1711                (joint_closed_internal_function
    1712                    (make_sem_graph_params p p')
    1713                    (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)
    1714                )
    1715             )
    1716             (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog)
    1717             sy)   
    1718     [ @find_symbol_transf]
    1719     #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec
    1720     #EQ destruct(EQ) >reg1_spec >m_return_bind
    1721     whd in match dph_store; normalize nodelta
    1722     lapply reg2_spec -reg2_spec
    1723     whd in match sigma_beval; normalize nodelta
    1724     @opt_safe_elim #y
    1725     whd in match sigma_beval_opt; normalize nodelta
    1726     whd in ⊢((??%?)→?); #EQ destruct(EQ)
    1727     @opt_safe_elim #graph_block >block_graph_spec
    1728     #EQ destruct(EQ) #reg2_spec
    1729     cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 =
    1730     (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
    1731           reg1 (sigma_state p p' graph_prog sigma gss st prf)))
    1732     [whd in match set_regs; normalize nodelta >e0 %]
    1733     #sigma_st1_spec <sigma_st1_spec >reg2_spec
    1734     >m_return_bind %
     1793    #st #prf
     1794    @(mfr_bind … (sigma_state … gss))
     1795    [ @(mfr_bind … (sigma_regs … gss))
     1796      [2: #r #prf' @mfr_return @wf_set_regs assumption ]
     1797    ]
     1798    @opt_safe_elim #bl #EQbl
     1799    @opt_safe_elim #bl'
     1800    >(find_symbol_transf …
     1801          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?);
     1802    >EQbl in ⊢ (%→?); #EQ destruct(EQ)
     1803    [ @dpl_store_commute
     1804    | #st' #st_prf'
     1805      @mfr_bind [3: @dph_store_commute |*:]
     1806      [2: #r #prf' @mfr_return @wf_set_regs assumption
     1807      ]
     1808    ] @bv_no_pc_wf %
    17351809  | (*C_OPACCS*)
    1736     #op #a #b #arg1 #arg2
    1737     #H @('bind_inversion H) -H
    1738     #val1 #val1_spec
    1739     elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec)
    1740     #wf_val1 #sigma_val1_commute
    1741     #H @('bind_inversion H) -H #val2 #val2_spec
    1742     elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec)
    1743     #wf_val2 #sigma_val2_commute
    1744     #H @('bind_inversion H) -H *
    1745     #opaccs1 #opaccs2 #opaccs_spec
    1746     elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec)
    1747     #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute
    1748     #H @('bind_inversion H) -H #st1 #st1_spec
    1749     elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec)
    1750     #wf_st1 #sigma_st1_commute #final_spec
    1751     elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec)
    1752     #wf_st' #sigma_final_commute
    1753     %{wf_st'}
    1754     whd in match helper_def_retrieve in sigma_val1_commute;
    1755     normalize nodelta in sigma_val1_commute;
    1756     whd in match acca_arg_retrieve; normalize nodelta
    1757     >sigma_val1_commute >m_return_bind
    1758     whd in match helper_def_retrieve in sigma_val2_commute;
    1759     normalize nodelta in sigma_val2_commute;
    1760     whd in match accb_arg_retrieve; normalize nodelta
    1761     >sigma_val2_commute >m_return_bind
    1762     >be_opaccs_commute >m_return_bind
    1763     whd in match helper_def_store in sigma_st1_commute;
    1764     normalize nodelta in sigma_st1_commute;
    1765     @('bind_inversion sigma_st1_commute)
    1766     #reg1 #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1767     whd in match acca_store; normalize nodelta
    1768     >reg1_spec >m_return_bind
    1769     whd in match set_regs; normalize nodelta >e0
    1770     whd in match helper_def_store in sigma_final_commute;
    1771     normalize nodelta in sigma_final_commute;
    1772     @('bind_inversion sigma_final_commute)
    1773     #reg2 #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1774     whd in match accb_store; normalize nodelta
    1775     >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta
    1776     >e1 %
     1810    #op #a #b #arg1 #arg2 #st #prf
     1811    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1812    [ @acca_arg_retrieve_commute ]
     1813    #bv1 #bv1_prf
     1814    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1815    [ @accb_arg_retrieve_commute ]
     1816    #bv2 #bv2_prf
     1817    @(mfr_bind … (combine_strong …
     1818        (sigma_beval p p' graph_prog sigma)
     1819        (sigma_beval p p' graph_prog sigma)))
     1820    [ @beopaccs_sigma_commute ]
     1821    * #res1 #res2 * #res1_prf #res2_prf
     1822    @(mfr_bind … (sigma_state … gss))
     1823    [ @mfr_bind [3: @acca_store__commute |*: ]
     1824      #r #r_prf @mfr_return @wf_set_regs assumption
     1825    ]
     1826    #st' #st_prf'
     1827    @mfr_bind [3: @accb_store_commute |*: ]
     1828    #r #r_prf @mfr_return @wf_set_regs assumption
    17771829  | (*C_OP1*)
    1778     #op #a #arg #H @('bind_inversion H) -H #val1 #val1_spec
    1779     elim (retrieve_commute p p' graph_prog sigma ?? ? (acca_retrieve_commute … gss) ??? prf val1_spec)
    1780     #wf_val1 #sigma_val1_commute #H @('bind_inversion H) #op_val1 #op_val1_spec
    1781     cut(∃ wf_opval1. be_op1 op (sigma_beval … wf_val1) = return sigma_beval p p' graph_prog sigma op_val1 wf_opval1)
    1782     [ whd in match be_op1 in op_val1_spec; normalize nodelta in op_val1_spec;
    1783       @('bind_inversion op_val1_spec) #bt1 #b1_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1784       % [ @hide_prf whd in match sigma_beval_opt; normalize nodelta % #ABS whd in ABS : (??%?);
    1785           destruct(ABS)]
    1786       whd in match Byte_of_val in b1_spec; normalize nodelta in b1_spec;
    1787       whd in match sigma_beval; normalize nodelta
    1788       @opt_safe_elim #sigma_val1 #sigma_val1_spec
    1789       @opt_safe_elim #sigma_op_val1 #sigma_op_val1_spec
    1790       cases(val1) in b1_spec op_val1_spec sigma_val1_spec; normalize nodelta
    1791       [4: #bt2  #EQ whd in EQ : (???%); destruct(EQ)
    1792           whd in match Byte_of_val; normalize nodelta >m_return_bind
    1793           #EQ whd in EQ : (??%%); destruct(EQ)
    1794           whd in match sigma_beval_opt; normalize nodelta
    1795           #EQ whd in EQ : (??%%); destruct(EQ)
    1796           whd in match sigma_beval_opt in sigma_op_val1_spec;
    1797           normalize nodelta in sigma_op_val1_spec; whd in sigma_op_val1_spec : (??%?);
    1798           destruct(sigma_op_val1_spec) //
    1799       |*: [3: #pt1 #pt2 #p] [4:#p] [5:#pt #p] [6:#pc #p] #ABS whd in ABS : (???%);
    1800           destruct(ABS)
    1801       ]
    1802     ] * #wf_op_val1 #sigma_op_val1_commute #H1
    1803     elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_op_val1 H1)
    1804     #wf_st' #final_commute %{wf_st'}
    1805     change with (acca_retrieve ????? = ?) in sigma_val1_commute;
    1806     >sigma_val1_commute >m_return_bind >sigma_op_val1_commute >m_return_bind
    1807     assumption
     1830    #op #a #arg #st #prf
     1831    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1832    [ @acca_retrieve_commute ]
     1833    #bv #bv_prf
     1834    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1835    [ @beop1_sigma_commute ]
     1836    #res #res_prf
     1837    @mfr_bind [3: @acca_store__commute |*: ]
     1838    #r #r_prf @mfr_return @wf_set_regs assumption
    18081839  | (*C_OP2*)
    1809      #op #a #arg1 #arg2 #H @('bind_inversion H) -H
    1810      @bv_pc_other (*val1*)
    1811      [ #pc_val1 #part_val1
    1812      | #val1 #val1_no_pc
    1813      ] #val1_spec
    1814      #H @('bind_inversion H) -H
    1815      [ #val2
    1816      | @bv_pc_other (*val2*)
    1817        [ #pc_val2 #part_val2
    1818        | #val2 #val2_no_pc
    1819        ]
    1820      ] #val2_spec
    1821      #H @('bind_inversion H) -H * #val3 #bit1
    1822      [1,2: [2: cases val1 [||#pt1 #pt2 #p|#by|#p|#pt #p|#pc #p] cases op ]
    1823        whd in ⊢(??%%→?); #EQ destruct(EQ) ]
    1824      #H cut (bv_no_pc val3)
    1825       [ lapply H -H
    1826         whd in match be_op2; normalize nodelta
    1827         cases val1 normalize nodelta
    1828         [1,7: [2: #pc #p] #ABS whd in ABS : (???%); destruct(ABS)
    1829         |2,3,5: [ |#pt1 #pt2 #p | #p ] cases op normalize nodelta
    1830           [1,2,3,4,6,7,8,9,10,12,13,14,15,16,17 : #ABS whd in ABS : (???%); destruct(ABS)]
    1831           cases val2 normalize nodelta
    1832           [1,2,3,4,5,6,7,8,9,12,13,14,15,16,17,18,21 :
    1833             [||#ptr1 #ptr2 #p| #byte2 | #p | #ptr #p | #pc #p | | | #p| #ptr #p | #pc #p | | | #pt1 #pt2 #p | #bt | #pc #p] 
    1834             #EQ whd in EQ : (??%%); destruct(EQ) //
    1835           | #pt3 #pt4 #p1 @if_elim [2: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
    1836             #_ @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    1837           | #bt @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1838             #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    1839           | #p3 @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1840             #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    1841           | #ptt #part @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1842             #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    1843           ]
    1844         |4,6: [ #bt1 | #ptr #p] cases val2 normalize nodelta
    1845           [1,3,4,5,7,8,9,10,14: [|#pt1 #pt2 #p
    1846                               | #bt2 #H @('bind_inversion H) #bit #bit_spec cases(op2 ? ? ? ? ?)
    1847                                 #x #y normalize nodelta
    1848                               | #p | #pc #part | | | #ptr #ptr' #p| #pc #p]
    1849                  #EQ whd in EQ : (??%%); destruct(EQ) //
    1850           |*: [|#ptr #p| #bt | #p | #ptr #p ] cases op normalize nodelta
    1851               [1,2,3,4,5,6,9,10,11,12,16,17,18,19,20,21,22,23,25,26,28,29:
    1852                  #EQ whd in EQ : (??%%); destruct(EQ) //
    1853               |7,8,13,14,15: whd in match be_add_sub_byte; normalize nodelta
    1854                 cases(ptype ?) normalize nodelta [2,4,6,8,10: #ABS whd in ABS : (??%%); destruct(ABS)]
    1855                 cases p * normalize nodelta #n_part_spec [2,6: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
    1856                 [1,2,4,5,7 : #H @('bind_inversion H) #bit #bit_spec
    1857                        @if_elim [1,3,5,7,9: #_ #ABS whd in ABS : (??%%); destruct(ABS)]
    1858                        #_ elim(op2 ? ? ? ? ?) #a1 #a2 normalize nodelta
    1859                        #EQ whd in EQ : (??%%); destruct(EQ) //
    1860                 |*: #_ cases(carry ? st) normalize nodelta
    1861                   [1,2,4,5,7,8 : [1,3,5: #bool ] #ABS whd in ABS : (???%); destruct(ABS)]
    1862                   #bool #pt #p1 #bitvect @if_elim #_ [2,4,6: #ABS whd in ABS : (???%); destruct(ABS)]
    1863                   @If_elim [2,4,6: #_ #ABS whd in ABS : (???%); destruct(ABS)]
    1864                   #proof elim(op2_bytes ?????) #a #b
    1865                   normalize nodelta #EQ whd in EQ : (???%); destruct(EQ) //
    1866                 ]
    1867               |24,30: @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) //
    1868               | cases(ptype ?) normalize nodelta [2: #ABS whd in ABS : (???%); destruct(ABS)]
    1869                 @if_elim #_ [2: #ABS whd in ABS : (??%%); destruct(ABS)]
    1870                 #H @('bind_inversion H) #b #_ elim(op2 ?????) #x #y normalize nodelta
    1871                 #EQ whd in EQ : (??%%); destruct(EQ) //
    1872               ]
    1873           ]
    1874         ]
    1875       ] #val3_spec lapply H -H #val3_op_spec #H @('bind_inversion H) #st1
    1876         #st1_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1877         elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val1_spec)
    1878         #wf_val1 #sigma_val1_commute
    1879         elim(retrieve_commute p p' graph_prog sigma ?? ? (snd_arg_retrieve_commute … gss) ??? prf val2_spec)
    1880         #wf_val2 #sigma_val2_commute
    1881        
    1882         elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf ? st1_spec)
    1883         [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta inversion val3 normalize nodelta
    1884           [7: #pc #p #H >H in val3_spec; #ABS @⊥ //
    1885           |*: [||#pt1 #pt2 #p|#bt|#p|#pt #p] #_ % #ABS whd in ABS : (??%%); destruct(ABS)
    1886           ]
    1887         ]
    1888         #wf_st1 #sigma_st1_commute   
    1889         %
    1890         [ @hide_prf % [2: @(proj2 … wf_st1)] % [2: @(proj2 … (proj1 … wf_st1))]
    1891           % [2:@(proj2 … (proj1 … (proj1 … wf_st1)))] 
    1892           @(proj1 … (proj1 … (proj1 … wf_st1)))
    1893         ]
    1894          change with ((acca_arg_retrieve ?????)=?) in sigma_val1_commute;
    1895          >sigma_val1_commute >m_return_bind
    1896          change with ((snd_arg_retrieve ?????)=?) in sigma_val2_commute;
    1897          >sigma_val2_commute >m_return_bind
    1898          >(sigma_bv_no_pc … val1_no_pc) >(sigma_bv_no_pc … val2_no_pc)
    1899          whd in match sigma_state in ⊢ (??(?????%?)?); normalize nodelta
    1900         >val3_op_spec >m_return_bind
    1901         change with ((acca_store ??????) = ?) in sigma_st1_commute;
    1902         >(sigma_bv_no_pc … val3_spec) in sigma_st1_commute;
    1903         #H >H >m_return_bind //
     1840    #op #a #arg1 #arg2 #st #prf
     1841    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1842    [ @acca_arg_retrieve_commute ]
     1843    #bv1 #bv1_prf
     1844    @(mfr_bind … (sigma_beval p p' graph_prog sigma))
     1845    [ @snd_arg_retrieve_commute ]
     1846    #bv2 #bv2_prf
     1847    @mfr_bind
     1848    [3: @beop2_sigma_commute |*: ]
     1849    * #res1 #carry' #res1_prf
     1850    @(mfr_bind … (sigma_state … gss))
     1851    [ @mfr_bind [3: @acca_store__commute |*: ]
     1852      #r #r_prf @mfr_return @wf_set_regs assumption
     1853    ]
     1854    #st' #st_prf' @mfr_return
    19041855  | (*C_CLEAR_CARRY*)
    1905      #EQ whd in EQ : (??%%); destruct(EQ)
    1906      %{prf} //
     1856     #st #prf @mfr_return
    19071857  | (*C_SET_CARRY*)
    1908     #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
     1858    #st #prf @mfr_return
    19091859  | (*C_LOAD*)
    1910     #a #dpl #dph #H @('bind_inversion H) -H #val1 #val1_spec
    1911     #H @('bind_inversion H) -H #val2 #val2_spec
    1912     #H @('bind_inversion H) -H #ptr #ptr_spec
    1913     #H @('bind_inversion H) -H #val3 #val3_spec #final_spec
    1914     elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec)
    1915     #wf_val1 #sigma_val1_commute
    1916     elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec)
    1917     #wf_val2 #sigma_val2_commute
    1918     lapply(opt_eq_from_res ???? val3_spec) -val3_spec #val3_spec
    1919     elim(beloadv_sigma_commute p p' graph_prog sigma ???? val3_spec)
    1920     [2: @hide_prf @(proj2 … prf)] #wf_val3 #sigma_val3_commute
    1921     elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_val3 final_spec)
    1922     #wf_st' #sigma_st_commute %{wf_st'}
    1923     change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute;
    1924     >sigma_val1_commute >m_return_bind
    1925     change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute;
    1926     >sigma_val2_commute >m_return_bind
    1927     >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec)
    1928     >m_return_bind >sigma_val3_commute >m_return_bind
    1929     change with (acca_store ?????? = ?) in sigma_st_commute; assumption
    1930   | (*C_STORE*)
    1931      #dpl #dph #a #H @('bind_inversion H) -H #val1 #val1_spec
    1932      #H @('bind_inversion H) -H #val2 #val2_spec
    1933      #H @('bind_inversion H) -H #ptr #ptr_spec
    1934      #H @('bind_inversion H) -H #val3 #val3_spec
    1935      #H @('bind_inversion H) -H #mem #mem_spec #EQ whd in EQ : (??%%); destruct(EQ)
    1936      elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec)
    1937      #wf_val1 #sigma_val1_commute   
    1938      elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec)
    1939      #wf_val2 #sigma_val2_commute
    1940      elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val3_spec)
    1941      #wf_val3 #sigma_val3_commute     
    1942      lapply(opt_eq_from_res ???? mem_spec) -mem_spec #mem_spec
    1943      elim(bestorev_sigma_commute p p' graph_prog sigma ????? wf_val3 mem_spec)
    1944      [2: @hide_prf @(proj2 … prf)]
    1945      #wf_mem #sigma_mem_commute
    1946      % [@hide_prf % [2: @wf_mem] % [2: @(proj2 … (proj1 … prf))] %
    1947         [ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))]
    1948        ]
    1949     change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute;
    1950     >sigma_val1_commute >m_return_bind
    1951     change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute;
    1952     >sigma_val2_commute >m_return_bind
    1953     >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec)
    1954     >m_return_bind
    1955     change with (acca_arg_retrieve ????? = ?) in sigma_val3_commute;
    1956     >sigma_val3_commute >m_return_bind >sigma_mem_commute
    1957     >m_return_bind //
    1958   | (*CALL*)
    1959      #f #args #dest
    1960      #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
     1860    #a #dpl #dph #st #prf
     1861    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
     1862    #bv1 #bv1_prf
     1863    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
     1864    #bv2 #bv2_prf
     1865    @mfr_bind [3: @sigma_ptr_commute |*:]
     1866    [ % assumption ]
     1867    #ptr *
     1868    @mfr_bind
     1869    [3:
     1870     @opt_to_res_preserve @beloadv_sigma_commute
     1871   |*:]
     1872   #res #res_prf
     1873   @mfr_bind [3: @acca_store__commute |*: ]
     1874   #r #r_prf @mfr_return @wf_set_regs assumption
     1875 | (*C_STORE*)
     1876    #dpl #dph #a #st #prf
     1877    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
     1878    #bv1 #bv1_prf
     1879    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
     1880    #bv2 #bv2_prf
     1881    @mfr_bind [3: @sigma_ptr_commute |*:]
     1882    [ % assumption ]
     1883    #ptr *
     1884    @mfr_bind
     1885    [3: @acca_arg_retrieve_commute |*:]
     1886    #res #res_prf
     1887    @mfr_bind
     1888    [3:
     1889     @opt_to_res_preserve @bestorev_sigma_commute
     1890    |*:]
     1891    #mem #wf_mem
     1892    @mfr_return
     1893    @wf_set_m assumption
     1894 | (*CALL*)
     1895     #f #args #dest #st #prf @mfr_return
    19611896 |  (*C_EXT*)
    1962     #s_ext #H
    1963     elim(eval_ext_seq_commute … sigma gss … prf H)
    1964     #wf_st' #H1 %{wf_st'} >H1 //
     1897    #s_ext #st #prf @eval_ext_seq_commute
    19651898 ]
    1966  skip
    19671899 qed.
    1968    (* check(save_frame_commute)*)
    1969    
    1970 lemma eval_statement_no_pc_sigma_commute :
    1971  ∀p,p',graph_prog.
    1972  let lin_prog ≝ linearise p graph_prog in
    1973  ∀stack_sizes.
    1974  ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
    1975  ∀f,fn,st,stmt,st'.
    1976  ∀prf : well_formed_state … gss st.
    1977   eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
    1978    f fn stmt st = return st' →
    1979   ∃prf'.
    1980   eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
    1981     f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
    1982        (sigma_state … gss st prf) =
    1983   return sigma_state … gss st' prf'.
    1984   #p #p' #graph_prog #stack_sizes #sigma #gss
    1985   #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
    1986   #st' #prf
    1987   whd in match eval_statement_no_pc; normalize nodelta
    1988   [ @eval_seq_no_pc_sigma_commute
    1989   |*: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    1990   ]
    1991 qed.
    1992 
    19931900
    19941901inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     
    20341941* #wf_prf #st2_EQ
    20351942
    2036 cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
    2037 * #EQfetch_stmt' #all_labels_in
    2038 
     1943cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
     1944cases stmt in EQfetch_stmt ex ex_advance; -stmt
     1945[ @cond_call_other
     1946  [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ]
     1947normalize nodelta
     1948#EQfetch_stmt
     1949whd in match eval_statement_no_pc in ⊢ (%→?); normalize nodelta
     1950#ex
     1951[| whd in match eval_statement_advance in ⊢ (%→?);
     1952  whd in match eval_seq_advance in ⊢ (%→?);
     1953  normalize nodelta
     1954| whd in match eval_statement_advance in ⊢ (%→?);
     1955  normalize nodelta
     1956  >(no_call_advance (mk_prog_params (make_sem_graph_params p p')
     1957    graph_prog stack_sizes))   in ⊢ (%→?); try assumption
     1958]
     1959#ex_advance
     1960#all_labels_in
    20391961letin lin_prog ≝ (linearise … graph_prog)
    20401962lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
    20411963whd in match eval_state in ⊢ (???%→?);
    20421964>st2_EQ in ⊢ (???%→?); normalize nodelta
    2043 >EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?);
     1965[ (* COND *)
     1966| (* CALL *)
     1967| (* SEQ *)
     1968  #ex'
     1969  * #lin_fetch_stmt #next_spec
     1970  whd in match (as_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1971  >EQfetch_stmt in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1972  normalize nodelta
     1973  whd in match joint_classify_step;
     1974  normalize nodelta
     1975  >no_call_other in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     1976  try assumption
     1977  normalize nodelta
     1978  >lin_fetch_stmt in ex' : (???%) ⊢ ?; >m_return_bind in ⊢ (???%→?);
     1979  whd in match eval_statement_no_pc in ⊢ (???%→?);
     1980  normalize nodelta
     1981  cases (eval_seq_no_pc_sigma_commute … gss … ex) in ⊢ ?;
     1982  [2: @hide_prf @(proj2 … wf_prf) ]
     1983  #st1_no_pc_wf #EQ >EQ in ⊢ (???%→?); -EQ
     1984   >m_return_bind in ⊢ (???%→?);
     1985  whd in match eval_statement_advance in ⊢ (%→?);
     1986  normalize nodelta
     1987  >(no_call_advance (mk_prog_params (make_sem_lin_params p p')
     1988    lin_prog stack_sizes))   in ⊢ (%→?); try assumption
     1989  whd in match (next ???) in ⊢ (%→?);
     1990  change with (sigma_pc ????? (hide_prf ??)) in match (pc ??) in ⊢ (%→?);
     1991  #ex'
     1992  cases next_spec
     1993  #succ_pc_nxt_wf *
     1994  [ #succ_pc_commute >succ_pc_commute in ex' ⊢ ?;
     1995    #ex'
     1996    % [2: %{(taaf_step … (taa_base …) …)} [2: @ex' ] |*:]
     1997    whd
     1998    [ whd in ⊢ (??%?);
     1999      >lin_fetch_stmt normalize nodelta
     2000      whd in match joint_classify_step; normalize nodelta
     2001      @no_call_other assumption
     2002    | normalize nodelta
     2003      cut (? : Prop)
     2004      [3: #H % [ % [ % | @H ]] |*:]
     2005      [ (* TODO lemma : sem_rel → label_rel *)
     2006        cases daemon
     2007      | whd in ex_advance : (??%%); destruct(ex_advance)
     2008        % [ % assumption | % ]
     2009      ]
     2010    ]
     2011  | #fetch_GOTO
     2012    cases (all_labels_in) #wf_next #_
     2013    cases (pc_of_label_sigma_commute … p' … good … EQfetchfn ?)
     2014    [2: @nxt |3: cases daemon ]
     2015    #wf_next' #EQ
     2016    % [2: %{(taaf_step … (taa_step … (taa_base …) …) …)}
     2017      [3: @ex'
     2018      |2: whd
     2019        whd in match eval_state; normalize nodelta
     2020        >fetch_GOTO in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
     2021         >m_return_bind in ⊢ (??%?);
     2022        whd in match eval_statement_advance; normalize nodelta
     2023        whd in match goto; normalize nodelta
     2024        whd in match (pc_block ?);
     2025        >sigma_pblock_eq_lemma >EQ in ⊢ (??%?); %
     2026      |7: normalize nodelta
     2027        cut (? : Prop)
     2028        [3: #H % [ % [ % | @H ]] |*:]
     2029        [ (* TODO lemma : sem_rel → label_rel *)
     2030          cases daemon
     2031        | whd in ex_advance : (??%%); destruct(ex_advance)
     2032          % [ % assumption | % ]
     2033        ]
     2034      |5: % * #H @H -H whd in ⊢ (??%?); >fetch_GOTO %
     2035      |4: whd whd in ⊢ (??%?);
     2036        >lin_fetch_stmt normalize nodelta
     2037        whd in match joint_classify_step; normalize nodelta
     2038        @no_call_other assumption
     2039      |1: whd whd in ⊢ (??%?);
     2040        >fetch_GOTO normalize nodelta %
     2041      |*:
     2042      ]
     2043    |*:
     2044    ]
     2045  ]
     2046| (* FIN *)
     2047]
     2048
     2049#stmt_spec
     2050
     2051
    20442052cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
    20452053#wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
     
    20492057normalize nodelta
    20502058
    2051 cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement;
    20522059normalize nodelta
    20532060[ whd in match joint_classify_step; @cond_call_other
Note: See TracChangeset for help on using the changeset viewer.