Changeset 3394 for LTS/Traces.ma


Ignore:
Timestamp:
Oct 30, 2013, 10:29:47 AM (8 years ago)
Author:
piccolo
Message:

Added abstract language and procedure to add call post labelled

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3391 r3394  
    5151coercion call_act_label_to_cost_label.
    5252
     53definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
     54λx,y.match x with [ a_non_functional_label n ⇒
     55                    match y with [a_non_functional_label m ⇒ eqb n m ] ].
     56
     57lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
     58(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
     59#P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
     60
     61definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
     62#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     63assumption
     64qed.
     65
     66unification hint  0 ≔ ;
     67    X ≟ DEQNonFunctionalLabel
     68(* ---------------------------------------- *) ⊢
     69    NonFunctionalLabel ≡ carr X.
     70
     71unification hint  0 ≔ p1,p2;
     72    X ≟ DEQNonFunctionalLabel
     73(* ---------------------------------------- *) ⊢
     74    eq_nf_label p1 p2 ≡ eqb X p1 p2.
     75
     76definition eq_function_name : FunctionName → FunctionName → bool ≝
     77λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].
     78
     79lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
     80(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
     81#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.
     82
     83definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
     84#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     85assumption
     86qed.
     87
     88unification hint  0 ≔ ;
     89    X ≟ DEQFunctionName
     90(* ---------------------------------------- *) ⊢
     91    FunctionName ≡ carr X.
     92
     93unification hint  0 ≔ p1,p2;
     94    X ≟ DEQFunctionName
     95(* ---------------------------------------- *) ⊢
     96    eq_function_name p1 p2 ≡ eqb X p1 p2.
     97
     98definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
     99λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
     100
     101lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     102(c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
     103#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
     104
     105definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
     106#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     107assumption
     108qed.
     109
     110unification hint  0 ≔ ;
     111    X ≟ DEQReturnPostCostLabel
     112(* ---------------------------------------- *) ⊢
     113    ReturnPostCostLabel ≡ carr X.
     114
     115unification hint  0 ≔ p1,p2;
     116    X ≟ DEQReturnPostCostLabel
     117(* ---------------------------------------- *) ⊢
     118    eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
     119
     120definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
     121λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
     122
     123lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     124(c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
     125#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
     126
     127definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
     128#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     129assumption
     130qed.
     131
     132unification hint  0 ≔ ;
     133    X ≟ DEQCallCostLabel
     134(* ---------------------------------------- *) ⊢
     135    CallCostLabel ≡ carr X.
     136
     137unification hint  0 ≔ p1,p2;
     138    X ≟ DEQCallCostLabel
     139(* ---------------------------------------- *) ⊢
     140    eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
     141
     142definition eq_costlabel : CostLabel → CostLabel → bool ≝
     143λc1.match c1 with
     144  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
     145  | a_return_post x1 ⇒
     146      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
     147  | a_non_functional_label x1 ⇒
     148     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
     149  ].
     150
     151lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     152(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
     153#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
     154try (@H2 % #EQ destruct)
     155[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     156  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     157| change with (eq_return_cost_lab ??) in ⊢ (?%);
     158   @eq_return_cost_lab_elim
     159   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     160| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
     161  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     162]
     163qed.
     164
     165
     166definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
     167#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     168assumption
     169qed.
     170
     171unification hint  0 ≔ ;
     172    X ≟ DEQCostLabel
     173(* ---------------------------------------- *) ⊢
     174    CostLabel ≡ carr X.
     175
     176unification hint  0 ≔ p1,p2;
     177    X ≟ DEQCostLabel
     178(* ---------------------------------------- *) ⊢
     179    eq_costlabel p1 p2 ≡ eqb X p1 p2.
     180
     181   
     182
     183
    53184inductive ActionLabel : Type[0] ≝
    54185 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
     
    76207 ; as_initial : as_status → bool
    77208 ; as_final : as_status → bool
    78  ; is_io_entering : NonFunctionalLabel → bool
    79  ; is_io_exiting : NonFunctionalLabel → bool
    80209 ; jump_emits : ∀s1,s2,l.
    81210      as_classify … s1 = cl_jump →
    82211      as_execute l s1 s2 → is_non_silent_cost_act l
     212 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
     213      as_execute l s1 s2 → is_non_silent_cost_act l
     214 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
     215     as_execute l s1 s2 → is_non_silent_cost_act l
    83216 }.
    84  
     217 (*
    85218definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
    86219λS,l.match l with
     
    104237| init_act ⇒ false
    105238].
    106 
     239*)
    107240
    108241inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
     
    182315λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    183316
    184 inductive silent_trace (S : abstract_status) :
     317inductive pre_silent_trace (S : abstract_status) :
    185318∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    186 | silent_empty : ∀st : S.as_classify … st ≠ cl_io → silent_trace … (t_base S st)
     319| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
    187320| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    188                 ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → silent_trace … tl →
    189                 silent_trace … (t_ind … prf … tl).
    190 
    191 lemma silent_io : ∀S : abstract_status.
    192 ∀s1,s2 : S. ∀t : raw_trace … s1 s2. silent_trace … t →
     321                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
     322                pre_silent_trace … (t_ind … prf … tl).
     323               
     324definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     325raw_trace S st1 st2 → bool ≝
     326λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     327
     328definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
     329raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
     330¬ (bool_to_Prop (is_trace_non_empty … t)).
     331
     332lemma pre_silent_io : ∀S : abstract_status.
     333∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
    193334as_classify … s2 ≠ cl_io.
    194335#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
     
    198339qed.
    199340
    200 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
    201 raw_trace S st1 st2 → bool ≝
    202 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    203341(*
    204342definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
Note: See TracChangeset for help on using the changeset viewer.