[3] | 1 | (* *********************************************************************) |
---|
| 2 | (* *) |
---|
| 3 | (* The Compcert verified compiler *) |
---|
| 4 | (* *) |
---|
| 5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
| 6 | (* *) |
---|
| 7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
| 8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
| 9 | (* under the terms of the GNU General Public License as published by *) |
---|
| 10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
| 11 | (* (at your option) any later version. This file is also distributed *) |
---|
| 12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
| 13 | (* *) |
---|
| 14 | (* *********************************************************************) |
---|
| 15 | |
---|
| 16 | (* * Tools for small-step operational semantics *) |
---|
| 17 | |
---|
| 18 | (* * This module defines generic operations and theorems over |
---|
| 19 | the one-step transition relations that are used to specify |
---|
| 20 | operational semantics in small-step style. *) |
---|
| 21 | |
---|
| 22 | (* |
---|
| 23 | Require Import Wf. |
---|
| 24 | Require Import Wf_nat. |
---|
| 25 | Require Import Classical. |
---|
| 26 | Require Import Coqlib. |
---|
| 27 | Require Import AST. |
---|
| 28 | *) |
---|
[700] | 29 | include "common/Events.ma". |
---|
[3] | 30 | (* |
---|
| 31 | Require Import Globalenvs. |
---|
| 32 | Require Import Integers. |
---|
| 33 | |
---|
| 34 | Set Implicit Arguments. |
---|
| 35 | *) |
---|
| 36 | (* * * Closures of transitions relations *) |
---|
| 37 | |
---|
[487] | 38 | record transrel : Type[1] ≝ { |
---|
| 39 | genv : Type[0]; |
---|
| 40 | state: Type[0]; |
---|
[3] | 41 | step : genv → state → trace → state → Prop |
---|
| 42 | }. |
---|
| 43 | |
---|
| 44 | (*Section CLOSURES. |
---|
| 45 | |
---|
| 46 | Variable genv: Type. |
---|
| 47 | Variable state: Type. |
---|
| 48 | |
---|
| 49 | (* * A one-step transition relation has the following signature. |
---|
| 50 | It is parameterized by a global environment, which does not |
---|
| 51 | change during the transition. It relates the initial state |
---|
| 52 | of the transition with its final state. The [trace] parameter |
---|
| 53 | captures the observable events possibly generated during the |
---|
| 54 | transition. *) |
---|
| 55 | |
---|
| 56 | Variable step: genv -> state -> trace -> state -> Prop. |
---|
| 57 | *) |
---|
| 58 | (* * No transitions: stuck state *) |
---|
| 59 | |
---|
[487] | 60 | definition nostep ≝ λtr:transrel. λge: genv tr. λs: state tr. |
---|
[3] | 61 | ∀t,s'. ¬((step tr) ge s t s'). |
---|
| 62 | |
---|
| 63 | (* * Zero, one or several transitions. Also known as Kleene closure, |
---|
| 64 | or reflexive transitive closure. *) |
---|
| 65 | |
---|
[487] | 66 | inductive star (tr:transrel) (ge: genv tr): state tr -> trace -> state tr -> Prop := |
---|
[3] | 67 | | star_refl: ∀s. |
---|
| 68 | star tr ge s E0 s |
---|
| 69 | | star_step: ∀s1,t1,s2,t2,s3,t. |
---|
| 70 | (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
| 71 | star tr ge s1 t s3. |
---|
| 72 | |
---|
[487] | 73 | lemma star_one: |
---|
[3] | 74 | ∀tr,ge,s1,t,s2. (step tr) ge s1 t s2 -> star tr ge s1 t s2. |
---|
[487] | 75 | #tr #ge #s1 #t #s2 #H @(star_step … H (star_refl …)) |
---|
| 76 | >(E0_right …) //; |
---|
| 77 | qed. |
---|
[3] | 78 | |
---|
[487] | 79 | lemma star_trans: |
---|
[3] | 80 | ∀tr,ge,s1,t1,s2. star tr ge s1 t1 s2 -> |
---|
| 81 | ∀t2,s3,t. star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> star tr ge s1 t s3. |
---|
[487] | 82 | #tr #ge #s1 #t1 #s2 #H elim H; |
---|
| 83 | [ #s #t2 #s3 #t #H0 #H1 >H1 normalize; //; |
---|
| 84 | | #s #t #s' #t' #s'' #t'' #H0 #H1 #H2 #H3 |
---|
| 85 | #t2 #s3 #t3 #H4 #H5 |
---|
| 86 | @(star_step … H0 (H3 … H4 …) ?) |
---|
| 87 | [ @(t'⧺t2) |
---|
| 88 | | // |
---|
[535] | 89 | | <(Eapp_assoc …) <H2 @H5 |
---|
[487] | 90 | ] |
---|
| 91 | ] |
---|
| 92 | qed. |
---|
[3] | 93 | |
---|
[487] | 94 | lemma star_left: |
---|
[3] | 95 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
| 96 | (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
| 97 | star tr ge s1 t s3. |
---|
[487] | 98 | @star_step |
---|
| 99 | qed. |
---|
[3] | 100 | |
---|
[487] | 101 | lemma star_right: |
---|
[3] | 102 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
| 103 | star tr ge s1 t1 s2 -> (step tr) ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
| 104 | star tr ge s1 t s3. |
---|
[487] | 105 | #tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3 |
---|
[535] | 106 | @(star_trans … H1 … (star_one … H2)) @H3 |
---|
[487] | 107 | qed. |
---|
[3] | 108 | |
---|
| 109 | (* * One or several transitions. Also known as the transitive closure. *) |
---|
| 110 | |
---|
[487] | 111 | inductive plus (tr:transrel) (ge: genv tr): state tr → trace → state tr → Prop ≝ |
---|
[3] | 112 | | plus_left: ∀s1,t1,s2,t2,s3,t. |
---|
| 113 | step tr ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
| 114 | plus tr ge s1 t s3. |
---|
| 115 | |
---|
[487] | 116 | lemma plus_one: |
---|
[3] | 117 | ∀tr,ge,s1,t,s2. |
---|
| 118 | step tr ge s1 t s2 -> plus tr ge s1 t s2. |
---|
[487] | 119 | #tr #ge #s1 #t #s2 #H @(plus_left … H (star_refl …)) |
---|
| 120 | >(E0_right …) //; |
---|
| 121 | qed. |
---|
[3] | 122 | |
---|
[487] | 123 | lemma plus_star: |
---|
[3] | 124 | ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2. |
---|
[487] | 125 | #tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1 |
---|
[535] | 126 | @(star_step … H1 H2 …) @e1; |
---|
[487] | 127 | qed. |
---|
[3] | 128 | |
---|
[487] | 129 | lemma plus_right: |
---|
[3] | 130 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
| 131 | star tr ge s1 t1 s2 -> step tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
| 132 | plus tr ge s1 t s3. |
---|
[487] | 133 | #tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar; |
---|
[1510] | 134 | [ #s2' #e2 #e3 #e4 #e5s destruct; @plus_one //; |
---|
| 135 | | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 #e6 |
---|
[891] | 136 | >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1) |
---|
[487] | 137 | [ 2: @(star_right … H2 Hstep) //; |
---|
| 138 | | skip; |
---|
| 139 | | // |
---|
| 140 | ] |
---|
| 141 | ] |
---|
[1510] | 142 | qed. |
---|
[3] | 143 | (* |
---|
| 144 | Lemma plus_left': |
---|
| 145 | forall ge s1 t1 s2 t2 s3 t, |
---|
| 146 | step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> |
---|
| 147 | plus ge s1 t s3. |
---|
| 148 | Proof. |
---|
| 149 | intros. eapply plus_left; eauto. apply plus_star; auto. |
---|
| 150 | Qed. |
---|
| 151 | |
---|
| 152 | Lemma plus_right': |
---|
| 153 | forall ge s1 t1 s2 t2 s3 t, |
---|
| 154 | plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> |
---|
| 155 | plus ge s1 t s3. |
---|
| 156 | Proof. |
---|
| 157 | intros. eapply plus_right; eauto. apply plus_star; auto. |
---|
| 158 | Qed. |
---|
| 159 | |
---|
| 160 | Lemma plus_star_trans: |
---|
| 161 | forall ge s1 t1 s2 t2 s3 t, |
---|
| 162 | plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
| 163 | Proof. |
---|
| 164 | intros. inversion H; subst. |
---|
| 165 | econstructor; eauto. eapply star_trans; eauto. |
---|
| 166 | traceEq. |
---|
| 167 | Qed. |
---|
| 168 | |
---|
| 169 | Lemma star_plus_trans: |
---|
| 170 | forall ge s1 t1 s2 t2 s3 t, |
---|
| 171 | star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
| 172 | Proof. |
---|
| 173 | intros. inversion H; subst. |
---|
| 174 | simpl; auto. |
---|
| 175 | rewrite Eapp_assoc. |
---|
| 176 | econstructor. eauto. eapply star_trans. eauto. |
---|
| 177 | apply plus_star. eauto. eauto. auto. |
---|
| 178 | Qed. |
---|
| 179 | |
---|
| 180 | Lemma plus_trans: |
---|
| 181 | forall ge s1 t1 s2 t2 s3 t, |
---|
| 182 | plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
| 183 | Proof. |
---|
| 184 | intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto. |
---|
| 185 | Qed. |
---|
| 186 | |
---|
| 187 | Lemma plus_inv: |
---|
| 188 | forall ge s1 t s2, |
---|
| 189 | plus ge s1 t s2 -> |
---|
| 190 | step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. |
---|
| 191 | Proof. |
---|
| 192 | intros. inversion H; subst. inversion H1; subst. |
---|
| 193 | left. rewrite E0_right. auto. |
---|
| 194 | right. exists s3; exists t1; exists (t0 ** t3); split. auto. |
---|
| 195 | split. econstructor; eauto. auto. |
---|
| 196 | Qed. |
---|
| 197 | |
---|
| 198 | Lemma star_inv: |
---|
| 199 | forall ge s1 t s2, |
---|
| 200 | star ge s1 t s2 -> |
---|
| 201 | (s2 = s1 /\ t = E0) \/ plus ge s1 t s2. |
---|
| 202 | Proof. |
---|
| 203 | intros. inv H. left; auto. right; econstructor; eauto. |
---|
| 204 | Qed. |
---|
| 205 | *) |
---|
| 206 | (* * Infinitely many transitions *) |
---|
| 207 | |
---|
[487] | 208 | coinductive forever (tr:transrel) (ge: genv tr): state tr -> traceinf -> Prop := |
---|
[3] | 209 | | forever_intro: ∀s1,t,s2,T. |
---|
| 210 | step tr ge s1 t s2 -> forever tr ge s2 T -> |
---|
| 211 | forever tr ge s1 (t ⧻ T). |
---|
| 212 | |
---|
[487] | 213 | lemma star_forever: |
---|
[3] | 214 | ∀tr,ge,s1,t,s2. star tr ge s1 t s2 -> |
---|
| 215 | ∀T. forever tr ge s2 T -> |
---|
| 216 | forever tr ge s1 (t ⧻ T). |
---|
[487] | 217 | #tr #ge #s1 #t1 #s2 #H elim H; |
---|
[535] | 218 | [ #s' #T #H2 @H2 |
---|
[487] | 219 | | #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3 |
---|
| 220 | >e1 >(Eappinf_assoc …) |
---|
| 221 | % /2/; |
---|
| 222 | ] qed. |
---|
[3] | 223 | (* |
---|
| 224 | (** An alternate, equivalent definition of [forever] that is useful |
---|
| 225 | for coinductive reasoning. *) |
---|
| 226 | |
---|
| 227 | Variable A: Type. |
---|
| 228 | Variable order: A -> A -> Prop. |
---|
| 229 | |
---|
| 230 | CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := |
---|
| 231 | | forever_N_star: forall s1 t s2 a1 a2 T1 T2, |
---|
| 232 | star ge s1 t s2 -> |
---|
| 233 | order a2 a1 -> |
---|
| 234 | forever_N ge a2 s2 T2 -> |
---|
| 235 | T1 = t *** T2 -> |
---|
| 236 | forever_N ge a1 s1 T1 |
---|
| 237 | | forever_N_plus: forall s1 t s2 a1 a2 T1 T2, |
---|
| 238 | plus ge s1 t s2 -> |
---|
| 239 | forever_N ge a2 s2 T2 -> |
---|
| 240 | T1 = t *** T2 -> |
---|
| 241 | forever_N ge a1 s1 T1. |
---|
| 242 | |
---|
| 243 | Hypothesis order_wf: well_founded order. |
---|
| 244 | |
---|
| 245 | Lemma forever_N_inv: |
---|
| 246 | forall ge a s T, |
---|
| 247 | forever_N ge a s T -> |
---|
| 248 | exists t, exists s', exists a', exists T', |
---|
| 249 | step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'. |
---|
| 250 | Proof. |
---|
| 251 | intros ge a0. pattern a0. apply (well_founded_ind order_wf). |
---|
| 252 | intros. inv H0. |
---|
| 253 | (* star case *) |
---|
| 254 | inv H1. |
---|
| 255 | (* no transition *) |
---|
| 256 | change (E0 *** T2) with T2. apply H with a2. auto. auto. |
---|
| 257 | (* at least one transition *) |
---|
| 258 | exists t1; exists s0; exists x; exists (t2 *** T2). |
---|
| 259 | split. auto. split. eapply forever_N_star; eauto. |
---|
| 260 | apply Eappinf_assoc. |
---|
| 261 | (* plus case *) |
---|
| 262 | inv H1. |
---|
| 263 | exists t1; exists s0; exists a2; exists (t2 *** T2). |
---|
| 264 | split. auto. |
---|
| 265 | split. inv H3. auto. |
---|
| 266 | eapply forever_N_plus. econstructor; eauto. eauto. auto. |
---|
| 267 | apply Eappinf_assoc. |
---|
| 268 | Qed. |
---|
| 269 | |
---|
| 270 | Lemma forever_N_forever: |
---|
| 271 | forall ge a s T, forever_N ge a s T -> forever ge s T. |
---|
| 272 | Proof. |
---|
| 273 | cofix COINDHYP; intros. |
---|
| 274 | destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]]. |
---|
| 275 | rewrite R. apply forever_intro with s'. auto. |
---|
| 276 | apply COINDHYP with a'; auto. |
---|
| 277 | Qed. |
---|
| 278 | |
---|
| 279 | (** Yet another alternative definition of [forever]. *) |
---|
| 280 | |
---|
| 281 | CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop := |
---|
| 282 | | forever_plus_intro: forall s1 t s2 T1 T2, |
---|
| 283 | plus ge s1 t s2 -> |
---|
| 284 | forever_plus ge s2 T2 -> |
---|
| 285 | T1 = t *** T2 -> |
---|
| 286 | forever_plus ge s1 T1. |
---|
| 287 | |
---|
| 288 | Lemma forever_plus_inv: |
---|
| 289 | forall ge s T, |
---|
| 290 | forever_plus ge s T -> |
---|
| 291 | exists s', exists t, exists T', |
---|
| 292 | step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'. |
---|
| 293 | Proof. |
---|
| 294 | intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2). |
---|
| 295 | split. auto. |
---|
| 296 | split. exploit star_inv; eauto. intros [[P Q] | R]. |
---|
| 297 | subst. simpl. auto. econstructor; eauto. |
---|
| 298 | traceEq. |
---|
| 299 | Qed. |
---|
| 300 | |
---|
| 301 | Lemma forever_plus_forever: |
---|
| 302 | forall ge s T, forever_plus ge s T -> forever ge s T. |
---|
| 303 | Proof. |
---|
| 304 | cofix COINDHYP; intros. |
---|
| 305 | destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]]. |
---|
| 306 | subst. econstructor; eauto. |
---|
| 307 | Qed. |
---|
| 308 | *) |
---|
| 309 | (* * Infinitely many silent transitions *) |
---|
| 310 | |
---|
[487] | 311 | coinductive forever_silent (tr:transrel) (ge: genv tr): state tr → Prop ≝ |
---|
[3] | 312 | | forever_silent_intro: ∀s1,s2. |
---|
| 313 | step tr ge s1 E0 s2 → forever_silent tr ge s2 → |
---|
| 314 | forever_silent tr ge s1. |
---|
| 315 | (* |
---|
| 316 | (** An alternate definition. *) |
---|
| 317 | |
---|
| 318 | CoInductive forever_silent_N (ge: genv) : A -> state -> Prop := |
---|
| 319 | | forever_silent_N_star: forall s1 s2 a1 a2, |
---|
| 320 | star ge s1 E0 s2 -> |
---|
| 321 | order a2 a1 -> |
---|
| 322 | forever_silent_N ge a2 s2 -> |
---|
| 323 | forever_silent_N ge a1 s1 |
---|
| 324 | | forever_silent_N_plus: forall s1 s2 a1 a2, |
---|
| 325 | plus ge s1 E0 s2 -> |
---|
| 326 | forever_silent_N ge a2 s2 -> |
---|
| 327 | forever_silent_N ge a1 s1. |
---|
| 328 | |
---|
| 329 | Lemma forever_silent_N_inv: |
---|
| 330 | forall ge a s, |
---|
| 331 | forever_silent_N ge a s -> |
---|
| 332 | exists s', exists a', |
---|
| 333 | step ge s E0 s' /\ forever_silent_N ge a' s'. |
---|
| 334 | Proof. |
---|
| 335 | intros ge a0. pattern a0. apply (well_founded_ind order_wf). |
---|
| 336 | intros. inv H0. |
---|
| 337 | (* star case *) |
---|
| 338 | inv H1. |
---|
| 339 | (* no transition *) |
---|
| 340 | apply H with a2. auto. auto. |
---|
| 341 | (* at least one transition *) |
---|
| 342 | exploit Eapp_E0_inv; eauto. intros [P Q]. subst. |
---|
| 343 | exists s0; exists x. |
---|
| 344 | split. auto. eapply forever_silent_N_star; eauto. |
---|
| 345 | (* plus case *) |
---|
| 346 | inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst. |
---|
| 347 | exists s0; exists a2. |
---|
| 348 | split. auto. inv H3. auto. |
---|
| 349 | eapply forever_silent_N_plus. econstructor; eauto. eauto. |
---|
| 350 | Qed. |
---|
| 351 | |
---|
| 352 | Lemma forever_silent_N_forever: |
---|
| 353 | forall ge a s, forever_silent_N ge a s -> forever_silent ge s. |
---|
| 354 | Proof. |
---|
| 355 | cofix COINDHYP; intros. |
---|
| 356 | destruct (forever_silent_N_inv H) as [s' [a' [P Q]]]. |
---|
| 357 | apply forever_silent_intro with s'. auto. |
---|
| 358 | apply COINDHYP with a'; auto. |
---|
| 359 | Qed. |
---|
| 360 | *) |
---|
| 361 | (* * Infinitely many non-silent transitions *) |
---|
| 362 | |
---|
[487] | 363 | coinductive forever_reactive (tr:transrel) (ge: genv tr): state tr → traceinf → Prop ≝ |
---|
[3] | 364 | | forever_reactive_intro: ∀s1,s2,t,T. |
---|
| 365 | star tr ge s1 t s2 → t ≠ E0 → forever_reactive tr ge s2 T → |
---|
| 366 | forever_reactive tr ge s1 (t ⧻ T). |
---|
| 367 | (* |
---|
[487] | 368 | lemma star_forever_reactive: |
---|
[3] | 369 | ∀tr,ge,s1,t,s2,T. |
---|
| 370 | star tr ge s1 t s2 → forever_reactive tr ge s2 T → |
---|
| 371 | forever_reactive tr ge s1 (t ⧻ T). |
---|
[487] | 372 | #tr #ge #s1 #t #s2 #T #H1 #H2 inversion H2; |
---|
[3] | 373 | Proof. |
---|
| 374 | intros. inv H0. rewrite <- Eappinf_assoc. econstructor. |
---|
| 375 | eapply star_trans; eauto. |
---|
| 376 | red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction. |
---|
| 377 | auto. |
---|
| 378 | Qed. |
---|
| 379 | *) |
---|
| 380 | (* * * Outcomes for program executions *) |
---|
| 381 | |
---|
| 382 | (* * The four possible outcomes for the execution of a program: |
---|
| 383 | - Termination, with a finite trace of observable events |
---|
| 384 | and an integer value that stands for the process exit code |
---|
| 385 | (the return value of the main function). |
---|
| 386 | - Divergence with a finite trace of observable events. |
---|
| 387 | (At some point, the program runs forever without doing any I/O.) |
---|
| 388 | - Reactive divergence with an infinite trace of observable events. |
---|
| 389 | (The program performs infinitely many I/O operations separated |
---|
| 390 | by finite amounts of internal computations.) |
---|
| 391 | - Going wrong, with a finite trace of observable events |
---|
| 392 | performed before the program gets stuck. |
---|
| 393 | *) |
---|
| 394 | |
---|
[487] | 395 | inductive program_behavior: Type[0] := |
---|
[3] | 396 | | Terminates: trace -> int -> program_behavior |
---|
| 397 | | Diverges: trace -> program_behavior |
---|
| 398 | | Reacts: traceinf -> program_behavior |
---|
| 399 | | Goes_wrong: trace -> program_behavior. |
---|
| 400 | |
---|
[487] | 401 | definition not_wrong : program_behavior → Prop ≝ λbeh. |
---|
[3] | 402 | match beh with |
---|
| 403 | [ Terminates _ _ => True |
---|
| 404 | | Diverges _ => True |
---|
| 405 | | Reacts _ => True |
---|
| 406 | | Goes_wrong _ => False |
---|
| 407 | ]. |
---|
| 408 | |
---|
| 409 | (* * Given a characterization of initial states and final states, |
---|
| 410 | [program_behaves] relates a program behaviour with the |
---|
| 411 | sequences of transitions that can be taken from an initial state |
---|
| 412 | to a final state. *) |
---|
| 413 | (* |
---|
| 414 | Variable initial_state: state -> Prop. |
---|
| 415 | Variable final_state: state -> int -> Prop. |
---|
| 416 | *) |
---|
[487] | 417 | inductive program_behaves (tr:transrel) |
---|
[3] | 418 | (initial_state:state tr → Prop) |
---|
| 419 | (final_state : state tr → int → Prop) |
---|
| 420 | (ge: genv tr) : program_behavior -> Prop ≝ |
---|
| 421 | | program_terminates: ∀s,t,s',r. |
---|
| 422 | initial_state s -> |
---|
| 423 | star tr ge s t s' -> |
---|
| 424 | final_state s' r -> |
---|
| 425 | program_behaves tr initial_state final_state ge (Terminates t r) |
---|
| 426 | | program_diverges: ∀s,t,s'. |
---|
| 427 | initial_state s -> |
---|
| 428 | star tr ge s t s' -> forever_silent tr ge s' -> |
---|
| 429 | program_behaves tr initial_state final_state ge (Diverges t) |
---|
| 430 | | program_reacts: ∀s,T. |
---|
| 431 | initial_state s -> |
---|
| 432 | forever_reactive tr ge s T -> |
---|
| 433 | program_behaves tr initial_state final_state ge (Reacts T) |
---|
| 434 | | program_goes_wrong: ∀s,t,s'. |
---|
| 435 | initial_state s -> |
---|
| 436 | star tr ge s t s' -> |
---|
| 437 | nostep tr ge s' -> |
---|
| 438 | (∀r. ¬final_state s' r) -> |
---|
| 439 | program_behaves tr initial_state final_state ge (Goes_wrong t) |
---|
| 440 | | program_goes_initially_wrong: |
---|
| 441 | (∀s. ¬initial_state s) -> |
---|
| 442 | program_behaves tr initial_state final_state ge (Goes_wrong E0). |
---|
| 443 | |
---|
| 444 | (*End CLOSURES.*) |
---|
| 445 | (* |
---|
| 446 | (** * Simulations between two small-step semantics. *) |
---|
| 447 | |
---|
| 448 | (** In this section, we show that if two transition relations |
---|
| 449 | satisfy certain simulation diagrams, then every program behaviour |
---|
| 450 | generated by the first transition relation can also occur |
---|
| 451 | with the second transition relation. *) |
---|
| 452 | |
---|
| 453 | Section SIMULATION. |
---|
| 454 | |
---|
| 455 | (** The first small-step semantics is axiomatized as follows. *) |
---|
| 456 | |
---|
| 457 | Variable genv1: Type. |
---|
| 458 | Variable state1: Type. |
---|
| 459 | Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. |
---|
| 460 | Variable initial_state1: state1 -> Prop. |
---|
| 461 | Variable final_state1: state1 -> int -> Prop. |
---|
| 462 | Variable ge1: genv1. |
---|
[20] | 463 | *) |
---|
[3] | 464 | |
---|
[487] | 465 | record semantics : Type[1] ≝ |
---|
[20] | 466 | { trans :> transrel |
---|
| 467 | ; initial : (state trans) → Prop |
---|
| 468 | ; final : (state trans) → int → Prop |
---|
| 469 | ; ge : (genv trans) |
---|
| 470 | }. |
---|
| 471 | |
---|
| 472 | (* |
---|
[3] | 473 | (** The second small-step semantics is also axiomatized. *) |
---|
| 474 | |
---|
[487] | 475 | Variable genv2: Type[0]. |
---|
| 476 | Variable state2: Type[0]. |
---|
[3] | 477 | Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. |
---|
| 478 | Variable initial_state2: state2 -> Prop. |
---|
| 479 | Variable final_state2: state2 -> int -> Prop. |
---|
| 480 | Variable ge2: genv2. |
---|
| 481 | |
---|
| 482 | (** We assume given a matching relation between states of both semantics. |
---|
| 483 | This matching relation must be compatible with initial states |
---|
| 484 | and with final states. *) |
---|
| 485 | |
---|
| 486 | Variable match_states: state1 -> state2 -> Prop. |
---|
| 487 | |
---|
| 488 | Hypothesis match_initial_states: |
---|
| 489 | forall st1, initial_state1 st1 -> |
---|
| 490 | exists st2, initial_state2 st2 /\ match_states st1 st2. |
---|
| 491 | |
---|
| 492 | Hypothesis match_final_states: |
---|
| 493 | forall st1 st2 r, |
---|
| 494 | match_states st1 st2 -> |
---|
| 495 | final_state1 st1 r -> |
---|
| 496 | final_state2 st2 r. |
---|
[20] | 497 | *) |
---|
[3] | 498 | |
---|
[487] | 499 | record related_semantics : Type[1] ≝ |
---|
[20] | 500 | { sem1 : semantics |
---|
| 501 | ; sem2 : semantics |
---|
| 502 | ; match_states : state sem1 → state sem2 → Prop |
---|
| 503 | ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2 |
---|
| 504 | ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r |
---|
| 505 | }. |
---|
| 506 | |
---|
| 507 | (* |
---|
[3] | 508 | (** Simulation when one transition in the first program |
---|
| 509 | corresponds to zero, one or several transitions in the second program. |
---|
| 510 | However, there is no stuttering: infinitely many transitions |
---|
| 511 | in the source program must correspond to infinitely many |
---|
| 512 | transitions in the second program. *) |
---|
| 513 | |
---|
| 514 | Section SIMULATION_STAR_WF. |
---|
| 515 | |
---|
| 516 | (** [order] is a well-founded ordering associated with states |
---|
| 517 | of the first semantics. Stuttering steps must correspond |
---|
| 518 | to states that decrease w.r.t. [order]. *) |
---|
| 519 | |
---|
| 520 | Variable order: state1 -> state1 -> Prop. |
---|
| 521 | Hypothesis order_wf: well_founded order. |
---|
| 522 | |
---|
| 523 | Hypothesis simulation: |
---|
| 524 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 525 | forall st2, match_states st1 st2 -> |
---|
| 526 | exists st2', |
---|
| 527 | (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1)) |
---|
| 528 | /\ match_states st1' st2'. |
---|
[20] | 529 | *) |
---|
[487] | 530 | record order_sim : Type[1] ≝ |
---|
[20] | 531 | { sem :> related_semantics |
---|
| 532 | ; order : state (sem1 sem) → state (sem1 sem) → Prop |
---|
| 533 | (* ; order_wf ? *) |
---|
| 534 | ; simulation : ∀st1,t,st1'. step (sem1 sem) (ge (sem1 sem)) st1 t st1' → |
---|
| 535 | ∀st2. match_states sem st1 st2 → |
---|
| 536 | ∃st2'. (plus (sem2 sem) (ge (sem2 sem)) st2 t st2' ∨ |
---|
| 537 | (star (sem2 sem) (ge (sem2 sem)) st2 t st2' ∧ |
---|
| 538 | order st1' st1)) |
---|
| 539 | ∧ match_states sem st1' st2' |
---|
| 540 | }. |
---|
[3] | 541 | |
---|
[487] | 542 | lemma simulation_star_star: ∀sim:order_sim. |
---|
[20] | 543 | ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' → |
---|
| 544 | ∀st2. match_states sim st1 st2 → |
---|
| 545 | ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'. |
---|
[487] | 546 | #sim #st1 #t #st1' #H elim H; |
---|
| 547 | [ #st1'' #st2 #Hmatch |
---|
| 548 | %{ st2} % //; |
---|
| 549 | | #st1 #tA #st1A #tB #st1B #t #Hstep #Hstar #Ht #IH #st2 #Hmatch |
---|
| 550 | elim (simulation sim ??? Hstep ? Hmatch); #st2' *; #A #B |
---|
| 551 | elim (IH ? B); #st3' *; #C #D |
---|
| 552 | %{ st3'} % //; |
---|
[535] | 553 | @(star_trans ??? tA st2' ? tB ?? C Ht) |
---|
| 554 | elim A /2/ * // |
---|
[487] | 555 | ] qed. |
---|
[3] | 556 | |
---|
[20] | 557 | (* |
---|
[3] | 558 | Lemma simulation_star_forever_silent: |
---|
| 559 | forall st1 st2, |
---|
| 560 | forever_silent step1 ge1 st1 -> match_states st1 st2 -> |
---|
| 561 | forever_silent step2 ge2 st2. |
---|
| 562 | Proof. |
---|
| 563 | assert (forall st1 st2, |
---|
| 564 | forever_silent step1 ge1 st1 -> match_states st1 st2 -> |
---|
| 565 | forever_silent_N step2 order ge2 st1 st2). |
---|
| 566 | cofix COINDHYP; intros. |
---|
| 567 | inversion H; subst. |
---|
| 568 | destruct (simulation H1 H0) as [st2' [A B]]. |
---|
| 569 | destruct A as [C | [C D]]. |
---|
| 570 | apply forever_silent_N_plus with st2' s2. |
---|
| 571 | auto. apply COINDHYP. assumption. assumption. |
---|
| 572 | apply forever_silent_N_star with st2' s2. |
---|
| 573 | auto. auto. apply COINDHYP. assumption. auto. |
---|
| 574 | intros. eapply forever_silent_N_forever; eauto. |
---|
| 575 | Qed. |
---|
| 576 | |
---|
| 577 | Lemma simulation_star_forever_reactive: |
---|
| 578 | forall st1 st2 T, |
---|
| 579 | forever_reactive step1 ge1 st1 T -> match_states st1 st2 -> |
---|
| 580 | forever_reactive step2 ge2 st2 T. |
---|
| 581 | Proof. |
---|
| 582 | cofix COINDHYP; intros. |
---|
| 583 | inv H. |
---|
| 584 | destruct (simulation_star_star H1 H0) as [st2' [A B]]. |
---|
| 585 | econstructor. eexact A. auto. |
---|
| 586 | eapply COINDHYP. eauto. auto. |
---|
| 587 | Qed. |
---|
| 588 | |
---|
| 589 | Lemma simulation_star_wf_preservation: |
---|
| 590 | forall beh, |
---|
| 591 | not_wrong beh -> |
---|
| 592 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
| 593 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
| 594 | Proof. |
---|
| 595 | intros. inv H0; simpl in H. |
---|
| 596 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
| 597 | destruct (simulation_star_star H2 B) as [s2' [C D]]. |
---|
| 598 | econstructor; eauto. |
---|
| 599 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
| 600 | destruct (simulation_star_star H2 B) as [s2' [C D]]. |
---|
| 601 | econstructor; eauto. |
---|
| 602 | eapply simulation_star_forever_silent; eauto. |
---|
| 603 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
| 604 | econstructor; eauto. eapply simulation_star_forever_reactive; eauto. |
---|
| 605 | contradiction. |
---|
| 606 | contradiction. |
---|
| 607 | Qed. |
---|
| 608 | |
---|
| 609 | End SIMULATION_STAR_WF. |
---|
| 610 | |
---|
| 611 | Section SIMULATION_STAR. |
---|
| 612 | |
---|
| 613 | (** We now consider the case where we have a nonnegative integer measure |
---|
| 614 | associated with states of the first semantics. It must decrease when we take |
---|
| 615 | a stuttering step. *) |
---|
| 616 | |
---|
| 617 | Variable measure: state1 -> nat. |
---|
| 618 | |
---|
| 619 | Hypothesis simulation: |
---|
| 620 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 621 | forall st2, match_states st1 st2 -> |
---|
| 622 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
| 623 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. |
---|
| 624 | |
---|
| 625 | Lemma simulation_star_preservation: |
---|
| 626 | forall beh, |
---|
| 627 | not_wrong beh -> |
---|
| 628 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
| 629 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
| 630 | Proof. |
---|
| 631 | intros. |
---|
| 632 | apply simulation_star_wf_preservation with (ltof _ measure). |
---|
| 633 | apply well_founded_ltof. intros. |
---|
| 634 | destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]]. |
---|
| 635 | exists st2'; auto. |
---|
| 636 | exists st2; split. right; split. rewrite B. apply star_refl. auto. auto. |
---|
| 637 | auto. auto. |
---|
| 638 | Qed. |
---|
| 639 | |
---|
| 640 | End SIMULATION_STAR. |
---|
| 641 | |
---|
| 642 | (** Lock-step simulation: each transition in the first semantics |
---|
| 643 | corresponds to exactly one transition in the second semantics. *) |
---|
| 644 | |
---|
| 645 | Section SIMULATION_STEP. |
---|
| 646 | |
---|
| 647 | Hypothesis simulation: |
---|
| 648 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 649 | forall st2, match_states st1 st2 -> |
---|
| 650 | exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'. |
---|
| 651 | |
---|
| 652 | Lemma simulation_step_preservation: |
---|
| 653 | forall beh, |
---|
| 654 | not_wrong beh -> |
---|
| 655 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
| 656 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
| 657 | Proof. |
---|
| 658 | intros. |
---|
| 659 | pose (measure := fun (st: state1) => 0%nat). |
---|
| 660 | assert (simulation': |
---|
| 661 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 662 | forall st2, match_states st1 st2 -> |
---|
| 663 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
| 664 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
| 665 | intros. destruct (simulation H1 H2) as [st2' [A B]]. |
---|
| 666 | left; exists st2'; split. apply plus_one; auto. auto. |
---|
| 667 | eapply simulation_star_preservation; eauto. |
---|
| 668 | Qed. |
---|
| 669 | |
---|
| 670 | End SIMULATION_STEP. |
---|
| 671 | |
---|
| 672 | (** Simulation when one transition in the first program corresponds |
---|
| 673 | to one or several transitions in the second program. *) |
---|
| 674 | |
---|
| 675 | Section SIMULATION_PLUS. |
---|
| 676 | |
---|
| 677 | Hypothesis simulation: |
---|
| 678 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 679 | forall st2, match_states st1 st2 -> |
---|
| 680 | exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'. |
---|
| 681 | |
---|
| 682 | Lemma simulation_plus_preservation: |
---|
| 683 | forall beh, |
---|
| 684 | not_wrong beh -> |
---|
| 685 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
| 686 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
| 687 | Proof. |
---|
| 688 | intros. |
---|
| 689 | pose (measure := fun (st: state1) => 0%nat). |
---|
| 690 | assert (simulation': |
---|
| 691 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 692 | forall st2, match_states st1 st2 -> |
---|
| 693 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
| 694 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
| 695 | intros. destruct (simulation H1 H2) as [st2' [A B]]. |
---|
| 696 | left; exists st2'; auto. |
---|
| 697 | eapply simulation_star_preservation; eauto. |
---|
| 698 | Qed. |
---|
| 699 | |
---|
| 700 | End SIMULATION_PLUS. |
---|
| 701 | |
---|
| 702 | (** Simulation when one transition in the first program |
---|
| 703 | corresponds to zero or one transitions in the second program. |
---|
| 704 | However, there is no stuttering: infinitely many transitions |
---|
| 705 | in the source program must correspond to infinitely many |
---|
| 706 | transitions in the second program. *) |
---|
| 707 | |
---|
| 708 | Section SIMULATION_OPT. |
---|
| 709 | |
---|
| 710 | Variable measure: state1 -> nat. |
---|
| 711 | |
---|
| 712 | Hypothesis simulation: |
---|
| 713 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 714 | forall st2, match_states st1 st2 -> |
---|
| 715 | (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
| 716 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. |
---|
| 717 | |
---|
| 718 | Lemma simulation_opt_preservation: |
---|
| 719 | forall beh, |
---|
| 720 | not_wrong beh -> |
---|
| 721 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
| 722 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
| 723 | Proof. |
---|
| 724 | assert (simulation': |
---|
| 725 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
| 726 | forall st2, match_states st1 st2 -> |
---|
| 727 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
| 728 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
| 729 | intros. elim (simulation H H0). |
---|
| 730 | intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto. |
---|
| 731 | intros [A [B C]]. right. intuition. |
---|
| 732 | intros. eapply simulation_star_preservation; eauto. |
---|
| 733 | Qed. |
---|
| 734 | |
---|
| 735 | End SIMULATION_OPT. |
---|
| 736 | |
---|
| 737 | End SIMULATION. |
---|
| 738 | |
---|
| 739 | (** * Additional results about infinite reduction sequences *) |
---|
| 740 | |
---|
| 741 | (** We now show that any infinite sequence of reductions is either of |
---|
| 742 | the "reactive" kind or of the "silent" kind (after a finite number |
---|
| 743 | of non-silent transitions). The proof necessitates the axiom of |
---|
| 744 | excluded middle. This result is used in [Csem] and [Cminor] to |
---|
| 745 | relate the coinductive big-step semantics for divergence with the |
---|
| 746 | small-step notions of divergence. *) |
---|
| 747 | |
---|
| 748 | Require Import Classical. |
---|
| 749 | Unset Implicit Arguments. |
---|
| 750 | |
---|
| 751 | Section INF_SEQ_DECOMP. |
---|
| 752 | |
---|
| 753 | Variable genv: Type. |
---|
| 754 | Variable state: Type. |
---|
| 755 | Variable step: genv -> state -> trace -> state -> Prop. |
---|
| 756 | |
---|
| 757 | Variable ge: genv. |
---|
| 758 | |
---|
| 759 | Inductive State: Type := |
---|
| 760 | ST: forall (s: state) (T: traceinf), forever step ge s T -> State. |
---|
| 761 | |
---|
| 762 | Definition state_of_State (S: State): state := |
---|
| 763 | match S with ST s T F => s end. |
---|
| 764 | Definition traceinf_of_State (S: State) : traceinf := |
---|
| 765 | match S with ST s T F => T end. |
---|
| 766 | |
---|
| 767 | Inductive Step: trace -> State -> State -> Prop := |
---|
| 768 | | Step_intro: forall s1 t T s2 S F, |
---|
| 769 | Step t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F)) |
---|
| 770 | (ST s2 T F). |
---|
| 771 | |
---|
| 772 | Inductive Steps: State -> State -> Prop := |
---|
| 773 | | Steps_refl: forall S, Steps S S |
---|
| 774 | | Steps_left: forall t S1 S2 S3, Step t S1 S2 -> Steps S2 S3 -> Steps S1 S3. |
---|
| 775 | |
---|
| 776 | Remark Steps_trans: |
---|
| 777 | forall S1 S2, Steps S1 S2 -> forall S3, Steps S2 S3 -> Steps S1 S3. |
---|
| 778 | Proof. |
---|
| 779 | induction 1; intros. auto. econstructor; eauto. |
---|
| 780 | Qed. |
---|
| 781 | |
---|
| 782 | Let Reactive (S: State) : Prop := |
---|
| 783 | forall S1, |
---|
| 784 | Steps S S1 -> |
---|
| 785 | exists S2, exists S3, exists t, Steps S1 S2 /\ Step t S2 S3 /\ t <> E0. |
---|
| 786 | |
---|
| 787 | Let Silent (S: State) : Prop := |
---|
| 788 | forall S1 t S2, Steps S S1 -> Step t S1 S2 -> t = E0. |
---|
| 789 | |
---|
| 790 | Lemma Reactive_or_Silent: |
---|
| 791 | forall S, Reactive S \/ (exists S', Steps S S' /\ Silent S'). |
---|
| 792 | Proof. |
---|
| 793 | intros. destruct (classic (exists S', Steps S S' /\ Silent S')). |
---|
| 794 | auto. |
---|
| 795 | left. red; intros. |
---|
| 796 | generalize (not_ex_all_not _ _ H S1). intros. |
---|
| 797 | destruct (not_and_or _ _ H1). contradiction. |
---|
| 798 | unfold Silent in H2. |
---|
| 799 | generalize (not_all_ex_not _ _ H2). intros [S2 A]. |
---|
| 800 | generalize (not_all_ex_not _ _ A). intros [t B]. |
---|
| 801 | generalize (not_all_ex_not _ _ B). intros [S3 C]. |
---|
| 802 | generalize (imply_to_and _ _ C). intros [D F]. |
---|
| 803 | generalize (imply_to_and _ _ F). intros [G J]. |
---|
| 804 | exists S2; exists S3; exists t. auto. |
---|
| 805 | Qed. |
---|
| 806 | |
---|
| 807 | Lemma Steps_star: |
---|
| 808 | forall S1 S2, Steps S1 S2 -> |
---|
| 809 | exists t, star step ge (state_of_State S1) t (state_of_State S2) |
---|
| 810 | /\ traceinf_of_State S1 = t *** traceinf_of_State S2. |
---|
| 811 | Proof. |
---|
| 812 | induction 1. |
---|
| 813 | exists E0; split. apply star_refl. auto. |
---|
| 814 | inv H. destruct IHSteps as [t' [A B]]. |
---|
| 815 | exists (t ** t'); split. |
---|
| 816 | simpl; eapply star_left; eauto. |
---|
| 817 | simpl in *. subst T. traceEq. |
---|
| 818 | Qed. |
---|
| 819 | |
---|
| 820 | Lemma Silent_forever_silent: |
---|
| 821 | forall S, |
---|
| 822 | Silent S -> forever_silent step ge (state_of_State S). |
---|
| 823 | Proof. |
---|
| 824 | cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros. |
---|
| 825 | assert (Step t (ST s1 (t *** T0) (forever_intro s1 t s0 f0)) |
---|
| 826 | (ST s2 T0 f0)). |
---|
| 827 | constructor. |
---|
| 828 | assert (t = E0). |
---|
| 829 | red in H. eapply H; eauto. apply Steps_refl. |
---|
| 830 | apply forever_silent_intro with (state_of_State (ST s2 T0 f0)). |
---|
| 831 | rewrite <- H1. assumption. |
---|
| 832 | apply COINDHYP. |
---|
| 833 | red; intros. eapply H. eapply Steps_left; eauto. eauto. |
---|
| 834 | Qed. |
---|
| 835 | |
---|
| 836 | Lemma Reactive_forever_reactive: |
---|
| 837 | forall S, |
---|
| 838 | Reactive S -> forever_reactive step ge (state_of_State S) (traceinf_of_State S). |
---|
| 839 | Proof. |
---|
| 840 | cofix COINDHYP; intros. |
---|
| 841 | destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply Steps_refl. |
---|
| 842 | destruct (Steps_star _ _ A) as [t' [P Q]]. |
---|
| 843 | inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. |
---|
| 844 | apply forever_reactive_intro with s2. |
---|
| 845 | eapply star_right; eauto. |
---|
| 846 | red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction. |
---|
| 847 | change (forever_reactive step ge (state_of_State (ST s2 T F)) (traceinf_of_State (ST s2 T F))). |
---|
| 848 | apply COINDHYP. |
---|
| 849 | red; intros. apply H. |
---|
| 850 | eapply Steps_trans. eauto. |
---|
| 851 | eapply Steps_left. constructor. eauto. |
---|
| 852 | Qed. |
---|
| 853 | |
---|
| 854 | Theorem forever_silent_or_reactive: |
---|
| 855 | forall s T, |
---|
| 856 | forever step ge s T -> |
---|
| 857 | forever_reactive step ge s T \/ |
---|
| 858 | exists t, exists s', exists T', |
---|
| 859 | star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'. |
---|
| 860 | Proof. |
---|
| 861 | intros. |
---|
| 862 | destruct (Reactive_or_Silent (ST s T H)). |
---|
| 863 | left. |
---|
| 864 | change (forever_reactive step ge (state_of_State (ST s T H)) (traceinf_of_State (ST s T H))). |
---|
| 865 | apply Reactive_forever_reactive. auto. |
---|
| 866 | destruct H0 as [S' [A B]]. |
---|
| 867 | exploit Steps_star; eauto. intros [t [C D]]. simpl in *. |
---|
| 868 | right. exists t; exists (state_of_State S'); exists (traceinf_of_State S'). |
---|
| 869 | split. auto. |
---|
| 870 | split. apply Silent_forever_silent. auto. |
---|
| 871 | auto. |
---|
| 872 | Qed. |
---|
| 873 | |
---|
| 874 | End INF_SEQ_DECOMP. |
---|
| 875 | |
---|
[487] | 876 | *) |
---|