Local soundness with syncing.

ConcurrentLambda.v

@@ -2279,8 +2279,8 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
 
   Inductive IsAllowChoiceLabel : Label -> Prop :=
     IsAllowChoiceLabelBase : forall l d, IsAllowChoiceLabel (AllowChoiceLabel l d)
-  | FunAllowChoiceLable : forall L, IsAllowChoiceLabel L -> IsAllowChoiceLabel (FunLabel L)
-  | ArgAllowChoiceLable : forall L, IsAllowChoiceLabel L -> IsAllowChoiceLabel (ArgLabel L).
+  | FunAllowChoiceLabel : forall L, IsAllowChoiceLabel L -> IsAllowChoiceLabel (FunLabel L)
+  | ArgAllowChoiceLabel : forall L, IsAllowChoiceLabel L -> IsAllowChoiceLabel (ArgLabel L).
 
   Lemma UnmergeRelStep' : forall E11 E12 E1 R E2,
       ConExprStep' E1 R E2 ->
@@ -2349,6 +2349,171 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
       eexists; eexists; split; [|split]; eauto with ConExpr; eapply MergeRelDiag.
   Qed.
 
+  Inductive AllowDirectedChoiceLabel : LRChoice -> Label -> Prop :=
+    AllowDirectedChoiceLabelBase : forall l d, AllowDirectedChoiceLabel d (AllowChoiceLabel l d)
+  | FunAllowDirectedChoice : forall d L,
+      AllowDirectedChoiceLabel d L -> AllowDirectedChoiceLabel d (FunLabel L)
+  | ArgAllowDirectedChoice : forall d L,
+      AllowDirectedChoiceLabel d L -> AllowDirectedChoiceLabel d (ArgLabel L).
+  Global Hint Constructors AllowDirectedChoiceLabel IsAllowChoiceLabel : ConExpr.
+
+  Lemma ChoiceLabelToDirected : forall L,
+      IsAllowChoiceLabel L -> exists d, AllowDirectedChoiceLabel d L.
+  Proof using.
+    intros L alc; induction alc; try (eexists; econstructor; eauto; fail).
+    all: destruct IHalc as [d IHalc]; try (eexists; econstructor; eauto; fail).
+  Qed.
+
+  Lemma DirectedChoiceToLabel : forall d L,
+      AllowDirectedChoiceLabel d L -> IsAllowChoiceLabel L.
+  Proof using.
+    intros d L adcl; induction adcl; constructor; auto.
+  Qed.
+
+  Inductive SameChoiceRedexShape : ConExprRedex -> ConExprRedex -> Prop :=
+    SameShapeLL : forall l,
+      SameChoiceRedexShape (AllowChoiceLRedex l) (AllowChoiceLRedex l)
+  | SameShapeLR : forall l,
+      SameChoiceRedexShape (AllowChoiceLRedex l) (AllowChoiceRRedex l)
+  | SameShapeRL : forall l,
+      SameChoiceRedexShape (AllowChoiceRRedex l) (AllowChoiceLRedex l)
+  | SameShapeRR : forall l,
+      SameChoiceRedexShape (AllowChoiceRRedex l) (AllowChoiceRRedex l)
+  | SameShapeFun : forall R1 R2,
+      SameChoiceRedexShape R1 R2 -> SameChoiceRedexShape (FunRedex R1) (FunRedex R2)
+  | SameChoiceRedexShapeArg : forall R1 R2,
+      SameChoiceRedexShape R1 R2 -> SameChoiceRedexShape (ArgRedex R1) (ArgRedex R2).
+  Global Hint Constructors SameChoiceRedexShape : ConExpr.
+
+  Lemma SameChoiceRedexShapeRefl : forall R,
+      IsAllowChoiceLabel (ConExprRedexToLabel R) ->
+      SameChoiceRedexShape R R.
+  Proof using.
+    intros R; induction R; intros iacl; inversion iacl; subst; constructor; auto.
+  Qed.
+
+  Lemma SameChoiceRedexShapeSym : forall R1 R2,
+      SameChoiceRedexShape R1 R2 -> SameChoiceRedexShape R2 R1.
+  Proof using.
+    intros R1 R2 scrs1; induction scrs1; constructor; auto.
+  Qed.
+
+  Lemma SameChoiceRedexShapeTrans : forall R1 R2 R3,
+      SameChoiceRedexShape R1 R2 -> SameChoiceRedexShape R2 R3 -> SameChoiceRedexShape R1 R3.
+  Proof using.
+    intros R1 R2 R3 scrs1; revert R3; induction scrs1; intros R3 scrs2;
+      inversion scrs2; subst; try (constructor; auto; fail).
+  Qed.
+
+  Global Hint Resolve SameChoiceRedexShapeRefl SameChoiceRedexShapeSym SameChoiceRedexShapeTrans : ConExpr.
+
+  Lemma SameShapeSameDirection : forall d R1 R2,
+      SameChoiceRedexShape R1 R2 ->
+      AllowDirectedChoiceLabel d (ConExprRedexToLabel R1) ->
+      AllowDirectedChoiceLabel d (ConExprRedexToLabel R2) ->
+      R1 = R2.
+  Proof using.
+    intros d R1 R2 scrs; revert d; induction scrs; cbn; intros d adcl1 adcl2;
+      inversion adcl1; inversion adcl2; subst; try discriminate; auto.
+    all: erewrite IHscrs; eauto.
+  Qed.
+  
+  Lemma UnmergeRelACStep' : forall E11 E12 E1 d R E2,
+      AllowDirectedChoiceLabel d (ConExprRedexToLabel R) ->
+      ConExprStep' E1 R E2 ->
+      ConExprMergeRel E11 E12 E1 ->
+      exists d1 R1 E21 d2 R2 E22,
+        ConExprStep' E11 R1 E21 /\
+        ConExprStep' E12 R2 E22 /\
+        SameChoiceRedexShape R1 R /\
+        SameChoiceRedexShape R2 R /\
+        AllowDirectedChoiceLabel d1 (ConExprRedexToLabel R1) /\
+        AllowDirectedChoiceLabel d2 (ConExprRedexToLabel R2) /\
+        ((d1 = d /\ d2 = d /\ ConExprMergeRel E21 E22 E2) \/
+         (d1 = d /\ d2 <> d) \/
+         (d1 <> d /\ d2 = d)).
+  Proof using.
+    intros E11 E12 E1 d R E2 adcl step;
+      revert E11 E12 d adcl; induction step;
+        intros E11 E12 d adcl merge; inversion adcl; subst; inversion merge; subst;
+          cbn in *.
+      all: try match goal with
+      | [IH : forall E11 E12 d,
+            AllowDirectedChoiceLabel d (ConExprRedexToLabel ?R) ->
+            ConExprMergeRel E11 E12 ?E1 ->
+            exists d1 R1 E21 d2 R2 E22,
+              ConExprStep' E11 R1 E21 /\
+              ConExprStep' E12 R2 E22 /\
+              SameChoiceRedexShape R1 ?R /\
+              SameChoiceRedexShape R2 ?R /\
+              AllowDirectedChoiceLabel d1 (ConExprRedexToLabel R1) /\
+              AllowDirectedChoiceLabel d2 (ConExprRedexToLabel R2) /\
+              ((d1 = d /\ d2 = d /\ ConExprMergeRel E21 E22 ?E2) \/
+               (d1 = d /\ d2 <> d) \/
+               (d1 <> d /\ d2 = d)),
+           H1 : AllowDirectedChoiceLabel ?d (ConExprRedexToLabel ?R),
+           H2 : ConExprMergeRel ?E11 ?E12 ?E1 |- _ ] =>
+        let d1 := fresh "d" in
+        let R1 := fresh "R" in
+        let E21 := fresh "E2" in
+        let d2 := fresh "d" in
+        let R2 := fresh "R" in
+        let E22 := fresh "E2" in
+        let step1 := fresh "step" in
+        let step2 := fresh "step" in
+        let scrs1 := fresh "scrs" in
+        let scrs2 := fresh "scrs" in
+        let adcl1 := fresh "adcl" in
+        let adcl2 := fresh "adcl" in
+        let eq1 := fresh "eq" in
+        let eq2 := fresh "eq" in
+        let neq := fresh "neq" in
+        let merge := fresh "merge" in
+        destruct (IH E11 E12 d)
+          as [d1 [R1 [E21 [d2 [R2 [E22 [step1 [step2 [scrs1 [scrs2 [adcl1 [adcl2 [[eq1 [eq2 merge]] | [[eq1 neq] | [eq1 neq]]]]]]]]]]]]]]]; subst; clear IH
+      end; auto with ConExpr.
+
+    all: try (eexists; eexists; eexists; eexists; eexists; eexists;
+              repeat match goal with |[|- _ /\ _ ] => split end; repeat (cbn; eauto with ConExpr); fail).
+
+    Ltac UnmergeRelACStep'Branch d1 d2 l :=
+      match d1 with
+      | LChoice =>
+          match d2 with
+            | LChoice => exists d1; exists (AllowChoiceLRedex l); eexists;
+                        exists d2; exists (AllowChoiceLRedex l); eexists
+            | RChoice => exists d1; exists (AllowChoiceLRedex l); eexists;
+                        exists d2; exists (AllowChoiceRRedex l); eexists
+          end
+      | RChoice =>
+        match d2 with
+        | LChoice => exists d1; exists (AllowChoiceRRedex l); eexists;
+                    exists d2; exists (AllowChoiceLRedex l); eexists
+        | RChoice => exists d1; exists (AllowChoiceRRedex l); eexists;
+                    exists d2; exists (AllowChoiceRRedex l); eexists
+        end
+      end; repeat match goal with |[|- _ /\ _ ] => split end; repeat (cbn; eauto with ConExpr).
+    - UnmergeRelACStep'Branch LChoice RChoice l. 
+      right; left; split; auto; discriminate. 
+    - UnmergeRelACStep'Branch LChoice LChoice l.
+    - UnmergeRelACStep'Branch RChoice LChoice l.
+      right; right; split; auto. intro eq; inversion eq.
+    - UnmergeRelACStep'Branch RChoice LChoice l.
+      right; right; split; auto. discriminate.
+    - UnmergeRelACStep'Branch LChoice LChoice l.
+    - UnmergeRelACStep'Branch LChoice RChoice l.
+      right; left; split; auto; discriminate.
+    - UnmergeRelACStep'Branch LChoice LChoice l.
+    - UnmergeRelACStep'Branch LChoice RChoice l.
+      right; right; split; auto; discriminate.
+    - UnmergeRelACStep'Branch LChoice RChoice l.
+      right; right; split; auto; discriminate.
+    - UnmergeRelACStep'Branch RChoice LChoice l.
+      right; left; split; auto; discriminate.
+    - UnmergeRelACStep'Branch RChoice LChoice l.
+      right; left; split; auto; discriminate.
+  Qed.
+
   Lemma UnmergeRelStep : forall E11 E12 E1 L E2,
       ConExprStep E1 L E2 ->
       ~ IsAllowChoiceLabel L ->