Skip to content

GitLab

Commit 09bf90db authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Finished clean up of code.

parent 04c5dba4
Hide whitespace changes
Inline Side-by-side
CtrlLang.v
View file @ 09bf90db
......@@ -91,6 +91,30 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
| AppGlobal E1 E2 => CtrlExprClosedAbove E1 n m /\
CtrlExprClosedAbove E2 n m
end.
Lemma CtrlExprClosedAboveMono : forall E a b c d,
a <= c -> b <= d -> CtrlExprClosedAbove E a b -> CtrlExprClosedAbove E c d.
Proof using.
intro E; induction E; intros a b c d a_le_c b_le_d clsd; cbn in *;
repeat match goal with
| [ H : _ /\ _ |- _ ] => destruct H
| [|- _ /\_ ] => split
| [H : ?a <= ?b, H' : ExprClosedAbove ?a ?e |- ExprClosedAbove ?b ?e ] =>
apply Nat.lt_eq_cases in H; destruct H; subst; auto;
apply ExprClosedAboveMono with (m := a); auto
| [IH : forall a b c d, a <= c -> b <= d ->
CtrlExprClosedAbove ?E a b -> CtrlExprClosedAbove ?E c d,
H : ?a <= ?c, H' : ?b <= ?d, H'' : CtrlExprClosedAbove ?E ?a ?b
|- CtrlExprClosedAbove ?E ?c ?d ] =>
apply (IH a b c d H H' H'')
| [H : ?a <= ?b |- context[S ?b]] =>
lazymatch goal with
| [_ : S a <= S b |- _ ] => fail
| _ => assert (S a <= S b) by (apply le_n_S in H; exact H)
end
end; auto.
apply lt_le_trans with (m := a); auto.
Qed.
(* RENAMING *)
......@@ -109,6 +133,17 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
Proof using.
intros ξ1 ξ2 ext_eq n; destruct n; cbn; auto.
Qed.
Lemma UpMono : forall ξ, (forall k l, ξ k < ξ l -> k < l) ->
forall k l, UpRename ξ k < UpRename ξ l -> k < l.
Proof using.
intros ξ mono' k l k_lt_l; unfold UpRename in k_lt_l.
destruct k; destruct l.
1,3: inversion k_lt_l.
apply Nat.lt_0_succ.
apply lt_n_S; apply lt_S_n in k_lt_l; apply mono'; auto.
Qed.
Fixpoint CtrlExprLocalRename (E : CtrlExpr) (ξ : nat -> nat) :=
match E with
......@@ -216,6 +251,52 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
all: intro n; destruct n; cbn; auto; destruct n; cbn; auto.
Qed.
Lemma CtrlExprClosedAboveGlobalRenaming : forall E ξ n m,
CtrlExprClosedAbove E n m -> (forall k l, k < l -> ξ k < ξ l) ->
CtrlExprClosedAbove (E ⟨ceg| ξ⟩) (ξ n) m.
Proof using.
intro E; induction E; try rename n into x; intros ξ n m clsd mono; cbn in *;
repeat match goal with
| [ H : _ /\ _ |- _] => destruct H
| [|- _ /\ _ ] => split
end; auto.
- apply IHE with (ξ := UpRename ξ) in clsd; auto.
intros k l k_lt_l; unfold UpRename.
destruct k. all: destruct l; [inversion k_lt_l|].
apply Nat.lt_0_succ. apply lt_S_n in k_lt_l. apply lt_n_S. apply mono; auto.
- apply IHE with (ξ := UpRename (UpRename ξ)) in clsd; auto.
unfold UpRename.
intros k l k_lt_l; destruct k.
all: destruct l; [inversion k_lt_l|].
apply Nat.lt_0_succ.
destruct k. apply lt_n_S. destruct l.
apply lt_S_n in k_lt_l; inversion k_lt_l. apply Nat.lt_0_succ.
destruct l. apply lt_S_n in k_lt_l; inversion k_lt_l.
repeat apply lt_S_n in k_lt_l; repeat apply lt_n_S; auto.
Qed.
Lemma CtrlExprClosedAboveGlobalRenaming' : forall E ξ n m,
CtrlExprClosedAbove (E ⟨ceg| ξ⟩) (ξ n) m -> (forall k l, ξ k < ξ l -> k < l) ->
CtrlExprClosedAbove E n m.
Proof using.
intro E; induction E; try rename n into x; intros ξ n m clsd mono; cbn in *;
repeat match goal with
| [ H : _ /\ _ |- _] => destruct H
| [|- _ /\ _ ] => split
| [ IH : forall ξ n m, CtrlExprClosedAbove (?E1 ⟨ceg|ξ⟩) (ξ n) m ->
(forall k l, ξ k < ξ l -> k < l) -> CtrlExprClosedAbove ?E1 n m,
H : CtrlExprClosedAbove (?E1 ⟨ceg|?ξ⟩) (?ξ ?n) ?m,
H' : forall k l, ?ξ k < ?ξ l -> k < l
|- CtrlExprClosedAbove ?E1 ?n ?m ] =>
apply (IH ξ n m H H')
end; auto.
- apply IHE with (ξ := UpRename ξ); cbn; auto.
apply UpMono; auto.
- apply IHE with (ξ := UpRename (UpRename ξ)); cbn; auto.
apply UpMono. apply UpMono. auto.
Qed.
(* SUBSTITUTION *)
Fixpoint CtrlExprLocalSubst (E : CtrlExpr) (σ : nat -> Expr) :=
......@@ -2198,6 +2279,13 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
intros d L adcl; induction adcl; constructor; auto.
Qed.
Lemma DirectionUnique : forall d1 d2 L,
AllowDirectedChoiceLabel d1 L -> AllowDirectedChoiceLabel d2 L -> d1 = d2.
Proof using.
intros d1 d2 R adcl1; revert d2; induction adcl1; intros d2 adcl2;
inversion adcl2; subst; auto.
Qed.
(*
We also have to know that everything is under the same stack of Arg and Fun
constructors. We define a partial equivalence relation that tells us when two labels
......@@ -3775,5 +3863,7 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
exists E1; split; auto. apply H7; auto.
Qed.
Definition DeadlockFree : ConSystem -> Prop :=
fun Π => forall Ls Π', SystemSteps Π Ls Π' -> ValueSystem Π' \/ exists L Π'', SystemStep Π' L Π''.
End CtrlLang.
EndPointProjection.v
View file @ 09bf90db
This source diff could not be displayed because it is too large. You can view the blob instead.
Pirouette.v
View file @ 09bf90db
......@@ -375,18 +375,18 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
| S n => (f n) ⟨global| S⟩
end.
Definition PirExprUpSubstForExpr : (nat -> PirExpr) -> Loc -> nat -> PirExpr :=
Definition PirExprUpSubstAllLocal : (nat -> PirExpr) -> Loc -> nat -> PirExpr :=
fun f l n => (f n) ⟨local|fun l' m => if L.eq_dec l l' then S m else m⟩.
Fixpoint PirExprSubst (C : PirExpr) (σ : nat -> PirExpr) :=
match C with
| Done l e => Done l e
| Var n => σ n
| Send l1 e l2 C => Send l1 e l2 (PirExprSubst C (PirExprUpSubstForExpr σ l2))
| Send l1 e l2 C => Send l1 e l2 (PirExprSubst C (PirExprUpSubstAllLocal σ l2))
| If l e C1 C2 => If l e (PirExprSubst C1 σ) (PirExprSubst C2 σ)
| Sync l1 d l2 C => Sync l1 d l2 (PirExprSubst C σ)
| DefLocal l C1 C2 => DefLocal l (PirExprSubst C1 σ) (PirExprSubst C2 (PirExprUpSubstForExpr σ l))
| FunLocal l C => FunLocal l (PirExprSubst C (PirExprUpSubst(PirExprUpSubstForExpr σ l)))
| DefLocal l C1 C2 => DefLocal l (PirExprSubst C1 σ) (PirExprSubst C2 (PirExprUpSubstAllLocal σ l))
| FunLocal l C => FunLocal l (PirExprSubst C (PirExprUpSubst(PirExprUpSubstAllLocal σ l)))
| FunGlobal C => FunGlobal (PirExprSubst C (PirExprUpSubst (PirExprUpSubst σ)))
| AppLocal l C e => AppLocal l (PirExprSubst C σ) e
| AppGlobal C1 C2 => AppGlobal (PirExprSubst C1 σ) (PirExprSubst C2 σ)
......@@ -400,11 +400,11 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
intros σ1 σ2 H n; unfold PirExprUpSubst; destruct n; cbn; auto. rewrite H; reflexivity.
Qed.
Lemma PirExprUpSubstForExprExt : forall σ1 σ2,
Lemma PirExprUpSubstAllLocalExt : forall σ1 σ2,
(forall n, σ1 n = σ2 n) ->
forall l n, PirExprUpSubstForExpr σ1 l n = PirExprUpSubstForExpr σ2 l n.
forall l n, PirExprUpSubstAllLocal σ1 l n = PirExprUpSubstAllLocal σ2 l n.
Proof using.
intros σ1 σ2 eqv l n; unfold PirExprUpSubstForExpr; rewrite eqv; reflexivity.
intros σ1 σ2 eqv l n; unfold PirExprUpSubstAllLocal; rewrite eqv; reflexivity.
Qed.
Lemma PirExprSubstExt : forall (C : PirExpr) (σ1 σ2 : nat -> PirExpr),
......@@ -415,7 +415,7 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
all: try (erewrite IHC; eauto).
all: try (erewrite IHC1; [erewrite IHC2|]; eauto).
3,4: repeat apply PirExprUpSubstExt; auto.
all: apply PirExprUpSubstForExprExt; auto.
all: apply PirExprUpSubstAllLocalExt; auto.
Qed.
Lemma PirExprSubstUpId : forall n, PirExprUpSubst PirExprIdSubst n = PirExprIdSubst n.
......@@ -423,10 +423,10 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
intro n; unfold PirExprUpSubst; unfold PirExprIdSubst; destruct n; auto.
Qed.
Lemma PirExprUpSubstForExprId : forall l n,
PirExprUpSubstForExpr PirExprIdSubst l n = PirExprIdSubst n.
Lemma PirExprUpSubstAllLocalId : forall l n,
PirExprUpSubstAllLocal PirExprIdSubst l n = PirExprIdSubst n.
Proof using.
intro n; unfold PirExprUpSubstForExpr; unfold PirExprIdSubst; cbn; reflexivity.
intro n; unfold PirExprUpSubstAllLocal; unfold PirExprIdSubst; cbn; reflexivity.
Qed.
Lemma PirExprSubstIdSpec : forall C, C[global|PirExprIdSubst] = C.
......@@ -773,16 +773,16 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
C [global| σ] = C.
Proof using.
intros C; induction C; intros σ m closed_b static_above; cbn in *; auto.
- rewrite (IHC (PirExprUpSubstForExpr σ ℓ2) m); auto.
unfold PirExprUpSubstForExpr.
- rewrite (IHC (PirExprUpSubstAllLocal σ ℓ2) m); auto.
unfold PirExprUpSubstAllLocal.
intros k lt; rewrite static_above; auto.
- destruct closed_b; rewrite (IHC1 σ m); auto; rewrite (IHC2 σ m); auto.
- rewrite (IHC σ m); auto.
- destruct closed_b; rewrite (IHC1 σ m); auto.
rewrite (IHC2 (PirExprUpSubstForExpr σ ℓ) m); auto.
unfold PirExprUpSubstForExpr; intros k lt; rewrite static_above; auto.
rewrite (IHC2 (PirExprUpSubstAllLocal σ ℓ) m); auto.
unfold PirExprUpSubstAllLocal; intros k lt; rewrite static_above; auto.
- rewrite IHC with (n := S m); auto.
intros n n_lt_Sm; unfold PirExprUpSubst; unfold PirExprUpSubstForExpr; destruct n; auto.
intros n n_lt_Sm; unfold PirExprUpSubst; unfold PirExprUpSubstAllLocal; destruct n; auto.
apply lt_S_n in n_lt_Sm; specialize (static_above n n_lt_Sm); rewrite static_above.
cbn; auto.
- rewrite IHC with (n := S (S m)); auto.
......@@ -949,14 +949,14 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
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 PirExprUpSubstForExpr. eapply PirExprLocalRenameClosedAbove; eauto.
unfold PirExprUpSubstAllLocal. eapply PirExprLocalRenameClosedAbove; eauto.
intros k' l k_lt_fp; cbn.
destruct (L.eq_dec ℓ2 l); subst; auto. apply Lt.lt_n_S; auto.
- eapply IHC2; eauto. intros k k_lt_n.
unfold PirExprUpSubstForExpr. eapply PirExprLocalRenameClosedAbove; eauto.
unfold PirExprUpSubstAllLocal. eapply PirExprLocalRenameClosedAbove; eauto.
intros k' l k_lt_fp; cbn.
destruct (L.eq_dec ℓ l); subst; auto. apply Lt.lt_n_S; auto.
- unfold PirExprUpSubst; unfold PirExprUpSubstForExpr.
- unfold PirExprUpSubst; unfold PirExprUpSubstAllLocal.
eapply IHC; eauto.
intros k lt_k_Sn.
destruct k. constructor. apply Nat.lt_0_succ.
......@@ -1248,7 +1248,7 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
intros σ C1 C2 eqv; revert σ; induction eqv; intro σ; cbn; auto with PirExpr.
transitivity (C2 [global| σ]); auto.
apply SmartSwapSendSend; auto. erewrite PirExprSubstExt; [reflexivity|].
intro n; unfold PirExprUpSubstForExpr.
intro n; unfold PirExprUpSubstAllLocal.
repeat rewrite PirExprLocalRenameFusion. apply PirExprLocalRenameExtensional.
intros l' m; destruct (L.eq_dec l2 l'); destruct (L.eq_dec l4 l'); subst;
try match goal with
......@@ -1273,10 +1273,10 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
Lemma WeakSubstUpForExprExt : forall (σ1 σ2 : nat -> PirExpr),
(forall n, σ1 n ≡ σ2 n) ->
forall l n, PirExprUpSubstForExpr σ1 l n ≡ PirExprUpSubstForExpr σ2 l n.
forall l n, PirExprUpSubstAllLocal σ1 l n ≡ PirExprUpSubstAllLocal σ2 l n.
Proof using.
intros σ1 σ2 eqv l n.
unfold PirExprUpSubstForExpr. apply EquivStableLocalRename; auto.
unfold PirExprUpSubstAllLocal. apply EquivStableLocalRename; auto.
Qed.
Global Hint Resolve WeakSubstUpForExprExt : PirExpr.
......@@ -1302,7 +1302,7 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
- apply SmartSwapSendSend; auto.
apply WeakSubstExt'.
(* At this point, we're done reasoning aobut C1 and C2. *)
intro n. unfold PirExprUpSubstForExpr. repeat rewrite PirExprLocalRenameFusion.
intro n. unfold PirExprUpSubstAllLocal. repeat rewrite PirExprLocalRenameFusion.
transitivity (σ2 n ⟨local| fun l n0 => if L.eq_dec l4 l
then S (if L.eq_dec l2 l then S n0 else n0)
else if L.eq_dec l2 l then S n0 else n0⟩).
......@@ -1416,6 +1416,49 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
all: repeat (right; auto).
Qed.
Lemma PirExprClosedAboveLocsInPirExpr : forall C f g n,
PirExprClosedAbove f n C ->
(forall l, In l (LocsInPirExpr C) -> f l = g l) ->
PirExprClosedAbove g n C.
Proof using.
intro C; induction C; intros f g m clsd eq;
inversion clsd; subst; constructor; auto; cbn in *;
repeat match goal with
| [ H : forall l', ?l = l' \/ ?P -> f l' = g l' |- _ ] =>
assert (f l = g l) by apply (H l ltac:(left; reflexivity));
let l'' := fresh "l" in
let H' := fresh in
assert (forall l', P -> f l' = g l')
by (intros l'' H'; apply (H l'' ltac:(right; exact H')));
clear H
| [ H: forall l, False -> _ |- _ ] => clear H
| [ H : ExprClosedAbove (?f ?l) ?e, H' : ?f ?l = ?g ?l'
|- ExprClosedAbove (?g ?l') ?e] => rewrite <- H'; exact H
| [ H : forall l', In l' (?a ++ ?b) -> ?P |- _ ] =>
let H' := fresh in
let l' := fresh "l" in
let H1 := fresh in
assert (forall l', In l' a -> P) as H1
by (intros l' H'; apply H; apply in_or_app; left; exact H');
assert (forall l', In l' b -> P)
by (intros l' H'; apply H; apply in_or_app; right; exact H');
clear H
| [IH : forall f g n, PirExprClosedAbove f n ?C ->
(forall l, In l (LocsInPirExpr ?C) -> f l = g l) ->
PirExprClosedAbove g n ?C,
H1 : PirExprClosedAbove ?f ?n ?C,
H2 : forall l, In l (LocsInPirExpr ?C) -> ?f l = ?g l
|- PirExprClosedAbove ?g ?n ?C] =>
apply (IH f g n H1 H2)
end; auto.
- apply IHC with (f := fun r => if L.eq_dec ℓ2 r then S (f ℓ2) else f r); auto.
intros l'' i; destruct (L.eq_dec ℓ2 l''); subst; auto.
- apply IHC2 with (f := fun r => if L.eq_dec ℓ r then S (f ℓ) else f r); auto.
intros l'' i; destruct (L.eq_dec ℓ l''); subst; auto.
- apply IHC with (f := fun r => if L.eq_dec ℓ r then S (f ℓ) else f r); auto.
intros l'' i; destruct (L.eq_dec ℓ l''); subst; auto.
Qed.
(* OPERATIONAL SEMANTICS VIA A LABELED-TRANSITION SYSTEM *)
(*
......@@ -1775,11 +1818,11 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
_ \/ exists m, In ?p (LocsInPirExpr (?σ m))] => right; exists n; auto
end.
all: try (left; right; apply in_or_app; auto; fail).
- right. unfold PirExprUpSubstForExpr in H0. exists n0.
- right. unfold PirExprUpSubstAllLocal in H0. exists n0.
rewrite PirExprLocalRenameSpec in H0. rewrite <- LocsInPirExprLocalSubst in H0; auto.
- right. unfold PirExprUpSubstForExpr in H0. exists n0.
- right. unfold PirExprUpSubstAllLocal in H0. exists n0.
rewrite PirExprLocalRenameSpec in H0. rewrite <- LocsInPirExprLocalSubst in H0; auto.
- right. unfold PirExprUpSubstForExpr in H0.
- right. unfold PirExprUpSubstAllLocal in H0.
unfold PirExprUpSubst in H0; destruct n0. cbn in H0; destruct H0.
rewrite LocsInPirExprRenaming in H0.
rewrite PirExprLocalRenameSpec in H0; rewrite <- LocsInPirExprLocalSubst in H0.
......
TypedPirouette.v
View file @ 09bf90db
......@@ -298,14 +298,14 @@ Module TypedPirouette (Import L : Locations) (Import LL : LocalLang)
try rename σ into ρ; intros σ Δ2 styping; cbn; auto with PirExpr.
- apply TSend with (τ := τ); auto. apply IHtyping.
unfold PirExprSubstTyping. intro n. unfold PirExprSubstTyping in styping.
unfold PirExprUpSubstForExpr. apply TypeLocalWeakening with (Γ1 := Γ); auto.
unfold PirExprUpSubstAllLocal. apply TypeLocalWeakening with (Γ1 := Γ); auto.
intros ℓ n0; destruct (L.eq_dec ℓ₂ ℓ); subst; auto.
- apply TDefLocal with (τ := τ). apply IHtyping1; auto.
unfold PirExprUpSubstForExpr. apply IHtyping2. unfold PirExprSubstTyping.
unfold PirExprUpSubstAllLocal. apply IHtyping2. unfold PirExprSubstTyping.
intro n; apply TypeLocalWeakening with (Γ1 := Γ); auto.
intros ℓ' n0; destruct (L.eq_dec ℓ ℓ'); auto.
- apply TFunLocal; apply IHtyping. unfold PirExprSubstTyping in *; intro n.
unfold PirExprUpSubst; unfold PirExprUpSubstForExpr; destruct n; cbn; auto.
unfold PirExprUpSubst; unfold PirExprUpSubstAllLocal; destruct n; cbn; auto.
apply TVar.
apply TypePirExprWeakening with (Δ1 := Δ2); auto.
apply TypeLocalWeakening with (Γ1 := Γ); auto.
......
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