From 93b89122000e42ac57abc39734fdf05d3a89e83c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Jul 2011 08:26:16 +0000 Subject: Merge of branch new-semantics: revised and strengthened top-level statements of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Behaviors.v | 700 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 700 insertions(+) create mode 100644 common/Behaviors.v (limited to 'common/Behaviors.v') diff --git a/common/Behaviors.v b/common/Behaviors.v new file mode 100644 index 00000000..ccb5749f --- /dev/null +++ b/common/Behaviors.v @@ -0,0 +1,700 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Whole-program behaviors *) + +Require Import Classical. +Require Import ClassicalEpsilon. +Require Import Coqlib. +Require Import AST. +Require Import Events. +Require Import Globalenvs. +Require Import Integers. +Require Import Smallstep. + +Set Implicit Arguments. + +(** * Behaviors for program executions *) + +(** The four possible outcomes for the execution of a program: +- Termination, with a finite trace of observable events + and an integer value that stands for the process exit code + (the return value of the main function). +- Divergence with a finite trace of observable events. + (At some point, the program runs forever without doing any I/O.) +- Reactive divergence with an infinite trace of observable events. + (The program performs infinitely many I/O operations separated + by finite amounts of internal computations.) +- Going wrong, with a finite trace of observable events + performed before the program gets stuck. +*) + +Inductive program_behavior: Type := + | Terminates: trace -> int -> program_behavior + | Diverges: trace -> program_behavior + | Reacts: traceinf -> program_behavior + | Goes_wrong: trace -> program_behavior. + +(** Operations and relations on behaviors *) + +Definition not_wrong (beh: program_behavior) : Prop := + match beh with + | Terminates _ _ => True + | Diverges _ => True + | Reacts _ => True + | Goes_wrong _ => False + end. + +Definition behavior_app (t: trace) (beh: program_behavior): program_behavior := + match beh with + | Terminates t1 r => Terminates (t ** t1) r + | Diverges t1 => Diverges (t ** t1) + | Reacts T => Reacts (t *** T) + | Goes_wrong t1 => Goes_wrong (t ** t1) + end. + +Lemma behavior_app_assoc: + forall t1 t2 beh, + behavior_app (t1 ** t2) beh = behavior_app t1 (behavior_app t2 beh). +Proof. + intros. destruct beh; simpl; f_equal; traceEq. +Qed. + +Lemma behavior_app_E0: + forall beh, behavior_app E0 beh = beh. +Proof. + destruct beh; auto. +Qed. + +Definition behavior_prefix (t: trace) (beh: program_behavior) : Prop := + exists beh', beh = behavior_app t beh'. + +Definition behavior_improves (beh1 beh2: program_behavior) : Prop := + beh1 = beh2 \/ exists t, beh1 = Goes_wrong t /\ behavior_prefix t beh2. + +Lemma behavior_improves_refl: + forall beh, behavior_improves beh beh. +Proof. + intros; red; auto. +Qed. + +Lemma behavior_improves_trans: + forall beh1 beh2 beh3, + behavior_improves beh1 beh2 -> behavior_improves beh2 beh3 -> + behavior_improves beh1 beh3. +Proof. + intros. red. destruct H; destruct H0; subst; auto. + destruct H as [t1 [EQ1 [beh2' EQ1']]]. + destruct H0 as [t2 [EQ2 [beh3' EQ2']]]. + subst. destruct beh2'; simpl in EQ2; try discriminate. inv EQ2. + right. exists t1; split; auto. exists (behavior_app t beh3'). apply behavior_app_assoc. +Qed. + +Lemma behavior_improves_bot: + forall beh, behavior_improves (Goes_wrong E0) beh. +Proof. + intros. right. exists E0; split; auto. exists beh. rewrite behavior_app_E0; auto. +Qed. + +Lemma behavior_improves_app: + forall t beh1 beh2, + behavior_improves beh1 beh2 -> + behavior_improves (behavior_app t beh1) (behavior_app t beh2). +Proof. + intros. red; destruct H. left; congruence. + destruct H as [t' [A [beh' B]]]. subst. + right; exists (t ** t'); split; auto. exists beh'. rewrite behavior_app_assoc; auto. +Qed. + +(** Associating behaviors to programs. *) + +Section PROGRAM_BEHAVIORS. + +Variable L: semantics. + +Inductive state_behaves (s: state L): program_behavior -> Prop := + | state_terminates: forall t s' r, + Star L s t s' -> + final_state L s' r -> + state_behaves s (Terminates t r) + | state_diverges: forall t s', + Star L s t s' -> Forever_silent L s' -> + state_behaves s (Diverges t) + | state_reacts: forall T, + Forever_reactive L s T -> + state_behaves s (Reacts T) + | state_goes_wrong: forall t s', + Star L s t s' -> + Nostep L s' -> + (forall r, ~final_state L s' r) -> + state_behaves s (Goes_wrong t). + +Inductive program_behaves: program_behavior -> Prop := + | program_runs: forall s beh, + initial_state L s -> state_behaves s beh -> + program_behaves beh + | program_goes_initially_wrong: + (forall s, ~initial_state L s) -> + program_behaves (Goes_wrong E0). + +Lemma state_behaves_app: + forall s1 t s2 beh, + Star L s1 t s2 -> state_behaves s2 beh -> state_behaves s1 (behavior_app t beh). +Proof. + intros. inv H0; simpl; econstructor; eauto; try (eapply star_trans; eauto). + eapply star_forever_reactive; eauto. +Qed. + +(** * Existence of behaviors *) + +(** We now show that any program admits at least one behavior. + The proof requires classical logic: the axiom of excluded middle + and an axiom of description. *) + +(** The most difficult part of the proof is to show the existence + of an infinite trace in the case of reactive divergence. *) + +Section TRACEINF_REACTS. + +Variable s0: state L. + +Hypothesis reacts: + forall s1 t1, Star L s0 t1 s1 -> + exists s2, exists t2, Star L s1 t2 s2 /\ t2 <> E0. + +Lemma reacts': + forall s1 t1, Star L s0 t1 s1 -> + { s2 : state L & { t2 : trace | Star L s1 t2 s2 /\ t2 <> E0 } }. +Proof. + intros. + destruct (constructive_indefinite_description _ (reacts H)) as [s2 A]. + destruct (constructive_indefinite_description _ A) as [t2 [B C]]. + exists s2; exists t2; auto. +Qed. + +CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : traceinf' := + match reacts' ST with + | existT s2 (exist t2 (conj A B)) => + Econsinf' t2 + (build_traceinf' (star_trans ST A (refl_equal _))) + B + end. + +Lemma reacts_forever_reactive_rec: + forall s1 t1 (ST: Star L s0 t1 s1), + Forever_reactive L s1 (traceinf_of_traceinf' (build_traceinf' ST)). +Proof. + cofix COINDHYP; intros. + rewrite (unroll_traceinf' (build_traceinf' ST)). simpl. + destruct (reacts' ST) as [s2 [t2 [A B]]]. + rewrite traceinf_traceinf'_app. + econstructor. eexact A. auto. apply COINDHYP. +Qed. + +Lemma reacts_forever_reactive: + exists T, Forever_reactive L s0 T. +Proof. + exists (traceinf_of_traceinf' (build_traceinf' (star_refl (step L) (globalenv L) s0))). + apply reacts_forever_reactive_rec. +Qed. + +End TRACEINF_REACTS. + +Lemma diverges_forever_silent: + forall s0, + (forall s1 t1, Star L s0 t1 s1 -> exists s2, Step L s1 E0 s2) -> + Forever_silent L s0. +Proof. + cofix COINDHYP; intros. + destruct (H s0 E0) as [s1 ST]. constructor. + econstructor. eexact ST. apply COINDHYP. + intros. eapply H. eapply star_left; eauto. +Qed. + +Lemma state_behaves_exists: + forall s, exists beh, state_behaves s beh. +Proof. + intros s0. + destruct (classic (forall s1 t1, Star L s0 t1 s1 -> exists s2, exists t2, Step L s1 t2 s2)). +(* 1 Divergence (silent or reactive) *) + destruct (classic (exists s1, exists t1, Star L s0 t1 s1 /\ + (forall s2 t2, Star L s1 t2 s2 -> + exists s3, Step L s2 E0 s3))). +(* 1.1 Silent divergence *) + destruct H0 as [s1 [t1 [A B]]]. + exists (Diverges t1); econstructor; eauto. + apply diverges_forever_silent; auto. +(* 1.2 Reactive divergence *) + destruct (@reacts_forever_reactive s0) as [T FR]. + intros. + generalize (not_ex_all_not _ _ H0 s1). intro A; clear H0. + generalize (not_ex_all_not _ _ A t1). intro B; clear A. + destruct (not_and_or _ _ B). contradiction. + destruct (not_all_ex_not _ _ H0) as [s2 C]; clear H0. + destruct (not_all_ex_not _ _ C) as [t2 D]; clear C. + destruct (imply_to_and _ _ D) as [E F]; clear D. + destruct (H s2 (t1 ** t2)) as [s3 [t3 G]]. eapply star_trans; eauto. + exists s3; exists (t2 ** t3); split. + eapply star_right; eauto. + red; intros. destruct (app_eq_nil t2 t3 H0). subst. elim F. exists s3; auto. + exists (Reacts T); econstructor; eauto. +(* 2 Termination (normal or by going wrong) *) + destruct (not_all_ex_not _ _ H) as [s1 A]; clear H. + destruct (not_all_ex_not _ _ A) as [t1 B]; clear A. + destruct (imply_to_and _ _ B) as [C D]; clear B. + destruct (classic (exists r, final_state L s1 r)) as [[r FINAL] | NOTFINAL]. +(* 2.1 Normal termination *) + exists (Terminates t1 r); econstructor; eauto. +(* 2.2 Going wrong *) + exists (Goes_wrong t1); econstructor; eauto. red. intros. + generalize (not_ex_all_not _ _ D s'); intros. + generalize (not_ex_all_not _ _ H t); intros. + auto. +Qed. + +Theorem program_behaves_exists: + exists beh, program_behaves beh. +Proof. + destruct (classic (exists s, initial_state L s)) as [[s0 INIT] | NOTINIT]. +(* 1. Initial state is defined. *) + destruct (state_behaves_exists s0) as [beh SB]. + exists beh; econstructor; eauto. +(* 2. Initial state is undefined *) + exists (Goes_wrong E0). apply program_goes_initially_wrong. + intros. eapply not_ex_all_not; eauto. +Qed. + +End PROGRAM_BEHAVIORS. + +(** * Forward simulations and program behaviors *) + +Section FORWARD_SIMULATIONS. + +Variable L1: semantics. +Variable L2: semantics. +Variable S: forward_simulation L1 L2. + +Lemma forward_simulation_state_behaves: + forall i s1 s2 beh1, + S i s1 s2 -> state_behaves L1 s1 beh1 -> + exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2. +Proof. + intros. inv H0. +(* termination *) + exploit simulation_star; eauto. intros [i' [s2' [A B]]]. + exists (Terminates t r); split. + econstructor; eauto. eapply fsim_match_final_states; eauto. + apply behavior_improves_refl. +(* silent divergence *) + exploit simulation_star; eauto. intros [i' [s2' [A B]]]. + exists (Diverges t); split. + econstructor; eauto. eapply simulation_forever_silent; eauto. + apply behavior_improves_refl. +(* reactive divergence *) + exists (Reacts T); split. + econstructor. eapply simulation_forever_reactive; eauto. + apply behavior_improves_refl. +(* going wrong *) + exploit simulation_star; eauto. intros [i' [s2' [A B]]]. + destruct (state_behaves_exists L2 s2') as [beh' SB]. + exists (behavior_app t beh'); split. + eapply state_behaves_app; eauto. + replace (Goes_wrong t) with (behavior_app t (Goes_wrong E0)). + apply behavior_improves_app. apply behavior_improves_bot. + simpl. decEq. traceEq. +Qed. + +Theorem forward_simulation_behavior_improves: + forall beh1, program_behaves L1 beh1 -> + exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2. +Proof. + intros. inv H. +(* initial state defined *) + exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]]. + exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]]. + exists beh2; split; auto. econstructor; eauto. +(* initial state undefined *) + destruct (classic (exists s', initial_state L2 s')). + destruct H as [s' INIT]. + destruct (state_behaves_exists L2 s') as [beh' SB]. + exists beh'; split. econstructor; eauto. apply behavior_improves_bot. + exists (Goes_wrong E0); split. + apply program_goes_initially_wrong. + intros; red; intros. elim H; exists s; auto. + apply behavior_improves_refl. +Qed. + +Corollary forward_simulation_same_safe_behavior: + forall beh, + program_behaves L1 beh -> not_wrong beh -> + program_behaves L2 beh. +Proof. + intros. exploit forward_simulation_behavior_improves; eauto. + intros [beh' [A B]]. destruct B. + congruence. + destruct H1 as [t [C D]]. subst. contradiction. +Qed. + +End FORWARD_SIMULATIONS. + +(** * Backward simulations and program behaviors *) + +Section BACKWARD_SIMULATIONS. + +Variable L1: semantics. +Variable L2: semantics. +Variable S: backward_simulation L1 L2. + +Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop := + forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 -> + (exists r, final_state L1 s' r) + \/ (exists t2, exists s'', Step L1 s' t2 s''). + +Remark safe_along_safe: + forall s b, safe_along_behavior s b -> safe L1 s. +Proof. + intros; red; intros. eapply H; eauto. symmetry; apply behavior_app_E0. +Qed. + +Remark star_safe_along: + forall s b t1 s' b2, + safe_along_behavior s b -> + Star L1 s t1 s' -> b = behavior_app t1 b2 -> + safe_along_behavior s' b2. +Proof. + intros; red; intros. eapply H. eapply star_trans; eauto. + subst. rewrite behavior_app_assoc. eauto. +Qed. + +Remark not_safe_along_behavior: + forall s b, + ~ safe_along_behavior s b -> + exists t, exists s', + behavior_prefix t b + /\ Star L1 s t s' + /\ Nostep L1 s' + /\ (forall r, ~(final_state L1 s' r)). +Proof. + intros. + destruct (not_all_ex_not _ _ H) as [t1 A]; clear H. + destruct (not_all_ex_not _ _ A) as [s' B]; clear A. + destruct (not_all_ex_not _ _ B) as [b2 C]; clear B. + destruct (imply_to_and _ _ C) as [D E]; clear C. + destruct (imply_to_and _ _ E) as [F G]; clear E. + destruct (not_or_and _ _ G) as [P Q]; clear G. + exists t1; exists s'. + split. exists b2; auto. + split. auto. + split. red; intros; red; intros. elim Q. exists t; exists s'0; auto. + intros; red; intros. elim P. exists r; auto. +Qed. + +Lemma backward_simulation_star: + forall s2 t s2', Star L2 s2 t s2' -> + forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) -> + exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'. +Proof. + induction 1; intros. + exists i; exists s1; split; auto. apply star_refl. + exploit (bsim_simulation S); eauto. eapply safe_along_safe; eauto. + intros [i' [s1' [A B]]]. + assert (Star L1 s0 t1 s1'). intuition. apply plus_star; auto. + exploit IHstar; eauto. eapply star_safe_along; eauto. + subst t; apply behavior_app_assoc. + intros [i'' [s2'' [C D]]]. + exists i''; exists s2''; split; auto. eapply star_trans; eauto. +Qed. + +Lemma backward_simulation_forever_silent: + forall i s1 s2, + Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> + Forever_silent L1 s1. +Proof. + assert (forall i s1 s2, + Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> + forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1). + cofix COINDHYP; intros. + inv H. destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]]. + destruct A as [C | [C D]]. + eapply forever_silent_N_plus; eauto. eapply COINDHYP; eauto. + eapply star_safe; eauto. apply plus_star; auto. + eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto. + eapply star_safe; eauto. + intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf. +Qed. + +Lemma backward_simulation_forever_reactive: + forall i s1 s2 T, + Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) -> + Forever_reactive L1 s1 T. +Proof. + cofix COINDHYP; intros. inv H. + destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto. + econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto. +Qed. + +Lemma backward_simulation_state_behaves: + forall i s1 s2 beh2, + S i s1 s2 -> state_behaves L2 s2 beh2 -> + exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2. +Proof. + intros. destruct (classic (safe_along_behavior s1 beh2)). +(* 1. Safe along *) + exists beh2; split; [idtac|apply behavior_improves_refl]. + inv H0. +(* termination *) + assert (Terminates t r = behavior_app t (Terminates E0 r)). + simpl. rewrite E0_right; auto. + rewrite H0 in H1. + exploit backward_simulation_star; eauto. + intros [i' [s1' [A B]]]. + exploit (bsim_match_final_states S); eauto. + eapply safe_along_safe. eapply star_safe_along; eauto. + intros [s1'' [C D]]. + econstructor. eapply star_trans; eauto. traceEq. auto. +(* silent divergence *) + assert (Diverges t = behavior_app t (Diverges E0)). + simpl. rewrite E0_right; auto. + rewrite H0 in H1. + exploit backward_simulation_star; eauto. + intros [i' [s1' [A B]]]. + econstructor. eauto. eapply backward_simulation_forever_silent; eauto. + eapply safe_along_safe. eapply star_safe_along; eauto. +(* reactive divergence *) + econstructor. eapply backward_simulation_forever_reactive; eauto. +(* goes wrong *) + assert (Goes_wrong t = behavior_app t (Goes_wrong E0)). + simpl. rewrite E0_right; auto. + rewrite H0 in H1. + exploit backward_simulation_star; eauto. + intros [i' [s1' [A B]]]. + exploit (bsim_progress S); eauto. eapply safe_along_safe. eapply star_safe_along; eauto. + intros [[r FIN] | [t' [s2' STEP2]]]. + elim (H4 _ FIN). + elim (H3 _ _ STEP2). + +(* 2. Not safe along *) + exploit not_safe_along_behavior; eauto. + intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]]. + exists (Goes_wrong t); split. + econstructor; eauto. + right. exists t; auto. +Qed. + +Theorem backward_simulation_behavior_improves: + forall beh2, program_behaves L2 beh2 -> + exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2. +Proof. + intros. inv H. +(* L2's initial state is defined. *) + destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT]. +(* L1's initial state is defined too. *) + exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]]. + exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]]. + exists beh1; split; auto. econstructor; eauto. +(* L1 has no initial state *) + exists (Goes_wrong E0); split. + apply program_goes_initially_wrong. + intros; red; intros. elim NOINIT; exists s0; auto. + apply behavior_improves_bot. +(* L2 has no initial state *) + exists (Goes_wrong E0); split. + apply program_goes_initially_wrong. + intros; red; intros. + exploit (bsim_initial_states_exist S); eauto. intros [s2 INIT2]. + elim (H0 s2); auto. + apply behavior_improves_refl. +Qed. + +Corollary backward_simulation_same_safe_behavior: + (forall beh, program_behaves L1 beh -> not_wrong beh) -> + (forall beh, program_behaves L2 beh -> program_behaves L1 beh). +Proof. + intros. exploit backward_simulation_behavior_improves; eauto. + intros [beh' [A B]]. destruct B. + congruence. + destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto. +Qed. + +End BACKWARD_SIMULATIONS. + +(** * Additional results about infinite reduction sequences *) + +(** We now show that any infinite sequence of reductions is either of + the "reactive" kind or of the "silent" kind (after a finite number + of non-silent transitions). The proof necessitates the axiom of + excluded middle. This result is used below to relate + the coinductive big-step semantics for divergence with the + small-step notions of divergence. *) + +Unset Implicit Arguments. + +Section INF_SEQ_DECOMP. + +Variable genv: Type. +Variable state: Type. +Variable step: genv -> state -> trace -> state -> Prop. + +Variable ge: genv. + +Inductive tstate: Type := + ST: forall (s: state) (T: traceinf), forever step ge s T -> tstate. + +Definition state_of_tstate (S: tstate): state := + match S with ST s T F => s end. +Definition traceinf_of_tstate (S: tstate) : traceinf := + match S with ST s T F => T end. + +Inductive tstep: trace -> tstate -> tstate -> Prop := + | tstep_intro: forall s1 t T s2 S F, + tstep t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F)) + (ST s2 T F). + +Inductive tsteps: tstate -> tstate -> Prop := + | tsteps_refl: forall S, tsteps S S + | tsteps_left: forall t S1 S2 S3, tstep t S1 S2 -> tsteps S2 S3 -> tsteps S1 S3. + +Remark tsteps_trans: + forall S1 S2, tsteps S1 S2 -> forall S3, tsteps S2 S3 -> tsteps S1 S3. +Proof. + induction 1; intros. auto. econstructor; eauto. +Qed. + +Let treactive (S: tstate) : Prop := + forall S1, + tsteps S S1 -> + exists S2, exists S3, exists t, tsteps S1 S2 /\ tstep t S2 S3 /\ t <> E0. + +Let tsilent (S: tstate) : Prop := + forall S1 t S2, tsteps S S1 -> tstep t S1 S2 -> t = E0. + +Lemma treactive_or_tsilent: + forall S, treactive S \/ (exists S', tsteps S S' /\ tsilent S'). +Proof. + intros. destruct (classic (exists S', tsteps S S' /\ tsilent S')). + auto. + left. red; intros. + generalize (not_ex_all_not _ _ H S1). intros. + destruct (not_and_or _ _ H1). contradiction. + unfold tsilent in H2. + generalize (not_all_ex_not _ _ H2). intros [S2 A]. + generalize (not_all_ex_not _ _ A). intros [t B]. + generalize (not_all_ex_not _ _ B). intros [S3 C]. + generalize (imply_to_and _ _ C). intros [D F]. + generalize (imply_to_and _ _ F). intros [G J]. + exists S2; exists S3; exists t. auto. +Qed. + +Lemma tsteps_star: + forall S1 S2, tsteps S1 S2 -> + exists t, star step ge (state_of_tstate S1) t (state_of_tstate S2) + /\ traceinf_of_tstate S1 = t *** traceinf_of_tstate S2. +Proof. + induction 1. + exists E0; split. apply star_refl. auto. + inv H. destruct IHtsteps as [t' [A B]]. + exists (t ** t'); split. + simpl; eapply star_left; eauto. + simpl in *. subst T. traceEq. +Qed. + +Lemma tsilent_forever_silent: + forall S, + tsilent S -> forever_silent step ge (state_of_tstate S). +Proof. + cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros. + assert (tstep t (ST s1 (t *** T0) (forever_intro s1 t s0 f0)) + (ST s2 T0 f0)). + constructor. + assert (t = E0). + red in H. eapply H; eauto. apply tsteps_refl. + apply forever_silent_intro with (state_of_tstate (ST s2 T0 f0)). + rewrite <- H1. assumption. + apply COINDHYP. + red; intros. eapply H. eapply tsteps_left; eauto. eauto. +Qed. + +Lemma treactive_forever_reactive: + forall S, + treactive S -> forever_reactive step ge (state_of_tstate S) (traceinf_of_tstate S). +Proof. + cofix COINDHYP; intros. + destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply tsteps_refl. + destruct (tsteps_star _ _ A) as [t' [P Q]]. + inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. + apply forever_reactive_intro with s2. + eapply star_right; eauto. + red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction. + change (forever_reactive step ge (state_of_tstate (ST s2 T F)) (traceinf_of_tstate (ST s2 T F))). + apply COINDHYP. + red; intros. apply H. + eapply tsteps_trans. eauto. + eapply tsteps_left. constructor. eauto. +Qed. + +Theorem forever_silent_or_reactive: + forall s T, + forever step ge s T -> + forever_reactive step ge s T \/ + exists t, exists s', exists T', + star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'. +Proof. + intros. + destruct (treactive_or_tsilent (ST s T H)). + left. + change (forever_reactive step ge (state_of_tstate (ST s T H)) (traceinf_of_tstate (ST s T H))). + apply treactive_forever_reactive. auto. + destruct H0 as [S' [A B]]. + exploit tsteps_star; eauto. intros [t [C D]]. simpl in *. + right. exists t; exists (state_of_tstate S'); exists (traceinf_of_tstate S'). + split. auto. + split. apply tsilent_forever_silent. auto. + auto. +Qed. + +End INF_SEQ_DECOMP. + +Set Implicit Arguments. + +(** * Big-step semantics and program behaviors *) + +Section BIGSTEP_BEHAVIORS. + +Variable B: bigstep_semantics. +Variable L: semantics. +Hypothesis sound: bigstep_sound B L. + +Lemma behavior_bigstep_terminates: + forall t r, + bigstep_terminates B t r -> program_behaves L (Terminates t r). +Proof. + intros. exploit (bigstep_terminates_sound sound); eauto. + intros [s1 [s2 [P [Q R]]]]. + econstructor; eauto. econstructor; eauto. +Qed. + +Lemma behavior_bigstep_diverges: + forall T, + bigstep_diverges B T -> + program_behaves L (Reacts T) + \/ exists t, program_behaves L (Diverges t) /\ traceinf_prefix t T. +Proof. + intros. exploit (bigstep_diverges_sound sound); eauto. intros [s1 [P Q]]. + exploit forever_silent_or_reactive; eauto. intros [X | [t [s' [T' [X [Y Z]]]]]]. + left. econstructor; eauto. constructor; auto. + right. exists t; split. econstructor; eauto. econstructor; eauto. exists T'; auto. +Qed. + +End BIGSTEP_BEHAVIORS. -- cgit