Commit 12990f1a authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Added simulation of equivalence for full chor steps.

parent 687237f2
......@@ -2403,7 +2403,206 @@ Module Choreography (Import E : Expression) (L : Locations).
(* intros l n; unfold ValueSubst. destruct (L.eq_dec l2 l); [|apply VarToOpenVal]. *)
(* destruct n; [apply ValToOpenVal; auto|apply VarToOpenVal]. *)
(* - *)
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)
| ROSendE : forall p e1 e2 q, RedexOf p (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)
| ROArg : forall l R, RedexOf l R -> RedexOf l (RArg R)
| ROFun : forall l R, RedexOf l R -> RedexOf l (RFun R).
Global Hint Constructors RedexOf: Chor.
Lemma UNoIStepInList : forall p B R,
In p B ->
RedexOf p R ->
forall C1 C2, ~ChorStep R B C1 C2.
Proof using.
intros p B R H H0 C1 C2 step; induction step; inversion H0; subst;
match goal with
| [ i : In ?p ?B, n : ~ In ?p ?B |- False ] =>
destruct (n 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 UNoDoneIStepInList : forall p B,
In p B ->
forall e1 e2 C1 C2, ~ChorStep (RDone p e1 e2) B C1 C2.
Proof using.
intros p B H e1 e2 C1 C2; apply UNoIStepInList with (p := p); auto; apply RODone.
Qed.
Corollary UNoSendEIStepInList1 : forall p B,
In p B ->
forall e1 e2 C1 C2 q, ~ChorStep (RSendE p e1 e2 q) B C1 C2.
Proof using.
intros p B H q e1 e2 C1 C2; apply UNoIStepInList with (p := p); auto; apply ROSendE.
Qed.
Corollary UNoSendVIStepInList1 : forall p B,
In p B ->
forall v q C1 C2, ~ChorStep (RSendV p v q) B C1 C2.
Proof using.
intros p B H v q C1 C2; apply UNoIStepInList with (p := p); auto; apply ROSendV1.
Qed.
Corollary UNoSendVIStepInList2 : forall B q,
In q B ->
forall p v C1 C2, ~ChorStep (RSendV p v q) B C1 C2.
Proof using.
intros B q H p v C1 C2; apply UNoIStepInList with (p := q); auto; apply ROSendV2.
Qed.
Corollary UNoIfEIStepInList : forall p B,
In p B ->
forall e1 e2 C1 C2, ~ChorStep (RIfE p e1 e2) B C1 C2.
Proof using.
intros p B H e1 e2 C1 C2; apply UNoIStepInList with (p := p); auto; apply ROIfE.
Qed.
Corollary UNoIfTTStepInList : forall p B,
In p B ->
forall C1 C2, ~ChorStep (RIfTT p) B C1 C2.
Proof using.
intros p B H C1 C2; apply UNoIStepInList with (p := p); auto; apply ROIfTT.
Qed.
Corollary UNoIfFFStepInList : forall p B,
In p B ->
forall C1 C2, ~ChorStep (RIfFF p) B C1 C2.
Proof using.
intros p B H C1 C2; apply UNoIStepInList with (p := p); auto; apply ROIfFF.
Qed.
Corollary UNoSyncStepInList1 : forall p B,
In p B ->
forall d q C1 C2, ~ChorStep (RSync p d q) B C1 C2.
Proof using.
intros p B H q C1 C2; apply UNoIStepInList with (p := p); auto; constructor.
Qed.
Corollary UNoSyncStepInList2 : forall B q,
In q B ->
forall p d C1 C2, ~ChorStep (RSync p d q) B C1 C2.
Proof using.
intros B q H p C1 C2; apply UNoIStepInList with (p := q); auto; constructor.
Qed.
Corollary UNoLDefStepInList : forall B p,
In p B ->
forall e C1 C2, ~ChorStep (RDefLocal p e) B C1 C2.
Proof using.
intros B p H e C1 C2; apply UNoIStepInList with (p := p); auto; constructor.
Qed.
Global Hint Resolve ChorStepRearrange UNoDoneIStepInList : Chor.
Global Hint Resolve UNoSendEIStepInList1 UNoSendVIStepInList1 UNoSendVIStepInList2 : Chor.
Global Hint Resolve UNoIfEIStepInList UNoIfTTStepInList UNoIfFFStepInList: Chor.
Global Hint Resolve UNoSyncStepInList1 UNoSyncStepInList2 UNoLDefStepInList : Chor.
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.
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.
Theorem EquivSimulation : forall C1 C2, C1 C2 -> forall R B C1',
ChorStep R B C1 C1' -> exists C2', ChorStep 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 : ChorStep ?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', ChorStep R B ?C C' -> exists C2', ChorStep R B ?C2 C2' /\ C' C2', H : ChorStep ?R ?B ?C ?C' |- _ ] =>
lazymatch goal with
| [ _ : ChorStep 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 UNoIStepInList; eauto; eauto with Chor; InList; fail).
all: try (eexists; split; [repeat econstructor |]; eauto with Chor; try NotInList; auto; try (eapply ChorStepRearrange; eauto with Chor; intros q; split; unfold In; intro i; tauto); fail).
(* - apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst. *)
(* - 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') C12); 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 CAppGlobalStep; 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 (CSendVStep 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.
apply CSendIStep. apply CSendVStep; auto; NotInList.
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.
apply CIfIStep; apply CSendVStep; auto; NotInList.
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 CSendVStep; 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.
End Choreography.
......@@ -81,22 +81,6 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
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.
......@@ -118,23 +102,26 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
- 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.
Inductive RestrictedRedexOf : Loc -> Redex -> Prop :=
| RRODone : forall p e1 e2, RestrictedRedexOf p (RDone p e1 e2)
| RROIfE : forall p e1 e2, RestrictedRedexOf p (RIfE p e1 e2)
| RROIfTT : forall p, RestrictedRedexOf p (RIfTT p)
| RROIfFF : forall p, RestrictedRedexOf p (RIfFF p)
| RROSendE1 : forall p e1 e2 q, RestrictedRedexOf p (RSendE p e1 e2 q)
| RROSendE2 : forall p e1 e2 q, RestrictedRedexOf q (RSendE p e1 e2 q)
| RROSendV1 : forall p v q, RestrictedRedexOf p (RSendV p v q)
| RROSendV2 : forall p v q, RestrictedRedexOf q (RSendV p v q)
| RROSync1 : forall p d q, RestrictedRedexOf p (RSync p d q)
| RROSync2 : forall p d q, RestrictedRedexOf q (RSync p d q)
| RROLDef : forall l e, RestrictedRedexOf l (RDefLocal l e)
| RRArg : forall l R, RestrictedRedexOf l R -> RestrictedRedexOf l (RArg R)
| RRFun : forall l R, RestrictedRedexOf l R -> RestrictedRedexOf l (RFun R).
Global Hint Constructors RestrictedRedexOf: Chor.
Lemma NoIStepInList : forall p B R,
In p B ->
RedexOf p R ->
RestrictedRedexOf 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;
......@@ -154,49 +141,49 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
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.
intros p B H e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply RRODone.
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.
intros p B H q e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply RROSendE1.
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.
intros B q H p e1 e2 C1 C2; apply NoIStepInList with (p := q); auto; apply RROSendE2.
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.
intros p B H v q C1 C2; apply NoIStepInList with (p := p); auto; apply RROSendV1.
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.
intros B q H p v C1 C2; apply NoIStepInList with (p := q); auto; apply RROSendV2.
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.
intros p B H e1 e2 C1 C2; apply NoIStepInList with (p := p); auto; apply RROIfE.
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.
intros p B H C1 C2; apply NoIStepInList with (p := p); auto; apply RROIfTT.
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.
intros p B H C1 C2; apply NoIStepInList with (p := p); auto; apply RROIfFF.
Qed.
Corollary NoSyncStepInList1 : forall p B,
In p B ->
......@@ -298,16 +285,8 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
(* | [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',
Theorem RestrictedEquivSimulation : 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;
......@@ -450,7 +429,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
- destruct IHstdstep as [R [C2'' [equiv step]]].
exists (RArg R); exists (AppGlobal 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']].
destruct (RestrictedEquivSimulation 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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment