Commit 472decdd authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Deadlock freedom.

parent 1ce866ff
......@@ -1552,6 +1552,11 @@ Module Choreography (Import E : Expression) (L : Locations).
ChorStep R B (Sync l1 d l2 C1) (Sync l1 d l2 C2).
Global Hint Constructors ChorStep : Chor.
Inductive ChorSteps : list Redex -> list Loc -> Chor -> Chor -> Prop :=
| NoChorSteps : forall B C, ChorSteps [] B C C
| AddChorStep : forall R Rs B C1 C2 C3,
ChorStep R B C1 C2 -> ChorSteps Rs B C2 C3 -> ChorSteps (R :: Rs) B C1 C3.
Global Hint Constructors ChorSteps : Chor.
Lemma ChorStepSub : forall R B1 C1 C2,
ChorStep R B1 C1 C2 -> forall B2, (forall q, In q B2 -> In q B1) -> ChorStep R B2 C1 C2.
......@@ -1780,6 +1785,201 @@ Module Choreography (Import E : Expression) (L : Locations).
destruct n; auto. destruct n; auto. cbn in i; destruct i.
Qed.
Lemma ThreadNamesAfterSteps : forall Rs B C1 C2 l,
ChorSteps Rs B C1 C2 ->
In l (ThreadNames C2) ->
In l (ThreadNames C1).
Proof using.
intros Rs; induction Rs as [|R Rs]; intros B C1 C2 l steps i;
inversion steps; subst; auto.
apply IHRs with (l := l) in H5; auto.
apply ThreadNamesAfterStep with (l := l) in H1; auto.
Qed.
Lemma ChorExprRenameClosedBelow : forall C f g ξ n,
(forall k l, k < f l -> ξ l k < g l) ->
ChorClosedBelow f n C ->
ChorClosedBelow g n (C ce| ξ⟩).
Proof using.
intros C; induction C; try rename n into x; intros f g ξ n ξ_bdd C_clsd;
inversion C_clsd; subst; auto; constructor; auto; try (eapply ExprRenameClosedBelow; eauto; fail).
all: try (eapply IHC; eauto; fail);
try (eapply IHC1; eauto; fail);
try (eapply IHC2; eauto; fail).
- eapply IHC; eauto. cbn; intros k p k_lt_fp.
unfold ChorUpExprRename. unfold ExprUpRename. destruct (L.eq_dec l0 p); subst.
destruct k. apply Nat.lt_0_succ. apply Lt.lt_S_n in k_lt_fp.
apply Lt.lt_n_S. 1,2: apply ξ_bdd; auto.
- eapply IHC2; eauto. cbn; intros k p k_lt_fp.
unfold ChorUpExprRename. unfold ExprUpRename. destruct (L.eq_dec l p); subst.
destruct k. apply Nat.lt_0_succ. apply Lt.lt_S_n in k_lt_fp.
apply Lt.lt_n_S. 1,2: apply ξ_bdd; auto.
- eapply IHC; eauto. cbn; intros k p k_lt_fp.
unfold ChorUpExprRename. unfold ExprUpRename. destruct (L.eq_dec l p); subst.
destruct k. apply Nat.lt_0_succ. apply Lt.lt_S_n in k_lt_fp.
apply Lt.lt_n_S. 1,2: apply ξ_bdd; auto.
Qed.
Lemma ChorExprSubstClosedBelow : forall C f g σ n,
(forall k l, k < f l -> ExprClosedBelow (g l) (σ l k)) ->
ChorClosedBelow f n C ->
ChorClosedBelow g n (C [ce| σ]).
Proof using.
intro C; ChorInduction C; try rename n into x; intros f g σ n σ_clsd C_clsd;
inversion C_clsd; subst; constructor; auto; try (eapply ExprSubstClosedBelow; eauto; fail).
all: try (eapply IHC; eauto; fail); try (eapply IHC1; eauto; fail);
try (eapply IHC2; eauto; fail).
- eapply IHC; eauto.
intros k p k_lt_fp; cbn in *. unfold ChorUpExprSubst; destruct (L.eq_dec l' p); subst.
destruct k. apply ExprVarClosed. apply Nat.lt_0_succ.
eapply ExprRenameClosedBelow with (n := g p).
intros k' lt_k'_fp; apply Lt.lt_n_S; auto.
1,2: apply σ_clsd; auto; apply Lt.lt_S_n in k_lt_fp; auto.
- eapply IHC2; eauto; cbn.
intros k p k_lt_fp. unfold ChorUpExprSubst.
destruct (L.eq_dec l p); subst.
destruct k. rewrite ExprVarClosed. apply Nat.lt_0_succ.
eapply ExprRenameClosedBelow with (n := g p).
intros k' lt_k'_fp; apply Lt.lt_n_S; auto.
1,2: apply σ_clsd; auto; apply Lt.lt_S_n in k_lt_fp; auto.
- eapply IHC; eauto; cbn.
intros k p k_lt_fp. unfold ChorUpExprSubst.
destruct (L.eq_dec l p); subst.
destruct k. rewrite ExprVarClosed. apply Nat.lt_0_succ.
eapply ExprRenameClosedBelow with (n := g p).
intros k' lt_k'_fp; apply Lt.lt_n_S; auto.
1,2: apply σ_clsd; auto; apply Lt.lt_S_n in k_lt_fp; auto.
Qed.
Lemma ChorClosedBelowRename : forall C f n m ξ,
ChorClosedBelow f n C ->
(forall k, k < n -> ξ k < m) ->
ChorClosedBelow f m (C c|ξ⟩).
Proof using.
intros C; ChorInduction C; try rename n into x; intros f n m ξ cclosed ξ_bdd;
inversion cclosed; subst; try (constructor; auto).
all: try (eapply IHC; eauto; fail); try (eapply IHC1; eauto; fail);
try (eapply IHC2; eauto; fail).
- eapply IHC; eauto. unfold ChorUpRename.
intros k k_lt_Sn; destruct k. apply Nat.lt_0_succ.
apply Lt.lt_S_n in k_lt_Sn. apply Lt.lt_n_S. auto.
- eapply IHC; eauto. unfold ChorUpRename.
intros k k_lt_Sn; destruct k. apply Nat.lt_0_succ.
apply Lt.lt_S_n in k_lt_Sn. apply Lt.lt_n_S. destruct k.
apply Nat.lt_0_succ. apply Lt.lt_S_n in k_lt_Sn. apply Lt.lt_n_S. auto.
Qed.
Lemma ChorClosedBelowSubst : forall C f n m σ,
ChorClosedBelow f n C ->
(forall k, k < n -> ChorClosedBelow f m (σ k)) ->
ChorClosedBelow f m (C [c| σ]).
Proof using.
intros C; ChorInduction C; try rename n into x; intros f n m σ c_clsd σ_clsd;
inversion c_clsd; subst; cbn ;auto; try (constructor; auto).
all: try (eapply IHC; eauto; fail); try (eapply IHC1; eauto; fail);
try (eapply IHC2; eauto; fail).
- eapply IHC; eauto. intros k k_lt_n.
unfold ChorUpSubstForExpr. eapply ChorExprRenameClosedBelow; eauto.
intros k' p k_lt_fp; cbn.
destruct (L.eq_dec l' p); subst; auto. apply Lt.lt_n_S; auto.
- eapply IHC2; eauto. intros k k_lt_n.
unfold ChorUpSubstForExpr. eapply ChorExprRenameClosedBelow; eauto.
intros k' p k_lt_fp; cbn.
destruct (L.eq_dec l p); subst; auto. apply Lt.lt_n_S; auto.
- unfold ChorUpSubst; unfold ChorUpSubstForExpr.
eapply IHC; eauto.
intros k lt_k_Sn.
destruct k. constructor. apply Nat.lt_0_succ.
apply ChorClosedBelowRename with (n := m).
apply Lt.lt_S_n in lt_k_Sn.
apply ChorExprRenameClosedBelow with (f := f); auto.
intros k' p k'_lt_fp. destruct (L.eq_dec l p); subst; auto.
apply lt_n_S; auto.
intros k0 H; apply lt_n_S; auto.
- eapply IHC; eauto. unfold ChorUpSubst.
intros k lt_k_SSn.
destruct k; [constructor; apply Nat.lt_0_succ|].
apply lt_S_n in lt_k_SSn.
destruct k; [constructor; apply lt_n_S; auto; apply Nat.lt_0_succ|].
apply ChorClosedBelowRename with (n := S m).
apply lt_S_n in lt_k_SSn.
apply ChorClosedBelowRename with (n := m); auto.
1,2: intros k' k'_lt_m; apply lt_n_S; auto.
Qed.
Lemma ChorClosedBelowAfterStep : forall R B C1 C2 f n,
ChorStep R B C1 C2 ->
ChorClosedBelow f n C1 ->
ChorClosedBelow f n C2.
Proof using.
intros R B C1 C2 f n step; revert f n; induction step; intros f n clsd;
inversion clsd; subst; auto; try (constructor; auto);
try (eapply ExprClosedAfterStep; eauto; fail);
try (eapply IHC; eauto; fail); try (eapply IHC1; eauto; fail);
try (eapply IHC2; eauto; fail).
- eapply ChorExprSubstClosedBelow; eauto; cbn; intros k p k_lt_fp.
unfold ValueSubst. destruct (L.eq_dec l2 p); subst.
destruct k.
destruct (f p). apply ExprValuesClosed; auto.
eapply ExprClosedBelowMono; [|apply ExprValuesClosed; auto]. apply Nat.lt_0_succ.
apply lt_S_n in k_lt_fp. all: apply ExprVarClosed; auto.
- eapply ChorExprSubstClosedBelow; eauto; cbn; intros k p k_lt_fp.
unfold ValueSubst. destruct (L.eq_dec l p); subst.
destruct k.
destruct (f p). apply ExprValuesClosed; auto.
eapply ExprClosedBelowMono; [|apply ExprValuesClosed; auto]. apply Nat.lt_0_succ.
apply lt_S_n in k_lt_fp. all: apply ExprVarClosed; auto.
- inversion H4; subst. apply ChorClosedBelowSubst with (n := S n); eauto.
eapply ChorExprSubstClosedBelow; eauto; cbn.
intros k p k_lt_p. unfold ValueSubst. destruct (L.eq_dec l p); subst.
destruct k; auto. apply lt_S_n in k_lt_p. 1,2: apply ExprVarClosed; auto.
intros k k_lt_Sn. unfold AppLocalSubst. destruct k; auto.
apply lt_S_n in k_lt_Sn; constructor; auto.
- inversion H4; subst. eapply ChorClosedBelowSubst with (n := S (S n)); auto.
intros k k_lt_SSn. unfold AppGlobalSubst. destruct k; auto.
destruct k; auto. do 2 apply lt_S_n in k_lt_SSn; constructor; auto.
Qed.
Lemma ChorClosedAfterStep : forall R B C1 C2,
ChorStep R B C1 C2 ->
ChorClosed C1 ->
ChorClosed C2.
Proof using.
intros R B C1 C2 H H0. unfold ChorClosed in *.
eapply ChorClosedBelowAfterStep; eauto.
Qed.
Lemma ChorClosedAfterSteps : forall Rs B C1 C2,
ChorClosed C1 ->
ChorSteps Rs B C1 C2 ->
ChorClosed C2.
Proof using.
intros Rs; induction Rs as [|R Rs]; intros B C1 C2 closed1 steps;
inversion steps; subst; auto.
apply ChorClosedAfterStep in H1; auto. eapply IHRs in H5; eauto.
Qed.
Lemma InvolvedWithThreadNames : forall R B C1 C2,
ChorStep R B C1 C2 ->
forall l, InvolvedWithRedex R l -> In l (ThreadNames C1).
Proof using.
intros R B C1; revert R B; ChorInduction C1; intros R B C' step p inv;
inversion step; subst; cbn in *; auto;
repeat match goal with
| [ H : False |- _ ] => destruct H
| [ H : _ \/ _ |- _] => destruct H; subst
| [ |- ?a = ?a \/ _ ] => left; reflexivity
| [ |- _ \/ ?a = ?a \/ _ ] => right; left; reflexivity
end; auto.
- right; right; eapply IHC1; eauto.
- right; apply in_or_app; left; eapply IHC0; eauto.
- right; right; eapply IHC1; eauto.
- right; apply in_or_app; left; eapply IHC0; eauto.
- right; eapply IHC1; eauto.
- apply in_or_app; left; eapply IHC0; eauto.
- apply in_or_app; right; eapply IHC2; eauto.
Qed.
(* Describes terms that are allowed in function position *)
Inductive FunctionOK : Chor -> Prop :=
| VarOK : forall n, FunctionOK (Var n)
......
This diff is collapsed.
This diff is collapsed.
......@@ -8,6 +8,7 @@ Module Type Expression.
Definition ExprClosed := ExprClosedBelow 0.
Parameter ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Parameter ExprClosedBelowMono : forall m n e, m < n -> ExprClosedBelow m e -> ExprClosedBelow n e.
Parameter ExprVarClosed : forall n m, ExprClosedBelow n (ExprVar m) <-> m < n.
Parameter IsExprVal : Expr -> bool.
Parameter IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true.
......@@ -91,6 +92,18 @@ Module Type Expression.
Parameter ExprStep : Expr -> Expr -> Prop.
Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Parameter ExprRenameClosedBelow : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e e| ξ⟩).
Parameter ExprSubstClosedBelow : forall e n σ m,
(forall k, k < n -> ExprClosedBelow m (σ k)) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e [e| σ]).
Parameter ExprClosedAfterStep : forall e1 e2 n,
ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
Parameter ExprOpenVal : Expr -> Prop.
Parameter OpenValRename :
forall e ξ, ExprOpenVal e -> ExprOpenVal (e e|ξ⟩).
......
......@@ -437,4 +437,80 @@ Module LambdaCalc <: Expression.
- inversion H; subst. apply IHe in H1; auto.
Qed.
Lemma ExprRenameClosedBelow : forall e n ξ m,
(forall k, k < n -> ξ k < m) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e e| ξ⟩).
Proof using.
intros e; induction e; cbn; try rename n into x; intros n ξ m ξ_bdd clsd_e; auto.
all: repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H
| [ |- _ /\ _ ] => split
end; auto;
try (eapply IHe; eauto; fail);
try (eapply IHe1; eauto; fail);
try (eapply IHe2; eauto; fail);
try (eapply IHe3; eauto; fail).
- destruct n. destruct clsd_e.
destruct (x <=? n) eqn:eq. apply Nat.leb_le in eq.
assert (x < S n) by (apply Lt.le_lt_n_Sm; auto).
destruct m. apply ξ_bdd in H. inversion H.
apply ξ_bdd in H. apply Lt.lt_n_Sm_le in H.
apply Nat.leb_le in H. rewrite H; auto.
destruct clsd_e.
- apply IHe with (n := S n); auto.
intros k k_lt_Sn; unfold ExprUpRename. destruct k. apply Nat.lt_0_succ.
apply Lt.lt_n_S. apply Lt.lt_S_n in k_lt_Sn. apply ξ_bdd; auto.
Qed.
Lemma ExprSubstClosedBelow : forall e n σ m,
(forall k, k < n -> ExprClosedBelow m (σ k)) ->
ExprClosedBelow n e ->
ExprClosedBelow m (e [e| σ]).
Proof using.
intros e; induction e; cbn; try rename n into x; intros n σ m σ_clsd e_clsd; auto;
repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H
| [ |- _ /\ _ ] => split
end; auto.
all: try (eapply IHe; eauto; fail);
try (eapply IHe1; eauto; fail);
try (eapply IHe2; eauto; fail);
try (eapply IHe3; eauto; fail).
- destruct n. destruct e_clsd. destruct (x <=? n) eqn:eq; [|destruct e_clsd].
apply Nat.leb_le in eq. assert (x < S n) by(apply Lt.le_lt_n_Sm; auto).
apply σ_clsd in H; auto.
- apply IHe with (n := S n); auto.
intros k k_lt_Sn; unfold ExprUpSubst; destruct k; cbn; auto.
apply ExprRenameClosedBelow with (n := m).
intros l lt_l_m; apply Lt.lt_n_S; auto.
apply σ_clsd; apply Lt.lt_S_n; auto.
Qed.
Theorem ExprClosedAfterStep : forall e1 e2 n,
ExprStep e1 e2 -> ExprClosedBelow n e1 -> ExprClosedBelow n e2.
Proof using.
intros e1 e2 n step; revert n; induction step; cbn; intros n clsd; auto;
repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H
| [ |- _ /\ _ ] => split
end; auto.
apply ExprSubstClosedBelow with (n := S n); auto.
intros k lt_k_Sn; unfold LCStepSubst. destruct k; auto; cbn.
destruct n. apply Lt.lt_S_n in lt_k_Sn; inversion lt_k_Sn.
apply Lt.lt_S_n in lt_k_Sn.
apply Lt.lt_n_Sm_le in lt_k_Sn. apply Nat.leb_le in lt_k_Sn; rewrite lt_k_Sn; auto.
Qed.
Theorem ExprVarClosed : forall n m, ExprClosedBelow n (ExprVar m) <-> m < n.
intros n m; cbn; split; intro H; destruct n; auto. destruct H.
destruct (m <=? n) eqn:eq. apply Nat.leb_le in eq; unfold lt; apply Le.le_n_S; auto.
destruct H.
inversion H. destruct (m <=? n) eqn:eq; auto.
apply Nat.leb_gt in eq. destruct m; [inversion eq|].
apply Lt.lt_S_n in H. apply Lt.lt_n_Sm_le in eq. apply Lt.le_lt_or_eq in eq.
destruct eq. assert (n < n) by (transitivity m; auto). apply Lt.lt_irrefl in H1; auto.
subst; apply Lt.lt_irrefl in H; auto.
Qed.
End LambdaCalc.
......@@ -18,6 +18,15 @@ Module SoundlyTypedChoreography (E : Expression) (TE : TypedExpression E) (STE :
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem StepsPreservation :
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (Rs : list Redex) (B : list L.t) (C': Chor),
ChorSteps Rs B C C' -> Γ;; Δ c C' ::: τ.
Proof.
apply RelativeStepsPreservation. intros Γ e τ H e' H0.
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem Progress :
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
ChorClosed C -> Γ;; Δ c C ::: τ ->
......
......@@ -382,7 +382,22 @@ Module TypedChoreography (L : Locations) (E : Expression) (TE : TypedExpression
- inversion H4; subst; eapply ChorSubstTypingSpec; eauto.
apply AppGlobalSubstTyping; auto.
Qed.
Theorem RelativeStepsPreservation :
(forall (Γ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
Γ e e ::: τ
-> forall e' : Expr, ExprStep e e'
-> Γ e e' ::: τ) ->
forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (Rs : list Redex) (B : list Loc) (C': Chor),
ChorSteps Rs B C C' -> Γ;; Δ c C' ::: τ.
Proof using.
intros expr_pres Γ Δ C τ typing Rs; revert Γ Δ C τ typing; induction Rs;
intros Γ Δ C τ typing B C' steps; inversion steps; subst; auto.
rename a into R; clear steps; rename H1 into step; rename H5 into steps.
eapply RelativePreservation in step; eauto.
Qed.
Lemma ChorClosedBelowTyping : forall (Γ1 Γ2 : Loc -> nat -> ExprTyp)
(Δ1 Δ2 : nat -> ChorTyp)
......
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