diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
| commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
| tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /common/Events.v | |
| parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
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
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 10 |
1 files changed, 7 insertions, 3 deletions
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, |