Ajout de common/Complements.v

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 10 insertions, 0 deletions

diff --git a/common/Smallstep.v b/common/Smallstep.v
index 7f6c776..f60746d 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -158,6 +158,16 @@ CoInductive forever (ge: genv): state -> traceinf -> Prop :=
       step ge s1 t s2 -> forever ge s2 T ->
       forever ge s1 (t *** T).
 
+Lemma star_forever:
+  forall ge s1 t s2, star ge s1 t s2 ->
+  forall T, forever ge s2 T ->
+  forever ge s1 (t *** T).
+Proof.
+  induction 1; intros. simpl. auto.
+  subst t. rewrite Eappinf_assoc. 
+  econstructor; eauto.
+Qed.  
+
 (** An alternate, equivalent definition of [forever] that is useful
     for coinductive reasoning. *)