TypedChoreography.v 22.4 KB
Newer Older
1
2
Require Export Expression.
Require Export TypedExpression.
3
Require Export Choreography.
4

5
Module TypedChoreography (L : Locations) (E : Expression) (TE : TypedExpression E).
6
7
  Import E.
  Import TE.
8
  Include (Choreography E L).
9

10
11
12
13
14
15
16
17
18
19
  Inductive ChorTyp : Set :=
  | LocatedType : Loc -> ExprTyp -> ChorTyp
  | LocalFun : Loc -> ExprTyp -> ChorTyp -> ChorTyp
  | ChorFun : ChorTyp -> ChorTyp -> ChorTyp.

  Reserved Notation "G ;; D ⊢c C ::: tau" (at level 30).
  Inductive ctyping : (Loc -> nat -> ExprTyp) -> (nat -> ChorTyp) -> Chor -> ChorTyp -> Prop :=
  | TDone : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
              (p : Loc) (e : Expr) (τ : ExprTyp),
       (Γ p) e e ::: τ ->
20
  (* ------------------------------ *)
21
22
      Γ ;; Δ c Done p e ::: (LocatedType p τ)
  | TVar : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (n : nat),
23
  (* ----------------------------- *)
24
25
26
      Γ ;; Δ c Var n ::: (Δ n)
  | TSend : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
              (p : Loc) (e : Expr) (τ : ExprTyp) (q : Loc) (C : Chor) (σ : ChorTyp),
27
      (Γ p) e e ::: τ ->
28
      (fun r n => if L.eq_dec q r
29
30
31
32
               then match n with
                    | 0 => τ
                    | S n => Γ r n
                    end
33
               else Γ r n);; Δ c C ::: σ ->
34
      p <> q ->
35
  (* --------------------------------------- *)
36
37
38
      Γ ;; Δ c (Send p e q C) ::: σ
  | TIf : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
            (p : Loc) (e : Expr) (C1 C2 : Chor) (τ : ChorTyp),
39
      (Γ p) e e ::: bool ->
40
41
      Γ ;; Δ c C1 ::: τ ->
      Γ ;; Δ c C2 ::: τ ->
42
  (* --------------------------------- *)
43
44
45
46
      Γ;; Δ c If p e C1 C2 ::: τ
  | TSync : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
              (p : Loc) (d : LRChoice) (q : Loc) (C : Chor) (τ : ChorTyp),
      Γ ;; Δ c C ::: τ ->
Andrew Hirsch's avatar
Andrew Hirsch committed
47
      p <> q ->
48
  (* ---------------------------------- *)
49
50
51
52
      Γ ;; Δ c Sync p d q C ::: τ
  | TDefLocal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
                  (p : Loc) (C1 C2 : Chor) (τ : ExprTyp) (σ : ChorTyp),
      Γ ;; Δ c C1 ::: (LocatedType p τ) ->
53
54
55
56
57
58
      (fun r n =>
         if L.eq_dec p r
         then match n with
              | 0 => τ
              | S n => Γ r n
              end
59
         else Γ r n);; Δ c C2 ::: σ ->
60
  (* ------------------------------------*)
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
      Γ ;; Δ c DefLocal p C1 C2 ::: σ
  | TRecLocal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) 
                 (C : Chor) (l : Loc) (τ : ExprTyp) (σ : ChorTyp),
      (fun r n =>
         if L.eq_dec r l
         then match n with
              | 0 => τ
              | S n => Γ r n
              end
         else Γ r n);; (fun n => match n with
                              | 0 => LocalFun l τ σ
                              | S n => Δ n
                              end) c C ::: σ ->
      Γ;; Δ c (RecLocal l C) ::: LocalFun l τ σ
  | TRecGlobal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
                 (C : Chor) (τ σ : ChorTyp),
      Γ;; (fun n => match n with
78
79
                 | 0 => τ
                 | 1 => ChorFun τ σ
80
81
82
83
84
85
86
87
88
89
90
91
92
93
                 | S (S n) => Δ n
                 end) c C ::: σ
      -> Γ;; Δ c RecGlobal C ::: ChorFun τ σ
  | TAppLocal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
                 (C : Chor) (l : Loc) (e : Expr) (τ : ExprTyp) (σ : ChorTyp),
      (Γ l) e e ::: τ ->
      Γ;; Δ c C ::: LocalFun l τ σ ->
      Γ;; Δ c AppLocal l C e ::: σ
  | TAppGlobal : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
                   (C1 C2 : Chor) (τ σ : ChorTyp),
      Γ;; Δ c C1 ::: ChorFun τ σ ->
      Γ;; Δ c C2 ::: τ ->
      Γ;; Δ c AppGlobal C1 C2 ::: σ
  where "Gamma ;; Delta ⊢c C ::: tau" := (ctyping Gamma Delta C tau).
94
  Global Hint Constructors ctyping : Chor.
95
96


97
  Theorem TypeExprWeakening : forall (Γ1 Γ2 : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp)
98
99
                               (ξ : Loc -> nat -> nat),
      (forall p n, Γ1 p n = Γ2 p (ξ p n)) ->
100
101
102
      forall (τ : ChorTyp) (C : Chor),
        Γ1;; Δ c C ::: τ ->
        Γ2;; Δ c Cce| ξ⟩ ::: τ.
103
  Proof using.
104
    intros Γ1 Γ2 Δ ξ eqv τ C typing; revert Γ2 ξ eqv; induction typing; intros Γ2 ξ eqv;
105
106
107
108
109
110
111
112
113
114
115
116
117
      cbn; repeat match goal with
                  | [ H : ?Γ ?p e ?e ::: ?t, eqv : forall p n, ?Γ p n = ?Γ2 p (?ξ p n) |- _] =>
                    lazymatch goal with
                    | [_ : Γ2 p e e e| ξ p  ::: t |- _ ] => fail
                    | _ => pose proof (ExprWeakening (Γ p) (Γ2 p) (ξ p) e t (eqv p) H)
                    end
                  end; auto with Chor.
    - apply TSend with (τ := τ); auto; apply IHtyping.
      intros p0 n; unfold ChorUpExprRename; unfold ExprUpRename;
        destruct (L.eq_dec q p0); destruct n; auto.
    - apply TDefLocal with (τ := τ); auto; apply IHtyping2.
      intros p0 n; unfold ChorUpExprRename; unfold ExprUpRename;
        destruct (L.eq_dec p p0); destruct n; auto.
118
119
120
121
122
123
124
125
    - apply TRecLocal; auto. apply IHtyping.
      intros p n; unfold ChorUpExprRename; unfold ExprUpRename.
      destruct (L.eq_dec p l); destruct (L.eq_dec l p); subst;
        try match goal with
            | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; destruct n; auto.
    - apply TAppLocal with (τ := τ); auto.
    - apply TAppGlobal with (τ := τ); auto.
126
127
  Qed.
      
128
  Theorem TypeChorWeakening : forall (Γ : Loc -> nat -> ExprTyp) (Δ1 Δ2 : nat -> ChorTyp)
129
130
                                (ξ : nat -> nat),
      (forall n, Δ1 n = Δ2 (ξ n)) ->
131
132
133
      forall (τ : ChorTyp) (C : Chor),
        Γ ;; Δ1 c C ::: τ ->
        Γ ;; Δ2 c C c| ξ⟩ ::: τ.
134
  Proof using.
135
    intros Γ Δ1 Δ2 ξ eqv τ C typing; revert Δ2 ξ eqv; induction typing;
136
      intros Δ2 ξ eqv; cbn; eauto with Chor.
137
138
139
140
141
    - rewrite eqv. apply TVar.
    - apply TRecLocal; apply IHtyping.
      unfold ChorUpRename; destruct n; auto.
    - apply TRecGlobal; apply IHtyping.
      unfold ChorUpRename; repeat (destruct n; auto).
142
143
  Qed.
  
144
145
  Theorem ChorTypingExt : forall (Γ1 Γ2 : Loc -> nat -> ExprTyp) (Δ1 Δ2 : nat -> ChorTyp)
                            (C : Chor) (τ : ChorTyp),
146
      (forall (p : Loc) (n : nat), Γ1 p n = Γ2 p n) ->
147
      (forall n : nat, Δ1 n = Δ2 n) ->
148
      Γ1;; Δ1 c C ::: τ -> Γ2;; Δ2 c C ::: τ.
149
  Proof.
150
    intros Γ1 Γ2 Δ1 Δ2 C τ eqΓ eqΔ typing; revert Γ2 Δ2 eqΓ eqΔ; induction typing;
151
152
153
154
155
156
157
158
      intros Γ2 Δ2 eqΓ eqΔ;
      repeat match goal with
             | [ H : ?Γ ?p e ?e ::: ?t, eqv : forall p n, ?Γ p n = ?Γ2 p n |- _ ] =>
               lazymatch goal with
               | [_ : Γ2 p e e ::: t |- _ ] => fail
               | _ => pose proof (ExprTypingExt (Γ p) (Γ2 p) e t (eqv p) H)
               end
             end; auto with Chor.
159
    - rewrite eqΔ; apply TVar; auto with Chor.
160
161
162
163
    - apply TSend with (τ := τ); auto with Chor; apply IHtyping; auto.
      intros p0 n; destruct (L.eq_dec q p0); destruct n; auto.
    - apply TDefLocal with (τ := τ); auto with Chor; apply IHtyping2; auto.
      intros p0 n; destruct (L.eq_dec p p0); destruct n; auto.
164
165
166
167
168
169
170
    - apply TRecLocal; apply IHtyping; auto.
      intros p n; destruct (L.eq_dec p l); destruct n; auto.
      intro n; destruct n; auto.
    - apply TRecGlobal; apply IHtyping; auto.
      destruct n; auto; destruct n; auto.
    - apply TAppLocal with (τ := τ); auto.
    - apply TAppGlobal with (τ := τ); auto.
171
172
  Qed.

173
  Definition ChorSubstTyping Γ Δ1 σ Δ2 :=
174
    (forall (n : nat), Γ;; Δ2 c (σ n) ::: (Δ1 n)).
175

176
177
  Theorem ChorExprSubstTypingSpec : forall Γ1 σ Γ2 Δ C τ,
      (forall q, Γ1 q es σ q  Γ2 q) -> Γ1 ;; Δ c C ::: τ -> Γ2 ;; Δ c C [ce| σ] ::: τ.
178
  Proof using.
179
    intros Γ1 σ Γ2 Δ C τ eqv typing; revert σ Γ2 eqv; induction typing; intros σ' Γ2 eqv;
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
      cbn; repeat match goal with
                  | [ H : ?Γ ?p e ?e ::: ?t, eqv : forall q, ?Γ q es ?σ' q  ?Γ2 q |- _] =>
                    lazymatch goal with
                    | [ _ : Γ2 p e e [e|σ' p] ::: t |- _] => fail
                    | _ => pose proof (ExprSubstType (Γ p) (Γ2 p) (σ' p) e t (eqv p) H)
                    end
                  end; eauto with Chor.
    - apply TSend with (τ := τ); auto; apply IHtyping.
      intro q0; unfold ExprSubstTyping; intro n; unfold ChorUpExprSubst;
        destruct (L.eq_dec q q0); destruct n; auto.
      apply ExprVarTyping. apply ExprWeakening with (Γ := Γ2 q0); auto.
      all: apply eqv.
    - apply TDefLocal with (τ := τ); auto; apply IHtyping2; auto.
      intro q0; unfold ChorUpExprSubst; intro n;
        destruct (L.eq_dec p q0); destruct n; auto with Chor.
      apply ExprVarTyping. apply ExprWeakening with (Γ := Γ2 q0); auto.
      all: apply eqv.
197
198
199
200
201
202
203
204
205
    - apply TRecLocal; apply IHtyping; auto.
      intro q; unfold ChorUpExprSubst; cbn. unfold ExprSubstTyping. intro n; cbn.
      destruct (L.eq_dec q l); destruct (L.eq_dec l q); subst;
        try match goal with
            | [ H : ?a <> ?a |- _] => destruct (H eq_refl)
            end; auto.
      destruct n; auto.
      apply ExprVarTyping. apply ExprWeakening with (Γ := Γ2 l); auto.
      apply eqv. apply eqv.
206
207
  Qed.      
         
208

209
210
211
  Lemma TypingLocalUp :forall Γ Δ C τ,
      Γ ;; Δ c C ::: τ  ->
      forall p σ, (fun r n => if L.eq_dec r p
212
213
214
215
                      then match n with
                           | 0 => σ
                           | S n => Γ r n
                           end
216
                      else Γ r n) ;; Δ c C ce| fun r n => if L.eq_dec r p then S n else n  ::: τ.
217
  Proof using.
218
    intros Γ Δ C τ H q σ.
219
220
221
222
    apply TypeExprWeakening with (Γ1 := Γ); auto.
    intros p0 n; destruct (L.eq_dec q p0); subst.
    destruct (L.eq_dec p0 p0) as [_ | neq]; [|destruct (neq eq_refl)]; auto.
    destruct (L.eq_dec p0 q) as [eq | _ ]; [destruct (n0 (eq_sym eq))|] ;auto.
223
  Qed.
224
225
226
  
  Theorem ChorSubstTypingSpec : forall Γ Δ1 σ Δ2,
      (ChorSubstTyping Γ Δ1 σ Δ2) ->
227
228
      forall (C : Chor) (τ : ChorTyp),
        (Γ;; Δ1 c C ::: τ) -> (Γ;; Δ2 c (C [c| σ]) ::: τ).
229
  Proof.
230
    intros Γ Δ1 σ Δ2 styping C τ typing; revert σ Δ2 styping; induction typing;
231
232
233
234
235
236
237
238
239
      try rename σ into ρ; intros σ Δ2 styping; cbn; auto with Chor.
    - apply TSend with (τ := τ); auto. apply IHtyping.
      unfold ChorSubstTyping. intro n. unfold ChorSubstTyping in styping.
      unfold ChorUpSubstForExpr. apply TypeExprWeakening with (Γ1 := Γ); auto.
      intros p0 n0; destruct (L.eq_dec q p0); auto.
    - apply TDefLocal with (τ := τ). apply IHtyping1; auto.
      unfold ChorUpSubstForExpr. apply IHtyping2. unfold ChorSubstTyping.
      intro n; apply TypeExprWeakening with (Γ1 := Γ); auto.
      intros p0 n0; destruct (L.eq_dec p p0); auto.
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
    - apply TRecLocal; apply IHtyping. unfold ChorSubstTyping in *; intro n.
      unfold ChorUpSubst; unfold ChorUpSubstForExpr; destruct n; cbn; auto.
      apply TVar.
      apply TypeChorWeakening with (Δ1 := Δ2); auto.
      apply TypeExprWeakening with (Γ1 := Γ); auto.
      intros p m; destruct (L.eq_dec p l); destruct (L.eq_dec l p); subst;
        try match goal with
            | [ H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; auto.
    - apply TRecGlobal; apply IHtyping; repeat unfold ChorUpSubst.
      unfold ChorSubstTyping in *.
      intro n.
      destruct n; [apply TVar|].
      destruct n; [apply TVar|].
      apply TypeChorWeakening with (Δ1 := fun m => match m with
255
                                               | 0 => ChorFun τ ρ
256
257
258
259
260
                                               | S m => Δ2 m
                                               end); auto.
      apply TypeChorWeakening with (Δ1 := Δ2); auto.
    - apply TAppLocal with (τ := τ); auto.
    - apply TAppGlobal with (τ := τ); auto.
261
262
  Qed.

263
  Lemma ValueSubstTyping: forall (Γ : Loc -> nat -> ExprTyp) (p : Loc) (e : Expr) (τ : ExprTyp),
264
265
266
267
268
269
      (Γ p e e ::: τ) ->
      forall q, ((fun r n => if L.eq_dec p r
                     then match n with
                          | 0 => τ
                          | S n => Γ r n
                          end
270
                     else Γ r n) q) es ValueSubst p e q  (Γ q).
271
  Proof using.
272
    intros Γ p e τ tpng q. unfold ValueSubst.
273
274
275
    unfold ExprSubstTyping. intro n. destruct n; destruct (L.eq_dec p q); subst; auto.
    all: apply ExprVarTyping.
  Qed.
276

277
278
279
280
281
282
283
284
285
286
  Lemma AppLocalSubstTyping : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (l : Loc) (τ : ExprTyp) (σ : ChorTyp) (C : Chor),
      (fun l' n => if L.eq_dec l' l
                then match n with
                     | 0 => τ
                     | S n => Γ l' n
                     end
                else Γ l' n);; (fun n => match n with
                                      | 0 => LocalFun l τ σ
                                      | S n => Δ n
                                      end) c C ::: σ ->
287
      ChorSubstTyping Γ (fun n => match n with
288
                               | 0 => LocalFun l τ σ
289
                               | S n => Δ n
290
                               end) (AppLocalSubst l C) Δ.
291
  Proof using.
292
293
294
    intros Γ Δ l τ σ C typing; unfold ChorSubstTyping; unfold AppLocalSubst;
      intro n; destruct n; [| apply TVar].
    apply TRecLocal; auto.
295
296
  Qed.

297
298
  Lemma AppGlobalSubstTyping : forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ σ : ChorTyp) (C1 C2 : Chor),
      Γ;; (fun n => match n with
299
300
                | 0 => τ
                | 1 => ChorFun τ σ
301
302
303
304
                | S (S n) => Δ n
                end) c C1 ::: σ ->
      Γ;; Δ c C2 ::: τ ->
      ChorSubstTyping Γ (fun n => match n with
305
306
                               | 0 => τ
                               | 1 => ChorFun τ σ
307
308
309
310
                               | S (S n) => Δ n
                               end) (AppGlobalSubst C1 C2) Δ.
  Proof using.
    intros Γ Δ τ σ C1 C2 typing1 typing2; unfold ChorSubstTyping; unfold AppGlobalSubst;
311
312
      intro n; destruct n; [| destruct n]; auto; [| apply TVar].
    apply TRecGlobal; auto. 
313
314
  Qed.
    
315
316
  Theorem ChorEquivTyping : forall (C1 C2 : Chor),
      C1  C2 ->
317
318
      forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
        Γ ;; Δ c C1 ::: τ -> Γ ;; Δ c C2 ::: τ.
319
  Proof using.
320
    intros C1 C2 equiv; induction equiv; intros Γ Δ τ typ; auto with Chor;
321
      repeat match goal with
322
             | [ H : ?Γ ;; ?Δ c ?C ::: ?t |- _ ] =>
323
324
325
326
327
               tryif let x := fresh "_" C in idtac
               then fail
               else inversion H; subst; clear H
             end; auto with Chor.
    all: repeat match goal with
328
329
                | [IH : forall G D t p, G ;; D c ?C1 ::: t  -> G ;; D c ?C2 ::: t,
                     H : ?Γ ;; ?Δ c ?C1 ::: ?τ |- _ ] =>
330
                  lazymatch goal with
331
                  | [_ : Γ ;; Δ c C2 ::: τ |- _ ] => fail
332
333
334
335
336
337
338
                  | _ => pose proof (IH Γ Δ τ p H)
                  end
                end; eauto with Chor.
    - apply TSend with (τ := τ1); auto.
      destruct (L.eq_dec l2 l3) as [eq | _ ]; [destruct (H1 eq)|]; auto.
      apply TSend with (τ := τ0); auto.
      destruct (L.eq_dec l4 l1) as [eq|_]; [destruct (H0 (eq_sym eq))|]; auto.
339
      eapply ChorTypingExt; [| |exact H14]; auto.
340
341
342
343
344
345
346
347
      intros p0 n; cbn; destruct (L.eq_dec l4 p0); destruct (L.eq_dec l2 p0); subst;
        try match goal with [H : ?a <> ?a |- _] => destruct (H eq_refl) end;
        auto.
    - apply TIf. destruct (L.eq_dec l2 l3) as [eq|_]; [destruct (H0 eq)|auto].
      all: apply TSend with (τ := τ0); auto.
    - apply TSend with (τ := τ0); auto.
      apply TIf; auto.
      destruct (L.eq_dec l3 l1) as [eq | _ ]; [destruct (H0 (eq_sym eq))| auto].
348
      rewrite (ExprTypingUnique (Γ l2) e' τ0 τ1 H11 H10); auto.
349
  Qed.      
350

351
  Theorem RelativePreservation :
352
353
354
355
    (forall (Γ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
        Γ e e ::: τ
        -> forall e' : Expr, ExprStep e e'
                       -> Γ e e' ::: τ) ->
356
357
    forall (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
      Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list Loc) (C': Chor),
358
        ChorStep R B C C' -> Γ;; Δ c C' ::: τ.
359
  Proof using.
360
361
    intros expr_pres Γ Δ C τ typing R B C' step; revert Γ Δ τ typing; induction step;
      intros Γ Δ τ typing; inversion typing; subst;
362
363
        repeat (match goal with
                | [ expr_typing : ?G e ?e ::: ?t, expr_step : ExprStep ?e ?e' |- _ ] =>
364
                  lazymatch goal with
365
366
                  | [_ : ?G e e' ::: t |- _ ] => fail
                  | _ => pose proof (expr_pres G e t expr_typing e' expr_step)
367
                  end
368
369
                end; eauto with Chor); try (econstructor; eauto with Chor; fail); auto.
    1,2: eapply ChorExprSubstTypingSpec; eauto.
370
371
    1,2: intro q; apply ValueSubstTyping; auto.
    2: inversion H6; subst.
372
    1,2: eapply ExprClosedTyping; eauto; apply ExprValuesClosed; auto.
373
374
375
376
377
378
379
380
381
382
383
    - eapply ChorSubstTypingSpec; eauto; [apply AppLocalSubstTyping|];
        inversion H7; subst; eauto.
      eapply ChorExprSubstTypingSpec; eauto. intro q; cbn.
      unfold ValueSubst. unfold ExprSubstTyping; intro n; destruct n; auto.
      all: destruct (L.eq_dec l q); destruct (L.eq_dec q l); subst;
        try match goal with
            | [H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; auto.
      all: apply ExprVarTyping.
    - inversion H4; subst; eapply ChorSubstTypingSpec; eauto.
      apply AppGlobalSubstTyping; auto.
384
385
  Qed.    
  
386
387

  Lemma ChorClosedBelowTyping : forall (Γ1 Γ2 : Loc -> nat -> ExprTyp)
388
389
                                  (Δ1 Δ2 : nat -> ChorTyp)
                                  (C : Chor) (τ : ChorTyp)
390
                                  (n : Loc -> nat) (m : nat),
391
      ChorClosedBelow n m C ->
392
393
394
      (forall (p : Loc) (k : nat), k < (n p) -> Γ1 p k = Γ2 p k) ->
      (forall k : nat, k < m -> Δ1 k = Δ2 k) ->
      Γ1;; Δ1 c C ::: τ -> Γ2;; Δ2 c C ::: τ.
395
  Proof.
396
    intros Γ1 Γ2 Δ1 Δ2 C τ n m cb eqΓ eqΔ typ; revert Γ2 Δ2 n m cb eqΓ eqΔ;
397
398
399
      induction typ; try rename n into n'; intros Γ2 Δ2 n m cb eqΓ eqΔ;
        inversion cb; subst.
    - apply TDone; eapply ExprClosedBelowTyping; [| apply eqΓ|]; eauto.
400
    - rewrite eqΔ; auto; apply TVar.
401
402
403
404
405
406
407
    - eapply TSend; eauto.
      eapply ExprClosedBelowTyping; [| | exact H]; eauto.
      eapply IHtyp; eauto. cbn in *; intros p0 k l.
      destruct (L.eq_dec q p0); subst; auto. destruct k; auto. apply eqΓ.
      apply Lt.lt_S_n in l; auto.
    - apply TIf. eapply ExprClosedBelowTyping; [| apply eqΓ|]; eauto.
      eapply IHtyp1; eauto. eapply IHtyp2; eauto.
Andrew Hirsch's avatar
Andrew Hirsch committed
408
    - apply TSync; auto; eapply IHtyp; eauto.
409
410
411
412
    - eapply TDefLocal. eapply IHtyp1; eauto.
      eapply IHtyp2; eauto. cbn in *; intros p0 k l.
      destruct (L.eq_dec p p0); subst; auto. destruct k; auto.
      apply eqΓ; apply Lt.lt_S_n in l; auto.
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
    - eapply TRecLocal; eauto; eapply IHtyp; eauto.
      intros p k k_lt; cbn in *.
      2: intros k k_lt.
      destruct (L.eq_dec p l); destruct (L.eq_dec l p); subst;
        try match goal with
            | [H : ?a <> ?a |- _ ] => destruct (H eq_refl)
            end; auto.
      all: destruct k; auto.
      all: apply Lt.lt_S_n in k_lt.
      apply eqΓ; auto. apply eqΔ; auto.
    - eapply TRecGlobal; eauto; eapply IHtyp; eauto.
      intros k k_lt; destruct k; auto; destruct k; auto.
      repeat apply Lt.lt_S_n in k_lt. apply eqΔ; auto.
    - eapply TAppLocal; eauto. eapply ExprClosedBelowTyping; [| apply eqΓ|]; eauto.
    - eapply TAppGlobal; eauto.       
428
429
  Qed.

Andrew Hirsch's avatar
Andrew Hirsch committed
430

431
432
433
  Lemma ChorClosedTyping : forall (Γ1 Γ2 : Loc -> nat -> ExprTyp) (Δ1 Δ2 : nat -> ChorTyp)
                             (C : Chor) (τ : ChorTyp),
      ChorClosed C -> Γ1;; Δ1 c C ::: τ -> Γ2;; Δ2 c C ::: τ.
434
  Proof.
435
    intros Γ1 Γ2 Δ1 Δ2 C τ H H0.
436
437
438
439
440
    unfold ChorClosed in H.
    apply ChorClosedBelowTyping with (Γ1 := Γ1) (Δ1 := Δ1) (n := fun _ => 0) (m := 0); auto.
    intros p0 k H1; inversion H1.
    intros k H1; inversion H1.
  Qed.
441
442
443
444
445
446
447
448

  Theorem ChorValueTyping : forall (C : Chor) (τ : ChorTyp),
      ChorVal C ->
       forall Γ1 Γ2 Δ1 Δ2, Γ1;; Δ1 c C ::: τ -> Γ2;; Δ2 c C ::: τ.
  Proof.
    intros C τ H Γ1 Γ2 Δ1 Δ2 H0.
    eapply ChorClosedTyping; eauto. apply ChorValuesClosed; auto.
  Qed.
449
  
450
451

  Corollary RelativeProgress :
452
453
454
455
456
    (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}) ->
457
458
    forall (C : Chor) (Γ : Loc -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
      ChorClosed C -> Γ;; Δ c C ::: τ ->
459
460
      ChorVal C \/ exists R C', ChorStep R nil C C'.
  Proof using.
461
    intros ExprProgress BoolInversion C Γ Δ τ cc typ; revert cc; induction typ; intro cc;
462
463
      inversion cc; subst.
    2: inversion H2.
464
465
466
    2-5,8,9: right.
    8,9: left; constructor; auto.
    - destruct (ExprProgress e τ (Γ p) ltac:(assumption) ltac:(assumption));
467
468
469
470
471
472
473
474
475
476
477
        [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]]].
478
479
480
481
482
483
484
485
486
487
488
      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.
489
      all: eexists; eexists; eauto with Chor.
490
  Qed.
491
  
492
493
End TypedChoreography.