RestrictedSemantics.v 31.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
Require Import Choreography.
Require Import TypedChoreography.

Require Import Coq.Arith.Arith.
Require Import Coq.Program.Wf.
Require Import Coq.Logic.JMeq.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Lists.List.
Require Import Sorted Orders Coq.Sorting.Mergesort Permutation.
Require Import Program.Tactics.
Require Import Coq.Structures.Orders.
Require Import Coq.Bool.Bool.
Require Import Psatz.
Require Import Coq.Program.Equality.

From Equations Require Import Equations.

Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression E) (L : Locations).
  Include (TypedChoreography L E TE). (* Note that a lot of results don't rely on typing, but the module system forces me to include it from the beginning *)
  Include ListNotations.

    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),
Andrew Hirsch's avatar
Andrew Hirsch committed
79
      ~ In l1 B -> ~ In l2 B -> l1 <> l2 ->
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
      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),
Andrew Hirsch's avatar
Andrew Hirsch committed
404
      l1 <> l2 ->
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
      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;
      try match goal with
          | [ H : ?C1  ?C2 |- Send ?l1 ?e ?l2 ?C1  _ ] =>
            transitivity (Send l1 e l2 C2); auto with Chor
          end.
      cbn. unfold ValueSubst at 2.
      destruct (L.eq_dec q l1) as [eq|_];[destruct (H (eq_sym eq))|].
      rewrite ExprIdentitySubstSpec. apply SendContext.
      erewrite ChorExprSubstExt ; [reflexivity|].
      intros l n. unfold ChorUpExprSubst; unfold ValueSubst.
      destruct (L.eq_dec q l); destruct (L.eq_dec l2 l); subst;
        try match goal with
            | [H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; auto.
      destruct n; auto; symmetry; apply ExprRenameVar.
    - induction ontop.
      all: inversion step; subst; ListClean.
      all: inversion step0; subst; ListClean.
      all: repeat match goal with
                  | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
                  | [ H : ?P, H' : ~?P |- _ ] => destruct (H' H)
                  | [ H : RedexOnTop ?R ?C |- _ ] =>
                    tryif (let H := fresh "_" C in idtac)
                    then fail
                    else inversion H; subst; clear H
                  end.
      all: repeat match goal with
                  | [ H : RChorStep ?R ?B _ _  |- _ ]=>
                    eapply NoIStepInList in H; [destruct H| |]; eauto with Chor;
                      InList; fail
                  end.
      all: eexists; eexists; split; [|split;[|split]]; [| | | eauto with Chor];
        try match goal with
            | [ |- RChorStep _ _ _ _ ] => eauto with Chor
            end;
      try match goal with
          | [ H : ?C1  ?C1', H' : ?C2  ?C2' |- If ?l1 ?e ?C1 ?C2  _ ] =>
            transitivity (If l1 e C1' C2'); auto with Chor
          end.
      cbn. unfold ValueSubst at 3.
      destruct (L.eq_dec q l1) as [eq|_];[destruct (H3 (eq_sym eq))|].
      rewrite ExprIdentitySubstSpec. reflexivity.
    - exists (DefLocal l C C2); exists (DefLocal l C0 C2); split; [|split;[|split]]; auto with Chor.
    - exists (AppLocal l C e); exists (AppLocal l C0 e); split; [|split;[|split]]; auto with Chor.
    - exists (AppGlobal C C2); exists (AppGlobal C0 C2); split; [|split;[|split]]; auto with Chor.
    - exists (AppGlobal (RecGlobal C1) C); exists (AppGlobal (RecGlobal C1) C0);
        split; [|split;[|split]]; auto with Chor.
    - 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;
      try match goal with
          | [ H : ?C1  ?C2 |- Sync ?l1 ?e ?l2 ?C1  _ ] =>
            transitivity (Sync l1 e l2 C2); auto with Chor
          end.
  Qed.

  Lemma RStepOnTopToStd : forall (C1 C2 : Chor) (R : Redex) (B : list Loc),
      RedexOnTop R C1 ->
      RChorStep R B C1 C2 ->
      StdChorStep C1 C2.
  Proof using.
    intros C1 C2 R B ontop rstep; induction rstep; inversion ontop; subst;
      eauto with Chor.
    all: try (inversion rstep; fail).
    - apply NoSendEIStepInList1 in rstep; [destruct rstep| left; reflexivity].
    - apply NoSendVIStepInList1 in rstep; [destruct rstep | left; reflexivity].
    - apply NoIfEIStepInList in rstep1; [destruct rstep1 | left; reflexivity].
    - apply NoIfTTStepInList in rstep1; [destruct rstep1 | left; reflexivity].
    - apply NoIfFFStepInList in rstep1; [destruct rstep1 | left; reflexivity].
    - inversion H1; subst; inversion rstep.
    - inversion H1.
    - apply NoSyncStepInList1 in rstep; [destruct rstep | left; reflexivity].
  Qed.

  Theorem RStepToStd : forall (C1 C2 : Chor) (R : Redex) (B : list Loc),
      RChorStep R B C1 C2 -> StdChorStep C1 C2.
  Proof using.
    intros C1 C2 R B rstep.
    apply RStepOnTop in rstep;
      destruct rstep as [C1' H]; destruct H as [C2' H];
      destruct H as [equiv1 H]; destruct H as [equiv2 H]; destruct H as [rstep ontop].
    apply StdEquivStep with (C1' := C1') (C2' := C2'); auto.
    apply RStepOnTopToStd with (R := R) (B := B); auto.
  Qed.

    Theorem LiftRestrictedChorStepToUnrestricted : forall C1 C2 B R, RChorStep B R C1 C2 -> ChorStep B R C1 C2.
  Proof using.
    intros C1 C2 B R step; induction step; auto with Chor.
  Qed.

  Corollary RestrictedRelativePreservation :
    (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 (R : Redex) (B : list Loc) (C': Chor),
        RChorStep R B C C' -> Γ;; Δ c C' ::: τ.
  Proof.
    intros H Γ Δ C τ H0 R B C' H1; apply LiftRestrictedChorStepToUnrestricted in H1.
    eapply RelativePreservation in H1; eauto.
  Qed.
  Theorem RestrictedRelativeProgress :
    (forall (e : Expr) (τ : ExprTyp) (Γ : nat -> ExprTyp),
        Γ e e ::: τ -> ExprClosed e ->
        ExprVal e \/ exists e' : Expr, ExprStep e e') ->
    (forall (v : Expr) (Γ : nat -> ExprTyp),
        Γ e v ::: bool -> ExprVal v -> {v = tt} + {v = ff}) ->
    forall (C : Chor) (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
      ChorClosed C -> Γ;; Δ c C ::: τ ->
      ChorVal C \/ exists R C', RChorStep R nil C C'.
  Proof.
    intros ExprProgress BoolInversion C Γ Δ τ cc typ; revert cc; induction typ; intro cc;
      inversion cc; subst.
    2: inversion H2.
    2-5,8,9: right.
    8,9: left; constructor; auto.
    - destruct (ExprProgress e τ (Γ p) ltac:(assumption) ltac:(assumption));
        [left; constructor; auto | right].
      destruct H0 as [e' step]; exists (RDone p e e'); exists (Done p e'); auto with Chor.
    - destruct (ExprProgress e τ (Γ p) ltac:(assumption) ltac:(assumption))
        as [eval | [e' step]];
        eexists; eexists; eauto with Chor.
    - destruct (ExprProgress e bool (Γ p) ltac:(assumption) ltac:(assumption))
        as [eval | [e' step]];
        [destruct (BoolInversion e (Γ p) ltac:(assumption) eval); subst|].
      all: eexists; eexists; eauto with Chor.
    - eexists; eexists; eauto with Chor.
    - destruct (IHtyp1 ltac:(assumption)) as [cval | [R [C' step]]].
      inversion cval; subst; inversion typ1; subst.
      all: eexists; eexists; eauto with Chor.
    - fold ChorClosed in H4; specialize (IHtyp H4); destruct IHtyp.
      inversion H0; subst; inversion typ; subst.
      destruct (ExprProgress _ _ _ H H6); [| destruct H2 as [e' step]];
        eexists; eexists; eauto with Chor.
      destruct H0 as [R [C' step]]; eexists; eexists; eauto with Chor.
    - specialize (IHtyp1 H3); specialize (IHtyp2 H4).
      destruct IHtyp1 as [IHtyp1 | [R [C' step]]]. 2: eexists; eexists; eauto with Chor.
      destruct IHtyp2 as [IHtyp2 | [R [C' step]]].
      all: inversion IHtyp1; subst; inversion typ1; subst.
      all: eexists; eexists; eauto with Chor.
  Qed.
  
End RestrictedSemantics.