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

Completeness done.

parent 16ce9dad
......@@ -1412,7 +1412,7 @@ Module Choreography (Import E : Expression) (L : Locations).
ChorStep RAppGlobal [] (AppGlobal (RecGlobal C1) C2)
(C1 [c| AppGlobalSubst C1 C2])
| CSyncStep : forall (l1 l2 : Loc) (d : LRChoice) (C : Chor) (B : list Loc),
~ In l1 B -> ~ In l2 B ->
~ In l1 B -> ~ In l2 B -> l1 <> l2 ->
ChorStep (RSync l1 d l2) B (Sync l1 d l2 C) C
| CSyncIStep : forall (l1 l2 : Loc) (d : LRChoice) (C1 C2 : Chor) (B : list Loc) (R : Redex),
ChorStep R (l1 :: l2 :: B) C1 C2 ->
......@@ -1463,6 +1463,151 @@ Module Choreography (Import E : Expression) (L : Locations).
intros q H1; apply H0; auto.
Qed.
Lemma ChorStepSendVDistinguish : forall p v q B C1 C2,
ChorStep (RSendV p v q) B C1 C2 ->
p <> q.
Proof using.
intros p v q B C1 C2 step; dependent induction step;
repeat match goal with
| [ IH : forall a b c, RSendV ?p ?v ?q = RSendV a b c -> _ |- _ ] =>
specialize (IH p v q eq_refl)
end; auto.
Qed.
Lemma ChorStepSyncDistinguish : forall p d q B C1 C2,
ChorStep (RSync p d q) B C1 C2 ->
p <> q.
Proof using.
intros p v q B C1 C2 step; dependent induction step;
repeat match goal with
| [ IH : forall a b c, RSync ?p ?v ?q = RSync a b c -> _ |- _ ] =>
specialize (IH p v q eq_refl)
end; auto.
Qed.
Definition InvolvedWithRedex (R : Redex) (l : L.t) : Prop :=
match R with
| RDone l' e1 e2 => l = l'
| RIfE l' e1 e2 => l = l'
| RIfTT l' => l = l'
| RIfFF l' => l = l'
| RSendE l1 e1 e2 l2 => l = l1
| RSendV l1 v l2 => l = l1 \/ l = l2
| RSync l1 d l2 => l = l1 \/ l = l2
| RDefLocal l' e => l = l'
| RAppLocalE l' e1 e2 => l = l'
| RAppLocal l' e => l = l'
| RAppGlobal => False
end.
Lemma NoChorStepInList : forall p B R,
In p B ->
InvolvedWithRedex R p ->
forall C1 C2, ~ChorStep R B C1 C2.
Proof using.
intros p B R H H0 C1 C2 step; induction step; cbn in 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
| [ H : _ \/ _ |- _ ] => destruct H; subst
| [ H1 : ?P, H2 : ~ ?P |- _ ] => destruct (H2 H1)
| _ => idtac
end.
all: try (apply IHstep; auto; right; right; auto; fail).
all: try (apply IHstep1; auto; right; auto; fail).
all: try match goal with
| [H1 : ?P, H2 : ~?P |- _] => destruct (H2 H1)
end.
all: inversion H.
Qed.
Lemma ThreadNamesExprSubst : forall C σ,
ThreadNames C = ThreadNames (C [ce| σ]).
Proof using.
intro C; ChorInduction C; intros σ; cbn; auto.
all: try (erewrite IHC; eauto; fail).
all: rewrite IHC1 with (σ := σ).
1,3: rewrite IHC2 with (σ := σ); reflexivity.
rewrite IHC2 with (σ := ChorUpExprSubst σ l); reflexivity.
Qed.
Lemma ThreadNamesRenaming : forall C ξ,
ThreadNames (C c| ξ⟩) = ThreadNames C.
Proof using.
intro C; ChorInduction C; intros ξ; cbn; auto.
all: try (erewrite IHC; eauto; fail).
all: rewrite IHC1 with (ξ := ξ); rewrite IHC2 with (ξ := ξ); auto.
Qed.
Lemma ThreadNamesSubst : forall C σ l,
In l (ThreadNames (C [c| σ])) ->
In l (ThreadNames C) \/ exists n, In l (ThreadNames (σ n)).
Proof using.
intro C; ChorInduction C; cbn; intros σ p i; auto;
repeat match goal with
| [ i : _ \/ _ |- _ ] => destruct i; auto
| [ i : In _ (_ ++ _) |- _ ] => apply in_app_or in i
| [ IH: forall σ l, In l (ThreadNames (?C [c|σ])) ->
In l (ThreadNames ?C) \/ (exists n, In l (ThreadNames (σ n))),
H : In ?l (ThreadNames (?C [c|?σ])) |- _ ] =>
lazymatch goal with
| [_ : In l (ThreadNames C) |- _ ] => fail
| [_ : In l (ThreadNames (σ _)) |- _ ] => fail
| _ => let H' := fresh in destruct (IH σ l H) as [H'|H'];
[| let n := fresh "n" in destruct H' as [n H']];
auto
end
| [ H : In ?p (ThreadNames (?σ ?n)) |-
_ \/ exists m, In ?p (ThreadNames (?σ m))] => right; exists n; auto
end.
all: try (left; right; apply in_or_app; auto; fail).
- right. unfold ChorUpSubstForExpr in H0. exists n0.
rewrite ChorExprRenameSpec in H0. rewrite <- ThreadNamesExprSubst in H0; auto.
- right. unfold ChorUpSubstForExpr in H0. exists n0.
rewrite ChorExprRenameSpec in H0. rewrite <- ThreadNamesExprSubst in H0; auto.
- right. unfold ChorUpSubstForExpr in H0.
unfold ChorUpSubst in H0; destruct n0. cbn in H0; destruct H0.
rewrite ThreadNamesRenaming in H0.
rewrite ChorExprRenameSpec in H0; rewrite <- ThreadNamesExprSubst in H0.
exists n0; auto.
- unfold ChorUpSubst in H. destruct n0; [cbn in H; destruct H|].
destruct n0; [cbn in H; destruct H|].
repeat rewrite ThreadNamesRenaming in H. right; exists n0; auto.
- left; apply in_or_app; auto.
- left; apply in_or_app; auto.
Qed.
Lemma ThreadNamesAfterStep : forall R B C1 C2 l,
ChorStep R B C1 C2 ->
In l (ThreadNames C2) ->
In l (ThreadNames C1).
Proof using.
intros R B C1 C2 l step; revert l; induction step;
cbn; intros p i; auto;
repeat match goal with
| [ i : _ \/ _ |- _ ] => destruct i; auto
| [ i : In _ (_ ++ _) |- _ ] => apply in_app_or in i
| [ IH : forall l, In l (ThreadNames ?C2) -> In l (ThreadNames ?C1),
i : In ?l (ThreadNames ?C2) |- _ ] =>
lazymatch goal with
| [ _ : In l (ThreadNames C1) |- _ ] => fail
| _ => pose proof (IH l i); auto
end
end.
rewrite <- ThreadNamesExprSubst in i; auto.
1-6: right; apply in_or_app; auto.
3-7: apply in_or_app; auto.
- rewrite <- ThreadNamesExprSubst in i; auto.
- apply ThreadNamesSubst in i; destruct i.
rewrite <- ThreadNamesExprSubst in H0; auto.
destruct H0 as [n i]; unfold AppLocalSubst in i.
destruct n; [| cbn in i; destruct i]. cbn in i; auto.
- apply ThreadNamesSubst in i; destruct i; auto.
destruct H0 as [n i]; unfold AppGlobalSubst in i.
destruct n; auto. destruct n; auto. cbn in i; destruct i.
Qed.
End Choreography.
Require Export Expression.
Require Export Locations.
Require Import LocationMap.
Require Export Choreography.
Require Export ConcurrentLambda.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Permutation.
From Equations Require Import Equations.
Import ListNotations.
Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : LocationMap L).
Module ICL := (InternalConcurrentLambda E L LM).
Import ICL.
Definition Loc := L.t.
Definition LRChoice : Set := C.LRChoice.
Fixpoint ProjectChor (C : C.Chor) (l : Loc) : option ConExpr :=
match C with
| C.Done p e =>
if L.eq_dec l p
then Some (Ret e)
else Some Unit
| C.Var x => Some (Var x)
| C.Send l1 e l2 C =>
if L.eq_dec l l1
then if L.eq_dec l l2
then None
else match ProjectChor C l with
| Some E => Some (Send l2 e E)
| None => None
end
else if L.eq_dec l l2
then match ProjectChor C l with
| Some E => Some (Recv l1 E)
| None => None
end
else ProjectChor C l
| C.If l' e C1 C2 =>
match ProjectChor C1 l with
| Some E1 =>
match ProjectChor C2 l with
| Some E2 =>
if L.eq_dec l l'
then Some (If e E1 E2)
else ConExprMerge E1 E2
| None => None
end
| None => None
end
| C.Sync p LR q C =>
if L.eq_dec l p
then if L.eq_dec l q
then None
else match ProjectChor C l with
| Some E => Some (Choose q LR E)
| None => None
end
else if L.eq_dec l q
then match ProjectChor C l with
| Some E => match LR with
| C.LChoice => Some (AllowChoiceL p E)
| C.RChoice => Some (AllowChoiceR p E)
end
| None => None
end
else ProjectChor C l
| C.DefLocal p C1 C2 =>
if L.eq_dec l p
then match ProjectChor C1 l, ProjectChor C2 l with
| Some E1, Some E2 => Some (LetRet E1 E2)
| _, _ => None
end
else match ProjectChor C1 l, ProjectChor C2 l with
| Some E1, Some E2 => Some (AppGlobal (RecGlobal (E2 ceg| fun n => 2 + n)) E1) (* Use renaming to make sure nothing binds to this binder *)
| _, _ => None
end
| C.RecLocal p C =>
if L.eq_dec l p
then match ProjectChor C l with
| Some E => Some (RecLocal E)
| None => None
end
else match ProjectChor C l with
| Some E => Some (RecGlobal (E ceg| S)) (* Global so we can feed it a dummy value *)
| None => None
end
| C.RecGlobal C =>
match ProjectChor C l with
| Some E => Some (RecGlobal E)
| None => None
end
| C.AppLocal p C e =>
if L.eq_dec p l
then match ProjectChor C l with
| Some E => Some (AppLocal E e)
| None => None
end
else match ProjectChor C l with
| Some E => Some (AppGlobal E Unit)
| None => None
end
| C.AppGlobal C1 C2 =>
match ProjectChor C1 l, ProjectChor C2 l with
| Some E1, Some E2 => Some (AppGlobal E1 E2)
| _, _ => None
end
end.
Theorem ProjectChorEquivToEq : forall C1 C2 l,
C.equiv C1 C2 -> ProjectChor C1 l = ProjectChor C2 l.
Proof using.
intros C1 C2 l eqv; revert l; induction eqv; intro p; cbn; auto;
repeat match goal with
| [ |- ?a = ?a ] => reflexivity
| [ H : ?a <> ?a |- _ ] => inversion H
| [ d : C.LRChoice |- _ ] => destruct d; cbn in *
| [ H : Some _ = None |- _ ] => inversion H
| [ H : None = Some _ |- _ ] => inversion H
| [ H : Some _ = Some _ |- _ ] => inversion H; subst; clear H; cbn in *
| [ H1 : ?a = Some _, H2 : ?a = None |- _ ] =>
rewrite H2 in H1; inversion H1
| [ |- 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[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
| [ IH : forall l, ProjectChor ?C1 l = ProjectChor ?C2 l |- context[ProjectChor ?C1 ?l]] =>
rewrite (IH l)
| [ |- context[ProjectChor ?C ?l]] =>
lazymatch goal with
| [e : ProjectChor C l = _ |- _ ] => rewrite e; cbn
| _ => let eq := fresh "eq" in
destruct (ProjectChor C l) eqn:eq; cbn
end
| [ |- context[ConExprMerge ?E1 ?E2]] =>
lazymatch goal with
| [e : ConExprMerge E1 E2 = _ |- _ ] => rewrite e; cbn
| _ => let eq := fresh "eq" in
destruct (ConExprMerge E1 E2) eqn:eq; cbn
end
| [H1 : ConExprMerge ?E1 ?E2 = Some ?E5,
H2 : ConExprMerge ?E3 ?E4 = Some ?E6,
H3 : ConExprMerge ?E1 ?E3 = Some ?E7,
H4 : ConExprMerge ?E2 ?E4 = Some ?E8,
H5 : ConExprMerge ?E5 ?E6 = ?a,
H6 : ConExprMerge ?E7 ?E8 = ?b |- _ ] =>
lazymatch goal with
| [ _ : a = b |- _ ] => fail
| _ => let H := fresh in
pose proof (MergeConExprIfs E1 E2 E3 E4 E5 E6 E7 E8 H1 H2 H3 H4) as H;
rewrite H5 in H; rewrite H6 in H
end
| [ H : ConExprMerge ?a ?b = ?c |- _ ] =>
lazymatch goal with
| [_ : ConExprMerge b a = c |- _ ] => fail
| _ => let H' := fresh in pose proof (MergeComm a b) as H'; rewrite H in H';
symmetry in H'
end
| [ H1 : ConExprMerge ?E1 ?E2 = None, H2 : ConExprMerge ?E2 ?E3 = Some ?E4 |- _ ] =>
lazymatch goal with
| [ _ : ConExprMerge E1 E4 = None |- _ ] => fail
| _ => pose proof (MergeAssocNone E1 E2 E3 E4 H1 H2)
end
end.
Qed.
Theorem ProjectChorExprSubst : forall C l E σ,
ProjectChor C l = Some E ->
ProjectChor (C.ChorExprSubst C σ) l = Some (E [cel| σ l]).
Proof using.
intros C; C.ChorInduction C; intros p E σ eq; cbn in *;
repeat match goal with
| [ |- ?a = ?a ] => reflexivity
| [ H : None = Some _ |- _ ] => inversion H
| [ H : Some _ = Some _ |- _ ] => inversion H; subst; clear H; cbn in *
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H : context[L.eq_dec ?a ?b] |- _ ] =>
destruct (L.eq_dec a b); subst; cbn in *
| [ H : context[ProjectChor ?C ?l] |- _ ] =>
lazymatch type of H with
| ProjectChor C l = _ => fail
| _ => lazymatch goal with
| [ H' : ProjectChor C l = _ |- _ ] => rewrite H' in H
| _ => let eq := fresh "eq" in
destruct (ProjectChor C l) eqn:eq; subst; cbn in *
end
end
| [ eq: ProjectChor ?C ?l = Some ?E,
IH : forall l E σ, ProjectChor ?C l = Some E -> ProjectChor (C.ChorExprSubst ?C σ) l = Some (E [cel| σ l]) |- context[ProjectChor (C.ChorExprSubst ?C ?σ) ?l] ] =>
rewrite (IH l E σ eq)
| [ n : ?p <> ?q |- context[C.ChorUpExprSubst σ ?p ?q]] =>
unfold C.ChorUpExprSubst;
destruct (L.eq_dec p q) as [e |_];
[destruct (n (eq_sym e))|]
| [ n : ?q <> ?p |- context[C.ChorUpExprSubst σ ?p ?q]] =>
let e := fresh "e" in
unfold C.ChorUpExprSubst;
destruct (L.eq_dec p q) as [e |_];
[destruct (n (eq_sym e))|]
| [ |- context[C.ChorUpExprSubst σ ?p ?p]] =>
let n := fresh "n" in
unfold C.ChorUpExprSubst;
destruct (L.eq_dec p p) as [_ |n];
[|destruct (n eq_refl)];
unfold ExprUpSubst
end; try reflexivity.
- erewrite MergeExprSubst; eauto.
- destruct d; inversion eq; subst; auto.
- rewrite LocalSubstGlobalRenameComm; reflexivity.
- rewrite LocalSubstGlobalRenameComm; reflexivity.
Qed.
Theorem ProjectUpSubstForExprNeq : forall σ l l' σ',
(forall n, ProjectChor (σ n) l = Some (σ' n)) ->
l <> l' ->
forall n, ProjectChor (C.ChorUpSubstForExpr σ l' n) l = Some (σ' n).
Proof using.
intros σ l l' σ' eq neq n.
unfold C.ChorUpSubstForExpr. rewrite C.ChorExprRenameSpec.
rewrite ProjectChorExprSubst with (E := σ' n); auto.
destruct (L.eq_dec l' l) as [e | _ ]; [destruct (neq (eq_sym e))|].
rewrite ConExprLocalIdSubst. reflexivity.
Qed.
Theorem ProjectUpSubstForExprEq : forall σ l σ',
(forall n, ProjectChor (σ n) l = Some (σ' n)) ->
forall n, ProjectChor (C.ChorUpSubstForExpr σ l n) l = Some (σ' n cel| S).
Proof using.
intros σ l σ' H n.
unfold C.ChorUpSubstForExpr. rewrite C.ChorExprRenameSpec.
rewrite ProjectChorExprSubst with (E := σ' n); auto.
destruct (L.eq_dec l l) as [_ | neq]; [| destruct (neq eq_refl)].
rewrite ConExprLocalRenameSpec; auto.
Qed.
Theorem ProjectChorRename : forall C l E ξ,
ProjectChor C l = Some E ->
ProjectChor (C.ChorRename C ξ) l = Some (E ceg| ξ⟩).
Proof using.
intros C; C.ChorInduction C; intros p E ξ eq; cbn in *;
repeat match goal with
| [ |- ?a = ?a ] => reflexivity
| [ d : C.LRChoice |- _ ] => destruct d
| [ H : None = Some _ |- _ ] => inversion H
| [ H : Some _ = Some _ |- _ ] => inversion H; subst; clear H; cbn in *
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H : context[L.eq_dec ?a ?b] |- _ ] =>
destruct (L.eq_dec a b); subst; cbn in *
| [ H : context[ProjectChor ?C ?l] |- _ ] =>
lazymatch type of H with
| ProjectChor C l = _ => fail
| _ => lazymatch goal with
| [ H' : ProjectChor C l = _ |- _ ] => rewrite H' in H
| _ => let eq := fresh "eq" in
destruct (ProjectChor C l) eqn:eq; subst; cbn in *
end
end
| [ IH: forall l E ξ, ProjectChor ?C l = Some E -> ProjectChor (C.ChorRename ?C ξ) l = Some (E ceg| ξ⟩), H : ProjectChor ?C ?l = Some ?E |- context[ProjectChor (C.ChorRename ?C ?ξ) ?l]] =>
rewrite (IH l E ξ H)
end.
- repeat rewrite GlobalRenameSpec. apply MergeSubst; auto.
- repeat rewrite ConExprGlobalRenameFusion; cbn. reflexivity.
- unfold C.ChorUpRename. unfold UpRename. reflexivity.
- repeat rewrite ConExprGlobalRenameFusion; cbn. unfold C.ChorUpRename. unfold UpRename.
reflexivity.
- repeat unfold C.ChorUpRename. repeat unfold UpRename. reflexivity.
Qed.
Theorem ProjectUpSubst : forall σ l σ',
(forall n, ProjectChor (σ n) l = Some (σ' n)) ->
forall n, ProjectChor (C.ChorUpSubst σ n) l = Some (GlobalUpSubst σ' n).
Proof using.
intros σ l σ' H n.
unfold C.ChorUpSubst; destruct n; cbn; auto.
apply ProjectChorRename; auto.
Qed.
Theorem ProjectChorSubst : forall C l E σ σ',
(forall n, ProjectChor (σ n) l = Some (σ' n)) ->
ProjectChor C l = Some E ->
ProjectChor (C.ChorSubst C σ) l = Some (E [ceg| σ']).
Proof using.
intro C; C.ChorInduction C; intros p E σ σ' eq_σ eq_C; cbn in *;
repeat match goal with
| [ |- ?a = ?a ] => reflexivity
| [ d : C.LRChoice |- _ ] => destruct d
| [ H : None = Some _ |- _ ] => inversion H
| [ H : Some _ = Some _ |- _ ] => inversion H; subst; clear H; cbn in *
| [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
| [ H : context[L.eq_dec ?a ?b] |- _ ] =>
destruct (L.eq_dec a b); subst; cbn in *
| [ H : context[ProjectChor ?C ?l] |- _ ] =>
lazymatch type of H with
| ProjectChor C l = _ => fail
| _ => lazymatch goal with
| [ H' : ProjectChor C l = _ |- _ ] => rewrite H' in H
| _ => let eq := fresh "eq" in
destruct (ProjectChor C l) eqn:eq; subst; cbn in *
end
end
| [ IH : (forall l E σ σ', (forall n, ProjectChor (σ n) l = Some (σ' n)) -> ProjectChor ?C l = Some E -> ProjectChor (C.ChorSubst ?C σ) l = Some (E [ceg| σ'])),
H : ProjectChor ?C ?l = Some ?E,
H' : (forall n, ProjectChor (?σ n) ?l = Some (?σ' n))
|- context[ProjectChor (C.ChorSubst ?C ?σ) ?l]] =>
rewrite (IH l E σ σ' H' H)
| [ H : (forall n, ProjectChor (?σ n) ?l = Some (?σ' n)),
neq : ?l <> ?l' |- context[C.ChorUpSubstForExpr ?σ ?l'] ] =>
lazymatch goal with
| [ _ : forall n, ProjectChor (C.ChorUpSubstForExpr σ l' n) l = Some (σ' n) |- _ ] =>
fail
| _ => pose proof (ProjectUpSubstForExprNeq σ l l' σ' H neq)
end
| [ H : (forall n, ProjectChor (?σ n) ?l = Some (?σ' n)),
neq : ?l' <> ?l |- context[C.ChorUpSubstForExpr ?σ ?l'] ] =>
lazymatch goal with
| [ _ : forall n, ProjectChor (C.ChorUpSubstForExpr σ l' n) l = Some (σ' n) |- _ ] =>
fail
| _ =>
pose proof (ProjectUpSubstForExprNeq σ l l' σ' H ltac:(let eq := fresh in intro eq; destruct (neq (eq_sym eq))))
end
| [ H : (forall n, ProjectChor (?σ n) ?l = Some (σ' n))
|- context[C.ChorUpSubstForExpr ?σ ?l]] =>
lazymatch goal with
| [ _ : forall n, ProjectChor (C.ChorUpSubstForExpr σ l n) l = Some ((fun m => σ' m cel| S) n) |- _ ] => fail
| _ => assert (forall n, ProjectChor (C.ChorUpSubstForExpr σ l n) l = Some ((fun m => σ' m cel| S) n)) by (apply ProjectUpSubstForExprEq; auto)
end
end.
- apply eq_σ.
- apply MergeSubst; auto.
- apply f_equal.
rewrite ConExprGlobalRenameSubstFusion.
rewrite ConExprGlobalSubstRenameFusion. cbn.
erewrite ConExprGlobalSubstExt; [reflexivity|].
intro m; cbn. rewrite ConExprGlobalRenameFusion; reflexivity.
- rewrite IHC with (E := c) (σ' := GlobalUpSubst (fun n => σ' n cel| S)); auto.
apply ProjectUpSubst. intro n; apply ProjectUpSubstForExprEq; auto.
- rewrite IHC with (E := c) (σ' := GlobalUpSubst σ'); auto.
2: { apply ProjectUpSubst. apply ProjectUpSubstForExprNeq; auto. }
rewrite ConExprGlobalSubstRenameFusion.
rewrite ConExprGlobalRenameSubstFusion; reflexivity.
- rewrite IHC with (E := c) (σ' := GlobalUpSubst (GlobalUpSubst σ')); auto.
repeat apply ProjectUpSubst; auto.
Qed.
Definition ProjectRedex (R : C.Redex) (l : Loc) : option Label :=
match R with
| C.RDone p _ _ =>
if L.eq_dec l p
then Some Tau