From 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jul 2008 12:04:42 +0000 Subject: Fusion partielle de la branche contsem: - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Smallstep.v | 177 +++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 123 insertions(+), 54 deletions(-) (limited to 'common/Smallstep.v') diff --git a/common/Smallstep.v b/common/Smallstep.v index ec7a416..a2634be 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -19,6 +19,8 @@ the one-step transition relations that are used to specify operational semantics in small-step style. *) +Require Import Wf. +Require Import Wf_nat. Require Import Coqlib. Require Import AST. Require Import Events. @@ -157,7 +159,8 @@ Proof. Qed. Lemma plus_inv: - forall ge s1 t s2, plus ge s1 t s2 -> + forall ge s1 t s2, + plus ge s1 t s2 -> step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. Proof. intros. inversion H; subst. inversion H1; subst. @@ -166,6 +169,14 @@ Proof. split. econstructor; eauto. auto. Qed. +Lemma star_inv: + forall ge s1 t s2, + star ge s1 t s2 -> + (s2 = s1 /\ t = E0) \/ plus ge s1 t s2. +Proof. + intros. inv H. left; auto. right; econstructor; eauto. +Qed. + (** Infinitely many transitions *) CoInductive forever (ge: genv): state -> traceinf -> Prop := @@ -186,61 +197,86 @@ Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) -CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop := - | forever_N_star: forall s1 t s2 p q T1 T2, +Variable A: Set. +Variable order: A -> A -> Prop. + +CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := + | forever_N_star: forall s1 t s2 a1 a2 T1 T2, star ge s1 t s2 -> - (p < q)%nat -> - forever_N ge p s2 T2 -> + order a2 a1 -> + forever_N ge a2 s2 T2 -> T1 = t *** T2 -> - forever_N ge q s1 T1 - | forever_N_plus: forall s1 t s2 p q T1 T2, + forever_N ge a1 s1 T1 + | forever_N_plus: forall s1 t s2 a1 a2 T1 T2, plus ge s1 t s2 -> - forever_N ge p s2 T2 -> + forever_N ge a2 s2 T2 -> T1 = t *** T2 -> - forever_N ge q s1 T1. + forever_N ge a1 s1 T1. -Remark Peano_induction: - forall (P: nat -> Prop), - (forall p, (forall q, (q < p)%nat -> P q) -> P p) -> - forall p, P p. -Proof. - intros P IH. - assert (forall p, forall q, (q < p)%nat -> P q). - induction p; intros. elimtype False; omega. - apply IH. intros. apply IHp. omega. - intro. apply H with (S p). omega. -Qed. +Hypothesis order_wf: well_founded order. Lemma forever_N_inv: - forall ge p s T, - forever_N ge p s T -> - exists t, exists s', exists q, exists T', - step ge s t s' /\ forever_N ge q s' T' /\ T = t *** T'. + forall ge a s T, + forever_N ge a s T -> + exists t, exists s', exists a', exists T', + step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'. Proof. - intros ge p. pattern p. apply Peano_induction; intros. - inv H0. + intros ge a0. pattern a0. apply (well_founded_ind order_wf). + intros. inv H0. (* star case *) inv H1. (* no transition *) - change (E0 *** T2) with T2. apply H with p1. auto. auto. + change (E0 *** T2) with T2. apply H with a2. auto. auto. (* at least one transition *) - exists t1; exists s0; exists p0; exists (t2 *** T2). + exists t1; exists s0; exists x; exists (t2 *** T2). split. auto. split. eapply forever_N_star; eauto. apply Eappinf_assoc. (* plus case *) inv H1. - exists t1; exists s0; exists (S p1); exists (t2 *** T2). - split. auto. split. eapply forever_N_star; eauto. + exists t1; exists s0; exists a2; exists (t2 *** T2). + split. auto. + split. inv H3. auto. + eapply forever_N_plus. econstructor; eauto. eauto. auto. apply Eappinf_assoc. Qed. Lemma forever_N_forever: - forall ge p s T, forever_N ge p s T -> forever ge s T. + forall ge a s T, forever_N ge a s T -> forever ge s T. Proof. cofix COINDHYP; intros. - destruct (forever_N_inv H) as [t [s' [q [T' [A [B C]]]]]]. - rewrite C. apply forever_intro with s'. auto. - apply COINDHYP with q; auto. + destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]]. + rewrite R. apply forever_intro with s'. auto. + apply COINDHYP with a'; auto. +Qed. + +(** Yet another alternative definition of [forever]. *) + +CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop := + | forever_plus_intro: forall s1 t s2 T1 T2, + plus ge s1 t s2 -> + forever_plus ge s2 T2 -> + T1 = t *** T2 -> + forever_plus ge s1 T1. + +Lemma forever_plus_inv: + forall ge s T, + forever_plus ge s T -> + exists s', exists t, exists T', + step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'. +Proof. + intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2). + split. auto. + split. exploit star_inv; eauto. intros [[P Q] | R]. + subst. simpl. auto. econstructor; eauto. + traceEq. +Qed. + +Lemma forever_plus_forever: + forall ge s T, forever_plus ge s T -> forever ge s T. +Proof. + cofix COINDHYP; intros. + destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]]. + subst. econstructor; eauto. Qed. (** * Outcomes for program executions *) @@ -329,19 +365,21 @@ Hypothesis match_final_states: in the source program must correspond to infinitely many transitions in the second program. *) -Section SIMULATION_STAR. +Section SIMULATION_STAR_WF. -(** [measure] is a nonnegative integer associated with states - of the first semantics. It must decrease when we take - a stuttering step. *) +(** [order] is a well-founded ordering associated with states + of the first semantics. Stuttering steps must correspond + to states that decrease w.r.t. [order]. *) -Variable measure: state1 -> nat. +Variable order: state1 -> state1 -> Prop. +Hypothesis order_wf: well_founded order. Hypothesis simulation: forall st1 t st1', step1 ge1 st1 t st1' -> forall st2, match_states st1 st2 -> - (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') - \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + exists st2', + (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1)) + /\ match_states st1' st2'. Lemma simulation_star_star: forall st1 t st1', star step1 ge1 st1 t st1' -> @@ -350,12 +388,13 @@ Lemma simulation_star_star: Proof. induction 1; intros. exists st2; split. apply star_refl. auto. - elim (simulation H H2). - intros [st2' [A B]]. + destruct (simulation H H2) as [st2' [A B]]. destruct (IHstar _ B) as [st3' [C D]]. - exists st3'; split. apply star_trans with t1 st2' t2. - apply plus_star; auto. auto. auto. auto. - intros [A [B C]]. rewrite H1. rewrite B. simpl. apply IHstar; auto. + exists st3'; split; auto. + apply star_trans with t1 st2' t2; auto. + destruct A as [F | [F G]]. + apply plus_star; auto. + auto. Qed. Lemma simulation_star_forever: @@ -365,19 +404,19 @@ Lemma simulation_star_forever: Proof. assert (forall st1 st2 T, forever step1 ge1 st1 T -> match_states st1 st2 -> - forever_N step2 ge2 (measure st1) st2 T). + forever_N step2 order ge2 st1 st2 T). cofix COINDHYP; intros. - inversion H; subst. elim (simulation H1 H0). - intros [st2' [A B]]. apply forever_N_plus with t st2' (measure s2) T0. + inversion H; subst. + destruct (simulation H1 H0) as [st2' [A B]]. + destruct A as [C | [C D]]. + apply forever_N_plus with t st2' s2 T0. auto. apply COINDHYP. assumption. assumption. auto. - intros [A [B C]]. - apply forever_N_star with t st2 (measure s2) T0. - rewrite B. apply star_refl. auto. - apply COINDHYP. assumption. auto. auto. + apply forever_N_star with t st2' s2 T0. + auto. auto. apply COINDHYP. assumption. auto. auto. intros. eapply forever_N_forever; eauto. Qed. -Lemma simulation_star_preservation: +Lemma simulation_star_wf_preservation: forall beh, program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. @@ -391,6 +430,36 @@ Proof. eapply simulation_star_forever; eauto. Qed. +End SIMULATION_STAR_WF. + +Section SIMULATION_STAR. + +(** We now consider the case where we have a nonnegative integer measure + associated with states of the first semantics. It must decrease when we take + a stuttering step. *) + +Variable measure: state1 -> nat. + +Hypothesis simulation: + forall st1 t st1', step1 ge1 st1 t st1' -> + forall st2, match_states st1 st2 -> + (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') + \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. + +Lemma simulation_star_preservation: + forall beh, + program_behaves step1 initial_state1 final_state1 ge1 beh -> + program_behaves step2 initial_state2 final_state2 ge2 beh. +Proof. + intros. + apply simulation_star_wf_preservation with (ltof _ measure). + apply well_founded_ltof. intros. + destruct (simulation H0 H1) as [[st2' [A B]] | [A [B C]]]. + exists st2'; auto. + exists st2; split. right; split. rewrite B. apply star_refl. auto. auto. + auto. +Qed. + End SIMULATION_STAR. (** Lock-step simulation: each transition in the first semantics -- cgit v1.2.3