Added concurrent lambda and proved (one direction of) simulation.

Choreography.v

@@ -1088,8 +1088,8 @@ Module Choreography (Import E : Expression) (L : Locations).
 
   Definition AppGlobalSubst (C1 C2 : Chor) : nat -> Chor :=
     fun n => match n with
-          | 0 => RecGlobal C1
-          | 1 => C2
+          | 0 => C2
+          | 1 => RecGlobal C1
           | S (S m) => Var m
           end.
 
@@ -1396,7 +1396,7 @@ Module Choreography (Import E : Expression) (L : Locations).
   | CAppLocalArgStep : forall (l : Loc) (C : Chor) (e1 e2 : Expr) B,
       ~ In l B ->
       ExprStep e1 e2 ->
-      ChorStep (RAppLocalE l e1 e2) B (AppLocal l C e1) (AppLocal l C e2)
+      ChorStep (RAppLocalE l e1 e2) B (AppLocal l (RecLocal l C) e1) (AppLocal l (RecLocal l C) e2)
   | CAppLocalStep : forall (l : Loc) (C : Chor) (v : Expr),
       ExprVal v ->
       ChorStep (RAppLocal l v) [] (AppLocal l (RecLocal l C) v)
@@ -1406,7 +1406,7 @@ Module Choreography (Import E : Expression) (L : Locations).
       ChorStep R B (AppGlobal C1 C2) (AppGlobal C1' C2)
   | CAppGlobalArgStep : forall (C1 C2 C2' : Chor) R B,
       ChorStep R B C2 C2' ->
-      ChorStep R B (AppGlobal C1 C2) (AppGlobal C1 C2')
+      ChorStep R B (AppGlobal (RecGlobal C1) C2) (AppGlobal (RecGlobal C1) C2')
   | CAppGlobalStep : forall (C1 C2 : Chor),
       ChorVal C2 ->
       ChorStep RAppGlobal [] (AppGlobal (RecGlobal C1) C2)

Expression.v

@@ -73,6 +73,8 @@ Module Type Expression.
   Parameter tt ff : Expr.
   Parameter ttValue : ExprVal tt.
   Parameter ffValue : ExprVal ff.
+  Parameter boolSeperation : tt <> ff.
   
   Parameter ExprStep : Expr -> Expr -> Prop.
+  Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
 End Expression.

LambdaCalc.v

@@ -290,4 +290,14 @@ Module LambdaCalc <: Expression.
                 end; eauto.
     apply Lt.lt_le_S in l. apply Lt.le_lt_or_eq in l; destruct l; subst; eauto.
   Qed.
+
+  Theorem NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
+  Proof using.
+    intros v; induction v; intros val_v e step; inversion val_v; subst;
+      inversion step; subst.
+    apply (IHv H0 e2 H1).
+  Qed.
+
+  Theorem boolSeperation : tt <> ff. discriminate. Qed.
+
 End LambdaCalc.

TypedChoreography.v

@@ -74,8 +74,8 @@ Module TypedChoreography (L : Locations) (E : Expression) (TE : TypedExpression
   | TRecGlobal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
                  (C : Chor) (τ σ : ChorTyp),
       Γ;; (fun n => match n with
-                 | 0 => ChorFun τ σ
-                 | 1 => τ
+                 | 0 => τ
+                 | 1 => ChorFun τ σ
                  | S (S n) => Δ n
                  end) ⊢c C ::: σ
       -> Γ;; Δ ⊢c RecGlobal C ::: ChorFun τ σ
@@ -251,7 +251,7 @@ Module TypedChoreography (L : Locations) (E : Expression) (TE : TypedExpression
       destruct n; [apply TVar|].
       destruct n; [apply TVar|].
       apply TypeChorWeakening with (Δ1 := fun m => match m with
-                                               | 0 => τ
+                                               | 0 => ChorFun τ ρ
                                                | S m => Δ2 m
                                                end); auto.
       apply TypeChorWeakening with (Δ1 := Δ2); auto.
@@ -295,20 +295,20 @@ Module TypedChoreography (L : Locations) (E : Expression) (TE : TypedExpression
 
   Lemma AppGlobalSubstTyping : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ σ : ChorTyp) (C1 C2 : Chor),
       Γ;; (fun n => match n with
-                | 0 => ChorFun τ σ
-                | 1 => τ
+                | 0 => τ
+                | 1 => ChorFun τ σ
                 | S (S n) => Δ n
                 end) ⊢c C1 ::: σ ->
       Γ;; Δ ⊢c C2 ::: τ ->
       ChorSubstTyping Γ (fun n => match n with
-                               | 0 => ChorFun τ σ
-                               | 1 => τ
+                               | 0 => τ
+                               | 1 => ChorFun τ σ
                                | S (S n) => Δ n
                                end) (AppGlobalSubst C1 C2) Δ.
   Proof using.
     intros Γ Δ τ σ C1 C2 typing1 typing2; unfold ChorSubstTyping; unfold AppGlobalSubst;
-      intro n; destruct n; [| destruct n]; auto; [|apply TVar].
-    apply TRecGlobal; auto.
+      intro n; destruct n; [| destruct n]; auto; [| apply TVar].
+    apply TRecGlobal; auto. 
   Qed.
     
   Theorem ChorEquivTyping : forall (C1 C2 : Chor),