From f6bdc196c093d413c900e38e894682b7b70d4483 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 31 Jan 2010 13:26:19 +0000 Subject: Existence of behaviors git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 63 ++++++++++++++++++++------ common/Smallstep.v | 128 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 176 insertions(+), 15 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 0f5d9d2..855c013 100644 --- a/common/Events.v +++ b/common/Events.v @@ -260,19 +260,6 @@ Inductive traceinf_prefix: trace -> traceinf -> Prop := traceinf_prefix t1 T2 -> traceinf_prefix (e :: t1) (Econsinf e T2). -(* -Lemma traceinf_prefix_compat: - forall T1 T2 T1' T2', - traceinf_prefix T1 T2 -> traceinf_sim T1 T1' -> traceinf_sim T2 T2' -> - traceinf_prefix T1' T2'. -Proof. - cofix COINDHYP; intros. - inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto. -Qed. - -Transparent trace E0 Eapp Eappinf. -*) - Lemma traceinf_prefix_app: forall t1 T2 t, traceinf_prefix t1 T2 -> @@ -284,3 +271,53 @@ Proof. constructor. auto. Qed. +(** An alternate presentation of infinite traces as + infinite concatenations of nonempty finite traces. *) + +CoInductive traceinf': Type := + | Econsinf': forall (t: trace) (T: traceinf'), t <> E0 -> traceinf'. + +Program Definition split_traceinf' (t: trace) (T: traceinf') (NE: t <> E0): event * traceinf' := + match t with + | nil => _ + | e :: nil => (e, T) + | e :: t' => (e, Econsinf' t' T _) + end. +Next Obligation. + elimtype False. elim NE. auto. +Qed. +Next Obligation. + red; intro. elim (H e). rewrite H0. auto. +Qed. + +CoFixpoint traceinf_of_traceinf' (T': traceinf') : traceinf := + match T' with + | Econsinf' t T'' NOTEMPTY => + let (e, tl) := split_traceinf' t T'' NOTEMPTY in + Econsinf e (traceinf_of_traceinf' tl) + end. + +Remark unroll_traceinf': + forall T, T = match T with Econsinf' t T' NE => Econsinf' t T' NE end. +Proof. + intros. destruct T; auto. +Qed. + +Remark unroll_traceinf: + forall T, T = match T with Econsinf t T' => Econsinf t T' end. +Proof. + intros. destruct T; auto. +Qed. + +Lemma traceinf_traceinf'_app: + forall t T NE, + traceinf_of_traceinf' (Econsinf' t T NE) = t *** traceinf_of_traceinf' T. +Proof. + induction t. + intros. elim NE. auto. + intros. simpl. + rewrite (unroll_traceinf (traceinf_of_traceinf' (Econsinf' (a :: t) T NE))). + simpl. destruct t. auto. +Transparent Eappinf. + simpl. f_equal. apply IHt. +Qed. diff --git a/common/Smallstep.v b/common/Smallstep.v index deab49b..cd61ec3 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -21,7 +21,6 @@ Require Import Wf. Require Import Wf_nat. -Require Import Classical. Require Import Coqlib. Require Import AST. Require Import Events. @@ -680,6 +679,132 @@ End SIMULATION_OPT. End SIMULATION. +(** * Existence of behaviors *) + +Require Import Classical. +Require Import ClassicalEpsilon. + +(** 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. *) + +Section EXISTS_BEHAVIOR. + +Variable genv: Type. +Variable state: Type. +Variable initial_state: state -> Prop. +Variable final_state: state -> int -> Prop. +Variable step: genv -> state -> trace -> state -> Prop. + +(** 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 ge: genv. +Variable s0: state. + +Hypothesis reacts: + forall s1 t1, star step ge s0 t1 s1 -> + exists s2, exists t2, star step ge s1 t2 s2 /\ t2 <> E0. + +Lemma reacts': + forall s1 t1, star step ge s0 t1 s1 -> + { s2 : state & { t2 : trace | star step ge 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) (t1: trace) (ST: star step ge 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 step ge s0 t1 s1), + forever_reactive step ge 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 step ge s0 T. +Proof. + exists (traceinf_of_traceinf' (build_traceinf' (star_refl step ge s0))). + apply reacts_forever_reactive_rec. +Qed. + +End TRACEINF_REACTS. + +Lemma diverges_forever_silent: + forall ge s0, + (forall s1 t1, star step ge s0 t1 s1 -> exists s2, step ge s1 E0 s2) -> + forever_silent step ge 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. + +Theorem program_behaves_exists: + forall ge, exists beh, program_behaves step initial_state final_state ge beh. +Proof. + intros. + destruct (classic (exists s, initial_state s)) as [[s0 INIT] | NOTINIT]. +(* 1. Initial state is defined. *) + destruct (classic (forall s1 t1, star step ge s0 t1 s1 -> exists s2, exists t2, step ge s1 t2 s2)). +(* 1.1 Divergence (silent or reactive) *) + destruct (classic (exists s1, exists t1, star step ge s0 t1 s1 /\ + (forall s2 t2, star step ge s1 t2 s2 -> + exists s3, step ge s2 E0 s3))). +(* 1.1.1 Silent divergence *) + destruct H0 as [s1 [t1 [A B]]]. + exists (Diverges t1); econstructor; eauto. + apply diverges_forever_silent; auto. +(* 1.1.2 Reactive divergence *) + destruct (@reacts_forever_reactive ge 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. +(* 1.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 s1 r)) as [[r FINAL] | NOTFINAL]. +(* 1.2.1 Normal termination *) + exists (Terminates t1 r); econstructor; eauto. +(* 1.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. +(* 2. Initial state is undefined *) + exists (Goes_wrong E0). apply program_goes_initially_wrong. + intros. eapply not_ex_all_not; eauto. +Qed. + +End EXISTS_BEHAVIOR. + (** * Additional results about infinite reduction sequences *) (** We now show that any infinite sequence of reductions is either of @@ -689,7 +814,6 @@ End SIMULATION. relate the coinductive big-step semantics for divergence with the small-step notions of divergence. *) -Require Import Classical. Unset Implicit Arguments. Section INF_SEQ_DECOMP. -- cgit v1.2.3