Commit 8917e2c3 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Move restricted semantics results to own file.

parent abe3058e
......@@ -78,29 +78,6 @@ Module Choreography (Import E : Expression) (L : Locations).
apply ChoiceEqDec.
Defined.
(* Fixpoint NumberOfIfs (C : Chor) : nat := *)
(* match C with *)
(* | Done p e => 0 *)
(* | Var n => 0 *)
(* | Send p e q C' => NumberOfIfs C' *)
(* | If p e C1 C2 => S (NumberOfIfs C1 + NumberOfIfs C2) *)
(* | Sync p d q C' => NumberOfIfs C' *)
(* | DefLocal p C1 C2 => NumberOfIfs C1 + NumberOfIfs C2 *)
(* | DefGlobal C1 C2 => NumberOfIfs C1 + NumberOfIfs C2 *)
(* end. *)
(* Fixpoint ChorSize (C : Chor) : nat := *)
(* match C with *)
(* | Done p e => 1 *)
(* | Var n => 1 *)
(* | Send p e q C' => S (ChorSize C') *)
(* | If p e C1 C2 => S(Nat.max (ChorSize C1) (ChorSize C2)) *)
(* | Sync p d q C' => S (ChorSize C') *)
(* | DefLocal p C1 C2 => S (ChorSize C1 + ChorSize C2) *)
(* | DefGlobal C1 C2 => S (ChorSize C1 + ChorSize C2) *)
(* end. *)
Definition ChorUpExprRename : (Loc -> nat -> nat) -> Loc -> Loc -> nat -> nat :=
fun ξ p q => if L.eq_dec p q
then ExprUpRename (ξ q)
......@@ -182,11 +159,6 @@ Module Choreography (Import E : Expression) (L : Locations).
apply ChorUpIdExprRename.
Qed.
(* Lemma ChorExprRenameSize : forall (C : Chor) (ξ : Loc -> nat -> nat), ChorSize (C ce| ξ ) = ChorSize C. *)
(* Proof using. *)
(* intro C; ChorInduction C; intros ξ; cbn; auto. *)
(* Qed. *)
Definition ChorUpRename : (nat -> nat) -> nat -> nat :=
fun f n => match n with
| 0 => 0
......@@ -343,12 +315,6 @@ Module Choreography (Import E : Expression) (L : Locations).
intros p n; unfold ChorUpExprSubst; unfold ChorUpExprRename; destruct (L.eq_dec l p); destruct n; auto; unfold ExprUpRename; rewrite ExprRenameVar; auto.
Qed.
(* Theorem ChorExprSubstSize : forall (C : Chor) (σ : Loc -> nat -> Expr), *)
(* ChorSize (C [ce| σ]) = ChorSize C. *)
(* Proof using. *)
(* intro C; ChorInduction C; intro σ; cbn; auto. *)
(* Qed. *)
Definition ChorUpSubst : (nat -> Chor) -> nat -> Chor :=
fun f n => match n with
| 0 => Var 0
......@@ -1139,581 +1105,6 @@ Module Choreography (Import E : Expression) (L : Locations).
destruct n; auto. rewrite ExprRenameVar; auto.
Qed.
Inductive RChorStep : Redex -> list Loc -> Chor -> Chor -> Prop :=
| DoneEStep : forall (l : Loc) (e1 e2 : Expr),
ExprStep e1 e2 -> RChorStep (RDone l e1 e2) nil (Done l e1) (Done l e2)
| SendEStep : forall (l1 l2 : Loc) (B : list Loc),
~ In l1 B -> ~ In l2 B -> l1 <> l2 ->
forall (e1 e2 : Expr) (C : Chor),
ExprStep e1 e2 -> RChorStep (RSendE l1 e1 e2 l2) B (Send l1 e1 l2 C) (Send l1 e2 l2 C)
| SendIStep : forall (l1 l2 : Loc) (e : Expr) (C1 C2 : Chor) (B : list Loc) (R : Redex),
RChorStep R (l1 :: l2 :: B) C1 C2 ->
RChorStep R B (Send l1 e l2 C1) (Send l1 e l2 C2)
| SendVStep : forall (l1 l2 : Loc) (v : Expr) (C : Chor) (B : list Loc),
~ In l1 B -> ~ In l2 B -> l1 <> l2 ->
ExprVal v ->
RChorStep (RSendV l1 v l2) B (Send l1 v l2 C) (C [ce| ValueSubst l2 v])
| IfEStep : forall (l1 : Loc) (e1 e2 : Expr) (C1 C2 : Chor) (B : list Loc),
~ In l1 B ->
ExprStep e1 e2 ->
RChorStep (RIfE l1 e1 e2) B (If l1 e1 C1 C2) (If l1 e2 C1 C2)
| IfIStep : forall (l1 : Loc) (e : Expr) (C1 C2 C3 C4 : Chor) (B : list Loc) (R : Redex),
RChorStep R (l1 :: B) C1 C3 ->
RChorStep R (l1 :: B) C2 C4 ->
RChorStep R B (If l1 e C1 C2) (If l1 e C3 C4)
| IfTrueStep : forall (l1 : Loc) (C1 C2 : Chor) (B : list Loc),
~ In l1 B ->
RChorStep (RIfTT l1) B (If l1 tt C1 C2) C1
| IfFalseStep : forall (l1 : Loc) (C1 C2 : Chor) (B : list Loc),
~ In l1 B ->
RChorStep (RIfFF l1) B (If l1 ff C1 C2) C2
| DefLocalIStep : forall R l C1 C1' C2,
RChorStep R [] C1 C1' ->
RChorStep R [] (DefLocal l C1 C2) (DefLocal l C1' C2)
| DefLocalStep : forall (l : Loc) (v : Expr) (C2 : Chor),
ExprVal v ->
RChorStep (RDefLocal l v) nil (DefLocal l (Done l v) C2) (C2 [ce| ValueSubst l v])
| AppLocalFunStep : forall l C1 C2 e R,
RChorStep R [] C1 C2 ->
RChorStep R [] (AppLocal l C1 e) (AppLocal l C2 e)
| AppLocalExprStep : forall l C e1 e2,
ExprStep e1 e2 ->
RChorStep (RAppLocalE l e1 e2) [] (AppLocal l (RecLocal l C) e1) (AppLocal l (RecLocal l C) e2)
| AppLocalValStep : forall l C v,
ExprVal v ->
RChorStep (RAppLocal l v) []
(AppLocal l (RecLocal l C) v)
(C [ce| ValueSubst l v] [c| AppLocalSubst l C])
| AppGlobalFunStep : forall C11 C12 C2 R,
RChorStep R [] C11 C12 ->
RChorStep R [] (AppGlobal C11 C2) (AppGlobal C12 C2)
| AppGlobalArgStep : forall C1 C21 C22 R,
RChorStep R [] C21 C22 ->
RChorStep R [] (AppGlobal (RecGlobal C1) C21) (AppGlobal (RecGlobal C1) C22)
| AppGlobalValStep : forall C1 C2,
ChorVal C2 ->
RChorStep RAppGlobal []
(AppGlobal (RecGlobal C1) C2)
(C1 [c| AppGlobalSubst C1 C2])
| SyncStep : forall (l1 l2 : Loc) (d : LRChoice) (C : Chor) (B : list Loc),
~ In l1 B -> ~ In l2 B ->
RChorStep (RSync l1 d l2) B (Sync l1 d l2 C) C
| SyncIStep : forall (l1 l2 : Loc) (d : LRChoice) (C1 C2 : Chor) (B : list Loc) (R : Redex),
RChorStep R (l1 :: l2 :: B) C1 C2 ->
RChorStep R B (Sync l1 d l2 C1) (Sync l1 d l2 C2).
Global Hint Constructors RChorStep : Chor.
Ltac NotInList :=
repeat match goal with
| [ |- ~ In ?a nil ] => let H := fresh in intro H; inversion H
| [ nin : ~ In ?a ?l |- ~ In ?a ?l ] => exact nin
| [ H : ~ In ?a (?b :: ?l) |- _ ] =>
match goal with
| [ _ : a <> b, _ : ~ In a l |- _ ] => fail 1
| _ => assert (a <> b) by (let eq := fresh in intro eq; apply H; left; auto);
assert(~ In a l) by (let i := fresh in intro i; apply H; right; auto)
end
| [ neq : ?a <> ?b |- ~ In ?a (?b :: ?l) ] =>
let H := fresh in
intro H; destruct H as [eq | i]; [exfalso; apply neq; auto | revert i; fold (not (In a l))]
| [i : ~ In ?p ?B1, ext : forall q, In q ?B1 <-> In q ?B2 |- ~ In ?p ?B2 ] =>
let H := fresh in intro H; rewrite <- ext in H; apply i; exact H
end.
Lemma RStepRearrange : forall R B1 C1 C2,
RChorStep R B1 C1 C2 -> forall B2, (forall q, In q B1 <-> In q B2) -> RChorStep R B2 C1 C2.
Proof using.
intros R B1 C1 C2 step; induction step; intros B2 ext.
all: try match goal with
| [H : forall q, In q [] <-> In q ?B |- _ ] =>
let H' := fresh in
assert (B = []) as H' by (let x := fresh in destruct B as [| x B]; [reflexivity | pose proof ((proj2 (H x)) ltac:(left; reflexivity)) as H'; inversion H']);
subst; clear H
| [H : forall q, In q ?B <-> In q [] |- _ ] =>
let H' := fresh in
assert (B = []) as H' by (let x := fresh in destruct B as [| x B]; [reflexivity | pose proof ((proj1 (H x)) ltac:(left; reflexivity)) as H'; inversion H']);
subst; clear H
end.
all: try (constructor; try NotInList; auto; fail).
- apply SendIStep; auto; apply IHstep; intro q; split; intro i; repeat (destruct i as [eq | i]; [left; exact eq | right]; auto); apply ext; auto.
- apply IfIStep; [apply IHstep1 | apply IHstep2]; intro q; split; intro i; repeat (destruct i as [eq | i]; [left | right]; auto); apply ext; auto.
- apply SyncIStep; auto; apply IHstep; intro q; split; intro i; repeat (destruct i as [eq | i]; [left; exact eq | right]; auto); apply ext; auto.
Qed.
Inductive RedexOf : Loc -> Redex -> Prop :=
| RODone : forall p e1 e2, RedexOf p (RDone p e1 e2)
| ROIfE : forall p e1 e2, RedexOf p (RIfE p e1 e2)
| ROIfTT : forall p, RedexOf p (RIfTT p)
| ROIfFF : forall p, RedexOf p (RIfFF p)
| ROSendE1 : forall p e1 e2 q, RedexOf p (RSendE p e1 e2 q)
| ROSendE2 : forall p e1 e2 q, RedexOf q (RSendE p e1 e2 q)
| ROSendV1 : forall p v q, RedexOf p (RSendV p v q)
| ROSendV2 : forall p v q, RedexOf q (RSendV p v q)
| ROSync1 : forall p d q, RedexOf p (RSync p d q)
| ROSync2 : forall p d q, RedexOf q (RSync p d q)
| ROLDef : forall l e, RedexOf l (RDefLocal l e).
Global Hint Constructors RedexOf: Chor.
Lemma NoIStepInList : forall p B R,
In p B ->
RedexOf p R ->
forall C1 C2, ~RChorStep R B C1 C2.
Proof using.
intros p B R H H0 C1 C2 step; induction step; inversion H0;
match goal with
| [ i : In ?p ?B, n : ~ In ?p' ?B, e : ?p = ?p' |- False ] =>
apply n; rewrite <- e; exact i
| [ i : In ?p ?B, n : ~ In ?p' ?B, e : ?p' = ?p |- False ] =>
apply n; rewrite e; exact i
| _ => idtac
end.
all: try (apply IHstep; auto; right; right; auto; fail).
all: try (apply IHstep1; auto; right; auto; fail).
all: inversion H.
Qed.
Corollary NoDoneIStepInList : forall p B,
In p B ->
forall e1 e2 C1 C2, ~RChorStep (RDone p e1 e2) B C1 C2.
Proof using.
intros p B H e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply RODone.
Qed.
Corollary NoSendEIStepInList1 : forall p B,
In p B ->
forall e1 e2 C1 C2 q, ~RChorStep (RSendE p e1 e2 q) B C1 C2.
Proof using.
intros p B H q e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply ROSendE1.
Qed.
Corollary NoSendEIStepInList2 : forall B q,
In q B ->
forall p e1 e2 C1 C2, ~RChorStep (RSendE p e1 e2 q) B C1 C2.
Proof using.
intros B q H p e1 e2 C1 C2; apply NoIStepInList with (p := q); auto; apply ROSendE2.
Qed.
Corollary NoSendVIStepInList1 : forall p B,
In p B ->
forall v q C1 C2, ~RChorStep (RSendV p v q) B C1 C2.
Proof using.
intros p B H v q C1 C2; apply NoIStepInList with (p := p); auto; apply ROSendV1.
Qed.
Corollary NoSendVIStepInList2 : forall B q,
In q B ->
forall p v C1 C2, ~RChorStep (RSendV p v q) B C1 C2.
Proof using.
intros B q H p v C1 C2; apply NoIStepInList with (p := q); auto; apply ROSendV2.
Qed.
Corollary NoIfEIStepInList : forall p B,
In p B ->
forall e1 e2 C1 C2, ~RChorStep (RIfE p e1 e2) B C1 C2.
Proof using.
intros p B H e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply ROIfE.
Qed.
Corollary NoIfTTStepInList : forall p B,
In p B ->
forall C1 C2, ~RChorStep (RIfTT p) B C1 C2.
Proof using.
intros p B H C1 C2; apply NoIStepInList with (p := p); auto; apply ROIfTT.
Qed.
Corollary NoIfFFStepInList : forall p B,
In p B ->
forall C1 C2, ~RChorStep (RIfFF p) B C1 C2.
Proof using.
intros p B H C1 C2; apply NoIStepInList with (p := p); auto; apply ROIfFF.
Qed.
Corollary NoSyncStepInList1 : forall p B,
In p B ->
forall d q C1 C2, ~RChorStep (RSync p d q) B C1 C2.
Proof using.
intros p B H q C1 C2; apply NoIStepInList with (p := p); auto; constructor.
Qed.
Corollary NoSyncStepInList2 : forall B q,
In q B ->
forall p d C1 C2, ~RChorStep (RSync p d q) B C1 C2.
Proof using.
intros B q H p C1 C2; apply NoIStepInList with (p := q); auto; constructor.
Qed.
Corollary NoLDefStepInList : forall B p,
In p B ->
forall e C1 C2, ~RChorStep (RDefLocal p e) B C1 C2.
Proof using.
intros B p H e C1 C2; apply NoIStepInList with (p := p); auto; constructor.
Qed.
Global Hint Resolve RStepRearrange NoDoneIStepInList : Chor.
Global Hint Resolve NoSendEIStepInList1 NoSendVIStepInList1 NoSendEIStepInList2 NoSendVIStepInList2 : Chor.
Global Hint Resolve NoIfEIStepInList NoIfTTStepInList NoIfFFStepInList: Chor.
Global Hint Resolve NoSyncStepInList1 NoSyncStepInList2 NoLDefStepInList : Chor.
Inductive RStepMany : list Redex -> list Loc -> Chor -> Chor -> Prop :=
| RStepManyZero : forall B C, RStepMany nil B C C
| RStepManyPlus : forall R Rs B C1 C2 C3, RChorStep R B C1 C2 -> RStepMany Rs B C2 C3 -> RStepMany (R :: Rs) B C1 C3.
Global Hint Constructors RStepMany : Chor.
Theorem RStepManyOne : forall (R : Redex) (B : list Loc) (C1 C2 : Chor),
RChorStep R B C1 C2 -> RStepMany [R] B C1 C2.
Proof using.
intros R B C1 C2 step.
eapply RStepManyPlus; [exact step | apply RStepManyZero].
Qed.
Global Hint Resolve RStepManyOne : Chor.
Program Fixpoint RStepManyTrans (Rs1 Rs2 : list Redex) (B : list Loc) (C1 C2 C3 : Chor)
(r1 : RStepMany Rs1 B C1 C2)
(r2 : RStepMany Rs2 B C2 C3) {struct r1} : RStepMany (Rs1 ++ Rs2) B C1 C3 :=
match r1 with
| RStepManyZero B C => r2
| RStepManyPlus R Rs B C1' C2' _ s1 r3 =>
RStepManyPlus _ _ _ _ _ _ s1 (RStepManyTrans _ _ _ _ _ _ r3 r2)
end.
(* Global Hint Resolve RStepManyTrans : AChor. *)
Lemma SendIStepMany : forall Rs B p e q C1 C2, RStepMany Rs (p :: q :: B) C1 C2 -> RStepMany Rs B (Send p e q C1) (Send p e q C2).
Proof using.
intros Rs B p e q C1 C2 step; revert e; dependent induction step; intros e; auto with Chor.
apply RStepManyPlus with (R := R) (C2 := Send p e q C2). apply SendIStep; auto.
apply IHstep; auto.
Qed.
Lemma IfIStepMany : forall Rs B p e C11 C12 C21 C22, RStepMany Rs (p :: B) C11 C12 -> RStepMany Rs (p :: B) C21 C22 -> RStepMany Rs B (If p e C11 C21) (If p e C12 C22).
Proof using.
intros Rs; induction Rs; intros B p e C11 C12 C21 C22 step1 step2; inversion step1; inversion step2; subst; auto with Chor.
apply RStepManyPlus with (C2 := If p e C2 C4); [apply IfIStep; auto|]. apply IHRs; auto.
Qed.
Lemma SyncIStepMany : forall Rs B d p q C1 C2, RStepMany Rs (p :: q :: B) C1 C2 -> RStepMany Rs B (Sync p d q C1) (Sync p d q C2).
Proof using.
intros Rs; induction Rs; intros B d p q C1 C2 step; inversion step; subst; auto with Chor.
apply RStepManyPlus with (C2 := Sync p d q C3); auto with Chor.
Qed.
Global Hint Resolve SendIStepMany IfIStepMany SyncIStepMany : Chor.
Lemma ConsNotIn : forall {A : Type} (a b : A) (l : list A),
a <> b -> ~ In a l -> ~ In a (b :: l).
Proof using.
intros A a b l H H0 H1.
destruct H1; auto.
Qed.
Lemma NotInCons : forall {A : Type} (a b : A) (l : list A),
~ In a (b :: l) -> a <> b /\ ~ In a l.
Proof using.
intros A a b l H; split; intro H0; apply H; [left | right]; auto.
Qed.
Global Hint Resolve ConsNotIn NotInCons : Chor.
(* Ltac ListHelper := *)
(* match goal with *)
(* | [H : ~ In ?p (?p :: _) |- _ ] => *)
(* exfalso; apply H; left; reflexivity *)
(* | [H : ~ In ?p (_ :: ?p :: _) |- _ ] => *)
(* exfalso; apply H; right; left; reflexivity *)
(* | [H : ~ In ?r (?p :: ?q :: ?B) |- ~ In ?r ?B] => *)
(* let H' := fresh in intro H'; apply H; right; right; exact H' *)
(* | [H : ~ In ?r (?p :: ?B) |- ~ In ?r ?B ] => *)
(* let H' := fresh in intro H'; apply H; right; exact H' *)
(* | [H : ~ In ?r (?p :: _) |- ?r <> ?p ] => *)
(* let H' := fresh H in intro H'; apply H; left; auto *)
(* | [H : ~ In ?r (?p :: _) |- ?p <> ?r ] => *)
(* let H' := fresh H in intro H'; apply H; left; auto *)
(* | [H : ~ In ?r (_ :: ?p :: _) |- ?p <> ?r ] => *)
(* let H' := fresh H in intro H'; apply H; right; left; auto *)
(* | [H : ~ In ?r (_ :: ?p :: _) |- ?r <> ?p ] => *)
(* let H' := fresh H in intro H'; apply H; right; left; auto *)
(* end. *)
Ltac InList := repeat match goal with
| [ H : ?P |- ?P ] => exact H
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ |- In ?a (?a :: _) ] => left; reflexivity
| [ i : In ?a (_ :: _) |- _ ] => destruct i; subst
| [ |- In ?a (_ :: _) ] => right
end.
Theorem EquivSimulation : forall C1 C2, C1 C2 -> forall R B C1',
RChorStep R B C1 C1' -> exists C2', RChorStep R B C2 C2' /\ C1' C2'.
Proof using.
intros C1 C2 equiv; induction equiv; intros R B Cstep step;
eauto with Chor; repeat match goal with
| [ H : RChorStep ?R ?B ?C1 ?C1' |- _ ] =>
tryif (let x := fresh "fail_" C1 in idtac)
then fail
else inversion H; subst; eauto with Chor; clear H
end.
all: try (eexists; split; eauto with Chor; fail).
all: repeat match goal with
| [IH : forall R B C', RChorStep R B ?C C' -> exists C2', RChorStep R B ?C2 C2' /\ C' C2', H : RChorStep ?R ?B ?C ?C' |- _ ] =>
lazymatch goal with
| [ _ : RChorStep R B C2 ?C2', _ : C' ?C2' |- _] => fail
| _ => let H' := fresh in
let C2 := fresh "C" in
let step := fresh "step" in
let eqv := fresh "eqv" in
pose proof (IH R B C' H) as H'; destruct H' as [C2 [step eqv]]
end
end; eauto with Chor.
apply RetEquivInversion in equiv1; subst; eexists; split; eauto with Chor.
all: try (exfalso; eapply NoIStepInList; eauto; eauto with Chor; InList; fail).
all: try (eexists; split; [repeat econstructor |]; eauto with Chor; try NotInList; auto; try (eapply RStepRearrange; eauto with Chor; intros q; split; unfold In; intro i; tauto); fail).
- apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst.
exists (AppLocal l (RecLocal l C') e2); split; auto with Chor.
- apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst.
exists (C' [ce|ValueSubst l e] [c|AppLocalSubst l C'] ); split; auto with Chor.
apply WeakSubstExt; [apply EquivStableExprSubst|]; auto.
intro n; destruct n; cbn; auto with Chor.
- apply RecGlobalEquivInversion in equiv1; destruct equiv1 as [C1' [eq equiv1]]; subst.
exists (AppGlobal (RecGlobal C1') C); split; auto with Chor.
- apply RecGlobalEquivInversion in equiv1; destruct equiv1 as [C1' [eq equiv1]]; subst.
exists (C1' [c| AppGlobalSubst C1' C22]); split; auto with Chor.
apply AppGlobalValStep; auto.
eapply ChorValStableEquiv; eauto.
apply WeakSubstExt; auto. intro n; destruct n; cbn; auto with Chor.
destruct n; auto with Chor.
- exists (l1 e l2 fby C [ce|ValueSubst l4 e']); split; eauto with Chor.
pose proof (SendVStep l3 l4 e' (l1 e l2 fby C) B ltac:(NotInList) ltac:(NotInList) H13 H14) as H3; cbn in H3.
unfold ValueSubst in H3 at 1; destruct (L.eq_dec l4 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|].
fold ExprIdSubst in H3; rewrite ExprIdentitySubstSpec in H3.
rewrite ChorExprSubstExt with (σ2 := ValueSubst l4 e') in H3; auto.
intros p n; unfold ChorUpExprSubst. unfold ValueSubst.
destruct (L.eq_dec l2 p) as [eq1 | neq1]; destruct(L.eq_dec l4 p) as [eq2 |neq2];
subst; try match goal with
| [H : ?a <> ?a |- _ ] => destruct (H eq_refl)
end.
destruct n; cbn; auto; apply ExprRenameVar.
all: reflexivity.
- exists (l3 e'⟫ l4 fby (C [ce|ValueSubst l2 e])); split; auto with Chor.
cbn; unfold ValueSubst at 1;
destruct (L.eq_dec l2 l3) as [eq |_]; [destruct (H1 eq)|].
fold ExprIdSubst; rewrite ExprIdentitySubstSpec.
rewrite ChorExprSubstExt with (σ2 := ValueSubst l2 e); auto with Chor.
intros p n; unfold ChorUpExprSubst; unfold ValueSubst.
destruct (L.eq_dec l4 p); destruct (L.eq_dec l2 p); subst;
try (match goal with | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl) end).
1,2: destruct n; cbn; auto. rewrite ExprRenameVar; reflexivity. reflexivity.
- exists (Cond l3 e' Then C1 [ce|ValueSubst l2 e] Else C2 [ce|ValueSubst l2 e]);
split; auto with Chor.
cbn; unfold ValueSubst at 1;
destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H0 eq)|].
fold ExprIdSubst; rewrite ExprIdentitySubstSpec; reflexivity.
- exists ((Cond l1 e Then C1 Else C2) [ce|ValueSubst l3 e']); split; auto with Chor.
apply SendVStep; try NotInList; auto.
cbn; unfold ValueSubst at 3; destruct (L.eq_dec l3 l1) as [eq | _];
[destruct (H0 (eq_sym eq))|].
fold ExprIdSubst; rewrite ExprIdentitySubstSpec; reflexivity.
Qed.
Inductive StdChorStep : Chor -> Chor -> Prop :=
| StdDoneEStep : forall (l : Loc) (e1 e2 : Expr),
ExprStep e1 e2
-> StdChorStep (Done l e1) (Done l e2)
| StdSendEStep : forall (l1 l2 : Loc) (e1 e2 : Expr) (C : Chor),
ExprStep e1 e2
-> l1 <> l2
-> StdChorStep (Send l1 e1 l2 C) (Send l1 e2 l2 C)
| StdSendVStep : forall (l1 l2 : Loc) (v : Expr) (C : Chor),
ExprVal v
-> l1 <> l2
-> StdChorStep (Send l1 v l2 C) (C [ce| ValueSubst l2 v])
| StdIfEStep : forall (l : Loc) (e1 e2 : Expr) (C1 C2 : Chor),
ExprStep e1 e2
-> StdChorStep (If l e1 C1 C2) (If l e2 C1 C2)
| StdIfTrueStep : forall (l : Loc) (C1 C2 : Chor),
StdChorStep (If l tt C1 C2) C1
| StdIfFalseStep : forall (l : Loc) (C1 C2 : Chor),
StdChorStep (If l ff C1 C2) C2
| StdSyncStep : forall (l1 l2 : Loc) (d : LRChoice) (C : Chor),
StdChorStep (Sync l1 d l2 C) C
| StdDefLocalIStep : forall (l : Loc) (C1 C1' C2 : Chor),
StdChorStep C1 C1' -> StdChorStep (DefLocal l C1 C2) (DefLocal l C1' C2)
| StdDefLocalStep : forall (l : Loc) (v : Expr) (C : Chor),
ExprVal v ->
StdChorStep (DefLocal l (Done l v) C) (C [ce|ValueSubst l v])
| StdAppLocalFunStep : forall l (C1 C2 : Chor) e,
StdChorStep C1 C2 ->
StdChorStep (AppLocal l C1 e) (AppLocal l C2 e)
| StdAppLocalArgStep : forall l C e1 e2,
ExprStep e1 e2 ->
StdChorStep (AppLocal l (RecLocal l C) e1) (AppLocal l (RecLocal l C) e2)
| StdAppLocalStep : forall l C v,
ExprVal v ->
StdChorStep (AppLocal l (RecLocal l C) v) (C [ce|ValueSubst l v] [c|AppLocalSubst l C])
| StdAppGlobalFunStep : forall (C1 C1' C2 : Chor),
StdChorStep C1 C1'
-> StdChorStep (AppGlobal C1 C2) (AppGlobal C1' C2)
| StdAppGlobalArgStep : forall (C1 C2 C2' : Chor),
StdChorStep C2 C2'
-> StdChorStep (AppGlobal (RecGlobal C1) C2) (AppGlobal (RecGlobal C1) C2')
| StdAppGlobalStep : forall (C1 C2 : Chor),
ChorVal C2 ->
StdChorStep (AppGlobal (RecGlobal C1) C2) (C1 [c|AppGlobalSubst C1 C2])
| StdEquivStep : forall (C1 C1' C2 C2' : Chor),
C1 C1'
-> StdChorStep C1' C2'
-> C2 C2'
-> StdChorStep C1 C2.
Global Hint Constructors StdChorStep : Chor.
Theorem StdToRStep : forall (C1 C2 : Chor),
StdChorStep C1 C2
-> exists R C2', C2 C2' /\ RChorStep R nil C1 C2'.
Proof using.
intros C1 C2 stdstep; induction stdstep.
all:try ( eexists; eexists; split; [reflexivity | constructor; auto]; fail).
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (LetLocal l new C2' fby C2); split; auto with Chor.
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (AppLocal l C2' e); split; auto with Chor.
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (AppGlobal C2' C2); split; auto with Chor.
- destruct IHstdstep as [R [C2'' [equiv step]]].
exists R; exists (AppGlobal (RecGlobal C1) C2''); split; auto with Chor.
- destruct IHstdstep as [R [C2'' [equiv step]]].
destruct (EquivSimulation C1' C1 ltac:(auto with Chor) R [] C2'' step) as [C2''' [step' equiv']].
exists R; exists C2'''; split; auto with Chor. transitivity C2'; auto; transitivity C2''; auto.
Qed.
Inductive RedexOnTop : Redex -> Chor -> Prop :=
| DoneOnTop : forall p e1 e2, RedexOnTop (RDone p e1 e2) (Done p e1)
| SendEOnTop : forall p e1 e2 q C, RedexOnTop (RSendE p e1 e2 q) (Send p e1 q C)
| SendVOnTop : forall p v q C, RedexOnTop (RSendV p v q) (Send p v q C)
| IfEOnTop : forall p e1 e2 C1 C2, RedexOnTop (RIfE p e1 e2) (If p e1 C1 C2)
| IfTTOnTop : forall p C1 C2, RedexOnTop (RIfTT p) (If p tt C1 C2)
| IfFFOnTop : forall p C1 C2, RedexOnTop (RIfFF p) (If p ff C1 C2)
| SyncOnTop : forall p d q C, RedexOnTop (RSync p d q) (Sync p d q C)
| IDefLocalOntop : forall l C1 C2 R, RedexOnTop R C1 -> RedexOnTop R (DefLocal l C1 C2)
| DefLocalOnTop : forall l e C, RedexOnTop (RDefLocal l e) (DefLocal l (Done l e) C)
| AppLocalEOnTop : forall l e1 e2 C, RedexOnTop (RAppLocalE l e1 e2) (AppLocal l (RecLocal l C) e1)
| AppLocalOnTop : forall l C e, RedexOnTop (RAppLocal l e) (AppLocal l (RecLocal l C) e)
| AppGlobalOnTop : forall C1 C2,
ChorVal C2 -> RedexOnTop RAppGlobal (AppGlobal (RecGlobal C1) C2)
| LocalFunOnTop : forall R l C e, RedexOnTop R C -> RedexOnTop R (AppLocal l C e)
| GlobalFunOnTop : forall R C1 C2, RedexOnTop R C1 -> RedexOnTop R (AppGlobal C1 C2)
| GlobalArgOnTop : forall R C1 C2, RedexOnTop R C2 -> RedexOnTop R (AppGlobal (RecGlobal C1) C2).
Global Hint Constructors RedexOnTop : Chor.
Ltac ListClean :=
repeat match goal with
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H1 : ?P, H2 : ~?P |- _ ] => destruct (H2 H1)
| [ H : ~ In ?a (?b :: ?c) |- _ ] =>
assert (b <> a) by (let eq:= fresh in intro eq; apply H; left; exact eq);
assert (~ In a c) by (let i := fresh in intro i; apply H; right; exact i);
clear H
end.
Lemma RStepOnTop : forall (R : Redex) (B : list Loc) (C1 C2 : Chor),
RChorStep R B C1 C2 ->
exists C1' C2', C1 C1' /\ C2 C2' /\ RChorStep R B C1' C2' /\ RedexOnTop R C1'.
Proof using.
intros R B C1 C2 step; induction step.
all: try(eexists; eexists; split; [|split; [|split]]; eauto with Chor; fail).
all: repeat match goal with
| [ IH : exists C1' C2', ?C1 C1' /\ ?C2 C2' /\ RChorStep ?R ?B C1' C2'
/\ RedexOnTop ?R C1' |- _ ] =>
let C1' := fresh "C" in
let C2' := fresh "C" in
let eqv1 := fresh "eqv" in
let eqv2 := fresh "eqv" in
let step := fresh "step" in
let ontop := fresh "ontop" in
destruct IH as [C1' [C2' [eqv1 [eqv2 [step ontop]]]]]
end.
- induction ontop.
all: inversion step0; subst; ListClean.
all: try (exfalso; eapply NoIStepInList; eauto; eauto with Chor; InList; fail).
all: eexists; eexists; split; [|split;[|split]]; [| | | eauto with Chor];
try match goal with
| [ |- RChorStep _ _ _ _ ] => auto with Chor
end;