Changeset 2801


Ignore:
Timestamp:
Mar 7, 2013, 1:29:31 PM (7 years ago)
Author:
piccolo
Message:

Partial commit not yet finished

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2796 r2801  
    6868 λ_.λ_.λst.
    6969  ! st' ← push_ra … st (pc … st) ;
    70   ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st);
     70  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
    7171  return
    7272  (set_frms ERTL_state
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2785 r2801  
    223223  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cases(stmt_at_spec … EQstmt1)
    224224  #labels * #registers ** #_ #EQregisters #_ -labels >EQregisters whd
    225   cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) ?
    226          (get_used_registers_from_seq … (functs ERTL) stmt))
    227   [3: #a cases(¬a∈registers) // |1: #H assumption] #H @⊥
     225  check excluded_middle_list
     226  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
     227         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     228  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
    228229  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
    229230  #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     
    628629 =return st2'.
    629630#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | #c_ptr]
    630 #args #dest #nxt #EQfetch lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     631#args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch
     632>m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     633whd in match eval_statement_advance; whd in match eval_call; normalize nodelta
     634>(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     635>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H
     636#c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
     637#EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ)
     638#H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #H
     639lapply(err_eq_from_io ????? H) -H  #EQfn1 normalize nodelta
     640[3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
     641      #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x
     642      #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta
     643      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H
     644#H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     645>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call;
     646normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?);
     647[2: @ID |4: @PTR] #EQst1''  #H @('bind_inversion H) -H #st1'''
     648whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H
     649#s_size #H lapply(opt_eq_from_res ???? H) -H
     650change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?);
     651whd in ⊢ (???% → ??%% → ?); #EQ #EQ1 destruct(EQ EQ1)
     652lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?);
    631653#EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt
    632654cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    633655#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    634 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    635 #_ #fresh_labs #fresh_regs #_ #_ #H cases(H … EQstmt) -H #labels * #registers
     656[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
     657#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    636658** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    637 whd in match translate_step;
    638 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
     659whd in match translate_step; normalize nodelta * #bl *
    639660cases registers in EQregisters; -registers normalize nodelta
    640661[2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    641662[ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    642 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); *
    643 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
     663#EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ)
     664* #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 #m_fetch_pre whd in ⊢ (% → ?);
     665* #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     666whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(pre_l) in m_fetch_pre EQmid1;
     667[* #x * #y ** #ABS destruct(ABS)
     668|4: #lab #tl * #ABS destruct(ABS)
     669| #l1 #tl #m_fetch_pre whd in ⊢ (???% → ?); #EQ destruct(EQ)
     670| * #_ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ)
     671]
     672%
     673[1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
     674cases(ertl_save_frame_ok prog f_lbls f_regs ?
     675  (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st2))))
     676  ? st1''' ?)
     677[2: @PTR
     678|3,7: [ %{(mk_state_pc ? (st_no_pc … st2)
     679                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     680                     (last_pop … st2))}
     681      |%{(st2)}
     682      ] @hide_prf whd in match sigma_pc_opt; normalize nodelta @if_elim
     683      [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     684           [1,3: #EQ destruct(EQ) |*: assumption]]
     685      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     686         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     687         ] >m_return_bind % whd in ⊢ (??%? → ?); #ABS destruct(ABS)
     688|6: @ID
     689|4,8: [change with (pc_block (pc … st2)) in match (pc_block ?);
     690       >EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
     691      |>EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
     692      ] normalize nodelta whd in match (st_no_pc ??);
     693      whd in match sigma_stored_pc in ⊢ (??(???(???%?))?);
     694      whd in match sigma_pc_opt; normalize nodelta @if_elim
     695     [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     696           [1,3: #EQ destruct(EQ) |*: assumption]]
     697      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     698         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     699         ] >m_return_bind normalize nodelta
     700         change with (pc_block (pc … st2)) in match (pc_block ?);
     701         >pc_of_point_of_pc assumption
     702] #st_no_pc_after_call normalize nodelta *
     703[ #H @('bind_inversion H) -H #st_no_pc_pre_call #EQst_no_pc_pre_call
     704  whd in match set_no_pc; normalize nodelta]
     705#EQst_no_pc_after_call #EQ destruct(EQ)
     706[ %{(mk_state_pc ? st_no_pc_pre_call
     707                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     708                   (last_pop … st2))}
     709| %{st2}
     710]
     711%
     712[1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
     713      >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind %]
     714%
     715[1,3: %
     716  [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?);
     717        normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     718        >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
     719       [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);]
     720       >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
     721       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
     722       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); %
     723  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
     724      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
     725      [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_
     726      >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption]
     727      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_
     728      [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     729      | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     730      ]
     731      >m_return_bind >pc_of_point_of_pc %
     732  ]
     733|4: %{(taa_base …)}
     734| lapply(produce_trace_any_any_free (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     735           st2 ?????
     736           (mk_state_pc ? st_no_pc_pre_call
     737                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     738                   (last_pop … st2)) EQcalling' m_fetch_pre ?)
     739  [2: #taaf inversion(taaf)
     740      [ #s #EQ #EQ1 @⊥ destruct(EQ EQ1) cases s in EQ1 EQst_no_pc_pre_call;
     741        * #fms #is #bb #regs #m #y #z #EQ #H @('bind_inversion H) -H #a1
     742        #H @('bind_inversion H) -H #is1 whd in ⊢ (??%% → ?); cases is in EQ;
     743        [2: #bv1 |3: #bv1 #bv2] #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
     744        whd in ⊢ (??%% → ??%% → ?); #EQ1 destruct(EQ1) normalize nodelta
     745        whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) destruct(EQ)
     746      |3: #s1 #s2 #s3 #taa #H1 #H2 #H3 #EQ #EQ1 @⊥ destruct(EQ EQ1)
     747          lapply H3 -H3 whd in ⊢ (% → ?); whd in match (as_label ??);
     748          whd in match fetch_statement; normalize nodelta
     749          whd in match (as_pc_of ??); >EQcalling' >m_return_bind
     750          whd in match point_of_pc; normalize nodelta; >point_of_offset_of_point
     751          >EQcall normalize nodelta whd in match cost_label_of_stmt;
     752          normalize nodelta * #H @H %
     753      ]
     754      #s1 #s2 #s3 #taa #H1 #H2 #EQst2 #EQs3 #_ <EQst2 in taa; <EQs3 in H1; #H1 #taa
     755       %{(taa_append_taa … taa (taa_step … H1 … (taa_base …)))}
     756                 xxxxxxxxxxxxxxxxxxxx
     757|3,7: whd in match sigma_pc_opt; normalize nodelta @if_elim
     758      [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
     759           [1,3: #EQ destruct(EQ) |*: assumption]]
     760      #_ [
     761
     762
     763whd in ⊢ (% → ?);
    644764[ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    645765  * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
     
    653773whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
    654774* #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    655  whd in match eval_state; normalize nodelta >EQfetch
    656 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
    657 whd in match eval_statement_advance; whd in match eval_call; normalize nodelta
    658 >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
    659 >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H
    660 #c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
    661 #EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ)
    662 #H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #EQfn1 normalize nodelta
    663 [3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
    664       #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x
    665       #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta
    666       whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H
    667 #H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
    668 >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call;
    669 normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?);
    670 [2: @PTR |4: @ID] #EQst1'' #H @('bind_inversion H) -H #st1'''
    671 whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H
    672 #s_size #H lapply(opt_eq_from_res ???? H) -H
    673 change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?);
    674 whd in ⊢ (???% → ?); #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
    675 [1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
     775
     776
     777
     778
     779
     780
     781
     782
     783
     784
     785 
    676786[ letin pairpc ≝ (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1))
    677787  letin st2_pre ≝ (mk_state_pc ?
     
    844954
    845955
     956
     957
     958
     959
     960
     961
    846962inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    847963    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2786 r2801  
    240240   (ps_reg_store r).
    241241#prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta
    242 #bv * #psd_r #hw_r @mfr_bind1
    243 [ @(sigma_register_env prog f_lbls restr)
    244 | whd in match reg_store; whd in match sigma_regs; normalize nodelta
    245   #x #x_spec %{(add RegisterTag beval psd_r r bv)} % // whd in x_spec : (???%);
    246   destruct whd in match sigma_register_env; normalize nodelta >map_add
     242#bv * #psd_r #hw_r @mfr_return_eq1
     243whd in match reg_store; whd in match sigma_regs; normalize nodelta
     244whd in match sigma_register_env; normalize nodelta >map_add
    247245  >add_set_minus [% | assumption]
    248 | #z @mfr_return_eq1 %
    249 qed. 
     246qed.
    250247(* 
    251248   lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
     
    705702include alias "basics/lists/listb.ma".
    706703
     704check eval_seq_no_pc
     705
     706xxxxxxxxxxxxxxxxxxxxxxxx
     707
    707708lemma eval_seq_no_pc_no_call_ok :
    708709∀prog : ertl_program.
     
    710711∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
    711712∀stack_size.
    712 ∀bl.∀id. ∀fn : (joint_closed_internal_function ? (prog_var_names ?? prog)).
    713 ∀fn_out : (joint_closed_internal_function ? (prog_var_names ?? trans_prog)).
     713∀bl.∀id.
    714714∀seq.
    715 (∀l. code_has_label … (joint_if_code … fn) l → 
     715(∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).
     716∀l. code_has_label … (joint_if_code … fn) l → 
    716717opt_All …
    717718       (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs)))
     
    723724      (eval_seq_no_pc ERTL_semantics
    724725             (globals (mk_prog_params ERTL_semantics prog stack_size))
    725              (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
     726             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id seq)
    726727      (eval_seq_no_pc ERTLptr_semantics
    727728             (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    728729             (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    729              id fn_out (seq_embed … seq)).
    730 #prog #f_lbls #f_regs #stack_size #bl #f #fn #fn_out #seq #fresh_regs
     730             id (seq_embed … seq)).
     731#prog #f_lbls #f_regs #stack_size #bl #f #seq #fresh_regs
    731732cases seq in fresh_regs;
    732733[ #c #_ #st @mfr_return1
     
    11621163qed.
    11631164
    1164 (*TO BE MOVED *)
    11651165lemma excluded_middle_list :
    1166 ∀A : Type[0]. ∀P : A → Prop. (∀a.decidable … (P a)) → ∀ l.
     1166∀A : Type[0]. ∀P : A → Prop.∀ l : list A. (∀a : A.In A l a → decidable … (P a)) →
    11671167All … P l ∨ Exists … (λa.¬(P a)) l.
    1168 #A #P #Dec #l elim l [% %] #hd #tl #IH
    1169 cases IH [ cases(Dec hd) [ #H1 #H2 % whd % assumption | #H #_ %2 whd % assumption]
     1168#A #P #l elim l [#_  % %] #hd #tl #IH #Dec
     1169cases IH [ cases(Dec hd ?)
     1170            [ #H1 #H2 % whd % assumption
     1171            | #H #_ %2 whd % assumption
     1172            | % %
     1173            ]
    11701174         | #H %2 whd %2 assumption
     1175         | #a #H @Dec %2 assumption
    11711176         ]
    11721177qed.
     
    15251530] qed.
    15261531
     1532
    15271533lemma ertl_save_frame_ok : ∀prog : ertl_program.
    15281534∀f_lbls.∀f_regs : regs_funct.∀kind,restr.
    15291535preserving1 ?? res_preserve1 ????
    1530            (λst. match fetch_internal_function … (globalenv_noinit … prog)
     1536      (λst : Σs: state_pc ERTLptr_semantics.
     1537             sigma_pc_opt prog f_lbls (pc … s) ≠ None ?
     1538      . match fetch_internal_function … (globalenv_noinit … prog)
    15311539                       (pc_block (pc … st)) with
    15321540                 [ OK y ⇒ let 〈f,fn〉 ≝ y in
     
    15411549           (ertl_save_frame kind it)
    15421550           (match kind with
    1543             [ID ⇒ ertlptr_save_frame ID it
     1551            [ID ⇒ ertlptr_save_frame kind it
    15441552            |PTR ⇒ λst. !st' ← push_ra … st (pc … st);
    1545                         ertlptr_save_frame ID it (set_no_pc … st' st)
     1553                        ertlptr_save_frame kind it (set_no_pc … st' st)
    15461554            ]).
    1547 cases daemon (*TODO *)
    1548 qed.
    1549 
    1550 
    1551 
     1555#prog #f_lbls #f_regs * #restr * #st #st_prf
     1556inversion(fetch_internal_function ???) normalize nodelta
     1557[1,3: * #f #fn #EQfn normalize nodelta whd in match ertl_save_frame; whd in match ertlptr_save_frame;
     1558      normalize nodelta @mfr_bind1
     1559      [2,5: @push_ra_ok [1,2: assumption] |1,4: skip
     1560      |*: #st1 [ >m_return_bind] @mfr_bind_inversion1
     1561          [1,4: @(λf.match sigma_frames_opt prog f_lbls f_regs f with [Some g ⇒  g | None ⇒ [ ]])
     1562          |2,5: @opt_to_res_preserve1 whd in match sigma_state; whd in match set_no_pc;
     1563                normalize nodelta cases(st_frms … st1) [1,3: @opt_preserve_none1]
     1564                #frames #frames1 whd in match sigma_frames; normalize nodelta
     1565                >m_return_bind #EQframes %{frames} % [%] >EQframes %
     1566          |*: #frames #H lapply(opt_eq_from_res ???? H) -H whd in match sigma_state;
     1567              normalize nodelta #EQt_frames #H lapply(opt_eq_from_res ???? H) -H
     1568              whd in match set_no_pc; normalize nodelta #EQframes >EQframes in EQt_frames;
     1569              whd in match sigma_frames; normalize nodelta >m_return_bind
     1570              inversion(sigma_frames_opt ???) [1,3: #_ #ABS destruct(ABS)]
     1571              #t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f
     1572              whd in match set_frms; normalize nodelta >m_return_bind
     1573              cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
     1574                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
     1575                      mk_state ERTL_semantics a1 b1 c1 d1 e1 =
     1576                      mk_state ERTL_semantics a2 b2 c2 d2 e2)
     1577              [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
     1578                    #H15 //] #APP @APP try %
     1579              [1,3: whd in match sigma_frames_opt; whd in match m_list_map;
     1580                    normalize nodelta  whd in match (foldr ?????); normalize nodelta
     1581                    >EQfn >m_return_bind normalize nodelta
     1582                    change with (sigma_frames_opt prog f_lbls f_regs frames)
     1583                                                         in match (foldr ?????);
     1584                    >EQt_frames >m_return_bind whd in match sigma_regs;
     1585                    normalize nodelta cases(regs … st1) #ps_reg #hw_reg
     1586                    >(pc_block_eq … st_prf) %
     1587              |*: whd in match set_regs; whd in match sigma_regs; normalize nodelta
     1588                  cases(regs … st1) #ps_r #hw_r normalize nodelta
     1589                  whd in match sigma_register_env; normalize nodelta
     1590                  @eq_f2 // change with (empty_map RegisterTag beval) in match (map RegisterTag ????);
     1591                  <(empty_set_minus … restr) %
     1592              ]
     1593          ]
     1594      ]   
     1595|*: #e #_ #x whd in match ertl_save_frame; normalize nodelta normalize nodelta
     1596    #H @('bind_inversion H) -H #y whd in match push_ra; normalize nodelta
     1597    #H @('bind_inversion H) -H #z whd in match push; normalize nodelta
     1598    whd in match (istack ??); whd in match is_push; normalize nodelta
     1599    >m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%% →?);
     1600    #EQ destruct(EQ) normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
     1601    #EQ destruct(EQ) whd in match (st_frms ??); whd in ⊢ (??%% → ?);
     1602    #EQ destruct(EQ)
     1603]
     1604qed.
  • src/common/ExtraIdentifiers.ma

    r2783 r2801  
    235235
    236236
    237 
    238 
     237lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
     238empty_map tag A ∖ m.
     239#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
     240cases opt_b normalize [2: #b] <IHl <IHr %
     241qed.
     242
     243
  • src/common/ExtraMonads.ma

    r2783 r2801  
    6969; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
    7070       ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
     71; mfr_bind_inversion1 :  ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
     72       ∀f,g.(∀x.m = return F x → n = return x → m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
    7173; m_frel_ext1 : ∀X,Y,F,G.(∀x.F  x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v
    7274}.
     
    9092mk_MonadFunctRel1 ??
    9193(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    92 ???.
     94????.
    9395[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    9496| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    9698  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    9799  >n_spec <w_spec % //
     100| #X #Y #Z #W #F #G * [ #x | #e ] #n #H #f #g #H1 #z
     101  whd in ⊢ (??%% → ?); [2: #EQ destruct(EQ)] #H2 cases(H x (refl …))
     102  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption ] #w
     103  * #w_spec #EQz %{w} >n_spec <w_spec % //
    98104| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    99105  % //
     
    118124  mk_MonadFunctRel1 ??
    119125  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    120 ???.
     126????.
    121127[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    122128| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    124130  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    125131  >n_spec <w_spec % //
     132| #X #Y #Z #W #F #G * [ | #x ] #n #H #f #g #H1 #z
     133  whd in ⊢ (??%% → ?); [ #EQ destruct(EQ)] #H2 cases(H x (refl …))
     134  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
     135  * #w_spec #EQz %{w} >n_spec <w_spec % //
    126136| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    127137  % //
     
    146156  λO,I.mk_MonadFunctRel1 ??
    147157  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    148 ???.
     158????.
    149159[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    150160| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    152162  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    153163  >n_spec <w_spec % //
     164| #X #Y #Z #W #F #G * [ #o #r | #x | #e ] #n #H #f #g #H1 #z
     165  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(H x (refl …))
     166  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
     167  * #w_spec #EQz %{w} >n_spec <w_spec % //
    154168| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    155169  % //
Note: See TracChangeset for help on using the changeset viewer.