From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 18 Aug 2010 09:06:55 +0000
Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has
 side-effects within expressions,   performs implicit casts, and has
 nondeterministic reduction semantics   for expressions - Cstrategy:
 deterministic red. sem. for the above - Clight: the previous source C
 language, with pure expressions.   Added: temporary variables + implicit
 casts. - New pass SimplExpr to pull side-effects out of expressions  
 (previously done in untrusted Caml code in cparser/) - Csharpminor: added
 temporary variables to match Clight. - Cminorgen: adapted, removed cast
 optimization (moved to back-end) - CastOptim: RTL-level optimization of casts
 - cparser: transformations Bitfields, StructByValue and StructAssign   now
 work on non-simplified expressions - Added pretty-printers for several
 intermediate languages,   and matching -dxxx command-line flags.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Smallstep.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

(limited to 'common/Smallstep.v')

diff --git a/common/Smallstep.v b/common/Smallstep.v
index cd61ec3..63426c1 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -66,6 +66,31 @@ Proof.
   intros. eapply star_step; eauto. apply star_refl. traceEq. 
 Qed.
 
+Lemma star_two:
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  star ge s1 t s3.
+Proof.
+  intros. eapply star_step; eauto. apply star_one; auto.  
+Qed.
+
+Lemma star_three:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  star ge s1 t s4.
+Proof.
+  intros. eapply star_step; eauto. eapply star_two; eauto. 
+Qed.
+
+Lemma star_four:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
+  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  star ge s1 t s5.
+Proof.
+  intros. eapply star_step; eauto. eapply star_three; eauto. 
+Qed.
+
 Lemma star_trans:
   forall ge s1 t1 s2, star ge s1 t1 s2 ->
   forall t2 s3 t, star ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3.
@@ -103,6 +128,31 @@ Proof.
   intros. econstructor; eauto. apply star_refl. traceEq.
 Qed.
 
+Lemma plus_two:
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  plus ge s1 t s3.
+Proof.
+  intros. eapply plus_left; eauto. apply star_one; auto.  
+Qed.
+
+Lemma plus_three:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  plus ge s1 t s4.
+Proof.
+  intros. eapply plus_left; eauto. eapply star_two; eauto. 
+Qed.
+
+Lemma plus_four:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
+  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  plus ge s1 t s5.
+Proof.
+  intros. eapply plus_left; eauto. eapply star_three; eauto. 
+Qed.
+
 Lemma plus_star:
   forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2.
 Proof.
-- 
cgit v1.2.3