Commit c1e752b1 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Local Soundness up to a few conditions and caveats.

First, only for tau steps.

Secondly, this currently doesn't take care of argument steps very
well. Essentially, the problem is that a single location can start
working on an argument (because to it, it looks like the function is
done),
while the function is not finished computing at the choreography
level.

I think to fix this, we'll need to change the compiler and possibly
the target language again.
parent a999d36c
......@@ -1668,4 +1668,394 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
exists El2; split; auto.
Qed.
Lemma TauUnique : forall R, RedexToSystemLabel R = SysTau ->
exists l, ProjectRedex R l = Some Tau /\
forall l', l <> l' -> ProjectRedex R l' = None.
Proof using.
intros R eq; destruct R; cbn in eq; try discriminate; cbn.
all: exists l; destruct (L.eq_dec l l) as [_|n]; [| destruct (n eq_refl)]; split; auto.
all: intros l' neq; destruct (L.eq_dec l' l) as [ eq'|_];
[destruct (neq (eq_sym eq'))|]; reflexivity.
Qed.
Inductive CompatibleRedices (l : Loc) : ConExprRedex -> C.Redex -> Prop :=
| RetCompat : forall e1 e2, CompatibleRedices l (RetE e1 e2) (C.RDone l e1 e2)
| IfECompat : forall e1 e2, CompatibleRedices l (IfE e1 e2) (C.RIfE l e1 e2)
| IfTTCompat : CompatibleRedices l IfTT (C.RIfTT l)
| IfFFCompat : CompatibleRedices l IfFF (C.RIfFF l)
| SendECompat : forall l' e1 e2,
l <> l' -> CompatibleRedices l (SendE l' e1 e2) (C.RSendE l e1 e2 l')
| SendVCompat : forall l' v,
l <> l' -> CompatibleRedices l (SendV l' v) (C.RSendV l v l')
| RecvCompat : forall l' v,
l <> l' -> CompatibleRedices l (RecvV l' v) (C.RSendV l' v l)
| ChooseCompat : forall l' d,
l <> l' -> CompatibleRedices l (ChooseRedex l' d) (C.RSync l d l')
| ChoiceLCompat : forall l',
l <> l' -> CompatibleRedices l (AllowChoiceLRedex l') (C.RSync l' C.LChoice l)
| ChoiceRCompat : forall l',
l <> l' -> CompatibleRedices l (AllowChoiceRRedex l') (C.RSync l' C.RChoice l)
| LetRetCompat : forall v, CompatibleRedices l (LetRetRedex v) (C.RDefLocal l v)
| AppLocalECompat : forall e1 e2, CompatibleRedices l (AppLocalE e1 e2) (C.RAppLocalE l e1 e2)
| AppLocalCompat : forall v, CompatibleRedices l (AppLocalRedex v) (C.RAppLocal l v)
| AppGlobalDefCompat : forall l' v,
l <> l' -> CompatibleRedices l AppGlobalRedex (C.RDefLocal l' v)
| AppGlobalLocCompat : forall l' v,
l <> l' -> CompatibleRedices l AppGlobalRedex (C.RAppLocal l' v)
| AppGlobalCompat : CompatibleRedices l AppGlobalRedex C.RAppGlobal.
Definition ProjectRedexToRedex (R : C.Redex) (l : Loc) : option ConExprRedex :=
match R with
| C.RDone l' e1 e2 =>
if L.eq_dec l l'
then Some (RetE e1 e2)
else None
| C.RIfE l' e1 e2 =>
if L.eq_dec l l'
then Some (IfE e1 e2)
else None
| C.RIfTT l' =>
if L.eq_dec l l'
then Some IfTT
else None
| C.RIfFF l' =>
if L.eq_dec l l'
then Some IfFF
else None
| C.RSendE l' e1 e2 l'' =>
if L.eq_dec l l'
then if L.eq_dec l l''
then None
else Some (SendE l'' e1 e2)
else None
| C.RSendV l' v l'' =>
if L.eq_dec l l'
then if L.eq_dec l l''
then None
else Some (SendV l'' v)
else if L.eq_dec l l''
then Some (RecvV l' v)
else None
| C.RSync l' d l'' =>
if L.eq_dec l l'
then if L.eq_dec l l''
then None
else Some (ChooseRedex l'' d)
else if L.eq_dec l l''
then match d with
| C.LChoice => Some (AllowChoiceLRedex l')
| C.RChoice => Some (AllowChoiceRRedex l')
end
else None
| C.RDefLocal l' v =>
if L.eq_dec l l'
then Some (LetRetRedex v)
else Some AppGlobalRedex
| C.RAppLocalE l' e1 e2 =>
if L.eq_dec l l'
then Some (AppLocalE e1 e2)
else None
| C.RAppLocal l' v =>
if L.eq_dec l l'
then Some (AppLocalRedex v)
else Some AppGlobalRedex
| C.RAppGlobal => Some AppGlobalRedex
end.
Lemma ProjectCompat : forall {l R1 R2},
ProjectRedexToRedex R1 l = Some R2 ->
CompatibleRedices l R2 R1.
Proof using.
intros l R1 R2; destruct R1; cbn; intro eq;
repeat match goal with
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H : Some _ = Some _ |- _] => inversion H; clear H; subst
| [ H : context[L.eq_dec ?a ?b] |- _ ] => destruct (L.eq_dec a b); subst
end; try discriminate; try (constructor; auto; fail).
destruct l1; inversion eq; clear eq; subst; constructor; auto.
Qed.
Lemma CompatProject : forall l R1 R2,
CompatibleRedices l R1 R2 ->
ProjectRedexToRedex R2 l = Some R1.
Proof using.
intros l R1 R2 compat; destruct R2; cbn; inversion compat; subst;
repeat match goal with
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ |- ?a = ?a ] => reflexivity
| [ |- context[L.eq_dec ?a ?b]] => destruct (L.eq_dec a b); subst
end.
Qed.
Program Definition TauConExprRedexToRedex (R : ConExprRedex) (pf : ConExprRedexToLabel R = Tau) (l : Loc) : C.Redex :=
match R with
| RetE e1 e2 => C.RDone l e1 e2
| IfE e1 e2 => C.RIfE l e1 e2
| IfTT => C.RIfTT l
| IfFF => C.RIfFF l
| SendE l' e1 e2 => C.RSendE l e1 e2 l'
| SendV x x0 => _
| RecvV x x0 => _
| ChooseRedex x x0 => _
| AllowChoiceLRedex x => _
| AllowChoiceRRedex x => _
| LetRetRedex x => _
| AppLocalE e1 e2 => C.RAppLocalE l e1 e2
| AppLocalRedex x => _
| AppGlobalRedex => _
end.
Inductive LocalCompleteAppliedIH : Loc -> ConExpr -> ConExprRedex -> ConExpr -> C.Chor -> Prop :=
| LCAIH : forall l E1 R E2 C, LocalCompleteAppliedIH l E1 R E2 C.
Ltac ProjectChorDestructor :=
repeat match goal with
| [ H : Some _ = Some _ |- _ ] => inversion H; clear H; subst
| [ H : context[L.eq_dec ?a ?b] |- _] =>
tryif unify a b
then let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n eq_refl)]
else lazymatch goal with
| [e : a = b |- _ ] =>
let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n e)]
| [e : b = a |- _ ] =>
let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n (eq_sym e))]
| [n : a <> b |- _ ] =>
let e := fresh in
destruct (L.eq_dec a b) as [e | _];
[destruct (n e)|]
| [n : b <> a |- _ ] =>
let e := fresh in
destruct (L.eq_dec a b) as [e | _];
[destruct (n (eq_sym e))|]
| _ => let eq := fresh "eq" in
let neq := fresh "neq" in
destruct (L.eq_dec a b) as [eq|neq]; subst
end
| [ |- context[L.eq_dec ?a ?b]] =>
tryif unify a b
then let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n eq_refl)]
else lazymatch goal with
| [e : a = b |- _ ] =>
let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n e)]
| [e : b = a |- _ ] =>
let n := fresh in
destruct (L.eq_dec a b) as [_ | n];
[| destruct (n (eq_sym e))]
| [n : a <> b |- _ ] =>
let e := fresh in
destruct (L.eq_dec a b) as [e | _];
[destruct (n e)|]
| [n : b <> a |- _ ] =>
let e := fresh in
destruct (L.eq_dec a b) as [e | _];
[destruct (n (eq_sym e))|]
| _ => let eq := fresh "eq" in
let neq := fresh "neq" in
destruct (L.eq_dec a b) as [eq|neq]; subst
end
| [ H : context[ExprEqDec ?a ?b] |- _] =>
tryif unify a b
then let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n eq_refl)]
else lazymatch goal with
| [e : a = b |- _ ] =>
let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n e)]
| [e : b = a |- _ ] =>
let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n (eq_sym e))]
| [n : a <> b |- _ ] =>
let e := fresh in
destruct (ExprEqDec a b) as [e | _];
[destruct (n e)|]
| [n : b <> a |- _ ] =>
let e := fresh in
destruct (ExprEqDec a b) as [e | _];
[destruct (n (eq_sym e))|]
| _ => let eq := fresh "eq" in
let neq := fresh "neq" in
destruct (ExprEqDec a b) as [eq|neq]; subst
end
| [ |-context[ExprEqDec ?a ?b]] =>
tryif unify a b
then let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n eq_refl)]
else lazymatch goal with
| [e : a = b |- _ ] =>
let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n e)]
| [e : b = a |- _ ] =>
let n := fresh in
destruct (ExprEqDec a b) as [_ | n];
[| destruct (n (eq_sym e))]
| [n : a <> b |- _ ] =>
let e := fresh in
destruct (ExprEqDec a b) as [e | _];
[destruct (n e)|]
| [n : b <> a |- _ ] =>
let e := fresh in
destruct (ExprEqDec a b) as [e | _];
[destruct (n (eq_sym e))|]
| _ => let eq := fresh "eq" in
let neq := fresh "neq" in
destruct (ExprEqDec a b) as [eq|neq]; subst
end
| [ H : context[ProjectChor ?C ?l] |- _ ] =>
lazymatch type of H with
| ProjectChor C l = _ => fail
| _ =>
lazymatch goal with
| [eq : ProjectChor C l = _ |- _ ] => rewrite eq in H
| _ => let eq := fresh "eq" in destruct (ProjectChor C l) eqn:eq
end
end
| [ |- context[ProjectChor ?C ?l] ] =>
lazymatch goal with
| [eq : ProjectChor C l = _ |- _ ] => rewrite eq
| _ => let eq := fresh "eq" in destruct (ProjectChor C l) eqn:eq
end
| [d : C.LRChoice |- _ ] => destruct d
| [H : ConExprMergeRel ?a ?b ?c |- context[ConExprMerge ?a ?b]] =>
rewrite (ConExprMergeRelSpec1 _ _ _ H)
| [H : ConExprMergeRel ?a ?b ?c |- context[ConExprMerge ?b ?a]] =>
rewrite MergeComm; rewrite (ConExprMergeRelSpec1 _ _ _ H)
end.
Lemma ProjectLetRetInversion : forall C l E1 E2, ProjectChor C l = Some (LetRet E1 E2) ->
exists C1 C2, ProjectChor C1 l = Some E1 /\
ProjectChor C2 l = Some E2.
Proof using.
intro C; C.ChorInduction C; intros p E1 E2 eq; cbn in eq; ProjectChorDestructor;
try discriminate.
all: try (apply IHC; auto; fail).
- apply ConExprMergeRelSpec2 in eq; inversion eq; subst.
apply IHC1 in eq0. apply IHC2 in eq1.
destruct eq0 as [C11 [C12 [proj11 proj12]]]; destruct eq1 as [C21 [C22 [proj21 proj22]]].
apply ConExprMergeRelSpec1 in H3; apply ConExprMergeRelSpec1 in H4.
exists (C.If l e C11 C21); exists (C.If l e C12 C22); split; cbn; ProjectChorDestructor; auto.
- exists C1; exists C2; split; auto.
Qed.
Lemma LocalTauSoundness' : forall C1 p E1 R E2 (pf : ConExprRedexToLabel R = Tau),
ConExprStep' E1 R E2 ->
ProjectChor C1 p = Some E1 ->
exists C2, ProjectChor C2 p = Some E2 /\
forall B, ~ In p B -> C.ChorStep (TauConExprRedexToRedex R pf p) B C1 C2.
Proof using.
intro C1; C.ChorInduction C1; cbn; intros p E1 R E2 pf step eq;
destruct R; cbn in pf; try discriminate; cbn; clear pf.
all: ProjectChorDestructor; try discriminate; inversion step; subst; cbn.
all: try (eexists; split; intros; eauto with Chor; cbn;
ProjectChorDestructor; auto; fail).
all: repeat match goal with
| [ eq : ConExprMerge ?a ?b = Some ?c |- _ ] =>
tryif let H := fresh "" c in idtac
then fail
else lazymatch goal with
| [ _ : ConExprMergeRel a b c |- _ ] => fail
| _ => let H := fresh "merge" in
pose proof (ConExprMergeRelSpec2 _ _ _ eq) as H;
inversion H; subst
end
| [ IH : forall p E1 R E2 (pf : ConExprRedexToLabel R = Tau),
ConExprStep' E1 R E2 ->
ProjectChor ?C1 p = Some E1 ->
exists C2, ProjectChor C2 p = Some E2 /\
(forall B, ~ In p B -> C.ChorStep (TauConExprRedexToRedex R pf p) B ?C1 C2),
step : ConExprStep' ?E1 ?R ?E2,
eq : ProjectChor ?C1 ?p = Some ?E1 |- _ ] =>
lazymatch goal with
| [ _ : LocalCompleteAppliedIH p E1 R E2 C1 |- _ ] => fail
| _ =>
let lcaih := fresh "lcaih" in
let C2 := fresh "C" in
let step' := fresh "step" in
let eq' := fresh "eq" in
pose proof (LCAIH p E1 R E2 C1) as lcaih;
destruct (IH p E1 R E2 ltac:(cbn; auto) step eq) as [C2 [eq' step']];
cbn in step'
end
| [H : ConExprMergeRel ?E1 ?E2 ?E3,
H' : ConExprStep' ?E3 ?R ?E4 |- _ ] =>
lazymatch goal with
| [ _ : ConExprStep' E1 _ _ |- _ ] => fail
| _ =>
let E1' := fresh "E" in
let E2' := fresh "E" in
let merge := fresh "merge" in
let step1 := fresh "step" in
let step2 := fresh "step" in
destruct (UnmergeRelTauStep' E1 E2 E3 _ E4 H' ltac:(cbn; auto) H)
as [E1' [E2' [merge [step1 step2]]]]
end
end.
all: try (eexists; split; [| intros; eauto with Chor; econstructor; eauto with Chor;
repeat match goal with
| [ neq : ?p <> ?l, ni : ~ In ?p ?B |- context[?l :: ?B]] =>
lazymatch goal with
| [ _ : ~ In p (l :: B) |- _ ] => fail
| _ =>
let i := fresh in
let eq := fresh in
assert (~ In p (l :: B))
by (intro i; destruct i as [eq|i];
[destruct (neq (eq_sym eq)) | destruct (ni i)])
end
| [ step : forall B, ~ In ?p B -> C.ChorStep ?R B ?C1 ?C2,
ni : ~ In ?p ?B |- _ ] =>
lazymatch goal with
| [ _ : C.ChorStep R B C1 C2 |- _ ] => fail
| _ => pose proof (step B ni)
end
end; auto]; repeat (cbn; ProjectChorDestructor; eauto); fail);
try match goal with
| [ H :ConExprStep' (RecGlobal _) _ _ |- _ ] => inversion H
| [ H :ConExprStep' Unit _ _ |- _ ] => inversion H
end.
- exists (C.AppLocal p C1 e1); split; cbn; ProjectChorDestructor; eauto with ConExpr.
admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
Admitted.
Theorem LocalTauSoundness : forall C1 p E1 E2,
ProjectChor C1 p = Some E1 ->
ConExprStep E1 Tau E2 ->
exists R C2, ProjectRedex R p = Some Tau /\
ProjectChor C2 p = Some E2 /\
C.ChorStep R [] C1 C2.
Proof using.
intros C1 p E1 E2 H H0.
destruct (ConExprStepToPrime H0) as [R [pf step]]; clear H0.
destruct (LocalTauSoundness' C1 p E1 R E2 pf step H) as [C2 [eq2 step']].
exists (TauConExprRedexToRedex R pf p); exists C2; split; [|split]; auto.
- destruct R; cbn in *; ProjectChorDestructor; auto; discriminate.
Qed.
End ChoreographyCompiler.
......@@ -7,6 +7,7 @@ Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Permutation.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Program.Equality.
From Equations Require Import Equations.
......@@ -1252,6 +1253,99 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
econstructor; eauto.
Qed.
Inductive ConExprRedex : Set :=
| RetE : Expr -> Expr -> ConExprRedex
| IfE : Expr -> Expr -> ConExprRedex
| IfTT : ConExprRedex
| IfFF : ConExprRedex
| SendE : Loc -> Expr -> Expr -> ConExprRedex
| SendV : Loc -> Expr -> ConExprRedex
| RecvV : Loc -> Expr -> ConExprRedex
| ChooseRedex : Loc -> LRChoice -> ConExprRedex
| AllowChoiceLRedex : Loc -> ConExprRedex
| AllowChoiceRRedex : Loc -> ConExprRedex
| LetRetRedex : Expr -> ConExprRedex
| AppLocalE : Expr -> Expr -> ConExprRedex
| AppLocalRedex : Expr -> ConExprRedex
| AppGlobalRedex : ConExprRedex.
Inductive ConExprStep' : ConExpr -> ConExprRedex -> ConExpr -> Prop :=
| RetStep' : forall e1 e2, ExprStep e1 e2 -> ConExprStep' (Ret e1) (RetE e1 e2) (Ret e2)
| IfEStep' : forall e1 e2 E1 E2, ExprStep e1 e2 ->
ConExprStep' (If e1 E1 E2) (IfE e1 e2) (If e2 E1 E2)
| IfTTStep' : forall E1 E2, ConExprStep' (If tt E1 E2) IfTT E1
| IfFFStep' : forall E1 E2, ConExprStep' (If ff E1 E2) IfFF E2
| SendEStep' : forall l e1 e2 E, ExprStep e1 e2 ->
ConExprStep' (Send l e1 E) (SendE l e1 e2) (Send l e2 E)
| SendVStep' : forall l v E, ExprVal v -> ConExprStep' (Send l v E) (SendV l v) E
| RecvStep' : forall l v E, ExprVal v ->
ConExprStep' (Recv l E) (RecvV l v) (E [cel| ValSubst v])
| ChooseStep' : forall l LR E, ConExprStep' (Choose l LR E) (ChooseRedex l LR) E
| AllowChoiceLStep' : forall l E,
ConExprStep' (AllowChoiceL l E) (AllowChoiceLRedex l) E
| AllowChoiceRStep' : forall l E,
ConExprStep' (AllowChoiceR l E) (AllowChoiceRRedex l) E
| AllowChoiceLRLStep' : forall l E1 E2,
ConExprStep' (AllowChoiceLR l E1 E2) (AllowChoiceLRedex l) E1
| AllowChoiceLRRStep' : forall l E1 E2,
ConExprStep' (AllowChoiceLR l E1 E2) (AllowChoiceRRedex l) E2
| LetRetEStep' : forall E1 R E1' E2,
ConExprStep' E1 R E1' -> ConExprStep' (LetRet E1 E2) R (LetRet E1' E2)
| LetRetStep' : forall v E2,
ExprVal v -> ConExprStep' (LetRet (Ret v) E2) (LetRetRedex v) (E2 [cel| ValSubst v])
| AppLocalFunStep' : forall F1 R F2 e,
ConExprStep' F1 R F2 ->
ConExprStep' (AppLocal F1 e) R (AppLocal F2 e)
| AppLocalArgStep' : forall F e1 e2,
ExprStep e1 e2 ->
ConExprStep' (AppLocal (RecLocal F) e1) (AppLocalE e1 e2) (AppLocal (RecLocal F) e2)
| AppLocalStep' : forall F v,
ExprVal v ->
ConExprStep' (AppLocal (RecLocal F) v) (AppLocalRedex v)
((F [cel| ValSubst v]) [ceg| RecLocalSubst F])
| AppGlobalFunStep' : forall F1 R F2 A,
ConExprStep' F1 R F2 ->
ConExprStep' (AppGlobal F1 A) R (AppGlobal F2 A)
| AppGlobalArgStep' : forall F A1 R A2,
ConExprStep' A1 R A2 ->
ConExprStep' (AppGlobal (RecGlobal F) A1) R (AppGlobal (RecGlobal F) A2)
| AppGlobalStep' : forall B V,
ConExprVal V ->
ConExprStep' (AppGlobal (RecGlobal B) V) AppGlobalRedex (B [ceg| RecGlobalSubst B V]).
Hint Constructors ConExprStep' : ConExpr.
Definition ConExprRedexToLabel (R : ConExprRedex) : Label :=
match R with
| RetE _ _ => Tau
| IfE _ _ => Tau
| IfTT => Tau
| IfFF => Tau
| SendE _ _ _ => Tau
| SendV l v => SendLabel l v
| RecvV l v => RecvLabel l v
| ChooseRedex l d => ChooseLabel l d
| AllowChoiceLRedex l => AllowChoiceLabel l C.LChoice
| AllowChoiceRRedex l => AllowChoiceLabel l C.RChoice
| LetRetRedex _ => SyncTau
| AppLocalE _ _ => Tau
| AppLocalRedex _ => SyncTau
| AppGlobalRedex => SyncTau
end.
Theorem ConExprStepToPrime : forall {E1 L E2},
ConExprStep E1 L E2 -> exists R, ConExprRedexToLabel R = L /\ ConExprStep' E1 R E2.
Proof using.
intros E1 L E2 step; induction step;
try (eexists; split; [|econstructor]; eauto; fail).
all: destruct IHstep as [R [eq step']]; exists R; split; [| constructor]; auto.
Qed.
Theorem ConExprStep'ToNormal : forall {E1 R E2},
ConExprStep' E1 R E2 -> ConExprStep E1 (ConExprRedexToLabel R) E2.
Proof using.
intros E1 L E2 step; induction step; cbn; auto with ConExpr.
Qed.
Lemma MergeStep : forall E11 E12 E21 E22 E1 E2 L,
ConExprStep E11 L E21 ->
ConExprStep E12 L E22 ->
......@@ -1462,6 +1556,67 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
rewrite MergeIdempotent in merge2; inversion merge2; subst; auto.
Qed.
Lemma UnmergeRelTauStep' : forall E11 E12 E1 R E2,
ConExprStep' E1 R E2 ->
ConExprRedexToLabel R = Tau ->
ConExprMergeRel E11 E12 E1 ->
exists E21 E22, ConExprMergeRel E21 E22 E2 /\
ConExprStep' E11 R E21 /\
ConExprStep' E12 R E22.
Proof using.
intros E11 E12 E1 R E2 step;
revert E11 E12; induction step;
intros E11 E12 eq1 merge1; inversion merge1; subst;
try (cbn in eq1; inversion eq1; fail).
all:
try (eexists; eexists; split; [econstructor; eauto|split];
eauto with ConExpr; fail).
- exists E0; exists E21; split; [|split]; auto with ConExpr.
- exists E3; exists E22; split; [|split]; auto with ConExpr.
- destruct (IHstep E0 E3 eq1 H3) as [E0' [E3' [merge2 [step1 step2]]]].
exists (LetRet E0' E21); exists (LetRet E3' E22); split;[|split]; auto with ConExpr.
- destruct (IHstep E1 E2 eq1 H2) as [E21 [E22 [merge2 [step1 step2]]]].
exists (AppLocal E21 e); exists (AppLocal E22 e); split; [|split]; auto with ConExpr.
- inversion H3; subst.
exists (AppLocal (RecLocal F) e2); exists (AppLocal (RecLocal F) e2);
split; [|split]; auto with ConExpr.
- destruct (IHstep E0 E21 eq1 H3) as [E0' [E21' [merge2 [step1 step2]]]].
exists (AppGlobal E0' E1); exists (AppGlobal E21' E22); split; [|split]; auto with ConExpr.
- inversion H3; subst.
destruct (IHstep E1 E22 eq1 H4) as [E1' [E22' [merge2 [step1 step2]]]].
exists (AppGlobal (RecGlobal F) E1'); exists (AppGlobal (RecGlobal F) E22');
split; [|split]; auto with ConExpr.
Qed.
Lemma UnmergeRelTauStep : forall E11 E12 E1 E2,
ConExprStep E1 Tau E2 ->
ConExprMergeRel E11 E12 E1 ->
exists E21 E22, ConExprMergeRel E21 E22 E2 /\
ConExprStep E11 Tau E21 /\
ConExprStep E12 Tau E22.
Proof using.
intros E11 E12 E1 E2 step;
revert E11 E12; dependent induction step;
intros E11 E12 eq1; inversion eq1; subst.
all:
try (eexists; eexists; split; [econstructor; eauto|split];
eauto with ConExpr; fail).
- exists E0; exists E21; split; [|split]; auto with ConExpr.
- exists E3; exists E22; split; [|split]; auto with ConExpr.
- destruct (IHstep eq_refl E0 E3 H3) as [E0' [E3' [merge2 [step1 step2]]]].
exists (LetRet E0' E21); exists (LetRet E3' E22); split;[|split]; auto with ConExpr.
- destruct (IHstep eq_refl E1 E2 H2) as [E21 [E22 [merge2 [step1 step2]]]].
exists (AppLocal E21 e); exists (AppLocal E22 e); split; [|split]; auto with ConExpr.
- inversion H3; subst.
exists (AppLocal (RecLocal F) e2); exists (AppLocal (RecLocal F) e2);
split; [|split]; auto with ConExpr.
- destruct (IHstep eq_refl E0 E21 H3) as [E0' [E21' [merge2 [step1 step2]]]].
exists (AppGlobal E0' E1); exists (AppGlobal E21' E22); split; [|split]; auto with ConExpr.
- inversion H3; subst.