Changeset 3576 for LTS


Ignore:
Timestamp:
Jun 19, 2015, 1:56:43 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3574 r3576  
    175175   #EQ destruct @H1 >(\P EQcond) %
    176176]
    177 qed.
     177qed.
     178
     179definition DeqInstructions ≝ λp,l_p.mk_DeqSet (Instructions p l_p) (eq_instructions p l_p) ?.
     180@hide_prf #i1 #i2 @eq_instructions_elim [ #EQ destruct % // | * #H % #EQ destruct cases H %]
     181qed.
     182
     183unification hint  0 ≔ p,l_p;
     184    X ≟ (DeqInstructions p l_p)
     185(* ---------------------------------------- *) ⊢
     186    (Instructions p l_p) ≡ carr X.
     187
     188unification hint  0 ≔ p,l_p,p1,p2;
     189    X ≟ (DeqInstructions p l_p)
     190(* ---------------------------------------- *) ⊢
     191    eq_instructions p l_p p1 p2 ≡ eqb X p1 p2.
    178192
    179193record env_params : Type[1] ≝
     
    299313{ env : list (env_item p p' l_p)
    300314; main : Instructions p' l_p
     315; initial_act : NonFunctionalLabel l_p
    301316}.
    302317
     
    306321λp,p',l_p,prog.
    307322   no_duplicates …
    308     (foldr
     323    (foldr ? (list (CostLabel l_p))
    309324      (λitem,acc.((a_call … (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc)
    310       (get_labels_of_code … (main … prog)) (env … prog)).
     325      ((a_non_functional_label … (initial_act … prog)) :: (get_labels_of_code … (main … prog))) (env … prog)).
    311326
    312327lemma no_duplicates_domain_of_fun:
     
    314329 ∀f,env_it.lookup p p' l_p (env … prog) f = return env_it →
    315330 no_duplicates … (get_labels_of_code … (f_body … env_it)).
    316 #p #p' #l_p * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)]
    317 #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it
     331#p #p' #l_p * #env elim env [ #main #initial_act normalize #_ #f #env_it #EQ destruct(EQ)]
     332#x #xs #IH #main #initial_act whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it
    318333whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta
    319334[ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ]
     
    328343 ].
    329344
    330 definition operational_semantics : ∀p : state_params.∀p'.Program p p p → abstract_status p ≝
    331 λp,p',prog.mk_abstract_status …
     345definition lang_initial : ∀p : state_params.sem_state_params p → Program p p p → state p → bool ≝
     346λp,p',prog,st.
     347  let spec_act ≝ cost_act … (Some ? (initial_act … prog)) in
     348  eq_instructions … (code … st) (EMPTY …) ∧
     349  eqb_list … (cont … st) [〈spec_act,(main … prog)〉 ; 〈spec_act,EMPTY …〉] ∧
     350  store … st == init_store … p' ∧ io_info … st.
     351
     352definition lang_final : ∀p.state p → bool ≝
     353λp,st.
     354 eq_instructions … (code … st) (EMPTY …) ∧ isnilb … (cont … st).
     355
     356definition operational_semantics : ∀p : state_params.sem_state_params p → Program p p p → abstract_status p ≝
     357λp,p',prog.mk_abstract_status ?
    332358                (state p)
    333359                (execute_l ? p' (env … prog))
     
    343369                    | _ ⇒ false
    344370                    ])
    345                 (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s)
    346                 (λs.match (cont … s) with
    347                     [ nil ⇒ match (code … s) with
    348                             [ EMPTY ⇒ true
    349                             | RETURN _ ⇒ true
    350                             | _ ⇒ false
    351                             ]
    352                     | _ ⇒ false
    353                     ])
     371                (lang_initial … p' … prog)
     372                (lang_final p)
    354373                ???.
    355374@hide_prf
     
    10321051lemma fresh_aux_ok : ∀p,p',l_p.∀prog : Program p p' l_p.∀n,m.n ⊑^{l_p} m →
    10331052fresh_for_prog_aux … prog n ⊑^{l_p} fresh_for_prog_aux … prog m.
    1034 #p #p' #l_p * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (???%%);
     1053#p #p' #l_p * #env #main #init_act elim env // #hd #tl #IH #n #m #H whd in ⊢ (???%%);
    10351054@IH whd in ⊢ (???%?); @(monotonic_magg … l_p … H)
    10361055qed.
     
    10571076let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in
    10581077let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in
    1059 〈mk_Program ??? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉.
     1078〈mk_Program ??? t_env (t_code … info_main) (initial_act … prog),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉.
    10601079
    10611080definition map_labels_on_trace : ∀p : label_params.
     
    11871206lemma is_fresh_fresh_for_prog : ∀p,p',l_p.∀prog : Program p p' l_p.
    11881207is_fresh_for_return … (labels_of_prog … prog) (fresh_for_prog … prog).
    1189 #p #p' #l_p * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (??%?);
     1208#p #p' #l_p * #env #main #initial_act whd in match fresh_for_prog; normalize nodelta whd in ⊢ (??%?);
    11901209elim env // * #sig #cost #i #tail #IH  whd in ⊢ (??%?); @fresh_append
    11911210[ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 //
    11921211| @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta
    11931212  whd in ⊢ (????%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(trans_po_rel …  IH1)
    1194   whd in ⊢ (????%); change with (fresh_for_prog_aux ??? (mk_Program ??? tl1 main) ?) in ⊢ (???%%);
     1213  whd in ⊢ (????%); change with (fresh_for_prog_aux ??? (mk_Program ??? tl1 main initial_act) ?) in ⊢ (???%%);
    11951214  @fresh_aux_ok @max_1 //
    11961215]
     
    12101229∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 →
    12111230(cast_return_to_cost_labels l_p keep) ⊆ (labels_of_prog p p' l_p prog).
    1212 #p #p' #l_p * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta
     1231#p #p' #l_p * #env #main #initial_act #t_prog #m #keep whd in match trans_prog; normalize nodelta
    12131232@pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct
    12141233lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh
     
    12271246      >memb_append_l2 // @(lab_to_keep_in_domain … H)
    12281247    | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
    1229       change with (labels_of_prog ??? (mk_Program ??? xs ?)) in match (foldr ?????);
     1248      change with (labels_of_prog ??? (mk_Program ??? xs ? initial_act)) in match (foldr ?????);
    12301249      @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
    12311250      >cast_return_append @subset_append_h1 //
    12321251    ]
    12331252  | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
    1234     change with (labels_of_prog ??? (mk_Program ??? xs ?)) in match (foldr ?????);
     1253    change with (labels_of_prog ??? (mk_Program ??? xs ? initial_act)) in match (foldr ?????);
    12351254    @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
    12361255     >cast_return_append @subset_append_h2 //
     
    12691288lapply EQt_prog normalize nodelta
    12701289generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?)));
    1271 #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog
     1290#keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #initial_act #EQprog
    12721291whd in match trans_prog; normalize nodelta
    12731292@pair_elim
    1274 cut(fresh_for_prog ??? prog ⊑^{p} fresh_for_prog ??? (mk_Program … env main)) [ >EQprog //]
     1293cut(fresh_for_prog ??? prog ⊑^{p} fresh_for_prog ??? (mk_Program … env main initial_act)) [ >EQprog //]
    12751294generalize in match (fresh_for_prog ????) in ⊢ (????% → %);
    12761295lapply t_prog0 lapply m0 lapply keep0
     
    12811300* #m_tail #keep_tail change with (translate_env ?????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2)
    12821301whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
    1283 change with (no_duplicates_labels p p p (mk_Program p p p tail main)) in match
    1284 (no_duplicates_labels p p p (mk_Program p p p tail main)); #no_dup_tail
     1302change with (no_duplicates_labels p p p (mk_Program p p p tail main initial_act)) in match
     1303(no_duplicates_labels p p p (mk_Program p p p tail main initial_act)); #no_dup_tail
    12851304lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta
    12861305#f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta
     
    13031322    normalize nodelta >get_element_append_l1
    13041323    [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail
    1305         [ whd in match (foldr ?????); @lab_map_in_domain // ]
     1324        [ whd in match (foldr ?????);
     1325          change with (orb ??) in match (orb ??); @orb_Prop_r
     1326           @lab_map_in_domain // ]
    13061327        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
    13071328        >memb_append_l2 // >IH %
  • LTS/Traces.ma

    r3549 r3576  
    277277                             ]
    278278].
     279
     280lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2).
     281#P #p * [#f #lab | * [| #lab] | * [| #lab] ] *
     282[1,4,7,10,13: #f' #lab' |2,5,8,14: * [2,4,6,8: #lab'] |*: * [2,4,6,8,10,12: #lab'] ] #H1 #H2
     283whd in match eq_ActionLabel; normalize nodelta
     284try(@H2 % #EQ destruct)
     285[ @eq_function_name_elim [ @eq_call_cost_lab_elim [| #H #_ lapply H -H ] ]  | @eq_return_cost_lab_elim | | @eq_fn_label_elim ]
     286normalize nodelta
     287[1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 %
     288|*: * #H @H2 % #EQ destruct cases H %
     289]
     290qed.
     291
     292definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?.
     293@hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % // | * #H % #EQ destruct cases H %]
     294qed.
     295
     296unification hint  0 ≔ p ;
     297    X ≟ (DeqActionLabel p)
     298(* ---------------------------------------- *) ⊢
     299    (ActionLabel p) ≡ carr X.
     300
     301unification hint  0 ≔ p,p1,p2;
     302    X ≟ (DeqActionLabel p)
     303(* ---------------------------------------- *) ⊢
     304    eq_ActionLabel p p1 p2 ≡ eqb X p1 p2.
    279305
    280306definition is_cost_label : ∀p.ActionLabel p → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.