Changeset 3549 for LTS/Traces.ma
 Timestamp:
 Apr 2, 2015, 3:44:19 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Traces.ma
r3535 r3549 17 17 include "basics/deqsets.ma". 18 18 include "../src/ASM/Util.ma". 19 include "basics/finset.ma". 20 include "../src/utilities/hide.ma". 21 include "utils.ma". 22 23 (*Label parameters*) 24 25 record 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 36 notation "hvbox(a break ⊑ ^ {b} break term 46 c)" 37 non associative with precedence 45 38 for @{ 'lab_leq $a $b $c}. 39 40 interpretation "label 'less or equal to'" 'lab_leq x y z = (po_rel ? (po_label y) x z). 41 42 lemma 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/ 44 qed. 45 46 lemma 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/ 48 qed. 49 50 lemma 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 // 53 qed. 54 55 (*flat labels*) 56 57 definition 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 ] 70 qed. 71 72 definition part_order_nat ≝ mk_partial_order ℕ le ???. 73 /2 by le_to_le_to_eq, transitive_le, le_n/ 74 qed. 75 76 definition 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 ] 94 qed. 19 95 20 96 (*LABELS*) … … 23 99  a_function_id : ℕ → FunctionName. 24 100 25 inductive CallCostLabel : Type[0] ≝26  a_call_label : ℕ → CallCostLabel.101 inductive CallCostLabel (p : label_params) : Type[0] ≝ 102  a_call_label : p → CallCostLabel p. 27 103 28 inductive ReturnPostCostLabel : Type[0] ≝29  a_return_cost_label : ℕ → ReturnPostCostLabel.104 inductive ReturnPostCostLabel (p : label_params) : Type[0] ≝ 105  a_return_cost_label : p → ReturnPostCostLabel p. 30 106 31 inductive NonFunctionalLabel : Type[0] ≝32  a_non_functional_label : ℕ → NonFunctionalLabel.107 inductive NonFunctionalLabel (p : label_params) : Type[0] ≝ 108  a_non_functional_label : p → NonFunctionalLabel p. 33 109 34 inductive CostLabel : Type[0] ≝35  a_call : CallCostLabel → CostLabel36  a_return_post : ReturnPostCostLabel → CostLabel37  a_non_functional_label : NonFunctionalLabel → CostLabel.110 inductive 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. 38 114 39 115 coercion a_call. … … 41 117 coercion a_non_functional_label. 42 118 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 ?. 119 definition 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 123 lemma 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 ] 129 qed. 130 131 definition DEQNonFunctionalLabel ≝ λp.mk_DeqSet (NonFunctionalLabel p) (eq_nf_label p) ?. 52 132 #x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 53 133 assumption 54 134 qed. 55 135 56 unification hint 0 ≔ ;57 X ≟ DEQNonFunctionalLabel136 unification hint 0 ≔ p; 137 X ≟ (DEQNonFunctionalLabel p) 58 138 (*  *) ⊢ 59 NonFunctionalLabel≡ carr X.60 61 unification hint 0 ≔ p 1,p2;62 X ≟ DEQNonFunctionalLabel139 (NonFunctionalLabel p) ≡ carr X. 140 141 unification hint 0 ≔ p,p1,p2; 142 X ≟ (DEQNonFunctionalLabel p) 63 143 (*  *) ⊢ 64 eq_nf_label p 1 p2 ≡ eqb X p1 p2.144 eq_nf_label p p1 p2 ≡ eqb X p1 p2. 65 145 66 146 definition eq_function_name : FunctionName → FunctionName → bool ≝ … … 86 166 eq_function_name p1 p2 ≡ eqb X p1 p2. 87 167 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 ?. 168 definition 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 171 lemma 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 ] 177 qed. 178 179 definition DEQReturnPostCostLabel ≝ λp.mk_DeqSet (ReturnPostCostLabel p) (eq_return_cost_lab …) ?. 96 180 #x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 97 181 assumption 98 182 qed. 99 183 100 unification hint 0 ≔ ;101 X ≟ DEQReturnPostCostLabel184 unification hint 0 ≔ p ; 185 X ≟ (DEQReturnPostCostLabel p) 102 186 (*  *) ⊢ 103 ReturnPostCostLabel≡ carr X.104 105 unification hint 0 ≔ p 1,p2;106 X ≟ DEQReturnPostCostLabel187 (ReturnPostCostLabel p) ≡ carr X. 188 189 unification hint 0 ≔ p,p1,p2; 190 X ≟ (DEQReturnPostCostLabel p) 107 191 (*  *) ⊢ 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 194 definition 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 197 lemma 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 ] 203 qed. 204 205 definition DEQCallCostLabel ≝ λp.mk_DeqSet (CallCostLabel p) (eq_call_cost_lab p) ?. 118 206 #x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 119 207 assumption 120 208 qed. 121 209 122 unification hint 0 ≔ ;123 X ≟ DEQCallCostLabel210 unification hint 0 ≔ p; 211 X ≟ (DEQCallCostLabel p) 124 212 (*  *) ⊢ 125 CallCostLabel≡ carr X.126 127 unification hint 0 ≔ p 1,p2;128 X ≟ DEQCallCostLabel213 (CallCostLabel p) ≡ carr X. 214 215 unification hint 0 ≔ p,p1,p2; 216 X ≟ (DEQCallCostLabel p) 129 217 (*  *) ⊢ 130 eq_call_cost_lab p 1 p2 ≡ eqb X p1 p2.131 132 definition eq_costlabel : CostLabel → CostLabel→ bool ≝133 λ c1.match c1 with218 eq_call_cost_lab p p1 p2 ≡ eqb X p1 p2. 219 220 definition eq_costlabel :∀p. (CostLabel p) → (CostLabel p) → bool ≝ 221 λp,c1.match c1 with 134 222 [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1  _ ⇒ false ] 135 223  a_return_post x1 ⇒ … … 139 227 ]. 140 228 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 ??);229 lemma 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 ??); 144 232 try (@H2 % #EQ destruct) 145 [ change with (eq_call_cost_lab ?? ) in ⊢ (?%); @eq_call_cost_lab_elim233 [ change with (eq_call_cost_lab ???) in ⊢ (?%); @eq_call_cost_lab_elim 146 234 [ #EQ destruct @H1 %  * #H @H2 % #EQ destruct @H % ] 147  change with (eq_return_cost_lab ?? ) in ⊢ (?%);235  change with (eq_return_cost_lab ???) in ⊢ (?%); 148 236 @eq_return_cost_lab_elim 149 237 [ #EQ destruct @H1 %  * #H @H2 % #EQ destruct @H % ] 150  change with (eq_nf_label ?? ) in ⊢ (?%); @eq_fn_label_elim238  change with (eq_nf_label ???) in ⊢ (?%); @eq_fn_label_elim 151 239 [ #EQ destruct @H1 %  * #H @H2 % #EQ destruct @H % ] 152 240 ] … … 154 242 155 243 156 definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel?.244 definition DEQCostLabel ≝ λp.mk_DeqSet (CostLabel p) (eq_costlabel p) ?. 157 245 #x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H 158 246 assumption 159 247 qed. 160 248 161 unification hint 0 ≔ ;162 X ≟ DEQCostLabel249 unification hint 0 ≔ p ; 250 X ≟ (DEQCostLabel p) 163 251 (*  *) ⊢ 164 CostLabel≡ carr X.165 166 unification hint 0 ≔ p 1,p2;167 X ≟ DEQCostLabel252 (CostLabel p) ≡ carr X. 253 254 unification hint 0 ≔ p,p1,p2; 255 X ≟ (DEQCostLabel p) 168 256 (*  *) ⊢ 169 eq_costlabel p 1 p2 ≡ eqb X p1 p2.170 171 inductive ActionLabel : Type[0] ≝172  call_act : FunctionName → CallCostLabel → ActionLabel173  ret_act : option(ReturnPostCostLabel ) → ActionLabel174  cost_act : option NonFunctionalLabel → ActionLabel.257 eq_costlabel p p1 p2 ≡ eqb X p1 p2. 258 259 inductive 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. 175 263 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 264 definition eq_ActionLabel : ∀p.ActionLabel p → ActionLabel p → bool ≝ 265 λp,c1,c2. 266 match 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 280 definition is_cost_label : ∀p.ActionLabel p → Prop ≝ 281 λp,act.match act with [ cost_act nf ⇒ True  _ ⇒ False ]. 282 283 definition is_non_silent_cost_act : ∀p.ActionLabel p → Prop ≝ 284 λp,act. ∃l. act = cost_act … (Some ? l). 285 286 definition is_cost_act : ∀p.ActionLabel p → Prop ≝ 287 λp,act.∃l.act = cost_act … l. 288 289 definition is_call_act : ∀p.ActionLabel p → Prop ≝ 290 λp,act.∃f,l.act = call_act … f l. 291 292 definition is_labelled_ret_act : ∀p.(ActionLabel p) → Prop ≝ 293 λp,act.∃l.act = ret_act … (Some ? l). 294 295 definition is_unlabelled_ret_act : ∀p.ActionLabel p → Prop ≝ 296 λp,act.act = ret_act … (None ?). 297 298 definition is_costlabelled_act : ∀p.ActionLabel p → Prop ≝ 299 λp,act.match act with [ call_act _ _ ⇒ True 196 300  ret_act x ⇒ match x with [ Some _ ⇒ True  None ⇒ False ] 197 301  cost_act x ⇒ match x with [ Some _ ⇒ True  None ⇒ False ] 198 302 ]. 199 303 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. 304 definition is_ret_call_act : ∀p.ActionLabel p → Prop ≝ 305 λp,a.match a with [ret_act _ ⇒ True  call_act _ _ ⇒ True  _ ⇒ False ]. 306 307 definition 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 311 lemma 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 205 316 #P #H1 #H2 * /2/ 206 317 [ * /2/ @H2 % *] * /2/ @H2 %* 207 318 qed. 319 320 lemma 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 324 qed. 325 326 lemma 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 330 qed. 331 332 (* TOOLS FOR FRESHING LABELS *) 333 334 definition 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 337 definition 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 340 definition 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)〉. 208 342 209 343 … … 215 349  cl_other : status_class. 216 350 217 record abstract_status : Type[2] ≝351 record abstract_status (p : label_params) : Type[2] ≝ 218 352 { as_status :> Type[0] 219 ; as_execute : ActionLabel→ relation as_status353 ; as_execute : (ActionLabel p) → relation as_status 220 354 ; as_syntactical_succ : relation as_status 221 355 ; as_classify : as_status → status_class … … 225 359 ; jump_emits : ∀s1,s2,l. 226 360 as_classify … s1 = cl_jump → 227 as_execute l s1 s2 → is_non_silent_cost_act l361 as_execute l s1 s2 → is_non_silent_cost_act … l 228 362 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io → 229 as_execute l s1 s2 → is_non_silent_cost_act l363 as_execute l s1 s2 → is_non_silent_cost_act … l 230 364 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io → 231 as_execute l s1 s2 → is_non_silent_cost_act l365 as_execute l s1 s2 → is_non_silent_cost_act … l 232 366 }. 233 367 234 368 (* RAW TRACES *) 235 369 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 ≝ 370 inductive 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 377 let 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 ≝ 244 379 match t1 245 return λst1,st2,tr.raw_trace S st2 st3 → raw_traceS st1 st3380 return λst1,st2,tr.raw_trace … S st2 st3 → raw_trace … S st1 st3 246 381 with 247 382 [ t_base st ⇒ λt2.t2 … … 249 384 ]. 250 385 251 interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2). 252 253 lemma append_nil_is_nil : ∀S : abstract_status. 386 interpretation "trace_append" 'append t1 t2 = (append_on_trace ????? t1 t2). 387 388 let rec len (p : label_params) (s : abstract_status p) (st1 : s) (st2 : s) (t : raw_trace p s st1 st2) 389 on t : ℕ ≝ 390 match t with 391 [ t_base s ⇒ O 392  t_ind s1 s2 s3 l prf lt ⇒ S (len … lt) 393 ]. 394 395 lemma len_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S. 396 ∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3. 397 len ???? (t1 @ t2) = (len ???? t1) + (len ???? t2). 398 #p #S #st1 #st2 #st3 #t1 elim t1 normalize // 399 qed. 400 401 lemma append_nil_is_nil : ∀p. ∀S : abstract_status p. 254 402 ∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1. 255 403 t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1. 256 # S #s1 #s2 #t1 elim t1 t1 s1 s2404 #p #S #s1 #s2 #t1 elim t1 t1 s1 s2 257 405 [ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/] 258 406 #s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 259 407 qed. 260 408 261 lemma append_associative : ∀ S,st1,st2,st3,st4.262 ∀t1 : raw_trace S st1 st2.∀t2 : raw_traceS st2 st3.263 ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).264 # S #st1 #st2 #st3 #st4 #t1 elim t1 t1409 lemma 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 265 413 [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % 266 414 qed. 267 415 268 definition trace_prefix: ∀ S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →416 definition trace_prefix: ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st1 st2 → 269 417 raw_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 420 definition trace_suffix : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st2 st3 → 273 421 raw_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 with422 λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. 423 424 definition actionlabel_to_costlabel ≝ λp. 425 λl : ActionLabel p.match l with 278 426 [ call_act f c ⇒ [ c ] 279 427  ret_act x ⇒ match x with 280 [ Some c ⇒ [ a_return_post c ]428 [ Some c ⇒ [ a_return_post … c ] 281 429  None ⇒ [] 282 430 ] 283 431  cost_act x ⇒ match x with 284 [ Some c ⇒ [ a_non_functional_label c ]432 [ Some c ⇒ [ a_non_functional_label … c ] 285 433  None ⇒ [] 286 434 ] 287 435 ]. 288 436 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≝437 let 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) ≝ 291 439 match t with 292 440 [ t_base st ⇒ [ ] 293 441  t_ind st1' st2' st3' l prf t' ⇒ 294 442 let tl ≝ get_costlabels_of_trace … t' in 295 actionlabel_to_costlabel l @ tl443 actionlabel_to_costlabel … l @ tl 296 444 ]. 297 445 298 lemma get_cost_label_append : ∀ S : abstract_status.∀st1,st2,st3 : S.446 lemma get_cost_label_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S. 299 447 ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. 300 448 get_costlabels_of_trace … (t1 @ t2) = 301 449 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' * 303 451 [#f * #l  * [ * #l]  * [ #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH 304 452 qed. 305 453 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.454 lemma 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. 310 458 311 459 lemma get_costlabelled_is_costlabelled : 312 ∀ S : abstract_status.∀s1,s2,s3 : S. ∀l.460 ∀p.∀S : abstract_status p.∀s1,s2,s3 : S. ∀l. 313 461 ∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3. 314 is_costlabelled_act l →462 is_costlabelled_act p l → 315 463 get_costlabels_of_trace … (t_ind … prf t) = 1 + get_costlabels_of_trace … t. 316 # S #s1 #s2 #s3 * normalize464 #p #S #s1 #s2 #s3 * normalize 317 465 [ /2 by monotonic_pred/ 318 466  * normalize /2 by lt_to_le, monotonic_pred/ #_ #t * … … 323 471 (*SILENT TRACES*) 324 472 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 →473 inductive 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 → 330 478 pre_silent_trace … (t_ind … prf … tl). 331 479 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 ∨480 definition is_trace_non_empty : ∀p.∀S : abstract_status p.∀st1,st2. 481 raw_trace p S st1 st2 → bool ≝ 482 λp,S,st1,st2,t.match t with [ t_base _ ⇒ false  _ ⇒ true ]. 483 484 definition silent_trace : ∀p.∀S:abstract_status p.∀s1,s2 : S. 485 raw_trace p S s1 s2 → Prop ≝ λp,S,s1,s2,t.pre_silent_trace … t ∨ 338 486 ¬ (bool_to_Prop (is_trace_non_empty … t)). 339 487 340 lemma pre_silent_io : ∀ S : abstract_status.488 lemma pre_silent_io : ∀p.∀S : abstract_status p. 341 489 ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → 342 490 as_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] 344 492 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H // 345 493 #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct … … 347 495 qed. 348 496 349 lemma append_silent : ∀ S : abstract_status.497 lemma append_silent : ∀p.∀S : abstract_status p. 350 498 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2. 351 499 ∀t2 : raw_trace … s2 s3.silent_trace … t1 → 352 500 silent_trace … t2 → 353 501 silent_trace … (t1 @ t2). 354 # S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2502 #p #S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2 355 503 [ #st #t2 #_ * /2 by or_introl, or_intror/ ] 356 504 #st1 #st2 #st3 #l #prf #tl #IH #t2 * … … 364 512 qed. 365 513 366 lemma silent_append_l2 : ∀ S : abstract_status.514 lemma silent_append_l2 : ∀p.∀S : abstract_status p. 367 515 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 368 516 silent_trace … (t1 @ t2) → silent_trace … t2. 369 # S #s1 #s2 #s3 #t1 elim t1 // s1 s2517 #p #S #s1 #s2 #s3 #t1 elim t1 // s1 s2 370 518 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] 371 519 #H @IH % inversion H in ⊢ ?; … … 375 523 qed. 376 524 377 lemma silent_append_l1 : ∀ S : abstract_status.525 lemma silent_append_l1 : ∀p.∀S : abstract_status p. 378 526 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 379 527 silent_trace … (t1 @ t2) → silent_trace … t1. 380 # S #s1 #s2 #s3 #t1 elim t1 s1 s2528 #p #S #s1 #s2 #s3 #t1 elim t1 s1 s2 381 529 [ #st #t2 #_ %2 % *] 382 530 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H … … 391 539 qed. 392 540 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 % ]541 lemma 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 % ] 396 544 #H inversion H 397 545 [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3 … … 399 547 qed. 400 548 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 Sst2 st3.549 lemma 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. 403 551 silent_trace … t1 → 404 552 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. 405 # S #st1 #st2 #st3 #t1 elim t1553 #p #S #st1 #st2 #st3 #t1 elim t1 406 554 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 * 407 555 [2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %] … … 409 557 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct 410 558 #_ whd in ⊢ (??%?); >IH [%] %1 assumption 411 qed. 412 413 lemma silent_suffix_cancellable : ∀ S : abstract_status.559 qed. 560 561 lemma silent_suffix_cancellable : ∀p.∀S : abstract_status p. 414 562 ∀s1,s2,s2',s3,s3',s4 : S.∀l,l'. 415 563 ∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3. … … 417 565 ∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'. 418 566 ∀t2' : raw_trace … s3' s4. 419 is_costlabelled_act l → is_costlabelled_actl' →567 is_costlabelled_act … l → is_costlabelled_act … l' → 420 568 silent_trace … t2 → silent_trace … t2' → 421 569 t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') → 422 570 s2 = 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' 424 572 lapply prf prf lapply prf' prf' lapply t1' t1' elim t1 425 573 [ normalize #st * normalize … … 445 593 (*PREMEASURABLE TRACES*) 446 594 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 Sst2 st3.452 as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →595 inductive 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 → 453 601 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. 455 603 as_classify … st1 ≠ cl_io → 456 ∀prf : as_execute S l st1 st2.∀tl : raw_trace Sst2 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 → 458 606 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 Sst2 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 → 462 610 pre_measurable_trace … tl → 463 611 pre_measurable_trace … (t_ind … prf … tl) 464 612  pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. 465 ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace Sst2 st3.466 ∀t2 : raw_trace S st4 st5.∀prf' : as_execute Sl2 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. 467 615 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 → 469 617 pre_measurable_trace … t1 → pre_measurable_trace … t2 → 470 as_syntactical_succ Sst1 st4 →471 is_unlabelled_ret_act l2 →618 as_syntactical_succ … st1 st4 → 619 is_unlabelled_ret_act … l2 → 472 620 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 622 lemma append_premeasurable : ∀p.∀S : abstract_status p. 623 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3. 624 pre_measurable_trace … t1 → pre_measurable_trace … t2 → 625 pre_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 ] 635 qed. 636 637 lemma append_premeasurable_silent : ∀p.∀S : abstract_status p. 638 ∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1. 511 639 pre_measurable_trace … t → silent_trace … t' → 512 640 pre_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] 515 643 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?; 516 644 [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct] 517 645 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 518 destruct #_ whd in ⊢ (???? %); %2646 destruct #_ whd in ⊢ (?????%); %2 519 647 [ assumption 520 648  %{(None ?)} % … … 524 652 qed. 525 653 526 lemma pre_silent_is_premeasurable : ∀ S : abstract_status.527 ∀st1,st2 : S. ∀t : raw_trace Sst1 st2.pre_silent_trace … t654 lemma pre_silent_is_premeasurable : ∀p.∀S : abstract_status p. 655 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_silent_trace … t 528 656 → pre_measurable_trace … t. 529 # S #st1 #st2 #t elim t657 #p #S #st1 #st2 #t elim t 530 658 [ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ] 531 659 #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ] … … 536 664 qed. 537 665 538 lemma append_silent_premeasurable : ∀ S : abstract_status.539 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace Sst1' st1.666 lemma append_silent_premeasurable : ∀p.∀S : abstract_status p. 667 ∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1. 540 668 pre_measurable_trace … t' → silent_trace … t → 541 669 pre_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' 543 671 [ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ] 544 672 inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11 … … 552 680 #r #pre_r normalize 553 681 >append_tind_commute >append_tind_commute >append_associative 554 <append_tind_commute in ⊢ (???? (??????%)); %5682 <append_tind_commute in ⊢ (?????(???????%)); %5 555 683 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption 556 684 qed. 557 685 558 lemma head_of_premeasurable_is_not_io : ∀ S : abstract_status.686 lemma head_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p. 559 687 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → 560 as_classify … st1 ≠ cl_io. 688 as_classify … st1 ≠ cl_io. #p 561 689 #S #st1 #st2 #t #H inversion H // 562 690 qed. 563 691 564 lemma get_costlabels_of_trace_empty : ∀ S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.692 lemma get_costlabels_of_trace_empty : ∀p.∀S : abstract_status p.∀s1,s2 : S.∀t : raw_trace … s1 s2. 565 693 get_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 H694 #p #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H s1 s2 inversion H 567 695 [ #H1 #H2 #H3 #H4 #H5 #H6 destruct 568 696  #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct … … 581 709 (*NOIO TRACES*) 582 710 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)711 inductive 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) 585 713  t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io → 586 714 no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl). 587 715 588 lemma no_io_append : ∀ S : abstract_status.716 lemma no_io_append : ∀p.∀S : abstract_status p. 589 717 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 590 718 ∀t2 : raw_trace … st2 st3. 591 719 no_io_trace … t1 → no_io_trace … t2 → 592 720 no_io_trace … (t1 @ t2). 593 # S #st1 #st2 #st3 #t1 lapply st3 elim t1721 #p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 594 722 [ #st #st3 #t2 #_ //] 595 723 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?; … … 599 727 qed. 600 728 601 lemma pre_measurable_no_io : ∀ S : abstract_status.729 lemma pre_measurable_no_io : ∀p.∀S : abstract_status p. 602 730 ∀st1,st2 : S. ∀t : raw_trace … st1 st2. 603 731 pre_measurable_trace … t → 604 732 no_io_trace … t. 605 # S #st1 #st2 #t #H elim H /2/ st1st2733 #p #S #st1 #st2 #t #H elim H /2/ st1st2 606 734 #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5 607 735 #H6 #IH1 #IH2 %2 // @no_io_append // %2 // 608 736 qed. 609 737 610 lemma head_of_no_io_is_no_io : ∀ S : abstract_status.738 lemma head_of_no_io_is_no_io : ∀p.∀S : abstract_status p. 611 739 ∀st1,st2 : S. ∀t : raw_trace … st1 st2. 612 740 no_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 // 742 qed. 743 744 745 lemma no_io_append_l1 : ∀p.∀S : abstract_status p. 618 746 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 619 747 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 620 748 no_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/] 622 750 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?; 623 751 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ] … … 626 754 qed. 627 755 628 lemma no_io_append_l2 : ∀ S : abstract_status.756 lemma no_io_append_l2 : ∀p.∀S : abstract_status p. 629 757 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2. 630 758 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) → 631 759 no_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 ] 633 761 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?; 634 762 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ] … … 638 766 (*MEASURABLE TRACES*) 639 767 640 definition measurable : 641 ∀S: abstract_status . ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝642 λ S,si,s1,s3,sn,t.768 definition 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. 643 771 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn. 644 772 ∃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_actl2 → 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)). 649 777 650 778 651 definition measurable_prefix ≝ 652 λS : abstract_status .779 definition measurable_prefix ≝ λp. 780 λS : abstract_status p. 653 781 λs1,s4 :S. 654 782 λt : raw_trace … s1 s4. … … 656 784 ∃l.∃prf : as_execute … l s2 s3. 657 785 ∃t34 : raw_trace … s3 s4. 658 silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.786 silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act … l. 659 787 660 788 lemma measurable_prefix_of_premeasurable : 661 ∀S : abstract_status. 789 ∀p. 790 ∀S : abstract_status p. 662 791 ∀s1,s4 : S. 663 792 ∀t : raw_trace … s1 s4. … … 665 794 get_costlabels_of_trace … t ≠ nil ? → 666 795 measurable_prefix … t. 667 # S #s1 #s4 #t elim t796 #p #S #s1 #s4 #t elim t 668 797 [ #st #_ * #H @⊥ @H %] 669 798 #st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) l … … 709 838 710 839 definition 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'. 712 841 ∃s1_em : S. 713 842 ∃t_pre_em : raw_trace … s1 s1_em. 714 843 ∃s1_postem : S. 715 844 ∃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. 718 847 ∃ex_em : as_execute … l_em s1_em s1_postem. 719 848 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. 722 851 723 852 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 \wedgesilent_trace … t) ∨ measurable_suffix … t.727 # S #s1 #s2 #s3 #l #prf #t lapply prf prf lapply s1 s1 cases t t s2 s3853 lemma 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. 855 measurable_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 728 857 [ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em ** 729 858 inversion t_pre in ⊢ ?; … … 747 876 qed. 748 877 749 lemma measurable_suffix_append : ∀ S : abstract_status.878 lemma measurable_suffix_append : ∀p.∀S : abstract_status p. 750 879 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 751 880 measurable_suffix … t2 → measurable_suffix … (t1 @ t2). 752 # S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post881 #p #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post 753 882 * #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost 754 883 %{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/ 755 884 qed. 756 885 757 lemma measurable_suffix_append_l1 : ∀ S : abstract_status.886 lemma measurable_suffix_append_l1 : ∀p.∀S : abstract_status p. 758 887 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 759 888 measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1. 760 # S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2889 #p #S #s1 #s2 #s3 #t1 elim t1 t1 s1 s2 761 890 [#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct 762 891 #Hcall #Hcost #H lapply(silent_append_l2 … H) H * [2: * #H cases(H I)] #H inversion H … … 771 900  #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em 772 901 ** #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) // 774 903 %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption 775 904 ] 776 905 qed. 777 906 778 lemma measurable_suffix_append_case : ∀ S : abstract_status.907 lemma measurable_suffix_append_case : ∀p.∀S : abstract_status p. 779 908 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3. 780 909 measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2. 781 # S #s1 #s2 #s3 #t1 elim t1 s1 s2910 #p #S #s1 #s2 #s3 #t1 elim t1 s1 s2 782 911 [ #st #t2 #H %2 assumption] 783 912 #st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff 784 913 cases(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 : (?????%); 786 915 @(measurable_suffix_append_l1 … Hsuff) /2/ 787 916  #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 // 789 918  /2/ 790 919 ] … … 792 921 qed. 793 922 794 lemma measurable_is_measurable_suffix : ∀ S : abstract_status.923 lemma measurable_is_measurable_suffix : ∀p.∀S : abstract_status p. 795 924 ∀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 ******* #_ 797 926 #EQ destruct /11 width=20 by conj,ex_intro/ 798 927 qed. 799 928 800 lemma prefix_of_measurable_suffix_is_premeasurable : ∀ S : abstract_status.929 lemma prefix_of_measurable_suffix_is_premeasurable : ∀p.∀S : abstract_status p. 801 930 ∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3. 802 931 ∀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)) →932 pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act … l → 933 silent_trace … t2 → (is_call_act … l → bool_to_Prop(is_call_post_label … s2)) → 805 934 pre_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 s2935 #p #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 t1 lapply t2 t2 lapply prf prf lapply s2 s2 807 936 lapply s3 s3 elim H t s1 s4 808 937 [ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?; … … 856 985 [ **] Hmeas IH1 EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost 857 986 * #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; 859 988 <append_associative in e0; <append_associative #e0 860 989 cases(silent_suffix_cancellable … e0) // e0 * #EQ1 #EQ2 #EQ3 destruct
Note: See TracChangeset
for help on using the changeset viewer.