Choreography.v 76.8 KB
Newer Older
1
Require Export Expression.
2
Require Export Locations.
3

4
5
6
7
8
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.
9
Require Import Sorted Orders Coq.Sorting.Mergesort Permutation.
Andrew Hirsch's avatar
Andrew Hirsch committed
10
Require Import Program.Tactics.
11
Require Import Coq.Structures.Orders.
12
13
14
15
16
Require Import Coq.Bool.Bool.
Require Import Psatz.
Require Import Coq.Program.Equality.

From Equations Require Import Equations.
17

18
Module Choreography (Import E : Expression) (L : Locations).
19

20
  Definition Loc : Set := L.t.
21
22
  (* Include (LocationNotations L). *)
  (* Module LF := (LocationFacts L). *)
23
24
25
26
27
28
29
30
  Import ListNotations.

  Inductive LRChoice : Set := LChoice | RChoice.
  Instance ChoiceEqDec : EqDec LRChoice.
  Proof using.
    unfold EqDec; decide equality.
  Defined.
  
31
  Inductive Chor : Set :=
32
33
34
35
36
37
    Done : Loc -> Expr -> Chor
  | Var : nat -> Chor
  | Send : Loc -> Expr -> Loc -> Chor -> Chor
  | If : Loc -> Expr -> Chor -> Chor -> Chor
  | Sync : Loc -> LRChoice -> Loc -> Chor -> Chor
  | DefLocal : Loc -> Chor -> Chor -> Chor
38
39
40
41
  | RecLocal : Loc -> Chor -> Chor (* rec local f(l.x). C *)
  | RecGlobal : Chor -> Chor (* rec global f(X). C *)
  | AppLocal : Loc -> Chor -> Expr -> Chor (* C e *) (* The location is necessary bookkeeping, we expect C to evaluate to rec local f(l.x). C' *)
  | AppGlobal : Chor -> Chor -> Chor (* C C *).
42
  Global Hint Constructors Chor : Chor.
43
44
45
46
47
48
49
  Notation "'Ret' p ⟪ e ⟫" := (Done p e) (at level 25).
  Notation "p ⟪ e ⟫ → q 'fby' C" := (Send p e q C) (at level 25).
  Notation "'Cond' p ⦃ e ⦄ 'Then' C1 'Else' C2" := (If p e C1 C2) (at level 25).
  Notation "p ⟨ d ⟩ → q 'fby' C" := (Sync p d q C) (at level 25).
  Notation "'LetLocal' p '⟪new⟫' ← C1 'fby' C2" := (DefLocal p C1 C2) (at level 25).

  Ltac ChorInduction C := let p := fresh "l" in
50
51
                          let e := fresh "e" in
                          let x := fresh "x" in
52
53
54
                          let q := fresh "l'" in
                          let C1 := fresh "C1" in
                          let C2 := fresh "C2" in
55
56
57
                          let IHC := fresh "IH" C in
                          let IHC1 := fresh "IH" C1 in
                          let IHC2 := fresh "IH" C2 in
58
59
                          let n := fresh "n" in
                          let d := fresh "d" in
60
61
                          induction C as [p e | n | p e q C IHC | p e C1 IHC1 C2 IHC2 | p d q C IHC |p C1 IHC1 C2 IHC2 | p C IHC | C IHC | p C IHC e | C1 IHC1 C2 IHC2].

62
  Ltac ChorDestruct C := let p := fresh "p" in
63
64
65
66
67
68
69
                         let n := fresh "n" in
                         let e := fresh "e" in
                         let x := fresh "x" in
                         let q := fresh "q" in
                         let d := fresh "d" in
                         let C1 := fresh "C1" in
                         let C2 := fresh "C2" in
70
71
                         destruct C as [p e | n | p e q C | p e C1 C2 |p d q C | p C1 C2 | p C | C | p C e | C1 C2 ].
  
72
73
74
75
76
77
78
79
  Instance ChorEqDec : EqDec Chor.
  Proof using.
    unfold EqDec; decide equality.
    all: try (apply ExprEqDec).
    all: try (apply L.eq_dec).
    apply Nat.eq_dec.
    apply ChoiceEqDec.
  Defined.
80

81
  Definition ChorUpExprRename : (Loc -> nat -> nat) -> Loc -> Loc -> nat -> nat :=
82
    fun ξ p q => if L.eq_dec p q
83
84
              then ExprUpRename (ξ q)
              else ξ q.
85
86

  Fixpoint ChorExprRename (C : Chor) (ξ : Loc -> nat -> nat) : Chor :=
87
    match C with
88
89
90
91
92
93
    | Done p e => Done p (e e| (ξ p))
    | Var n => Var n
    | Send p e q C => Send p (e e| (ξ p)) q (ChorExprRename C (ChorUpExprRename ξ q))
    | If p e C1 C2 => If p (e e| (ξ p)) (ChorExprRename C1 ξ) (ChorExprRename C2 ξ)
    | Sync p d q C1 => Sync p d q (ChorExprRename C1 ξ)
    | DefLocal p C1 C2 => DefLocal p (ChorExprRename C1 ξ) (ChorExprRename C2 (ChorUpExprRename ξ p))
94
95
96
97
    | RecLocal p C => RecLocal p (ChorExprRename C (ChorUpExprRename ξ p))
    | RecGlobal C => RecGlobal (ChorExprRename C ξ)
    | AppLocal p C e => AppLocal p (ChorExprRename C ξ) (e e| ξ p)
    | AppGlobal C1 C2 => AppGlobal (ChorExprRename C1 ξ) (ChorExprRename C2 ξ)
98
    end.
99
  Notation "C ⟨ce| x ⟩" := (ChorExprRename C x) (at level 20).
100

101
  Definition ChorIdExprRename : Loc -> nat -> nat := fun _ n => n.
102
  
103
104
  Lemma ChorUpIdExprRename : forall p q n, ChorUpExprRename ChorIdExprRename p q n = ChorIdExprRename p n.
  Proof using.
105
    intros p q n; destruct n; unfold ChorUpExprRename; unfold ChorIdExprRename.
106
    all: destruct (L.eq_dec p q) as [_|neq]; simpl; reflexivity.
107
108
  Qed.

109
110
111
112
  Lemma ChorUpExprRenameExt : forall (ξ1 ξ2 : Loc -> nat -> nat),
      (forall (p : Loc) (n : nat), ξ1 p n = ξ2 p n) ->
      forall (p q : Loc) (n : nat), ChorUpExprRename ξ1 p q n = ChorUpExprRename ξ2 p q n.
  Proof using.
113
    intros ξ1 ξ2 eq p q n. unfold ChorUpExprRename. unfold ExprUpRename.
114
    destruct (L.eq_dec p q); auto.
115
116
    destruct n; auto.
  Qed.
117

118
119
120
121
122
  Lemma ChorExprRenameExtensional : forall (ξ1 ξ2 : Loc -> nat -> nat),
      (forall (p : Loc) (n : nat), ξ1 p n = ξ2 p n) ->
      forall (C : Chor), C ce| ξ1  = C ce| ξ2.
  Proof using.
    intros ξ1 ξ2 eqv C; revert ξ1 ξ2 eqv; ChorInduction C; intros ξ1 ξ2 eqv; cbn; auto.
123
124
125
126
    all: try (rewrite ExprRenameExt with (ξ2 := ξ2 l)); auto.
    all: try (rewrite IHC with (ξ2 := ξ2); auto; fail).
    all: try (rewrite IHC1 with (ξ2 := ξ2); [rewrite IHC2 with (ξ2 := ξ2)|]; auto; fail).
    - rewrite IHC with (ξ2 := ChorUpExprRename ξ2 l'); auto.
127
      apply ChorUpExprRenameExt; auto.
128
    - rewrite IHC1 with (ξ2 := ξ2); [rewrite IHC2 with (ξ2 := ChorUpExprRename ξ2 l)|]; auto; apply ChorUpExprRenameExt; auto.
129
130
    - rewrite IHC with (ξ2 := ChorUpExprRename ξ2 l); auto.
      apply ChorUpExprRenameExt; auto.
131
132
133
134
135
136
  Qed.
  
  Lemma ChorExprRenameFusion : forall (C : Chor) (ξ1 ξ2 : Loc -> nat -> nat), (C ce| ξ1)ce| ξ2 = C ce| fun p n => ξ2 p (ξ1 p n).
  Proof using.
    intros C; ChorInduction C; intros ξ1 ξ2; cbn; auto.
    all: try (rewrite ExprRenameFusion; auto).
137
138
139
140
141
142
143
144
    all: try (rewrite IHC; auto; fail).
    all: try (rewrite IHC1; auto; rewrite IHC2; auto; fail).
    - rewrite IHC. rewrite ChorExprRenameExtensional with (ξ1 := fun p n => ChorUpExprRename ξ2 l' p (ChorUpExprRename ξ1 l' p n)) (ξ2 := ChorUpExprRename (fun p n => ξ2 p (ξ1 p n)) l'); auto.
      unfold ChorUpExprRename; unfold ExprUpRename; intros p n; destruct (L.eq_dec l' p); destruct n; auto.
    - rewrite IHC1; rewrite IHC2; auto.
      rewrite ChorExprRenameExtensional with (ξ1 := fun p n => ChorUpExprRename ξ2 l p (ChorUpExprRename ξ1 l p n)) (ξ2 := ChorUpExprRename (fun p n => ξ2 p (ξ1 p n)) l); auto.
      unfold ChorUpExprRename; unfold ExprUpRename; intros p n; destruct (L.eq_dec l p); destruct n; auto.
    - rewrite IHC.
145
146
147
      rewrite ChorExprRenameExtensional with (ξ1 := fun p n => ChorUpExprRename ξ2 l p (ChorUpExprRename ξ1 l p n)) (ξ2 := ChorUpExprRename (fun p n => ξ2 p (ξ1 p n)) l); auto.
      unfold ChorUpExprRename; unfold ExprUpRename; intros p n; destruct (L.eq_dec l p); destruct n; auto.
  Qed.
148

149
150
151
152
153
154
155
156
157
  Lemma ChorIdExprRenameSpec : forall C, C ce| ChorIdExprRename = C.
  Proof using.
    intros C; ChorInduction C; cbn; auto.
    all: try (rewrite IHC; auto).
    all: try (rewrite ExprIdRenamingSpec; auto).
    all: try (rewrite IHC1; rewrite IHC2; auto; fail).
    - rewrite ChorExprRenameExtensional with (ξ2 := ChorIdExprRename); [rewrite IHC; auto|].
      apply ChorUpIdExprRename.
    - rewrite IHC1. rewrite ChorExprRenameExtensional with (ξ2 := ChorIdExprRename); [rewrite IHC2| apply ChorUpIdExprRename]; auto.
158
159
    - rewrite ChorExprRenameExtensional with (ξ2 := ChorIdExprRename); [rewrite IHC|]; auto.
      apply ChorUpIdExprRename.
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
  Qed.

  Definition ChorUpRename : (nat -> nat) -> nat -> nat :=
    fun f n => match n with
            | 0 => 0
            | S n => S (f n)
            end.
  Fixpoint ChorRename (C : Chor) (ξ : nat -> nat) :=
    match C with
    | Done l e => Done l e
    | Var n => Var (ξ n)
    | Send l1 e l2 C => Send l1 e l2 (ChorRename C ξ)
    | If l e C1 C2 => If l e (ChorRename C1 ξ) (ChorRename C2 ξ)
    | Sync l1 d l2 C => Sync l1 d l2 (ChorRename C ξ)
    | DefLocal l C1 C2 => DefLocal l (ChorRename C1 ξ) (ChorRename C2 ξ)
175
176
177
178
    | RecLocal l C => RecLocal l (ChorRename C (ChorUpRename ξ))
    | RecGlobal C => RecGlobal (ChorRename C (ChorUpRename (ChorUpRename ξ))) (* We need two up, because we're defining two global variables *)
    | AppLocal l C e => AppLocal l (ChorRename C ξ) e
    | AppGlobal C1 C2 => AppGlobal (ChorRename C1 ξ) (ChorRename C2 ξ)
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
    end.
  Notation "C ⟨c| x ⟩" := (ChorRename C x) (at level 20).

  Definition ChorIdRename := fun n : nat => n.

  Lemma ChorUpIdRename : forall n, ChorUpRename ChorIdRename n = ChorIdRename n.
  Proof using.
    intro n; destruct n; cbn; unfold ChorIdRename; auto.
  Qed.
  Lemma ChorUpRenameExt : forall ξ1 ξ2, (forall n, ξ1 n = ξ2 n) -> forall n, ChorUpRename ξ1 n = ChorUpRename ξ2 n.
  Proof using.
    intros ξ1 ξ2 eqv n; destruct n; cbn; auto.
  Qed.

  Lemma ChorRenameExt : forall C ξ1 ξ2, (forall n, ξ1 n = ξ2 n) -> C c| ξ1 = C c| ξ2.
  Proof using.
    intros C; ChorInduction C; intros ξ1 ξ2 eqv; cbn; auto.
196
    all: try (rewrite IHC with (ξ2 := ξ2); auto; fail).
197
    all: try (rewrite IHC1 with (ξ2 := ξ2); [rewrite IHC2 with (ξ2 := ξ2)|]; auto; fail).
198
199
200
    rewrite IHC with (ξ2 := ChorUpRename ξ2); [| apply ChorUpRenameExt]; auto.
    rewrite IHC with (ξ2 := ChorUpRename (ChorUpRename ξ2)); auto.
    repeat apply ChorUpRenameExt; auto.
201
202
203
204
205
  Qed.    
  
  Lemma ChorIdRenameSpec : forall C, C c| ChorIdRename  = C.
  Proof using.
    intro C; ChorInduction C; cbn; auto.
206
207
208
209
    all: try (rewrite IHC); auto.
    all: try (rewrite IHC1; rewrite IHC2; auto).
    all: rewrite ChorRenameExt with (ξ2 := ChorIdRename); [rewrite IHC; reflexivity|].
    all: intro n; destruct n as [|n]; cbn; auto; destruct n; cbn; auto.
210
211
  Qed.

212
213
214
215
  Definition ChorRenameFusion : forall C ξ1 ξ2, (C c| ξ1) c|ξ2 = C c| fun n => ξ2 (ξ1 n).
  Proof using.
    intro C; ChorInduction C; intros ξ1 ξ2; cbn; auto.
    all: try (rewrite IHC; auto).
216
    all: try (rewrite IHC1; rewrite IHC2; auto).
217
    rewrite ChorRenameExt with (ξ2 := ChorUpRename (fun n => ξ2 (ξ1 n))).
218
219
220
    3: rewrite ChorRenameExt with (ξ2 := ChorUpRename (ChorUpRename (fun n => ξ2 (ξ1 n)))).
    1,3: reflexivity.
    all: intro n; unfold ChorUpRename; destruct n; auto; destruct n; auto.
221
  Qed.
222

223
  Definition ChorUpExprSubst : (Loc -> nat -> Expr) -> Loc -> Loc -> nat -> Expr :=
224
    fun σ p q n =>
225
      if L.eq_dec p q then
226
227
228
229
230
        match n with
        | 0 => ExprVar 0
        | S n => (σ q n) e| S 
        end
      else σ q n.
231
232
  Definition SendUpChorExprSubst (σk : nat -> Chor) (p : Loc) : nat -> Chor :=
    fun n => (σk n)ce| fun q m => if L.eq_dec p q then S m else m.
233

234
  Fixpoint ChorExprSubst (C : Chor) (σ : Loc -> nat -> Expr) : Chor :=
235
    match C with
236
237
238
239
240
241
    | Done p e => Done p (e [e| (σ p)])
    | Var n => Var n
    | Send p e q C => Send p (e [e| (σ p)]) q (ChorExprSubst C (ChorUpExprSubst σ q))
    | If p e C1 C2 => If p (e [e| (σ p)]) (ChorExprSubst C1 σ) (ChorExprSubst C2 σ)
    | Sync p d q C => Sync p d q (ChorExprSubst C σ)
    | DefLocal p C1 C2 => DefLocal p (ChorExprSubst C1 σ) (ChorExprSubst C2 (ChorUpExprSubst σ p))
242
243
244
245
    | RecLocal p C => RecLocal p (ChorExprSubst C (ChorUpExprSubst σ p))
    | RecGlobal C => RecGlobal (ChorExprSubst C σ)
    | AppLocal p C e => AppLocal p (ChorExprSubst C σ) (e [e| (σ p)])
    | AppGlobal C1 C2 => AppGlobal (ChorExprSubst C1 σ) (ChorExprSubst C2 σ)
246
    end.
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
  Notation "C [ce| s ]" := (ChorExprSubst C s) (at level 20).

  Lemma ChorUpExprSubstExt : forall (σ1 σ2 : Loc -> nat -> Expr),
      (forall (p : Loc) (n : nat), σ1 p n = σ2 p n) ->
      forall (p q : Loc) (n : nat), ChorUpExprSubst σ1 p q n = ChorUpExprSubst σ2 p q n.
  Proof using.
    intros σ1 σ2 eq p q n; unfold ChorUpExprSubst; destruct n; auto; repeat (rewrite eq); reflexivity.
  Qed.

  Lemma ChorExprSubstExt : forall (σ1 σ2 : Loc -> nat -> Expr),
      (forall (p : Loc) (n : nat), σ1 p n = σ2 p n) ->
      forall C, C [ce| σ1] = C [ce| σ2].
  Proof using.
    intros σ1 σ2 eqv C; revert σ1 σ2 eqv; ChorInduction C; intros σ1 σ2 eqv; cbn.
    all: try (rewrite ExprSubstExt with (σ2 := σ2 l)); auto.
    all: try (rewrite IHC with (σ2 := σ2); auto; fail).
263
    all: try (rewrite IHC1 with (σ2 := σ2); [rewrite IHC2 with (σ2 := σ2)|]; auto; fail).
264
265
    - rewrite IHC with (σ2 := ChorUpExprSubst σ2 l'); auto; apply ChorUpExprSubstExt; auto.
    - rewrite IHC1 with (σ2 := σ2); [rewrite IHC2 with (σ2 := ChorUpExprSubst σ2 l)|]; auto; apply ChorUpExprSubstExt; auto.
266
    - erewrite IHC; eauto; apply ChorUpExprSubstExt; auto.
267
268
  Qed.
  
269
  Definition ChorIdExprSubst : Loc -> nat -> Expr := fun _ n => ExprVar n.
270
  
271
272
273
274
  Lemma ChorIdExprSubstFibre : forall (p : Loc),
      ChorIdExprSubst p = ExprIdSubst.
  Proof using.
    intros p. unfold ChorIdExprSubst. unfold ExprIdSubst. reflexivity.
275
276
  Qed.

277
278
279
280
  Lemma ChorUpIdExprSubst : forall p q n, ChorIdExprSubst p n
                                 = ChorUpExprSubst ChorIdExprSubst q p n.
  Proof using.
    intros p q n; unfold ChorUpExprSubst; unfold ChorIdExprSubst;
281
      destruct (L.eq_dec q p); destruct n; auto; rewrite ExprRenameVar; reflexivity.
282
283
  Qed.
  
284
285
286
287
  Lemma ChorExprSubstIdSpec : forall (C : Chor), C [ce| ChorIdExprSubst] = C.
  Proof using.
    intro C; ChorInduction C; unfold ChorIdExprSubst; cbn; auto.
    all: try (rewrite ChorIdExprSubstFibre).
288
289
    all: try (rewrite ExprIdentitySubstSpec); auto.
    all: fold ChorIdExprSubst; try (rewrite IHC; auto; fail); try (rewrite IHC1; rewrite IHC2; auto; fail).
290
291
292
    - rewrite ChorExprSubstExt with (σ2 := ChorIdExprSubst); [rewrite IHC|]; auto.
      intros p n; unfold ChorUpExprSubst; unfold ChorIdExprSubst; cbn.
      destruct (L.eq_dec l' p); cbn; destruct n; auto; rewrite ExprRenameVar; reflexivity.
293
    - rewrite IHC1.
294
      rewrite ChorExprSubstExt with (σ2 := ChorIdExprSubst); [rewrite IHC2; reflexivity|].
295
296
297
      intros p n; symmetry; apply ChorUpIdExprSubst.
    - rewrite ChorExprSubstExt with (σ2 := ChorIdExprSubst); [rewrite IHC; reflexivity|].
      intros p n; symmetry; apply ChorUpIdExprSubst.
298
299
  Qed.
      
300
301
302
303
  Theorem ChorExprRenameSpec : forall (C : Chor) (ξ : Loc -> nat -> nat),
      C ce| ξ  = C[ce| (fun p n => ExprVar (ξ p n))].
  Proof using.
    intro C; ChorInduction C; intros ξ; cbn.
304
305
    all: repeat (rewrite ExprRenameSpec).
    all: try (repeat (rewrite IHC)).
306
    all: try (rewrite IHC1; rewrite IHC2).
307
    all: try reflexivity.
308
309
310
311
312
313
    - rewrite ChorExprSubstExt with (σ2 := ChorUpExprSubst (fun p n => ExprVar (ξ p n)) l'); [reflexivity|].
      intros p n; unfold ChorUpExprSubst; unfold ChorUpExprRename; destruct (L.eq_dec l' p); destruct n; auto.
      unfold ExprUpRename. rewrite ExprRenameVar. reflexivity.
    - rewrite ChorExprSubstExt with (σ1 := fun p n => ExprVar (ChorUpExprRename ξ l p n )) (σ2 := ChorUpExprSubst (fun p n => ExprVar (ξ p n)) l); [reflexivity|].
      intros p n; unfold ChorUpExprSubst; unfold ChorUpExprRename; destruct (L.eq_dec l p); destruct n; auto.
      unfold ExprUpRename; rewrite ExprRenameVar; reflexivity.
314
315
    - rewrite ChorExprSubstExt with (σ2 := ChorUpExprSubst (fun p n => ExprVar (ξ p n)) l); auto.
      intros p n; unfold ChorUpExprSubst; unfold ChorUpExprRename; destruct (L.eq_dec l p); destruct n; auto; unfold ExprUpRename; rewrite ExprRenameVar; auto.
316
317
318
319
320
321
322
323
324
325
  Qed.

  Definition ChorUpSubst : (nat -> Chor) -> nat -> Chor :=
    fun f  n => match n with
             | 0 => Var 0
             | S n => (f n) c| S
             end.

  Definition ChorUpSubstForExpr : (nat -> Chor) -> Loc -> nat -> Chor :=
    fun f l n => (f n) ce|fun l' m => if L.eq_dec l l' then S m else m.
326

327
  Fixpoint ChorSubst (C : Chor) (σ : nat -> Chor) :=
328
    match C with
329
330
331
332
333
334
    | Done l e => Done l e
    | Var n => σ n
    | Send l1 e l2 C => Send l1 e l2 (ChorSubst C (ChorUpSubstForExpr σ l2))
    | If l e C1 C2 => If l e (ChorSubst C1 σ) (ChorSubst C2 σ)
    | Sync l1 d l2 C => Sync l1 d l2 (ChorSubst C σ)
    | DefLocal l C1 C2 => DefLocal l (ChorSubst C1 σ) (ChorSubst C2 (ChorUpSubstForExpr σ l))
335
336
337
338
    | RecLocal l C => RecLocal l (ChorSubst C (ChorUpSubst(ChorUpSubstForExpr σ l)))
    | RecGlobal C => RecGlobal (ChorSubst C (ChorUpSubst (ChorUpSubst σ)))
    | AppLocal l C e => AppLocal l (ChorSubst C σ) e
    | AppGlobal C1 C2 => AppGlobal (ChorSubst C1 σ) (ChorSubst C2 σ)
339
    end.
340
341
342
343
344
345
346
  Notation "C [c| s ]" := (ChorSubst C s) (at level 20).
  Definition ChorIdSubst := fun n => Var n.

  Lemma ChorUpSubstExt : forall σ1 σ2 : nat -> Chor,
      (forall n, σ1 n = σ2 n) -> forall n, ChorUpSubst σ1 n = ChorUpSubst σ2 n.
  Proof using.
    intros σ1 σ2 H n; unfold ChorUpSubst; destruct n; cbn; auto. rewrite H; reflexivity.
347
348
  Qed.

349
350
351
352
353
354
  Lemma ChorUpSubstForExprExt : forall σ1 σ2,
      (forall n, σ1 n = σ2 n) ->
      forall l n, ChorUpSubstForExpr σ1 l n = ChorUpSubstForExpr σ2 l n.
  Proof using.
    intros σ1 σ2 eqv l n; unfold ChorUpSubstForExpr; rewrite eqv; reflexivity.
  Qed.
355

356
357
358
359
  Lemma ChorSubstExt : forall (C : Chor) (σ1 σ2 : nat -> Chor), (forall n, σ1 n = σ2 n) -> C[c|σ1] = C[c|σ2].
  Proof using.
    intro C; ChorInduction C; intros σ1 σ2 eqv; cbn; auto.
    all: try (erewrite IHC; eauto).
360
361
362
    all: try (erewrite IHC1; [erewrite IHC2|]; eauto).
    3,4: repeat apply ChorUpSubstExt; auto.
    all: apply ChorUpSubstForExprExt; auto.
363
364
365
366
367
  Qed.
  Lemma ChorSubstUpId : forall n, ChorUpSubst ChorIdSubst n = ChorIdSubst n.
  Proof using.
    intro n; unfold ChorUpSubst; unfold ChorIdSubst; destruct n; auto.
  Qed.
368

369
370
371
372
373
374
375
376
377
  Lemma ChorUpSubstForExprId : forall l n, ChorUpSubstForExpr ChorIdSubst l n = ChorIdSubst n.
  Proof using.
    intro n; unfold ChorUpSubstForExpr; unfold ChorIdSubst; cbn; reflexivity.
  Qed.
    
  Lemma ChorSubstIdSpec : forall C, C[c|ChorIdSubst] = C.
  Proof using.
    intro C; ChorInduction C; cbn; auto.
    all: try (rewrite IHC; auto).
378
379
380
381
    all: try (rewrite IHC1); try (rewrite IHC2); auto.
    1,3,4: erewrite ChorSubstExt; [rewrite IHC; reflexivity|].
    4: erewrite ChorSubstExt; [rewrite IHC2; reflexivity|].
    all: intro n; destruct n; cbn; auto; destruct n; auto.
382
  Qed.      
383

384
385
386
387
388
  Lemma ChorRenameSpec : forall C ξ, C c| ξ⟩ = C [c| fun n => Var (ξ n)].
  Proof using.
    intros C; ChorInduction C; intros ξ; cbn; auto.
    all: try (rewrite IHC; auto).
    all: try (rewrite IHC1; rewrite IHC2; auto; fail).
389
390
    all: erewrite ChorSubstExt; [reflexivity|].
    all: intro n; destruct n; cbn; auto; destruct n; auto.
391
  Qed.
392
393
    
  (* You might wonder why we don't have the ability to move over a def. It's because it's unsound! If you have l1 e  l2 x fby (let l3 y := C1 fby C2) (in the named form) then, you don't know if l2 uses x in C1 or not! *)
Andrew Hirsch's avatar
Andrew Hirsch committed
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416

  Fixpoint ChorExprClosedBelow (l : Loc) (n : nat) (C: Chor) : Prop :=
    match C with
    | Done l' e => if L.eq_dec l l'
                  then ExprClosedBelow n e
                  else True
    | Var x => True
    | Send l1 e l2 C => (if L.eq_dec l l1
                       then ExprClosedBelow n e
                       else True)
                       /\ if L.eq_dec l l2
                         then ChorExprClosedBelow l (S n) C
                         else ChorExprClosedBelow l n C
    | If l' e C1 C2 => (if L.eq_dec l l'
                      then ExprClosedBelow n e
                       else True)
                      /\ ChorExprClosedBelow l n C1
                      /\ ChorExprClosedBelow l n C2
    | Sync l1 d l2 C2 => ChorExprClosedBelow l n C2
    | DefLocal l' C1 C2 => ChorExprClosedBelow l n C1
                          /\ if L.eq_dec l l'
                            then ChorExprClosedBelow l (S n) C2
                            else ChorExprClosedBelow l n C2
417
418
419
420
421
422
423
424
425
426
    | RecLocal l' C => if L.eq_dec l l'
                      then ChorExprClosedBelow l (S n) C
                      else ChorExprClosedBelow l n C
    | RecGlobal C => ChorExprClosedBelow l n C
    | AppLocal l' C e => (if L.eq_dec l l'
                         then ExprClosedBelow n e
                         else True)
                        /\ ChorExprClosedBelow l n C
    | AppGlobal C1 C2 => ChorExprClosedBelow l n C1 /\ ChorExprClosedBelow l n C2

Andrew Hirsch's avatar
Andrew Hirsch committed
427
428
429
430
431
432
433
434
435
436
    end.

  Fixpoint ChorChorClosedBelow (n : nat) (C : Chor) : Prop :=
    match C with
    | Done l e => True
    | Var m => m < n
    | Send l1 e l2 C => ChorChorClosedBelow n C
    | If l e C1 C2 => ChorChorClosedBelow n C1 /\ ChorChorClosedBelow n C2
    | Sync l1 d l2 C => ChorChorClosedBelow n C
    | DefLocal l C1 C2 => ChorChorClosedBelow n C1 /\ ChorChorClosedBelow n C2
437
438
439
440
    | RecLocal l C => ChorChorClosedBelow (S n) C
    | RecGlobal C => ChorChorClosedBelow (S (S n)) C
    | AppLocal l C e => ChorChorClosedBelow n C
    | AppGlobal C1 C2 => ChorChorClosedBelow n C1 /\ ChorChorClosedBelow n C2
Andrew Hirsch's avatar
Andrew Hirsch committed
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
    end.
  
  Inductive ChorClosedBelow : (Loc -> nat) -> nat -> Chor -> Prop :=
  | DoneClosedBelow : forall n m p e, ExprClosedBelow (n p) e -> ChorClosedBelow n m (Done p e)
  | VarClosedBelow : forall n m k, lt k m -> ChorClosedBelow n m (Var k)
  | SendClosedBelow : forall p e q C n m,
      ExprClosedBelow (n p) e
      -> ChorClosedBelow (fun r => if L.eq_dec q r then S (n q) else n r) m C 
      -> ChorClosedBelow n m (Send p e q C)
  | SyncClosedBelow : forall n m p d q C,
      ChorClosedBelow n m C -> ChorClosedBelow n m (Sync p d q C)
  | IfClosedBelow : forall n m p e C1 C2,
      ExprClosedBelow (n p) e -> ChorClosedBelow n m C1 -> ChorClosedBelow n m C2
      -> ChorClosedBelow n m (If p e C1 C2)
  | DefLocalClosedBelow : forall n m l C1 C2,
      ChorClosedBelow n m C1 ->
      ChorClosedBelow (fun l' => if L.eq_dec l l' then S (n l) else n l') m C2 ->
      ChorClosedBelow n m (DefLocal l C1 C2)
459
460
461
462
463
464
465
466
467
468
469
470
  | RecLocalClosedBelow : forall n m l C,
      ChorClosedBelow (fun l' => if L.eq_dec l l' then S (n l) else n l') (S m) C ->
      ChorClosedBelow n m (RecLocal l C)
  | RecGlobalClosedBelow : forall n m C,
      ChorClosedBelow n (S (S m)) C ->
      ChorClosedBelow n m (RecGlobal C)
  | AppLocalClosedBelow : forall n m l C e,
      ChorClosedBelow n m C -> ExprClosedBelow (n l) e ->
      ChorClosedBelow n m (AppLocal l C e)
  | AppGlobalClosedBelow : forall n m C1 C2,
      ChorClosedBelow n m C1 -> ChorClosedBelow n m C2 ->
      ChorClosedBelow n m (AppGlobal C1 C2).
Andrew Hirsch's avatar
Andrew Hirsch committed
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

  Lemma ChorClosedBelow_Spec : forall (C : Chor) (f : Loc -> nat) (n : nat),
      ChorClosedBelow f n C <-> ChorChorClosedBelow n C /\ forall l, ChorExprClosedBelow l (f l) C.
  Proof using.
    intro C; ChorInduction C; intros f m.
    all: split; [intro cb; split;[|intro l1] | intros [ccb ceb]]; cbn in *; auto.
    all: repeat (match goal with
                 | [|- True ] => exact I
                 | [H : ?P |- ?P ] => exact H
                 | [ H : ChorClosedBelow ?f ?m ?C |- _ ] =>
                   tryif (let test := fresh "eq_" C in idtac)
                   then fail
                   else inversion H; subst; clear H
                 | [ H : context[L.eq_dec ?a ?b] |- _ ] => destruct (L.eq_dec a b); subst
                 | [ |- context[L.eq_dec ?a ?b]] => destruct (L.eq_dec a b); subst
                 | [ |- _ /\ _ ] => split
                 | [ H : _ /\ _ |- _ ] => destruct H
                 | [ H : forall l, ChorExprClosedBelow l (?f l) ?C |- ChorExprClosedBelow ?l (?f ?l) ?C ] => exact (H l)
                 | [ |- ChorClosedBelow ?f ?m ?C ] =>
                   tryif (let test := fresh "eq_" C in idtac)
                   then fail
                   else econstructor; eauto
                 | [ IHC : forall f n, ChorClosedBelow f n ?C <-> ChorChorClosedBelow n ?C /\ forall l, ChorExprClosedBelow l (f l) ?C, H: ChorClosedBelow ?f ?n ?C |- _ ] =>
                   lazymatch goal with
                   | [_ : ChorChorClosedBelow n C, _ : forall l, ChorExprClosedBelow l _ C |- _ ] => fail
                   | _ => let H1 := fresh in
                         let H2 := fresh in
                         pose proof ((proj1 (IHC f n)) H) as [H1 H2]
                   end
                 end);
                 repeat (match goal with
                         | [ H : forall l, ChorExprClosedBelow l (if L.eq_dec ?l' l
                                                             then _
                                                             else _) ?C |- _ ] =>
                           pose proof (H l');
                           let n := fresh "n" in
                           destruct (L.eq_dec l' l') as [_ | n]; [|destruct (n eq_refl)];
                           assert (forall l, l' <> l -> ChorExprClosedBelow l (f l) C)
                             by (let l := fresh in
                                 let neq := fresh in
                                 intros l neq; specialize (H l);
                                 destruct (L.eq_dec l' l) as [eq | _]; [destruct (neq eq)|];
                                 auto); clear H
                         end; cbn; auto).
    - pose proof (ceb l); destruct (L.eq_dec l l) as [_ |n];[|destruct (n eq_refl)]; auto.
    - specialize (ceb l); destruct (L.eq_dec l l) as [_|n];[|destruct (n eq_refl)]; auto.
      destruct ceb; auto.
    - apply IHC; split; auto; intro l''; specialize (ceb l''); destruct ceb;
        destruct (L.eq_dec l' l''); subst; auto.
      destruct (L.eq_dec l'' l'') as [_ | n]; [| destruct (n eq_refl)]; auto.
      destruct (L.eq_dec l'' l') as [eq |_ ]; [destruct (n (eq_sym eq))|]; auto.
    - specialize (ceb l); destruct ceb; destruct (L.eq_dec l l) as [_ | n];
        [|destruct (n eq_refl)]; auto.
    - apply IHC1; split; auto. intro l''; specialize (ceb l'');
                                 destruct ceb as [ceb1 [ceb2 ceb3]]; auto.
    - apply IHC2; split; auto. intro l''; specialize (ceb l'');
                                 destruct ceb as [ceb1 [ceb2 ceb3]]; auto.
    - apply IHC; split; auto.
    - apply IHC1; split; auto.
      intro l''; specialize (ceb l''); destruct ceb; auto.
    - apply IHC2; split; auto.
      intro l''; specialize (ceb l''); destruct ceb;
        destruct (L.eq_dec l l''); destruct (L.eq_dec l'' l); subst;
          try match goal with
              | [ H : ?l <> ?l |- _ ] => destruct (H eq_refl)
              end; auto.
537
538
539
540
541
542
543
544
545
546
547
548
    - apply IHC; split; auto; intro l'; specialize (ceb l').
      destruct (L.eq_dec l' l); destruct (L.eq_dec l l'); subst;
        try match goal with
            | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; auto.
    - apply IHC; split; auto.
    - apply IHC; split; auto; intro l'; specialize (ceb l'); destruct ceb;
        destruct (L.eq_dec l' l); subst; auto.
    - specialize (ceb l); destruct (L.eq_dec l l) as [_|neq];[|destruct (neq eq_refl)];
        destruct ceb; auto.
    - apply IHC1; split; auto. intro l; apply ceb; auto.
    - apply IHC2; split; auto. intro l; apply ceb; auto.
Andrew Hirsch's avatar
Andrew Hirsch committed
549
550
551
552
553
554
555
556
557
558
  Qed.

  Definition ChorExprClosed (C : Chor) := forall l, ChorExprClosedBelow l 0 C.
  Definition ChorChorClosed := ChorChorClosedBelow 0.
  Definition ChorClosed := ChorClosedBelow (fun _ => 0) 0.
  Corollary ChorClosedSpec : forall C, ChorClosed C <->  ChorChorClosed C /\ ChorExprClosed C.
  Proof using.
    unfold ChorExprClosed; unfold ChorChorClosed; unfold ChorClosed.
    intro C; apply ChorClosedBelow_Spec.
  Qed.
559
560
561
562
563
564
565
566
567
568

  Inductive ChorVal : Chor -> Prop :=
  | ReturnVal : forall (l : Loc) (v : Expr),
      ExprVal v -> ChorVal (Done l v)
  | RecLocalVal : forall l C, ChorClosedBelow (fun l' => if L.eq_dec l l' then 1 else 0) 1 C
                         -> ChorVal (RecLocal l C)
  | RecGlobalVal : forall C, ChorClosedBelow (fun _ => 0) 2 C ->
                        ChorVal (RecGlobal C).

  
Andrew Hirsch's avatar
Andrew Hirsch committed
569
570
  Lemma ChorValuesClosed : forall C : Chor, ChorVal C -> ChorClosed C.
  Proof.
571
572
573
574
    intros C H; induction H; unfold ChorClosed.
    apply DoneClosedBelow; apply ExprValuesClosed in H; unfold ExprClosed in H; exact H.
    apply RecLocalClosedBelow; auto.
    apply RecGlobalClosedBelow; auto.
Andrew Hirsch's avatar
Andrew Hirsch committed
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
  Qed.

  Lemma ChorExprClosedBelow_Subst : forall (C : Chor) (σ : Loc -> nat -> Expr) (f : Loc -> nat),
      (forall l, ChorExprClosedBelow l (f l) C) -> (forall l n, n < f l -> σ l n = ExprVar n) ->
      C [ce|σ] = C.
  Proof using.
    intro C; ChorInduction C; intros σ f closed_b static_above; cbn in *; auto.
    - specialize (closed_b l). destruct (L.eq_dec l l) as [_ | n]; [|destruct (n eq_refl)].
      rewrite ExprClosedBelowSubst with (n := f l); auto.
    - rewrite (IHC (ChorUpExprSubst σ l') (fun l => if L.eq_dec l l'
                                                 then S (f l)
                                                 else f l)).
      rewrite ExprClosedBelowSubst with (n := f l); auto.
      -- specialize (closed_b l); destruct (L.eq_dec l l) as [_ | n];
           [|destruct (n eq_refl)]; destruct closed_b; auto.
      -- intro l''; specialize (closed_b l''); destruct closed_b.
         destruct (L.eq_dec l'' l'); subst; auto.
      -- intros l0 n H; specialize (closed_b l0); destruct closed_b;
           destruct (L.eq_dec l0 l); subst; unfold ChorUpExprSubst.
         destruct (L.eq_dec l l'); destruct (L.eq_dec l' l); subst;
           try match goal with
               | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
               end. destruct n; auto. apply lt_S_n in H. rewrite static_above; auto.
         rewrite ExprRenameVar; auto.
         apply static_above; auto.
         destruct (L.eq_dec l' l0); destruct (L.eq_dec l0 l'); subst;
           try match goal with
               | [H : ?a <> ?a |- _ ] => destruct (H eq_refl)
               end.
         destruct n; auto. apply lt_S_n in H; rewrite static_above; auto.
         rewrite ExprRenameVar; auto.
         apply static_above; auto.
    - rewrite (IHC1  σ f); auto.
      rewrite (IHC2 σ f); auto.
      2,3: intro l'; specialize (closed_b l'); destruct closed_b as [H1 [H2 H3]]; auto.
      rewrite ExprClosedBelowSubst with (n := f l); auto.
      specialize (closed_b l); destruct closed_b as [H1 H2];
        destruct (L.eq_dec l l) as [_ |n]; [|destruct (n eq_refl)]; auto.
    - rewrite (IHC σ f); auto.
    - rewrite (IHC1 σ f); auto.
      2: intro l0; specialize (closed_b l0); destruct closed_b; auto.
      rewrite (IHC2 (ChorUpExprSubst σ l) (fun l' => if L.eq_dec l l'
                                                  then S (f l')
                                                  else f l')); auto.
      all: intro l0; 
        destruct (closed_b l0) as [H1 H2];
        destruct (L.eq_dec l l0); destruct (L.eq_dec l0 l); subst;
          try match goal with
              | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
              end; auto.
      all: intros m lt; unfold ChorUpExprSubst.
      destruct (L.eq_dec l l) as [_ |n]; [|destruct (n eq_refl)]. destruct m; auto.
      apply lt_S_n in lt. rewrite static_above; auto. apply ExprRenameVar.
      destruct (L.eq_dec l l0) as [eq|_]; [destruct (n eq)|]. apply static_above; auto.
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
    - rewrite IHC with (f := fun l' => if L.eq_dec l' l then S (f l') else f l'); auto.
      intro l'; specialize (closed_b l'); destruct (L.eq_dec l' l); auto.
      intros l' m; unfold ChorUpExprSubst;
        destruct (L.eq_dec l l'); destruct (L.eq_dec l' l); subst;
        try match goal with
            | [H : ?a <> ?a |- _] => destruct (H eq_refl)
            | [H : ?a = ?a |- _ ] => clear H
            end; intro m_lt_f; auto.
      destruct m; auto. apply lt_S_n in m_lt_f. rewrite static_above; auto.
      apply ExprRenameVar.
    - rewrite IHC with (f := f); auto.
    - rewrite ExprClosedBelowSubst with (n := f l).
      rewrite IHC with (f := f); auto.
      intro l'; apply closed_b.
      specialize (closed_b l); destruct closed_b;
        destruct (L.eq_dec l l) as [_|neq];[|destruct (neq eq_refl)]; auto.
      specialize (static_above l); auto.
    - rewrite IHC1 with (f := f); auto. rewrite IHC2 with (f := f); auto.
      all: intro l; apply closed_b; auto.
Andrew Hirsch's avatar
Andrew Hirsch committed
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
  Qed.
      
  Corollary ChorExprClosed_Subst : forall (C : Chor) (σ : Loc -> nat -> Expr),
      ChorExprClosed C -> C[ce|σ] = C.
  Proof using.
    intros C σ; unfold ChorExprClosed; intro closed;
      apply ChorExprClosedBelow_Subst with (f := fun _ => 0); auto.
    intros l n H. inversion H.
  Qed.

  Corollary ChorClosed_ExprSubst : forall (C : Chor) (σ : Loc -> nat -> Expr),
      ChorClosed C -> C [ce|σ] = C.
  Proof using.
    intros C σ H; apply ChorClosedSpec in H; destruct H; apply ChorExprClosed_Subst; auto.
  Qed.

  Lemma ChorChorClosedBelow_Subst : forall (C : Chor) (σ : nat -> Chor) (n : nat),
      ChorChorClosedBelow n C -> (forall m, m < n -> σ m = Var m) ->
      C [c| σ] = C.
  Proof using.
    intros C; ChorInduction C; intros σ m closed_b static_above; cbn in *; auto.
    - rewrite (IHC (ChorUpSubstForExpr σ l') m); auto.
      unfold ChorUpSubstForExpr.
      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 (ChorUpSubstForExpr σ l) m); auto.
      unfold ChorUpSubstForExpr; intros k lt; rewrite static_above; auto.
677
678
679
680
681
682
683
684
685
686
    - rewrite IHC with (n := S m); auto.
      intros n n_lt_Sm; unfold ChorUpSubst; unfold ChorUpSubstForExpr; 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.
      intros n n_lt_SSm; unfold ChorUpSubst; destruct n; auto; destruct n; auto.
      rewrite static_above; cbn; auto.
      apply lt_S_n in n_lt_SSm; apply lt_S_n in n_lt_SSm; auto.
    - rewrite IHC with (n := m); auto.
    - destruct closed_b; rewrite IHC1 with (n := m); auto; rewrite IHC2 with (n := m); auto.
Andrew Hirsch's avatar
Andrew Hirsch committed
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
  Qed.

  Corollary ChorChorClosed_Subst : forall (C : Chor) (σ : nat -> Chor),
      ChorChorClosed C -> C [c| σ] = C.
  Proof using.
    intros C σ H; unfold ChorChorClosed in H;
      apply ChorChorClosedBelow_Subst with (n := 0); auto.
    intros m H0; inversion H0.
  Qed.

  Corollary ChorClosed_ChorSubst : forall (C : Chor) (σ : nat -> Chor),
      ChorClosed C -> C [c| σ] = C.
  Proof using.
    intros C σ H; apply ChorClosedSpec in H; destruct H ;apply ChorChorClosed_Subst; auto.
  Qed.

  Lemma ChorExprClosedBelowMono : forall (C : Chor) (n m : nat) (l : Loc),
      n < m -> ChorExprClosedBelow l n C -> ChorExprClosedBelow l m C.
  Proof using.
    intro C; ChorInduction C; intros m k p lt closed_n; cbn in *; eauto.
    destruct (L.eq_dec p l); subst; eauto. eapply ExprClosedBelowMono; eauto.
    destruct (L.eq_dec p l); destruct (L.eq_dec p l'); subst; destruct closed_n; split;
      eauto.
    all: try match goal with
             | [ H : ?a < ?b, H' : ExprClosedBelow ?a ?e |- ExprClosedBelow ?b ?e ] =>
               apply (ExprClosedBelowMono a b e H H')
             end.
    1,2: apply lt_n_S in lt; eauto.
    all: repeat match goal with
                | [ |- True ] => exact I
                | [ H : ?P |- ?P ] => exact H
                | [ H : _ /\ _ |- _ ] => destruct H
                | [ |- _ /\ _ ] => split
                | [ H : context[L.eq_dec ?a ?b] |- _ ] => destruct (L.eq_dec a b); subst
                | [ |- context[L.eq_dec ?a ?b]] => destruct (L.eq_dec a b); subst
                | [ IH :forall n m l, n < m -> ChorExprClosedBelow l n ?C -> ChorExprClosedBelow l m ?C,
                      H : ?a < ?b, H' : ChorExprClosedBelow ?l ?a ?C |- _ ] =>
                  lazymatch goal with
                  | [ _ : ChorExprClosedBelow l b C |- _ ] => fail
                  | _ => pose proof (IH a b l H H')
                  end
                | [ H : ?a < ?b, H' : ExprClosedBelow ?a ?e |- ExprClosedBelow ?b ?e ] =>
                  apply (ExprClosedBelowMono a b e H H')
                end.
731
    all: apply lt_n_S in lt; eauto.
Andrew Hirsch's avatar
Andrew Hirsch committed
732
733
734
735
736
737
738
  Qed.

  Lemma ChorChorClosedBelowMono : forall (C : Chor) (n m : nat),
      n < m -> ChorChorClosedBelow n C -> ChorChorClosedBelow m C.
  Proof using.
    intros C; ChorInduction C; intros m k pf closed_below; cbn in *; eauto.
    transitivity m; auto.
739
    all: try (destruct closed_below; split; eauto).
Andrew Hirsch's avatar
Andrew Hirsch committed
740
    all: apply lt_n_S in pf; eauto.
741
    apply lt_n_S in pf; eauto.
Andrew Hirsch's avatar
Andrew Hirsch committed
742
  Qed.
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
  
  Reserved Notation "C1 ≡ C2" (at level 30).
  Inductive equiv : Chor -> Chor -> Prop :=
  | equivTrans : forall C1 C2 C3, C1  C2 -> C2  C3 -> C1  C3
  | DoneRefl : forall l e, Done l e  Done l e
  | VarRefl : forall n, Var n  Var n
  | SendContext : forall l1 e l2 C1 C2,
      C1  C2 ->
      l1 e  l2 fby C1  l1 e  l2 fby C2
  | SyncContext : forall l1 d l2 C1 C2,
      C1  C2 ->
      l1 d  l2 fby C1  l1 d  l2 fby C2                  
  | IfContext : forall l e C11 C12 C21 C22,
      C11  C21 -> C12  C22 ->
      Cond l  e  Then C11 Else C12  Cond le Then C21 Else C22
  | DefLocalContext : forall l C11 C12 C21 C22,
      C11  C21 -> C12  C22 ->
      LetLocal l new  C11 fby C12  LetLocal l new  C21 fby C22
761
762
763
764
765
766
767
768
769
770
  | RecLocalContext : forall l C1 C2, (* Equivalence does work under lambda *)
      C1  C2 ->
      RecLocal l C1  RecLocal l C2
  | RecGlobalContext : forall C1 C2,
      C1  C2 ->
      RecGlobal C1  RecGlobal C2
  | AppLocalContext : forall C1 C2 l e,
      C1  C2 ->
      AppLocal l C1 e  AppLocal l C2 e
  | AppGlobalContext : forall C11 C12 C21 C22,
771
      C11  C21 -> C12  C22 ->
772
      AppGlobal C11 C12  AppGlobal C21 C22
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
  | SwapSendSend : forall l1 e l2 l3 e' l4 C,
      l1 <> l3 -> l1 <> l4 -> l2 <> l3 -> l2 <> l4 ->
      l1 e  l2 fby (l3 e'⟫  l4 fby C)  l3 e'⟫  l4 fby (l1 e  l2 fby C)
  | SwapSendSync : forall l1 e l2 l3 d l4 C,
      l1 <> l3 -> l1 <> l4 -> l2 <> l3 -> l2 <> l4 ->
      l1 e  l2 fby (l3 d  l4 fby C)  l3 d  l4 fby (l1 e  l2 fby C)
  | SwapSyncSend : forall l1 d l2 l3 e l4 C,
      l1 <> l3 -> l1 <> l4 -> l2 <> l3 -> l2 <> l4 ->
      l1 d  l2 fby (l3 e  l4 fby C)  l3 e  l4 fby (l1 d  l2 fby C)
  | SwapSendIf : forall l1 e l2 l3 e' C1 C2,
      l1 <> l3 -> l2 <> l3 ->
      l1 e  l2 fby (Cond l3 e'⦄ Then C1 Else C2)  Cond l3 e'⦄ Then (l1 e  l2 fby C1) Else (l1 e  l2 fby C2)
  | SwapIfSend : forall l1 e l2 e' l3 C1 C2,
      l1 <> l2 -> l1 <> l3 ->
      Cond l1 e Then (l2 e'⟫  l3 fby C1) Else (l2 e'⟫  l3 fby C2)  l2 e'⟫  l3 fby (Cond l1 e Then C1 Else C2)
  | SwapSyncSync : forall l1 d l2 l3 d' l4 C,
      l1 <> l3 -> l1 <> l4 -> l2 <> l3 -> l2 <> l4 ->
      l1 d  l2 fby (l3 d'⟩  l4 fby C)  l3 d'⟩  l4 fby (l1 d  l2 fby C)
  | SwapSyncIf : forall l1 d l2 l3 e C1 C2,
      l1 <> l3 -> l2 <> l3 ->
      l1 d  l2 fby (Cond l3 e Then C1 Else C2)  Cond l3 e Then (l1 d  l2 fby C1) Else (l1 d  l2 fby C2)
  | SwapIfSync : forall l1 e l2 d l3 C1 C2,
      l1 <> l2 -> l1 <> l3 ->
      Cond l1 e Then (l2 d  l3 fby C1) Else (l2 d  l3 fby C2)  l2 d  l3 fby (Cond l1 e Then C1 Else C2)
  | SwapIfIf : forall l1 e l2 e' C1 C2 C3 C4,
      l1 <> l2 ->
      Cond l1 e Then (Cond l2 e'⦄ Then C1 Else C2) Else (Cond l2 e'⦄ Then C3 Else C4)  Cond l2 e'⦄ Then (Cond l1 e Then C1 Else C3) Else (Cond l1 e Then C2 Else C4)
  where "C1 ≡ C2" := (equiv C1 C2).
801
  Global Hint Constructors equiv : Chor.
802

803
804
805
806
807
808
809
810
  Fixpoint equivRefl (C : Chor) : C  C :=
    match C with
    | Done l e => DoneRefl l e
    | Var n => VarRefl n
    | Send l1 e l2 C => SendContext l1 e l2 C C (equivRefl C)
    | If l e C1 C2 => IfContext l e C1 C2 C1 C2 (equivRefl C1) (equivRefl C2)
    | Sync l1 d l2 C => SyncContext l1 d l2 C C (equivRefl C)
    | DefLocal l C1 C2 => DefLocalContext l C1 C2 C1 C2 (equivRefl C1) (equivRefl C2)
811
812
813
814
    | RecLocal l C => RecLocalContext l C C (equivRefl C)
    | RecGlobal C => RecGlobalContext C C (equivRefl C)
    | AppLocal l C e => AppLocalContext C C l e (equivRefl C)
    | AppGlobal C1 C2 => AppGlobalContext C1 C2 C1 C2 (equivRefl C1) (equivRefl C2)
815
    end.
816
  Global Hint Resolve equivRefl : Chor.
817
818
819
820
821
  Instance : Reflexive equiv := equivRefl.

  Theorem equivSym : forall C1 C2 : Chor, C1  C2 -> C2  C1.
  Proof using.
    intros C1 C2 equiv; induction equiv; eauto with Chor.
822
  Qed.
823
  Global Hint Resolve equivSym : Chor.
824
  Instance : Symmetric equiv := equivSym.
825

826
827
  Instance : Transitive equiv := equivTrans.
  
828
  (* Smart constructors for  *)
829
830
831
832
833
834
  Lemma SmartSwapSendSend : forall (p q r s : Loc) (C1 C2 : Chor) (e1 e2 : Expr),
      p <> r -> q <> r -> p <> s -> q <> s ->
      C1  C2 ->
      Send p e1 q (Send r e2 s C1)  Send r e2 s (Send p e1 q C2).
  Proof using.
    intros p q r s C1 C2 e1 e2 neq_p_r neq_q_r neq_p_s neq_q_s eqv; etransitivity; [apply SwapSendSend|]; auto with Chor.
835
  Qed.
836
837
  Lemma SmartSwapSendIf : forall p e1 q e2 r C1 C1' C2 C2',
      p <> q -> p <> r ->
838
      C1  C1' -> C2  C2' ->
839
840
841
      Send q e2 r (If p e1 C1 C2)  If p e1 (Send q e2 r C1') (Send q e2 r C2').
  Proof using.
    intros n p e1 q e2 r C1 C1' C2 C2' neq1 neq2 equiv1; etransitivity; [apply SwapSendIf |]; eauto with Chor.
842
  Qed.
843
844
  Lemma SmartSwapIfSend : forall p e1 q e2 r C1 C1' C2 C2',
      p <> q -> p <> r ->
845
      C1  C1' -> C2  C2' ->
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
      If p e1 (Send q e2 r C1) (Send q e2 r C2)  Send q e2 r (If p e1 C1' C2').
  Proof using.
    intros n p e1 q e2 r C1 C1' C2 C2' neq1 neq2 equiv1; etransitivity; [apply SwapIfSend|]; eauto with Chor.
  Qed.
  Lemma SmartSwapSendSync : forall (p q r s : Loc) (e : Expr) (d : LRChoice) (C C' : Chor),
      p <> r -> p <> s -> q <> r -> q <> s -> C  C' ->
      Send p e q (Sync r d s C)  Sync r d s (Send p e q C').
  Proof using.
    intros p q r s e d C C' neq1 neq2 neq3 neq4 equiv; etransitivity; [apply SwapSendSync|]; eauto with Chor.
  Qed.
  Lemma SmartSwapSyncSend : forall (p q r s : Loc) (e : Expr) (d : LRChoice) (C C' : Chor),
      p <> r -> p <> s -> q <> r -> q <> s -> C  C' ->
      Sync p d q (Send r e s C)  Send r e s (Sync p d q C').
  Proof using.
    intros p q r s e d C C' neq1 neq2 neq3 neq4 equiv; etransitivity; [apply SwapSyncSend|]; eauto with Chor.
  Qed.
  Lemma SmartSwapIfIf : forall p e1 q e2 C11 C11' C12 C12' C21 C21' C22 C22',
      p <> q ->
      C11  C11' -> C12  C12' -> C21  C21' -> C22  C22' ->
      If p e1 (If q e2 C11 C12) (If q e2 C21 C22)  If q e2 (If p e1 C11' C21') (If p e1 C12' C22').
  Proof using.
    intros n p e1 m q e2 C11 C11' C12 C12' C21 C21' C22 C22' neq equiv1; etransitivity; [apply SwapIfIf|]; eauto with Chor.
  Qed.
  Lemma SmartSwapIfSync : forall (p q r : Loc) (e : Expr) (d : LRChoice) (C1 C1' C2 C2' : Chor),
      p <> q -> p <> r -> C1  C1' -> C2  C2' ->
      If p e (Sync q d r C1) (Sync q d r C2)  Sync q d r (If p e C1' C2').
  Proof using.
    intros m p q r e d C1 C1' C2 C2' neq1 neq2 equiv1; etransitivity; [apply SwapIfSync|]; eauto with Chor.
  Qed.
  Lemma SmartSwapSyncIf : forall (p q r : Loc) (e : Expr) (d : LRChoice) (C1 C1' C2 C2' : Chor),
      p <> r -> q <> r -> C1  C1' -> C2  C2' ->
      Sync p d q (If r e C1 C2)  If r e (Sync p d q C1') (Sync p d q C2').
  Proof using.
    intros m p q r e d C1 C1' C2 C2' neq1 neq2 equiv1; etransitivity; [apply SwapSyncIf|]; eauto with Chor.
  Qed.
  Lemma SmartSwapSyncSync : forall (p q r s : Loc) (d d' : LRChoice) (C C' : Chor),
      p <> r -> p <> s -> q <> r -> q <> s -> C  C' ->
      Sync p d q (Sync r d' s C)  Sync r d' s (Sync p d q C').
  Proof using.
    intros p q r s d d' C1 C1' neq1 neq2 neq3 neq4 equiv; etransitivity; [apply SwapSyncSync|]; auto with Chor.
886
  Qed.
887
  Global Hint Resolve SmartSwapSendSend SmartSwapSendIf SmartSwapIfSend SmartSwapIfIf SmartSwapSendSync SmartSwapSyncSend SmartSwapIfSync SmartSwapSyncSync : Chor.
888

889
890
891
892
893
894
895
896
897
898
899
900
901
902
  Lemma EquivStableExprRename : forall (ξ : Loc -> nat -> nat) (C1 C2 : Chor),
      C1  C2 -> C1 ce| ξ   C2 ce| ξ⟩.
  Proof using.
    intros ξ C1 C2 eqv; revert ξ; induction eqv; intros ξ; cbn; auto; try reflexivity.
    etransitivity; eauto.
    all: eauto with Chor.
    - unfold ChorUpExprRename at 1 4. destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H1 eq)|].
      destruct (L.eq_dec l4 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|]. apply SmartSwapSendSend; auto.
      erewrite ChorExprRenameExtensional; [reflexivity|]. intros p n; unfold ChorUpExprRename.
      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; auto.
    - etransitivity; [apply SwapSendIf|]; auto.
      unfold ChorUpExprRename at 1; destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H0 eq)|]; reflexivity.
    - etransitivity; [apply SwapIfSend|]; auto.
      unfold ChorUpExprRename at 3. destruct (L.eq_dec l3 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|]; reflexivity.
903
904
  Qed.

905
906
907
908
909
910
911
912
913
914
915
916
  Lemma EquivStableExprSubst : forall(σ : Loc -> nat -> Expr) (C1 C2 : Chor), C1  C2 -> C1 [ce| σ]  C2 [ce| σ].
  Proof using.
    intros σ C1 C2 eqv; revert σ; induction eqv; intros σ; cbn; auto; try reflexivity.
    etransitivity; eauto.
    all: eauto with Chor.
    - unfold ChorUpExprSubst at 1 4; destruct (L.eq_dec l2 l3); destruct (L.eq_dec l4 l1); subst; try match goal with [H : ?a <> ?a |- _ ] => destruct (H eq_refl) end; auto.
      etransitivity; [apply SwapSendSend|]; auto; erewrite ChorExprSubstExt; [reflexivity|].
      intros p n1; unfold ChorUpExprSubst. 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; auto.
    - etransitivity; [apply SwapSendIf|]; auto.
      unfold ChorUpExprSubst at 1; destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H0 eq)|]; reflexivity.
    - etransitivity; [apply SwapIfSend|]; auto.
      unfold ChorUpExprSubst at 3; destruct (L.eq_dec l3 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|]; reflexivity.
917
918
  Qed.

919
920
921
922
  Lemma EquivStableRename : forall (ξ : nat -> nat) (C1 C2 : Chor), C1  C2 -> C1 c| ξ⟩  C2 c| ξ .
  Proof using.
    intros ξ C1 C2 eqv; revert ξ; induction eqv; intro ξ; cbn; auto with Chor.
    transitivity (C2 c| ξ⟩); auto.
923
924
  Qed.

925
926
927
928
929
930
931
932
933
934
935
  Lemma EquivStableSubst : forall (σ : nat -> Chor) (C1 C2 : Chor), C1  C2 -> C1 [c| σ ]  C2 [c| σ].
  Proof using.
    intros σ C1 C2 eqv; revert σ; induction eqv; intro σ; cbn; auto with Chor.
    transitivity (C2 [c| σ]); auto.
    apply SmartSwapSendSend; auto. erewrite ChorSubstExt; [reflexivity|].
    intro n; unfold ChorUpSubstForExpr.
    repeat rewrite ChorExprRenameFusion. apply ChorExprRenameExtensional.
    intros l' m; destruct (L.eq_dec l2 l'); destruct (L.eq_dec l4 l'); subst;
      try match goal with
          | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
          end; reflexivity.
936
  Qed.
937
938
939
940
941

  Lemma WeakSubstUpExt : forall (σ1 σ2 : nat -> Chor), (forall n, σ1 n  σ2 n) -> forall n, ChorUpSubst σ1 n  ChorUpSubst σ2 n.
  Proof using.
    intros σ1 σ2 H n; destruct n; unfold ChorUpSubst; cbn; auto with Chor. apply EquivStableRename; auto.
  Qed.
942
  Global Hint Resolve EquivStableExprRename EquivStableExprSubst EquivStableRename EquivStableSubst WeakSubstUpExt : Chor.
943
944
945
946
947
948

  Lemma WeakSubstUpForExprExt : forall (σ1 σ2 : nat -> Chor),
      (forall n, σ1 n  σ2 n) -> forall l n, ChorUpSubstForExpr σ1 l n  ChorUpSubstForExpr σ2 l n.
  Proof using.
    intros σ1 σ2 eqv l n.
    unfold ChorUpSubstForExpr. apply EquivStableExprRename; auto.
949
  Qed.
950
  Global Hint Resolve WeakSubstUpForExprExt : Chor.
951
952
953
954
955

  Lemma WeakSubstExt' : forall (σ1 σ2 : nat -> Chor) (C :Chor), (forall n, σ1 n  σ2 n) -> C [c| σ1]  C[c|σ2].
  Proof using.
    intros σ1 σ2 C; revert σ1 σ2; ChorInduction C; intros σ1 σ2 eqv; cbn; auto with Chor.
  Qed.
956
  Global Hint Resolve WeakSubstExt' : Chor.
957
958
959
960
961
962
963
964
965
966
967
968
969
  Lemma WeakSubstExt : forall (σ1 σ2 : nat -> Chor) (C1 C2 : Chor), C1  C2 -> (forall n, σ1 n  σ2 n) -> C1 [c| σ1]  C2 [c| σ2].
  Proof using.
    intros σ1 σ2 C1 C2 eqv; revert σ1 σ2; induction eqv; intros σ1 σ2 eqvσ; cbn; auto with Chor.
    transitivity (C2 [c|σ2]); auto with Chor.
    apply SmartSwapSendSend; auto. apply WeakSubstExt'.
    intro n. unfold ChorUpSubstForExpr. repeat rewrite ChorExprRenameFusion.
    transitivity (σ2 n ce| fun p n0 => if L.eq_dec l4 p
                                     then S (if L.eq_dec l2 p then S n0 else n0)
                                     else if L.eq_dec l2 p then S n0 else n0).
    apply EquivStableExprRename; auto.
    erewrite ChorExprRenameExtensional; [reflexivity|].
    intros p n0; cbn. destruct (L.eq_dec l4 p); destruct (L.eq_dec l2 p); auto.
  Qed.
970
  Global Hint Resolve WeakSubstExt : Chor.
971

972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
  Lemma WeakSubstExprExt : forall (σ : Loc -> nat -> Expr) (C1 C2 : Chor),
      C1  C2 -> C1 [ce|σ]  C2 [ce|σ].
  Proof using.
    intros σ C1 C2 equiv; revert σ; induction equiv; intro σ; cbn; auto with Chor.
    - transitivity (C2 [ce|σ]); auto.
    - unfold ChorUpExprSubst at 1; destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H1 eq)|].
      unfold ChorUpExprSubst at 3; destruct (L.eq_dec l4 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|].
      rewrite ChorExprSubstExt with (σ1 := ChorUpExprSubst (ChorUpExprSubst σ l2) l4) (σ2 := ChorUpExprSubst (ChorUpExprSubst σ l4) l2).
      constructor; auto; fail.
      intros p n; unfold ChorUpExprSubst; destruct n; cbn.
      -- destruct (L.eq_dec l4 p); subst; auto.
         destruct (L.eq_dec l2 p); auto.
      -- destruct (L.eq_dec l4 p); subst; auto.
         destruct (L.eq_dec l2 p) as [eq|_]; [destruct (H2 eq)|]; auto.
    - unfold ChorUpExprSubst at 1; destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H0 eq)|].
      constructor; auto; fail.
    - unfold ChorUpExprSubst at 3; destruct (L.eq_dec l3 l1) as [eq|_];
        [destruct (H0 (eq_sym eq))|].
      constructor; auto; fail.
991
992
993
994
995
996
997
998
999
1000
  Qed.


    Lemma RetEquivInversion : forall l e C, Done l e  C -> C = Done l e.
  Proof using.
    intros l e C eqv; dependent induction eqv; auto.
  Qed.

  Lemma RecLocalEquivInversion : forall l C1 C2,
      RecLocal l C1  C2 -> exists C1', C2 = RecLocal l C1' /\ C1  C1'.