From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 28 Aug 2007 12:57:58 +0000 Subject: Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index 83a7a19..e9070e1 100644 --- a/common/Events.v +++ b/common/Events.v @@ -66,14 +66,18 @@ Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed. Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3). Proof. intros. unfold Eapp, trace. apply app_ass. Qed. +Lemma E0_left_inf: forall T, E0 *** T = T. +Proof. auto. Qed. + Lemma Eappinf_assoc: forall t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T). Proof. induction t1; intros; simpl. auto. decEq; auto. Qed. -Hint Rewrite E0_left E0_right Eapp_assoc: trace_rewrite. +Hint Rewrite E0_left E0_right Eapp_assoc + E0_left_inf Eappinf_assoc: trace_rewrite. -Opaque trace E0 Eextcall Eapp. +Opaque trace E0 Eextcall Eapp Eappinf. (** The following [traceEq] tactic proves equalities between traces or infinite traces. *) @@ -251,7 +255,7 @@ Proof. inv H; inv H0; inv H1; constructor; eapply COINDHYP; eauto. Qed. -Transparent trace E0 Eapp. +Transparent trace E0 Eapp Eappinf. Lemma traceinf_prefix_app: forall T1 T2 t, -- cgit v1.2.3