| 1 | (**************************************************************************) |
|---|
| 2 | (* ___ *) |
|---|
| 3 | (* ||M|| *) |
|---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
|---|
| 5 | (* ||T|| *) |
|---|
| 6 | (* ||I|| Developers: *) |
|---|
| 7 | (* ||T|| The HELM team. *) |
|---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
|---|
| 9 | (* \ / *) |
|---|
| 10 | (* \ / This file is distributed under the terms of the *) |
|---|
| 11 | (* v GNU General Public License Version 2 *) |
|---|
| 12 | (* *) |
|---|
| 13 | (**************************************************************************) |
|---|
| 14 | |
|---|
| 15 | include "arithmetics/nat.ma". |
|---|
| 16 | include "basics/types.ma". |
|---|
| 17 | include "basics/deqsets.ma". |
|---|
| 18 | include "../src/ASM/Util.ma". |
|---|
| 19 | |
|---|
| 20 | inductive FunctionName : Type[0] ≝ |
|---|
| 21 | | a_function_id : ℕ → FunctionName. |
|---|
| 22 | |
|---|
| 23 | inductive CallCostLabel : Type[0] ≝ |
|---|
| 24 | | a_call_label : ℕ → CallCostLabel. |
|---|
| 25 | |
|---|
| 26 | inductive ReturnPostCostLabel : Type[0] ≝ |
|---|
| 27 | | a_return_cost_label : ℕ → ReturnPostCostLabel. |
|---|
| 28 | |
|---|
| 29 | inductive NonFunctionalLabel : Type[0] ≝ |
|---|
| 30 | | a_non_functional_label : ℕ → NonFunctionalLabel. |
|---|
| 31 | |
|---|
| 32 | inductive CostLabel : Type[0] ≝ |
|---|
| 33 | | a_call : CallCostLabel → CostLabel |
|---|
| 34 | | a_return_post : ReturnPostCostLabel → CostLabel |
|---|
| 35 | | a_non_functional_label : NonFunctionalLabel → CostLabel. |
|---|
| 36 | |
|---|
| 37 | coercion a_call. |
|---|
| 38 | coercion a_return_post. |
|---|
| 39 | coercion a_non_functional_label. |
|---|
| 40 | |
|---|
| 41 | (* |
|---|
| 42 | definition ret_act_label_to_cost_label : |
|---|
| 43 | (ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝ |
|---|
| 44 | λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b]. |
|---|
| 45 | |
|---|
| 46 | coercion ret_act_label_to_cost_label. |
|---|
| 47 | |
|---|
| 48 | definition call_act_label_to_cost_label : |
|---|
| 49 | (CallCostLabel + NonFunctionalLabel) → CostLabel ≝ |
|---|
| 50 | λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b]. |
|---|
| 51 | |
|---|
| 52 | coercion call_act_label_to_cost_label. |
|---|
| 53 | *) |
|---|
| 54 | |
|---|
| 55 | definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝ |
|---|
| 56 | λx,y.match x with [ a_non_functional_label n ⇒ |
|---|
| 57 | match y with [a_non_functional_label m ⇒ eqb n m ] ]. |
|---|
| 58 | |
|---|
| 59 | lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel. |
|---|
| 60 | (l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2). |
|---|
| 61 | #P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed. |
|---|
| 62 | |
|---|
| 63 | definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?. |
|---|
| 64 | #x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H |
|---|
| 65 | assumption |
|---|
| 66 | qed. |
|---|
| 67 | |
|---|
| 68 | unification hint 0 ≔ ; |
|---|
| 69 | X ≟ DEQNonFunctionalLabel |
|---|
| 70 | (* ---------------------------------------- *) ⊢ |
|---|
| 71 | NonFunctionalLabel ≡ carr X. |
|---|
| 72 | |
|---|
| 73 | unification hint 0 ≔ p1,p2; |
|---|
| 74 | X ≟ DEQNonFunctionalLabel |
|---|
| 75 | (* ---------------------------------------- *) ⊢ |
|---|
| 76 | eq_nf_label p1 p2 ≡ eqb X p1 p2. |
|---|
| 77 | |
|---|
| 78 | definition eq_function_name : FunctionName → FunctionName → bool ≝ |
|---|
| 79 | λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ]. |
|---|
| 80 | |
|---|
| 81 | lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2. |
|---|
| 82 | (f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2). |
|---|
| 83 | #P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed. |
|---|
| 84 | |
|---|
| 85 | definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?. |
|---|
| 86 | #x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H |
|---|
| 87 | assumption |
|---|
| 88 | qed. |
|---|
| 89 | |
|---|
| 90 | unification hint 0 ≔ ; |
|---|
| 91 | X ≟ DEQFunctionName |
|---|
| 92 | (* ---------------------------------------- *) ⊢ |
|---|
| 93 | FunctionName ≡ carr X. |
|---|
| 94 | |
|---|
| 95 | unification hint 0 ≔ p1,p2; |
|---|
| 96 | X ≟ DEQFunctionName |
|---|
| 97 | (* ---------------------------------------- *) ⊢ |
|---|
| 98 | eq_function_name p1 p2 ≡ eqb X p1 p2. |
|---|
| 99 | |
|---|
| 100 | definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝ |
|---|
| 101 | λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]]. |
|---|
| 102 | |
|---|
| 103 | lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → |
|---|
| 104 | (c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2). |
|---|
| 105 | #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed. |
|---|
| 106 | |
|---|
| 107 | definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?. |
|---|
| 108 | #x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H |
|---|
| 109 | assumption |
|---|
| 110 | qed. |
|---|
| 111 | |
|---|
| 112 | unification hint 0 ≔ ; |
|---|
| 113 | X ≟ DEQReturnPostCostLabel |
|---|
| 114 | (* ---------------------------------------- *) ⊢ |
|---|
| 115 | ReturnPostCostLabel ≡ carr X. |
|---|
| 116 | |
|---|
| 117 | unification hint 0 ≔ p1,p2; |
|---|
| 118 | X ≟ DEQReturnPostCostLabel |
|---|
| 119 | (* ---------------------------------------- *) ⊢ |
|---|
| 120 | eq_return_cost_lab p1 p2 ≡ eqb X p1 p2. |
|---|
| 121 | |
|---|
| 122 | definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝ |
|---|
| 123 | λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]]. |
|---|
| 124 | |
|---|
| 125 | lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → |
|---|
| 126 | (c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2). |
|---|
| 127 | #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed. |
|---|
| 128 | |
|---|
| 129 | definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?. |
|---|
| 130 | #x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H |
|---|
| 131 | assumption |
|---|
| 132 | qed. |
|---|
| 133 | |
|---|
| 134 | unification hint 0 ≔ ; |
|---|
| 135 | X ≟ DEQCallCostLabel |
|---|
| 136 | (* ---------------------------------------- *) ⊢ |
|---|
| 137 | CallCostLabel ≡ carr X. |
|---|
| 138 | |
|---|
| 139 | unification hint 0 ≔ p1,p2; |
|---|
| 140 | X ≟ DEQCallCostLabel |
|---|
| 141 | (* ---------------------------------------- *) ⊢ |
|---|
| 142 | eq_call_cost_lab p1 p2 ≡ eqb X p1 p2. |
|---|
| 143 | |
|---|
| 144 | definition eq_costlabel : CostLabel → CostLabel → bool ≝ |
|---|
| 145 | λc1.match c1 with |
|---|
| 146 | [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ] |
|---|
| 147 | | a_return_post x1 ⇒ |
|---|
| 148 | λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ] |
|---|
| 149 | | a_non_functional_label x1 ⇒ |
|---|
| 150 | λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ] |
|---|
| 151 | ]. |
|---|
| 152 | |
|---|
| 153 | lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → |
|---|
| 154 | (c1 ≠ c2 → P false) → P (eq_costlabel c1 c2). |
|---|
| 155 | #P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??); |
|---|
| 156 | try (@H2 % #EQ destruct) |
|---|
| 157 | [ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim |
|---|
| 158 | [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] |
|---|
| 159 | | change with (eq_return_cost_lab ??) in ⊢ (?%); |
|---|
| 160 | @eq_return_cost_lab_elim |
|---|
| 161 | [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] |
|---|
| 162 | | change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim |
|---|
| 163 | [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] |
|---|
| 164 | ] |
|---|
| 165 | qed. |
|---|
| 166 | |
|---|
| 167 | |
|---|
| 168 | definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?. |
|---|
| 169 | #x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H |
|---|
| 170 | assumption |
|---|
| 171 | qed. |
|---|
| 172 | |
|---|
| 173 | unification hint 0 ≔ ; |
|---|
| 174 | X ≟ DEQCostLabel |
|---|
| 175 | (* ---------------------------------------- *) ⊢ |
|---|
| 176 | CostLabel ≡ carr X. |
|---|
| 177 | |
|---|
| 178 | unification hint 0 ≔ p1,p2; |
|---|
| 179 | X ≟ DEQCostLabel |
|---|
| 180 | (* ---------------------------------------- *) ⊢ |
|---|
| 181 | eq_costlabel p1 p2 ≡ eqb X p1 p2. |
|---|
| 182 | |
|---|
| 183 | |
|---|
| 184 | |
|---|
| 185 | |
|---|
| 186 | inductive ActionLabel : Type[0] ≝ |
|---|
| 187 | | call_act : FunctionName → CallCostLabel → ActionLabel |
|---|
| 188 | | ret_act : option(ReturnPostCostLabel) → ActionLabel |
|---|
| 189 | | cost_act : option NonFunctionalLabel → ActionLabel |
|---|
| 190 | | init_act : ActionLabel. |
|---|
| 191 | |
|---|
| 192 | definition is_cost_label : ActionLabel → Prop ≝ |
|---|
| 193 | λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ]. |
|---|
| 194 | |
|---|
| 195 | inductive status_class : Type[0] ≝ |
|---|
| 196 | | cl_jump : status_class |
|---|
| 197 | | cl_io : status_class |
|---|
| 198 | | cl_other : status_class. |
|---|
| 199 | |
|---|
| 200 | definition is_non_silent_cost_act : ActionLabel → Prop ≝ |
|---|
| 201 | λact. ∃l. act = cost_act (Some ? l). |
|---|
| 202 | |
|---|
| 203 | record abstract_status : Type[2] ≝ |
|---|
| 204 | { as_status :> Type[0] |
|---|
| 205 | ; as_execute : ActionLabel → relation as_status |
|---|
| 206 | ; as_syntactical_succ : relation as_status |
|---|
| 207 | ; as_classify : as_status → status_class |
|---|
| 208 | ; is_call_post_label : as_status → bool |
|---|
| 209 | ; as_initial : as_status → bool |
|---|
| 210 | ; as_final : as_status → bool |
|---|
| 211 | ; jump_emits : ∀s1,s2,l. |
|---|
| 212 | as_classify … s1 = cl_jump → |
|---|
| 213 | as_execute l s1 s2 → is_non_silent_cost_act l |
|---|
| 214 | ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io → |
|---|
| 215 | as_execute l s1 s2 → is_non_silent_cost_act l |
|---|
| 216 | ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io → |
|---|
| 217 | as_execute l s1 s2 → is_non_silent_cost_act l |
|---|
| 218 | }. |
|---|
| 219 | (* |
|---|
| 220 | definition is_act_io_entering : abstract_status → ActionLabel → bool ≝ |
|---|
| 221 | λS,l.match l with |
|---|
| 222 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ] |
|---|
| 223 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
|---|
| 224 | | inr c' ⇒ is_io_entering S c'] |
|---|
| 225 | | None ⇒ false |
|---|
| 226 | ] |
|---|
| 227 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ] |
|---|
| 228 | | init_act ⇒ false |
|---|
| 229 | ]. |
|---|
| 230 | |
|---|
| 231 | definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝ |
|---|
| 232 | λS,l.match l with |
|---|
| 233 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ] |
|---|
| 234 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
|---|
| 235 | | inr c' ⇒ is_io_exiting S c'] |
|---|
| 236 | | None ⇒ false |
|---|
| 237 | ] |
|---|
| 238 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ] |
|---|
| 239 | | init_act ⇒ false |
|---|
| 240 | ]. |
|---|
| 241 | *) |
|---|
| 242 | |
|---|
| 243 | inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝ |
|---|
| 244 | | t_base : ∀st : S.raw_trace S st st |
|---|
| 245 | | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 246 | as_execute S l st1 st2 → raw_trace S st2 st3 → |
|---|
| 247 | raw_trace S st1 st3. |
|---|
| 248 | |
|---|
| 249 | definition is_cost_act : ActionLabel → Prop ≝ |
|---|
| 250 | λact.∃l.act = cost_act l. |
|---|
| 251 | |
|---|
| 252 | definition is_call_act : ActionLabel → Prop ≝ |
|---|
| 253 | λact.∃f,l.act = call_act f l. |
|---|
| 254 | |
|---|
| 255 | definition is_labelled_ret_act : ActionLabel → Prop ≝ |
|---|
| 256 | λact.∃l.act = ret_act (Some ? l). |
|---|
| 257 | |
|---|
| 258 | definition is_unlabelled_ret_act : ActionLabel → Prop ≝ |
|---|
| 259 | λact.act = ret_act (None ?). |
|---|
| 260 | |
|---|
| 261 | definition is_costlabelled_act : ActionLabel → Prop ≝ |
|---|
| 262 | λact.match act with [ call_act _ _ ⇒ True |
|---|
| 263 | | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
|---|
| 264 | | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
|---|
| 265 | | init_act ⇒ False |
|---|
| 266 | ]. |
|---|
| 267 | (* |
|---|
| 268 | lemma well_formed_trace_inv : |
|---|
| 269 | ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2. |
|---|
| 270 | well_formed_trace … t → |
|---|
| 271 | (st1 = st2 ∧ t ≃ t_base S st1) ∨ |
|---|
| 272 | (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. |
|---|
| 273 | well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧ |
|---|
| 274 | t ≃ t_ind … prf … tl) ∨ |
|---|
| 275 | (∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2. |
|---|
| 276 | well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨ |
|---|
| 277 | (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. |
|---|
| 278 | well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧ |
|---|
| 279 | is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*) |
|---|
| 280 | #S #st1 #st2 #t #H inversion H |
|---|
| 281 | [ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/ |
|---|
| 282 | | #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_ |
|---|
| 283 | % %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/ |
|---|
| 284 | | #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'} |
|---|
| 285 | %{l} %{prf} %{tl} % // % // |
|---|
| 286 | (*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3 |
|---|
| 287 | destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *) |
|---|
| 288 | ] |
|---|
| 289 | qed. |
|---|
| 290 | |
|---|
| 291 | *) |
|---|
| 292 | |
|---|
| 293 | let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S) |
|---|
| 294 | (t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝ |
|---|
| 295 | match t1 |
|---|
| 296 | return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3 |
|---|
| 297 | with |
|---|
| 298 | [ t_base st ⇒ λt2.t2 |
|---|
| 299 | | t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2) |
|---|
| 300 | ]. |
|---|
| 301 | |
|---|
| 302 | interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2). |
|---|
| 303 | |
|---|
| 304 | lemma append_associative : ∀S,st1,st2,st3,st4. |
|---|
| 305 | ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. |
|---|
| 306 | ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3). |
|---|
| 307 | #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1 |
|---|
| 308 | [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % |
|---|
| 309 | qed. |
|---|
| 310 | |
|---|
| 311 | definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 → |
|---|
| 312 | raw_trace … st1 st3 → Prop≝ |
|---|
| 313 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3. |
|---|
| 314 | |
|---|
| 315 | definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 → |
|---|
| 316 | raw_trace … st1 st3 → Prop≝ |
|---|
| 317 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. |
|---|
| 318 | |
|---|
| 319 | inductive pre_silent_trace (S : abstract_status) : |
|---|
| 320 | ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ |
|---|
| 321 | | silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st) |
|---|
| 322 | | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. |
|---|
| 323 | ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl → |
|---|
| 324 | pre_silent_trace … (t_ind … prf … tl). |
|---|
| 325 | |
|---|
| 326 | definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2. |
|---|
| 327 | raw_trace S st1 st2 → bool ≝ |
|---|
| 328 | λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ]. |
|---|
| 329 | |
|---|
| 330 | definition silent_trace : ∀S:abstract_status.∀s1,s2 : S. |
|---|
| 331 | raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨ |
|---|
| 332 | ¬ (bool_to_Prop (is_trace_non_empty … t)). |
|---|
| 333 | |
|---|
| 334 | lemma pre_silent_io : ∀S : abstract_status. |
|---|
| 335 | ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → |
|---|
| 336 | as_classify … s2 ≠ cl_io. |
|---|
| 337 | #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct] |
|---|
| 338 | #st1 #st2 #st3 #l #prf #tl #IH #H inversion H // |
|---|
| 339 | #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct |
|---|
| 340 | #EQ destruct #_ @IH assumption |
|---|
| 341 | qed. |
|---|
| 342 | |
|---|
| 343 | (* |
|---|
| 344 | definition silent_trace : ∀S : abstract_status.∀st1,st2 : S. |
|---|
| 345 | raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧ |
|---|
| 346 | well_formed_trace … t. |
|---|
| 347 | |
|---|
| 348 | lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S. |
|---|
| 349 | ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t. |
|---|
| 350 | #S #st1 #st2 #t * // |
|---|
| 351 | qed. *) |
|---|
| 352 | (* elim t -t |
|---|
| 353 | [ #st #_ %] |
|---|
| 354 | #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2 |
|---|
| 355 | [2: >cl % #EQ destruct] |
|---|
| 356 | @IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] |
|---|
| 357 | #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_ |
|---|
| 358 | % [ assumption | #_ assumption] |
|---|
| 359 | qed.*) |
|---|
| 360 | |
|---|
| 361 | inductive pre_measurable_trace (S : abstract_status) : |
|---|
| 362 | ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ |
|---|
| 363 | | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st) |
|---|
| 364 | | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 365 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 366 | as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → |
|---|
| 367 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 368 | | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 369 | as_classify … st1 ≠ cl_io → |
|---|
| 370 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 371 | is_labelled_ret_act l → pre_measurable_trace … tl → |
|---|
| 372 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 373 | | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel. |
|---|
| 374 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
|---|
| 375 | as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 → |
|---|
| 376 | pre_measurable_trace … tl → |
|---|
| 377 | pre_measurable_trace … (t_ind … prf … tl) |
|---|
| 378 | | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. |
|---|
| 379 | ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. |
|---|
| 380 | ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. |
|---|
| 381 | as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io |
|---|
| 382 | → is_call_act l1 → ¬ is_call_post_label … st1 → |
|---|
| 383 | pre_measurable_trace … t1 → pre_measurable_trace … t2 → |
|---|
| 384 | as_syntactical_succ S st1 st4 → |
|---|
| 385 | is_unlabelled_ret_act l2 → |
|---|
| 386 | pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). |
|---|
| 387 | |
|---|
| 388 | lemma pre_measurable_trace_inv : ∀S : abstract_status. |
|---|
| 389 | ∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t → |
|---|
| 390 | (st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨ |
|---|
| 391 | (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. |
|---|
| 392 | t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧ |
|---|
| 393 | pre_measurable_trace … tl) ∨ |
|---|
| 394 | (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. |
|---|
| 395 | t = t_ind … prf … tl ∧ |
|---|
| 396 | as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨ |
|---|
| 397 | (∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl. |
|---|
| 398 | t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧ |
|---|
| 399 | (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨ |
|---|
| 400 | (∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'. |
|---|
| 401 | ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2. |
|---|
| 402 | ∃prf' : as_execute S l2 st1'' st1'''. |
|---|
| 403 | t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧ |
|---|
| 404 | as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧ |
|---|
| 405 | bool_to_Prop (¬ is_call_post_label … st1) ∧ |
|---|
| 406 | pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧ |
|---|
| 407 | as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2). |
|---|
| 408 | #S #st1 #st2 #t #H inversion H |
|---|
| 409 | [ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % // |
|---|
| 410 | | #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
|---|
| 411 | %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // |
|---|
| 412 | | #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
|---|
| 413 | %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // |
|---|
| 414 | | #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
|---|
| 415 | % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % // |
|---|
| 416 | | #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1 |
|---|
| 417 | #H1st1' #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 |
|---|
| 418 | %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2} |
|---|
| 419 | %{prf'} /12 by conj/ |
|---|
| 420 | ] |
|---|
| 421 | qed. |
|---|
| 422 | |
|---|
