Changeset 3549 for LTS/Traces.ma


Ignore:
Timestamp:
Apr 2, 2015, 3:44:19 PM (5 years ago)
Author:
piccolo
Message:

added paolo's trick

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3535 r3549  
    1717include "basics/deqsets.ma".
    1818include "../src/ASM/Util.ma".
     19include "basics/finset.ma".
     20include "../src/utilities/hide.ma".
     21include "utils.ma".
     22
     23(*Label parameters*)
     24
     25record label_params : Type[1] ≝
     26{ label_type :> monoid
     27; abelian_magg : is_abelian … label_type
     28; succ_label : label_type → label_type
     29; po_label : partial_order label_type
     30; no_maps_in_id : ∀x.succ_label x ≠ x
     31; le_lab_ok : ∀x,y.po_label … (op … x (succ_label y)) (succ_label (op … x y))
     32; magg_def : ∀x,y.po_label … x (op … x y)
     33; monotonic_magg : ∀x,y,z.po_label … x y → po_label … (op … x z) (op … y z)
     34}.
     35
     36notation "hvbox(a break ⊑ ^ {b} break term 46 c)"
     37  non associative with precedence 45
     38for @{ 'lab_leq $a $b $c}.
     39
     40interpretation "label 'less or equal to'" 'lab_leq x y z = (po_rel ? (po_label y) x z).
     41
     42lemma max_1 : ∀p : label_params.∀n,m,k : p.k ⊑^{p} m → k ⊑^{p} op … p m n.
     43#p #m #n #k #H /2 by magg_def, trans_po_rel/
     44qed.
     45
     46lemma max_2 : ∀p : label_params.∀n,m,k: p.k ⊑^{p} n → k ⊑^{p} op … p m n.
     47#p #m #n #k #H >(abelian_magg … p) /2 by magg_def, trans_po_rel/
     48qed.
     49
     50lemma lab_po_rel_succ : ∀p : label_params.∀x : p.x ⊑^{p} succ_label … x.
     51#p #x @(trans_po_rel … (op … p … x (succ_label … (e … p)))) [ @(magg_def … p)]
     52@(trans_po_rel … (le_lab_ok … p …)) >neutral_r //
     53qed.
     54
     55(*flat labels*)
     56
     57definition deqnat_monoid ≝ mk_monoid DeqNat max O ???.
     58@hide_prf // [* //] #x #y #z normalize inversion(leb x y) normalize nodelta
     59#leb_xy
     60[ inversion(leb y z) normalize nodelta #leb_yz
     61  [ >(le_to_leb_true …) // @(transitive_le … y) @leb_true_to_le //
     62  | >leb_xy %
     63  ]
     64| inversion(leb x z) normalize nodelta #leb_xz
     65  [ >(le_to_leb_true … y z) normalize nodelta [>leb_xz %] @(transitive_le … x) /2 by leb_true_to_le/
     66    lapply(not_le_to_lt … (leb_false_to_not_le … leb_xy)) #H1 /2/
     67  | cases(leb y z) normalize nodelta [ >leb_xz | >leb_xy ] //
     68  ]
     69]
     70qed.
     71
     72definition part_order_nat ≝ mk_partial_order ℕ le ???.
     73/2 by le_to_le_to_eq, transitive_le, le_n/
     74qed.
     75
     76definition flat_labels ≝ mk_label_params deqnat_monoid ? S part_order_nat ????.
     77@hide_prf
     78[ normalize #x #y @leb_elim normalize nodelta
     79  [2: #H >le_to_leb_true //  lapply(not_le_to_lt …  H) #H1 /2/
     80  | * -y [ >le_to_leb_true //] #y #H >not_le_to_leb_false // @lt_to_not_le /2 by le_to_lt_to_lt/
     81  ]
     82| normalize #x /2 by sym_not_eq/
     83| normalize #x #y @(leb_elim … x y) normalize nodelta
     84  [ #H >le_to_leb_true /3 by le_to_lt_to_lt, monotonic_pred, le_n/
     85  | #H @leb_elim normalize nodelta [ #H1 @le_S_S lapply(not_le_to_lt …  H) #H3 /2/ ]
     86    #_ /2/
     87  ]
     88| normalize #x #y @leb_elim //
     89| normalize #x #y #z #H @(leb_elim … y z)
     90  [ #H1 >(le_to_leb_true … (transitive_le … H H1)) //
     91  | #H1 normalize cases(leb ??) normalize /3 by not_le_to_lt, lt_to_le/
     92  ]
     93]
     94qed.
    1995
    2096(*LABELS*)
     
    2399 | a_function_id : ℕ → FunctionName.
    24100 
    25 inductive CallCostLabel : Type[0] ≝
    26  | a_call_label : ℕ → CallCostLabel.
     101inductive CallCostLabel (p : label_params) : Type[0] ≝
     102 | a_call_label : p → CallCostLabel p.
    27103 
    28 inductive ReturnPostCostLabel : Type[0] ≝
    29  | a_return_cost_label : ℕ → ReturnPostCostLabel.
     104inductive ReturnPostCostLabel (p : label_params) : Type[0] ≝
     105 | a_return_cost_label : p → ReturnPostCostLabel p.
    30106 
    31 inductive NonFunctionalLabel : Type[0] ≝
    32  | a_non_functional_label : ℕ → NonFunctionalLabel.
     107inductive NonFunctionalLabel (p : label_params) : Type[0] ≝
     108 | a_non_functional_label : p → NonFunctionalLabel p.
    33109 
    34 inductive CostLabel : Type[0] ≝
    35  | a_call : CallCostLabel → CostLabel
    36  | a_return_post : ReturnPostCostLabel → CostLabel
    37  | a_non_functional_label : NonFunctionalLabel → CostLabel.
     110inductive CostLabel (p : label_params) : Type[0] ≝
     111 | a_call : CallCostLabel p → CostLabel p
     112 | a_return_post : ReturnPostCostLabel p → CostLabel p
     113 | a_non_functional_label : NonFunctionalLabel p → CostLabel p.
    38114
    39115coercion a_call.
     
    41117coercion a_non_functional_label.
    42118
    43 definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
    44 λx,y.match x with [ a_non_functional_label n ⇒
    45                     match y with [a_non_functional_label m ⇒ eqb n m ] ].
    46 
    47 lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
    48 (l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
    49 #P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
    50 
    51 definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
     119definition eq_nf_label : ∀p.NonFunctionalLabel p → NonFunctionalLabel p → bool ≝
     120λp,x,y.match x with [ a_non_functional_label n ⇒
     121                    match y with [a_non_functional_label m ⇒ eqb … n m ] ].
     122
     123lemma eq_fn_label_elim : ∀P : bool → Prop.∀p.∀l1,l2 : NonFunctionalLabel p.
     124(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label … l1 l2).
     125#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H
     126[ @H1 >(\P H) %
     127| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
     128]
     129qed.
     130 
     131definition DEQNonFunctionalLabel ≝ λp.mk_DeqSet (NonFunctionalLabel p) (eq_nf_label p) ?.
    52132#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
    53133assumption
    54134qed.
    55135
    56 unification hint  0 ≔ ;
    57     X ≟ DEQNonFunctionalLabel
     136unification hint  0 ≔ p;
     137    X ≟ (DEQNonFunctionalLabel p)
    58138(* ---------------------------------------- *) ⊢
    59     NonFunctionalLabel ≡ carr X.
    60 
    61 unification hint  0 ≔ p1,p2;
    62     X ≟ DEQNonFunctionalLabel
     139    (NonFunctionalLabel p) ≡ carr X.
     140
     141unification hint  0 ≔ p,p1,p2;
     142    X ≟ (DEQNonFunctionalLabel p)
    63143(* ---------------------------------------- *) ⊢
    64     eq_nf_label p1 p2 ≡ eqb X p1 p2.
     144    eq_nf_label p p1 p2 ≡ eqb X p1 p2.
    65145
    66146definition eq_function_name : FunctionName → FunctionName → bool ≝
     
    86166    eq_function_name p1 p2 ≡ eqb X p1 p2.
    87167
    88 definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
    89 λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
    90 
    91 lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    92 (c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
    93 #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
    94 
    95 definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
     168definition eq_return_cost_lab :∀p.ReturnPostCostLabel p → ReturnPostCostLabel p → bool ≝
     169λp,c1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb … n m]].
     170
     171lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) →
     172(c1 ≠ c2 → P false) → P (eq_return_cost_lab p c1 c2).
     173#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H
     174[ @H1 >(\P H) %
     175| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
     176]
     177qed.
     178
     179definition DEQReturnPostCostLabel ≝ λp.mk_DeqSet (ReturnPostCostLabel p) (eq_return_cost_lab …) ?.
    96180#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
    97181assumption
    98182qed.
    99183
    100 unification hint  0 ≔ ;
    101     X ≟ DEQReturnPostCostLabel
     184unification hint  0 ≔ p ;
     185    X ≟ (DEQReturnPostCostLabel p)
    102186(* ---------------------------------------- *) ⊢
    103     ReturnPostCostLabel ≡ carr X.
    104 
    105 unification hint  0 ≔ p1,p2;
    106     X ≟ DEQReturnPostCostLabel
     187    (ReturnPostCostLabel p) ≡ carr X.
     188
     189unification hint  0 ≔ p,p1,p2;
     190    X ≟ (DEQReturnPostCostLabel p)
    107191(* ---------------------------------------- *) ⊢
    108     eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
    109 
    110 definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
    111 λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
    112 
    113 lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    114 (c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
    115 #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
    116 
    117 definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
     192    eq_return_cost_lab p p1 p2 ≡ eqb X p1 p2.
     193
     194definition eq_call_cost_lab : ∀p.(CallCostLabel p) → (CallCostLabel p) → bool ≝
     195λp,c1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb … x y ]].
     196
     197lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) →
     198(c1 ≠ c2 → P false) → P (eq_call_cost_lab p c1 c2).
     199#P #p * #l1 * #l2 #H1 #H2 normalize inversion(?==?) #H
     200[ @H1 >(\P H) %
     201| @H2 % #EQ destruct lapply(\Pf H) * #H3 @H3 %
     202]
     203qed.
     204
     205definition DEQCallCostLabel ≝ λp.mk_DeqSet (CallCostLabel p) (eq_call_cost_lab p) ?.
    118206#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
    119207assumption
    120208qed.
    121209
    122 unification hint  0 ≔ ;
    123     X ≟ DEQCallCostLabel
     210unification hint  0 ≔ p;
     211    X ≟ (DEQCallCostLabel p)
    124212(* ---------------------------------------- *) ⊢
    125     CallCostLabel ≡ carr X.
    126 
    127 unification hint  0 ≔ p1,p2;
    128     X ≟ DEQCallCostLabel
     213    (CallCostLabel p) ≡ carr X.
     214
     215unification hint  0 ≔ p,p1,p2;
     216    X ≟ (DEQCallCostLabel p)
    129217(* ---------------------------------------- *) ⊢
    130     eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
    131 
    132 definition eq_costlabel : CostLabel → CostLabel → bool ≝
    133 λc1.match c1 with
     218    eq_call_cost_lab p p1 p2 ≡ eqb X p1 p2.
     219
     220definition eq_costlabel :∀p. (CostLabel p) → (CostLabel p) → bool ≝
     221λp,c1.match c1 with
    134222  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
    135223  | a_return_post x1 ⇒
     
    139227  ].
    140228
    141 lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
    142 (c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
    143 #P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
     229lemma eq_costlabel_elim : ∀P : bool → Prop.∀p.∀c1,c2.(c1 = c2 → P true) →
     230(c1 ≠ c2 → P false) → P (eq_costlabel p c1 c2).
     231#P #p * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
    144232try (@H2 % #EQ destruct)
    145 [ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     233[ change with (eq_call_cost_lab ???) in ⊢ (?%); @eq_call_cost_lab_elim
    146234  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
    147 | change with (eq_return_cost_lab ??) in ⊢ (?%);
     235| change with (eq_return_cost_lab ???) in ⊢ (?%);
    148236   @eq_return_cost_lab_elim
    149237   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
    150 | change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
     238| change with (eq_nf_label ???) in ⊢ (?%); @eq_fn_label_elim
    151239  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
    152240]
     
    154242
    155243
    156 definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
     244definition DEQCostLabel ≝ λp.mk_DeqSet (CostLabel p) (eq_costlabel p) ?.
    157245#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
    158246assumption
    159247qed.
    160248
    161 unification hint  0 ≔ ;
    162     X ≟ DEQCostLabel
     249unification hint  0 ≔ p ;
     250    X ≟ (DEQCostLabel p)
    163251(* ---------------------------------------- *) ⊢
    164     CostLabel ≡ carr X.
    165 
    166 unification hint  0 ≔ p1,p2;
    167     X ≟ DEQCostLabel
     252    (CostLabel p) ≡ carr X.
     253
     254unification hint  0 ≔ p,p1,p2;
     255    X ≟ (DEQCostLabel p)
    168256(* ---------------------------------------- *) ⊢
    169     eq_costlabel p1 p2 ≡ eqb X p1 p2.
    170 
    171 inductive ActionLabel : Type[0] ≝
    172  | call_act : FunctionName → CallCostLabel → ActionLabel
    173  | ret_act : option(ReturnPostCostLabel) → ActionLabel
    174  | cost_act : option NonFunctionalLabel → ActionLabel.
     257    eq_costlabel p p1 p2 ≡ eqb X p1 p2.
     258
     259inductive ActionLabel (p : label_params) : Type[0] ≝
     260 | call_act : FunctionName → CallCostLabel p → ActionLabel p
     261 | ret_act : option(ReturnPostCostLabel p) → ActionLabel p
     262 | cost_act : option (NonFunctionalLabel p) → ActionLabel p.
    175263 
    176 definition is_cost_label : ActionLabel → Prop ≝
    177 λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
    178 
    179 definition is_non_silent_cost_act : ActionLabel → Prop ≝
    180 λact. ∃l. act = cost_act (Some ? l).
    181 
    182 definition is_cost_act : ActionLabel → Prop ≝
    183 λact.∃l.act = cost_act l.
    184 
    185 definition is_call_act : ActionLabel → Prop ≝
    186 λact.∃f,l.act = call_act f l.
    187 
    188 definition is_labelled_ret_act : ActionLabel → Prop ≝
    189 λact.∃l.act = ret_act (Some ? l).
    190 
    191 definition is_unlabelled_ret_act : ActionLabel → Prop ≝
    192 λact.act = ret_act (None ?).
    193 
    194 definition is_costlabelled_act : ActionLabel → Prop ≝
    195 λact.match act with [ call_act _ _ ⇒ True
     264definition eq_ActionLabel : ∀p.ActionLabel p → ActionLabel p → bool ≝
     265λp,c1,c2.
     266match c1 with
     267[ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false]
     268| ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
     269                                                      | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
     270                                                      ]
     271                            | _ ⇒ false
     272                            ]
     273| cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false]
     274                                                        | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false]
     275                                                        ]
     276                             | _ ⇒ false
     277                             ]
     278].
     279
     280definition is_cost_label : ∀p.ActionLabel p → Prop ≝
     281λp,act.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
     282
     283definition is_non_silent_cost_act : ∀p.ActionLabel p → Prop ≝
     284λp,act. ∃l. act = cost_act … (Some ? l).
     285
     286definition is_cost_act : ∀p.ActionLabel p → Prop ≝
     287λp,act.∃l.act = cost_act … l.
     288
     289definition is_call_act : ∀p.ActionLabel p → Prop ≝
     290λp,act.∃f,l.act = call_act … f l.
     291
     292definition is_labelled_ret_act : ∀p.(ActionLabel p) → Prop ≝
     293λp,act.∃l.act = ret_act … (Some ? l).
     294
     295definition is_unlabelled_ret_act : ∀p.ActionLabel p → Prop ≝
     296λp,act.act = ret_act … (None ?).
     297
     298definition is_costlabelled_act : ∀p.ActionLabel p → Prop ≝
     299λp,act.match act with [ call_act _ _ ⇒ True
    196300                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    197301                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    198302                    ].
    199303                   
    200 lemma is_costlabelled_act_elim :
    201 ∀P : ActionLabel → Prop.
    202 (∀l. is_costlabelled_act l → P l) →
    203 (∀l. ¬is_costlabelled_act l → P l) →
    204 ∀l.P l.
     304definition is_ret_call_act : ∀p.ActionLabel p → Prop ≝
     305λp,a.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].
     306
     307definition is_silent_cost_act_b : ∀p.ActionLabel p → bool ≝
     308λp,act. match act with
     309 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
     310                   
     311lemma is_costlabelled_act_elim : ∀p.
     312∀P : ActionLabel p → Prop.
     313(∀l. is_costlabelled_act p l → P l) →
     314(∀l. ¬is_costlabelled_act p l → P l) →
     315∀l.P l. #p
    205316#P #H1 #H2 * /2/
    206317[ * /2/ @H2 % *] * /2/ @H2 %*
    207318qed.
     319
     320lemma eq_a_call_label : ∀p.
     321∀c1,c2.c1 == c2 → a_call p c1 == a_call p c2.
     322#p #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
     323#EQ destruct >(\b (refl …)) @I
     324qed.
     325
     326lemma eq_a_non_functional_label : ∀p.
     327∀c1,c2.c1 == c2 → a_non_functional_label p c1 == a_non_functional_label p c2.
     328#p #c1 #c2 #EQ cases(eqb_true (DEQNonFunctionalLabel ?) c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
     329#EQ destruct >(\b (refl …)) @I
     330qed.
     331
     332(* TOOLS FOR FRESHING LABELS *)
     333
     334definition fresh_nf_label : ∀p : label_params.p → NonFunctionalLabel p × p ≝
     335λp,x.〈a_non_functional_label … (succ_label … p x),(succ_label … p x)〉.
     336
     337definition fresh_cc_labe : ∀p : label_params.p → CallCostLabel p × p ≝
     338λp,x.〈a_call_label … (succ_label … p x),(succ_label … p x)〉.
     339
     340definition fresh_rc_label : ∀p : label_params.p → ReturnPostCostLabel p × p ≝
     341λp,x.〈a_return_cost_label … (succ_label … p x),(succ_label … p x)〉.
    208342
    209343
     
    215349 | cl_other : status_class.
    216350 
    217 record abstract_status : Type[2] ≝
     351record abstract_status (p : label_params) : Type[2] ≝
    218352 { as_status :> Type[0]
    219  ; as_execute : ActionLabel → relation as_status
     353 ; as_execute : (ActionLabel p) → relation as_status
    220354 ; as_syntactical_succ : relation as_status
    221355 ; as_classify : as_status → status_class
     
    225359 ; jump_emits : ∀s1,s2,l.
    226360      as_classify … s1 = cl_jump →
    227       as_execute l s1 s2 → is_non_silent_cost_act l
     361      as_execute l s1 s2 → is_non_silent_cost_act l
    228362 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
    229       as_execute l s1 s2 → is_non_silent_cost_act l
     363      as_execute l s1 s2 → is_non_silent_cost_act l
    230364 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
    231      as_execute l s1 s2 → is_non_silent_cost_act l
     365     as_execute l s1 s2 → is_non_silent_cost_act l
    232366 }.
    233367
    234368(* RAW TRACES *)
    235369
    236 inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
    237   | t_base : ∀st : S.raw_trace S st st
    238   | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
    239              as_execute S l st1 st2 → raw_trace S st2 st3 →
    240              raw_trace S st1 st3.
    241 
    242 let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
    243 (t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
     370inductive raw_trace (p : label_params) (S : abstract_status p) : S → S → Type[0] ≝
     371  | t_base : ∀st : S.raw_trace … S st st
     372  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel p.
     373             as_execute … S l st1 st2 → raw_trace … S st2 st3 →
     374             raw_trace … S st1 st3.
     375             
     376
     377let rec append_on_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S) (st3 : S)
     378(t1 : raw_trace … S st1 st2) on t1 : raw_trace …  S st2 st3 → raw_trace … S st1 st3 ≝
    244379match t1
    245 return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
     380return λst1,st2,tr.raw_trace … S st2 st3 → raw_trace … S st1 st3
    246381with
    247382[ t_base st ⇒ λt2.t2
     
    249384].
    250385
    251 interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
    252 
    253 lemma append_nil_is_nil : ∀S : abstract_status.
     386interpretation "trace_append" 'append t1 t2 = (append_on_trace ????? t1 t2).
     387
     388let rec len (p : label_params) (s : abstract_status p) (st1 : s) (st2 : s) (t : raw_trace p s st1 st2)
     389on t : ℕ ≝
     390match t with
     391[ t_base s ⇒ O
     392| t_ind s1 s2 s3 l prf lt ⇒ S (len … lt)
     393].
     394
     395lemma len_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
     396∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
     397len  ???? (t1 @ t2)  = (len  ????  t1) + (len  ???? t2).
     398#p #S #st1 #st2 #st3 #t1 elim t1 normalize //
     399qed.
     400
     401lemma append_nil_is_nil : ∀p. ∀S : abstract_status p.
    254402∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
    255403t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
    256 #S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
     404#p #S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
    257405[ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
    258406#s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    259407qed.
    260408
    261 lemma append_associative : ∀S,st1,st2,st3,st4.
    262 ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    263 ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
    264 #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
     409lemma append_associative : ∀p.∀S,st1,st2,st3,st4.
     410∀t1 : raw_trace p S st1 st2.∀t2 : raw_trace … S st2 st3.
     411∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
     412#p #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
    265413[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
    266414qed.
    267415
    268 definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
     416definition trace_prefix: ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st1 st2 →
    269417raw_trace … st1 st3 → Prop≝
    270 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
    271 
    272 definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
     418λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
     419
     420definition trace_suffix : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st2 st3 →
    273421raw_trace … st1 st3 → Prop≝
    274 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    275 
    276 definition actionlabel_to_costlabel ≝
    277 λl : ActionLabel.match l with
     422λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
     423
     424definition actionlabel_to_costlabel ≝ λp.
     425λl : ActionLabel p.match l with
    278426    [ call_act f c ⇒ [ c ]
    279427    | ret_act x ⇒ match x with
    280                   [ Some c ⇒ [ a_return_post c ]
     428                  [ Some c ⇒ [ a_return_post c ]
    281429                  | None ⇒ []
    282430                  ]
    283431    | cost_act x ⇒ match x with
    284                   [ Some c ⇒ [ a_non_functional_label c ]
     432                  [ Some c ⇒ [ a_non_functional_label  … c ]
    285433                  | None ⇒ []
    286434                  ]
    287435   ].
    288436
    289 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
    290 (t : raw_trace S st1 st2) on t : list CostLabel
     437let rec get_costlabels_of_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S)
     438(t : raw_trace p S st1 st2) on t : list (CostLabel p)
    291439match t with
    292440[ t_base st ⇒ [ ]
    293441| t_ind st1' st2' st3' l prf t' ⇒
    294442    let tl ≝ get_costlabels_of_trace … t' in
    295     actionlabel_to_costlabel l  @ tl
     443    actionlabel_to_costlabel l  @ tl
    296444].
    297445
    298 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     446lemma get_cost_label_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
    299447∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
    300448get_costlabels_of_trace … (t1 @ t2) =
    301449 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
    302 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
     450#p #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
    303451[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
    304452qed.
    305453
    306 lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
    307     ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
    308     ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
    309 #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.
     454lemma append_tind_commute : ∀p.∀S : abstract_status p.∀st1,st2,st3,st4 : S.∀l.
     455    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace p S st2 st3.
     456    ∀t2 : raw_trace p S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
     457#p #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.
    310458
    311459lemma get_costlabelled_is_costlabelled :
    312 S : abstract_status.∀s1,s2,s3 : S. ∀l.
     460p.∀S : abstract_status p.∀s1,s2,s3 : S. ∀l.
    313461∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
    314 is_costlabelled_act l →
     462is_costlabelled_act p l →
    315463|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
    316 #S #s1 #s2 #s3 * normalize
     464#p #S #s1 #s2 #s3 * normalize
    317465  [ /2 by monotonic_pred/
    318466  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
     
    323471(*SILENT TRACES*)
    324472
    325 inductive pre_silent_trace (S : abstract_status) :
    326 ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    327 | silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
    328 | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    329                 ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
     473inductive pre_silent_trace (p : label_params) (S : abstract_status p) :
     474∀st1,st2 : S.raw_trace p S st1 st2 → Prop ≝
     475| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base p S st)
     476| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute p S (cost_act  … (None ?)) st1 st2.
     477                ∀tl : raw_trace p S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
    330478                pre_silent_trace … (t_ind … prf … tl).
    331479               
    332 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
    333 raw_trace S st1 st2 → bool ≝
    334 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    335 
    336 definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
    337 raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
     480definition is_trace_non_empty : ∀p.∀S : abstract_status p.∀st1,st2.
     481raw_trace p S st1 st2 → bool ≝
     482λp,S,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     483
     484definition silent_trace : ∀p.∀S:abstract_status p.∀s1,s2 : S.
     485raw_trace p S s1 s2 → Prop ≝ λp,S,s1,s2,t.pre_silent_trace … t ∨
    338486¬ (bool_to_Prop (is_trace_non_empty … t)).
    339487
    340 lemma pre_silent_io : ∀S : abstract_status.
     488lemma pre_silent_io : ∀p.∀S : abstract_status p.
    341489∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
    342490as_classify … s2 ≠ cl_io.
    343 #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
     491#p #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
    344492#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
    345493#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
     
    347495qed.
    348496
    349 lemma append_silent : ∀S : abstract_status.
     497lemma append_silent : ∀p.∀S : abstract_status p.
    350498∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
    351499∀t2 : raw_trace … s2 s3.silent_trace … t1 →
    352500silent_trace … t2 →
    353501silent_trace … (t1 @ t2).
    354 #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     502#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
    355503[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
    356504#st1 #st2 #st3 #l #prf #tl #IH #t2 *
     
    364512qed.
    365513
    366 lemma silent_append_l2 : ∀S : abstract_status.
     514lemma silent_append_l2 : ∀p.∀S : abstract_status p.
    367515∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    368516silent_trace … (t1 @ t2) → silent_trace … t2.
    369 #S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
     517#p #S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
    370518#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
    371519#H @IH % inversion H in ⊢ ?;
     
    375523qed.
    376524
    377 lemma silent_append_l1 : ∀S : abstract_status.
     525lemma silent_append_l1 : ∀p.∀S : abstract_status p.
    378526∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    379527silent_trace … (t1 @ t2) → silent_trace … t1.
    380 #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     528#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
    381529[ #st #t2 #_ %2 % *]
    382530#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
     
    391539qed.
    392540
    393 lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
    394 ∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
    395 #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
     541lemma get_cost_label_silent_is_empty : ∀p.∀S : abstract_status p.
     542∀st1,st2.∀t : raw_trace p S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
     543#p #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
    396544#H inversion H
    397545[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
     
    399547qed.
    400548
    401 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
    402 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     549lemma get_cost_label_invariant_for_append_silent_trace_l :∀p.∀S : abstract_status p.
     550∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
    403551silent_trace … t1 →
    404552get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
    405 #S #st1 #st2 #st3 #t1 elim t1
     553#p #S #st1 #st2 #st3 #t1 elim t1
    406554[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
    407555[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
     
    409557#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
    410558#_ whd in ⊢ (??%?); >IH [%] %1 assumption
    411 qed. 
    412 
    413 lemma silent_suffix_cancellable : ∀S : abstract_status.
     559qed.
     560
     561lemma silent_suffix_cancellable : ∀p.∀S : abstract_status p.
    414562∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
    415563∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
     
    417565∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
    418566∀t2' : raw_trace … s3' s4.
    419 is_costlabelled_act l → is_costlabelled_act l' →
     567is_costlabelled_act … l → is_costlabelled_act … l' →
    420568silent_trace … t2 → silent_trace … t2' →
    421569t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
    422570s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
    423 #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
     571#p #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
    424572lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
    425573[ normalize #st * normalize
     
    445593(*PRE-MEASURABLE TRACES*)
    446594
    447 inductive pre_measurable_trace (S : abstract_status) :
    448 ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
    449  | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
    450  | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
    451                       ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    452                       as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
     595inductive pre_measurable_trace (p : label_params) (S : abstract_status p) :
     596∀st1,st2 : S.raw_trace st1 st2 → Prop ≝
     597 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base st)
     598 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel p.
     599                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
     600                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
    453601                      pre_measurable_trace … (t_ind … prf … tl)
    454  | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
     602 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel p.
    455603                      as_classify … st1 ≠ cl_io →
    456                       ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    457                       is_labelled_ret_act l → pre_measurable_trace … tl →
     604                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
     605                      is_labelled_ret_act l → pre_measurable_trace … tl →
    458606                      pre_measurable_trace … (t_ind … prf … tl)
    459  | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
    460                       ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    461                       as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
     607 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel p.
     608                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
     609                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
    462610                      pre_measurable_trace … tl →
    463611                      pre_measurable_trace … (t_ind … prf … tl)
    464612 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
    465                       ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
    466                       ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
     613                      ∀prf : as_execute … l1 st1 st2.∀t1 : raw_trace … st2 st3.
     614                      ∀t2 : raw_trace … st4 st5.∀prf' : as_execute … l2 st3 st4.
    467615                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
    468                       →  is_call_act l1 → ¬ is_call_post_label … st1 →
     616                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
    469617                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
    470                       as_syntactical_succ S st1 st4 →
    471                       is_unlabelled_ret_act l2 →
     618                      as_syntactical_succ st1 st4 →
     619                      is_unlabelled_ret_act l2 →
    472620                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
    473                      
    474 lemma pre_measurable_trace_inv : ∀S : abstract_status.
    475 ∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
    476 (st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
    477 (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
    478  t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
    479  pre_measurable_trace … tl) ∨
    480 (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
    481  t = t_ind … prf … tl ∧
    482  as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
    483 (∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
    484  t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
    485  (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
    486 (∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
    487  ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
    488  ∃prf' : as_execute S l2 st1'' st1'''.
    489  t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
    490  as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
    491  bool_to_Prop (¬ is_call_post_label … st1) ∧
    492  pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
    493  as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
    494 #S #st1 #st2 #t #H inversion H
    495 [ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
    496 | #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
    497   %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
    498 | #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
    499   %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
    500 | #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
    501   % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
    502 | #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
    503   #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
    504   %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
    505   %{prf'} /12 by conj/
    506 ]
    507 qed.
    508 
    509 lemma append_premeasurable_silent : ∀S : abstract_status.
    510 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     621
     622lemma append_premeasurable : ∀p.∀S : abstract_status p.
     623∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
     624pre_measurable_trace … t1 → pre_measurable_trace … t2 →
     625pre_measurable_trace … (t1 @ t2).
     626#p #S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
     627[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
     628  %2 // @IH //
     629| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
     630| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
     631| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
     632  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
     633  normalize >append_associative in ⊢ (?????(????????%)); %5 // @IH2 //
     634]
     635qed.
     636
     637lemma append_premeasurable_silent : ∀p.∀S : abstract_status p.
     638∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
    511639pre_measurable_trace … t → silent_trace … t' → 
    512640pre_measurable_trace … (t' @ t).
    513 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    514 [ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
     641#p #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     642[ #st #t #Hpre #_ whd in ⊢ (?????%); assumption]
    515643#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
    516644[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
    517645#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
    518 destruct #_ whd in ⊢ (????%); %2
     646destruct #_ whd in ⊢ (?????%); %2
    519647[ assumption
    520648| %{(None ?)} %
     
    524652qed.
    525653
    526 lemma pre_silent_is_premeasurable : ∀S : abstract_status.
    527 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
     654lemma pre_silent_is_premeasurable : ∀p.∀S : abstract_status p.
     655∀st1,st2 : S. ∀t : raw_trace st1 st2.pre_silent_trace … t
    528656→ pre_measurable_trace … t.
    529 #S #st1 #st2 #t elim t
     657#p #S #st1 #st2 #t elim t
    530658[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
    531659#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
     
    536664qed.
    537665
    538 lemma append_silent_premeasurable : ∀S : abstract_status.
    539 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     666lemma append_silent_premeasurable : ∀p.∀S : abstract_status p.
     667∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
    540668pre_measurable_trace … t' → silent_trace … t →
    541669pre_measurable_trace … (t' @ t).
    542 #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
     670#p #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
    543671[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
    544672  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
     
    552680#r #pre_r normalize
    553681>append_tind_commute >append_tind_commute >append_associative
    554 <append_tind_commute in ⊢ (????(??????%)); %5
     682<append_tind_commute in ⊢ (?????(???????%)); %5
    555683try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
    556684qed.
    557685
    558 lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
     686lemma head_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p.
    559687∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
    560 as_classify … st1 ≠ cl_io.
     688as_classify … st1 ≠ cl_io. #p
    561689#S #st1 #st2 #t #H inversion H //
    562690qed.
    563691
    564 lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
     692lemma get_costlabels_of_trace_empty : ∀p.∀S : abstract_status p.∀s1,s2 : S.∀t : raw_trace … s1 s2.
    565693get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
    566 #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
     694#p #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
    567695[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    568696| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     
    581709(*NO-IO TRACES*)
    582710
    583 inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
    584   t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
     711inductive no_io_trace (p : label_params) (S : abstract_status p) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
     712  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
    585713| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
    586714                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
    587715
    588 lemma no_io_append : ∀S : abstract_status.
     716lemma no_io_append : ∀p.∀S : abstract_status p.
    589717∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    590718∀t2 : raw_trace … st2 st3.
    591719no_io_trace … t1 → no_io_trace … t2 →
    592720no_io_trace … (t1 @ t2).
    593 #S #st1 #st2 #st3 #t1 lapply st3 elim t1
     721#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1
    594722[ #st #st3 #t2 #_ //]
    595723#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
     
    599727qed.
    600728
    601 lemma pre_measurable_no_io : ∀S : abstract_status.
     729lemma pre_measurable_no_io : ∀p.∀S : abstract_status p.
    602730∀st1,st2 : S. ∀t : raw_trace … st1 st2.
    603731pre_measurable_trace … t →
    604732no_io_trace … t.
    605 #S #st1 #st2 #t #H elim H /2/ -st1-st2
     733#p #S #st1 #st2 #t #H elim H /2/ -st1-st2
    606734#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
    607735#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
    608736qed.
    609737
    610 lemma head_of_no_io_is_no_io : ∀S : abstract_status.
     738lemma head_of_no_io_is_no_io : ∀p.∀S : abstract_status p.
    611739∀st1,st2 : S. ∀t : raw_trace … st1 st2.
    612740no_io_trace … t → as_classify … st1 ≠ cl_io.
    613 #S #st1 #st2 #t #H elim H //
    614 qed.
    615 
    616 
    617 lemma no_io_append_l1 : ∀S : abstract_status.
     741#p #S #st1 #st2 #t #H elim H //
     742qed.
     743
     744
     745lemma no_io_append_l1 : ∀p.∀S : abstract_status p.
    618746∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    619747∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
    620748no_io_trace … t1.
    621 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
     749#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
    622750#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
    623751[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     
    626754qed.
    627755
    628 lemma no_io_append_l2 : ∀S : abstract_status.
     756lemma no_io_append_l2 : ∀p.∀S : abstract_status p.
    629757∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    630758∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
    631759no_io_trace … t2.
    632 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
     760#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
    633761#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
    634762[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     
    638766(*MEASURABLE TRACES*)
    639767
    640 definition measurable :
    641  ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
    642 λS,si,s1,s3,sn,t.
     768definition measurable : ∀p.
     769 ∀S: abstract_status p. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
     770λp,S,si,s1,s3,sn,t.
    643771 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
    644772 ∃l1,l2,prf1,prf2.
    645  pre_measurable_trace … t12 ∧
    646   t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
    647  ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
    648  ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
     773 pre_measurable_trace p … t12 ∧
     774  t = ti0 @  t_ind … s0 s1 sn l1 prf1 … (t12 @ (t_ind … s2 s3 sn l2 prf2 … t3n))
     775 ∧ is_costlabelled_act … l1 ∧ is_costlabelled_act … l2 ∧ (is_call_act … l2 → bool_to_Prop (is_call_post_label … s2))
     776 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
    649777
    650778 
    651 definition measurable_prefix ≝ 
    652 λS : abstract_status.
     779definition measurable_prefix ≝  λp.
     780λS : abstract_status p.
    653781λs1,s4 :S.
    654782λt : raw_trace … s1 s4.
     
    656784∃l.∃prf : as_execute … l s2 s3.
    657785∃t34 : raw_trace … s3 s4.
    658 silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
     786silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
    659787
    660788lemma measurable_prefix_of_premeasurable :
    661 ∀S : abstract_status.
     789∀p.
     790∀S : abstract_status p.
    662791∀s1,s4 : S.
    663792∀t : raw_trace … s1 s4.
     
    665794get_costlabels_of_trace … t ≠ nil ? →
    666795measurable_prefix … t.
    667 #S #s1 #s4 #t elim t
     796#p #S #s1 #s4 #t elim t
    668797[ #st #_ * #H @⊥ @H %]
    669798#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
     
    709838
    710839definition measurable_suffix ≝
    711  λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
     840λp. λS : abstract_status p.λs1,s1' : S.λt : raw_trace … s1 s1'.
    712841∃s1_em : S.
    713842∃t_pre_em : raw_trace … s1 s1_em.
    714843∃s1_postem : S.
    715844     ∃t_post_em : raw_trace … s1_postem s1'.
    716      silent_trace S ?? t_post_em ∧
    717      ∃l_em : ActionLabel.
     845     silent_trace S ?? t_post_em ∧
     846     ∃l_em : ActionLabel p.
    718847     ∃ex_em : as_execute … l_em s1_em s1_postem.
    719848     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
    720      (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
    721      is_costlabelled_act l_em.
     849     (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
     850     is_costlabelled_act l_em.
    722851     
    723852
    724 lemma measurable_suffix_tind : ∀S : abstract_status.
    725 ∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
    726 measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t.
    727 #S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
     853lemma measurable_suffix_tind : ∀p.∀S : abstract_status p.
     854∀s1,s2,s3 : S.∀l : ActionLabel p.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
     855measurable_suffix … (t_ind … prf t) → (is_costlabelled_act … l ∧ silent_trace … t) ∨ measurable_suffix … t.
     856#p #S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
    728857[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
    729858 inversion t_pre in ⊢ ?;
     
    747876qed.
    748877
    749 lemma measurable_suffix_append : ∀S : abstract_status.
     878lemma measurable_suffix_append : ∀p.∀S : abstract_status p.
    750879∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    751880measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
    752 #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
     881#p #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
    753882* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
    754883%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
    755884qed.
    756885
    757 lemma measurable_suffix_append_l1 : ∀S : abstract_status.
     886lemma measurable_suffix_append_l1 : ∀p.∀S : abstract_status p.
    758887∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    759888measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
    760 #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     889#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
    761890[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
    762891 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
     
    771900| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
    772901  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
    773   change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) //
     902  change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append @(IH t2) //
    774903  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
    775904]
    776905qed.
    777906
    778 lemma measurable_suffix_append_case : ∀S : abstract_status.
     907lemma measurable_suffix_append_case : ∀p.∀S : abstract_status p.
    779908∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    780909measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
    781 #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     910#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
    782911[ #st #t2 #H %2 assumption]
    783912#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
    784913cases(measurable_suffix_tind … Hsuff)
    785 [ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%);
     914[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ??????? tl) @ t2) in Hsuff : (?????%);
    786915 @(measurable_suffix_append_l1 … Hsuff) /2/
    787916| #H cases(IH … H)
    788   [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append //
     917  [ * #H1 #H2 %% // change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append //
    789918  | /2/
    790919  ]
     
    792921qed.
    793922
    794 lemma measurable_is_measurable_suffix : ∀S : abstract_status.
     923lemma measurable_is_measurable_suffix : ∀p.∀S : abstract_status p.
    795924∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
    796 #S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
     925#p #S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
    797926#EQ destruct /11 width=20 by conj,ex_intro/
    798927qed.
    799928
    800 lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status.
     929lemma prefix_of_measurable_suffix_is_premeasurable : ∀p.∀S : abstract_status p.
    801930∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
    802931∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
    803 pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
    804 silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
     932pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
     933silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
    805934pre_measurable_trace … t1.
    806 #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
     935#p #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
    807936lapply s3 -s3 elim H -t -s1 -s4
    808937[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
     
    856985      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
    857986      * #l_em * #ex_em ** #EQ destruct #H1 #H2
    858       change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0;
     987      change with (t_ind … (t_base …) @ ?) in match (t_ind ????????) in e0;
    859988      <append_associative in e0; <append_associative #e0
    860989      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
Note: See TracChangeset for help on using the changeset viewer.